(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
(* -------------------------------------------------------------------- *)
(* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
(* Copyright (c) - 2015--2018 - Inria                                   *)
(* Copyright (c) - 2016--2018 - Polytechnique                           *)
(* -------------------------------------------------------------------- *)

From mathcomp Require Import all_ssreflect.
Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

(******************************************************************************)
(*                              Classical Logic                               *)
(*                                                                            *)
(* This file provides the axioms of classical logic and tools to perform      *)
(* classical reasoning in the Mathematical Compnent framework. The three      *)
(* axioms are taken from the standard library of Coq, more details can be     *)
(* found in Section 5 of                                                      *)
(*   Reynald Affeldt, Cyril Cohen, Damien Rouhling:                          *)
(*   Formalization Techniques for Asymptotic Reasoning in Classical Analysis. *)
(*   Journal of Formalized Reasoning, 2018                                    *)
(*                                                                            *)
(* * Axioms                                                                   *)
(* functional_extensionality_dep == functional extensionality (on dependently *)
(*                     typed functions), i.e., functions that are pointwise   *)
(*                     equal are equal                                        *)
(* propositional_extensionality == propositional extensionality, i.e., iff    *)
(*                     and equality are the same on Prop                      *)
(* constructive_indefinite_description == existential in Prop (ex) implies    *)
(*                     existential in Type (sig)                              *)
(*              cid := constructive_indefinite_description (shortcut)         *)
(* --> A number of properties are derived below from these axioms and are     *)
(* often more pratical to use than directly using the axioms. For instance    *)
(* propext, funext, the excluded middle (EM),...                              *)
(*                                                                            *)
(* * Boolean View of Prop                                                     *)
(*         `[< P >] == boolean view of P : Prop, see all lemmas about asbool  *)
(*                                                                            *)
(* * Mathematical Components Structures                                       *)
(*  {classic T} == Endow T : Type with a canonical eqType/choiceType.         *)
(*                 This is intended for local use.                            *)
(*                 E.g., T : Type |- A : {fset {classic T}}                   *)
(*                 Alternatively one may use elim/Pchoice: T => T in H *.     *)
(*                 to substitute T with T : choiceType once and for all.      *)
(* {eclassic T} == Endow T : eqType with a canonical choiceType.              *)
(*                 On the model of {classic _}.                               *)
(*                 See also the lemmas Peq and eqPchoice.                     *)
(*                                                                            *)
(* --> Functions into a porderType (resp. latticeType) are equipped with      *)
(* a porderType (resp. latticeType), (f <= g)%O when f x <= g x for all x,    *)
(* see lemma lefP.                                                            *)
(******************************************************************************)

Set   Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope box_scope.
Declare Scope quant_scope.

(* -------------------------------------------------------------------- *)

Axiom functional_extensionality_dep :
       forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
       (forall x : A, f x = g x) -> f = g.
Axiom propositional_extensionality :
       forall P Q : Prop, P <-> Q -> P = Q.

Axiom constructive_indefinite_description :
  forall (A : Type) (P : A -> Prop),
  (exists x : A, P x) -> {x : A | P x}.
Notation cid := constructive_indefinite_description.

Lemma cid2 (A : Type) (P Q : A -> Prop) :
  (exists2 x : A, P x & Q x) -> {x : A | P x & Q x}.
A: Type
P, Q: A -> Prop
(exists2 x : A, P x & Q x) -> {x : A | P x & Q x}
Proof.
2
move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a.
5
6
PQA: exists2 x : A, P x & Q x
{x : A | P x /\ Q x}
by apply: cid; case: PQA => x; exists x.
Qed.

(* -------------------------------------------------------------------- *)
Record mextentionality := {
  _ : forall (P Q : Prop), (P <-> Q) -> (P = Q);
  _ : forall {T U : Type} (f g : T -> U),
        (forall x, f x = g x) -> f = g;
}.

Fact extentionality : mextentionality.
mextentionality
Proof.
10
split.
forall P Q : Prop, P <-> Q -> P = Q
forall (T U : Type) (f g : T -> U),
(forall x : T, f x = g x) -> f = g
-
15 exact: propositional_extensionality.
1a
-
1d by move=> T U f g; apply: functional_extensionality_dep.
Qed.

Lemma propext (P Q : Prop) : (P <-> Q) -> (P = Q).
P, Q: Prop
P <-> Q -> P = Q
Proof.
21 by have [propext _] := extentionality; apply: propext. Qed.

Lemma funext {T U : Type} (f g : T -> U) : (f =1 g) -> f = g.
T, U: Type
f, g: T -> U
f =1 g -> f = g
Proof.
28 by case: extentionality=> _; apply. Qed.

Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q).
23
(P = Q) = (P <-> Q)
Proof.
30 by apply: propext; split=> [->|/propext]. Qed.

Lemma propeqP (P Q : Prop) : (P = Q) <-> (P <-> Q).
23
P = Q <-> (P <-> Q)
Proof.
35 by rewrite propeqE. Qed.

Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g).
2a
(f = g) = (f =1 g)
Proof.
3a by rewrite propeqE; split=> [->//|/funext]. Qed.

Lemma funeq2E {T U V : Type} (f g : T -> U -> V) : (f = g) = (f =2 g).
T, U, V: Type
f, g: T -> U -> V
(f = g) = (f =2 g)
Proof.
3f
by rewrite propeqE; split=> [->//|?]; rewrite funeqE=> x; rewrite funeqE.
Qed.

Lemma funeq3E {T U V W : Type} (f g : T -> U -> V -> W) :
  (f = g) = (forall x y z, f x y z = g x y z).
T, U, V, W: Type
f, g: T -> U -> V -> W
(f = g) =
(forall (x : T) (y : U) (z : V), f x y z = g x y z)
Proof.
47
by rewrite propeqE; split=> [->//|?]; rewrite funeq2E=> x y; rewrite funeqE.
Qed.

Lemma funeqP {T U : Type} (f g : T -> U) : (f = g) <-> (f =1 g).
2a
f = g <-> f =1 g
Proof.
4f by rewrite funeqE. Qed.

Lemma funeq2P {T U V : Type} (f g : T -> U -> V) : (f = g) <-> (f =2 g).
41
f = g <-> f =2 g
Proof.
54 by rewrite funeq2E. Qed.

Lemma funeq3P {T U V W : Type} (f g : T -> U -> V -> W) :
  (f = g) <-> (forall x y z, f x y z = g x y z).
49
f = g <->
(forall (x : T) (y : U) (z : V), f x y z = g x y z)
Proof.
59 by rewrite funeq3E. Qed.

Lemma predeqE {T} (P Q : T -> Prop) : (P = Q) = (forall x, P x <-> Q x).
T: Type
P, Q: T -> Prop
(P = Q) = (forall x : T, P x <-> Q x)
Proof.
5e
by rewrite propeqE; split=> [->//|?]; rewrite funeqE=> x; rewrite propeqE.
Qed.

Lemma predeq2E {T U} (P Q : T -> U -> Prop) :
   (P = Q) = (forall x y, P x y <-> Q x y).
2b
P, Q: T -> U -> Prop
(P = Q) = (forall (x : T) (y : U), P x y <-> Q x y)
Proof.
66
by rewrite propeqE; split=> [->//|?]; rewrite funeq2E=> ??; rewrite propeqE.
Qed.

Lemma predeq3E {T U V} (P Q : T -> U -> V -> Prop) :
   (P = Q) = (forall x y z, P x y z <-> Q x y z).
42
P, Q: T -> U -> V -> Prop
(P = Q) =
(forall (x : T) (y : U) (z : V), P x y z <-> Q x y z)
Proof.
6d
by rewrite propeqE; split=> [->//|?]; rewrite funeq3E=> ???; rewrite propeqE.
Qed.

Lemma predeqP {T} (A B : T -> Prop) : (A = B) <-> (forall x, A x <-> B x).
61
A, B: T -> Prop
A = B <-> (forall x : T, A x <-> B x)
Proof.
74 by rewrite predeqE. Qed.

Lemma predeq2P {T U} (P Q : T -> U -> Prop) :
   (P = Q) <-> (forall x y, P x y <-> Q x y).
68
P = Q <-> (forall (x : T) (y : U), P x y <-> Q x y)
Proof.
7b by rewrite predeq2E. Qed.

Lemma predeq3P {T U V} (P Q : T -> U -> V -> Prop) :
   (P = Q) <-> (forall x y z, P x y z <-> Q x y z).
6f
P = Q <->
(forall (x : T) (y : U) (z : V), P x y z <-> Q x y z)
Proof.
80 by rewrite predeq3E. Qed.

Lemma propT {P : Prop} : P -> P = True.
P: Prop
P -> P = True
Proof.
85 by move=> p; rewrite propeqE. Qed.

Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.
88
x, y: P
x = y
Proof.
8c by move: x (x) y => /propT-> [] []. Qed.
#[global] Hint Resolve Prop_irrelevance : core.

(* -------------------------------------------------------------------- *)
Record mclassic := {
  _ : forall (P : Prop), {P} + {~P};
  _ : forall T, Choice.mixin_of T
}.

Lemma choice X Y (P : X -> Y -> Prop) :
  (forall x, exists y, P x y) -> {f & forall x, P x (f x)}.
X, Y: Type
P: X -> Y -> Prop
(forall x : X, exists y : Y, P x y) ->
{f : X -> Y & forall x : X, P x (f x)}
Proof.
93 by move=> /(_ _)/constructive_indefinite_description -/all_tag. Qed.

(* Diaconescu Theorem *)
Theorem EM P : P \/ ~ P.
87
P \/ ~ P
Proof.
9b
pose U val := fun Q : bool => Q = val \/ P.
88
U:= fun val Q : bool => Q = val \/ P: bool -> bool -> Prop
9d
have Uex val : exists b, U val b by exists val; left.
88
a3
Uex: forall val : bool, exists b : bool, U val b
9d
pose f val := projT1 (cid (Uex val)).
88
a3
a8
f:= fun val : bool => projT1 (cid (Uex val)): bool -> bool
9d
pose Uf val : U val (f val) := projT2 (cid (Uex val)).
88
a3
a8
ad
Uf:= (fun val : bool => projT2 (cid (Uex val)))
  : (forall val : bool, U val (f val)): forall val : bool, U val (f val)
9d
have : f true != f false \/ P.
b1
f true != f false \/ P
b1
f true != f false \/ P -> P \/ ~ P
  have [] := (Uf true, Uf false); rewrite /U.
b1
f true = true \/ P ->
f false = false \/ P -> f true != f false \/ P
b7
  by move=> [->|?] [->|?] ; do ?[by right]; left.
b1
b9
move=> [/eqP fTFN|]; [right=> p|by left]; apply: fTFN.
88
a3
a8
ad
b2
p: P
f true = f false
have UTF : U true = U false by rewrite predeqE /U => b; split=> _; right.
88
a3
a8
ad
b2
c5
UTF: U true = U false
c6
rewrite /f; move: (Uex true) (Uex false); rewrite UTF => p1 p2.
88
a3
a8
ad
b2
c5
cb
p1, p2: exists b : bool, U false b
projT1 (cid p1) = projT1 (cid p2)
by congr (projT1 (cid _)).
Qed.

Lemma pselect (P : Prop): {P} + {~P}.
87
{P} + {~ P}
Proof.
d3
have : exists b, if b then P else ~ P.
87
exists b : bool, if b then P else ~ P
87
(exists b : bool, if b then P else ~ P) -> {P} + {~ P}
  by case: (EM P); [exists true|exists false].
87
dd
by move=> /cid [[]]; [left|right].
Qed.

Lemma pselectT T : (T -> False) + T.
61
((T -> False) + T)%type
Proof.
e2
have [/cid[]//|NT] := pselect (exists t : T, True); first by right.
61
NT: ~ (exists _ : T, True)
e5
by left=> t; case: NT; exists t.
Qed.

Lemma classic : mclassic.
mclassic
Proof.
ed
split=> [|T]; first exact: pselect.
e4
choiceMixin T
exists (fun (P : pred T) (n : nat) =>
  if pselect (exists x, P x) isn't left ex then None
  else Some (projT1 (cid ex)))
  => [P n x|P [x Px]|P Q /funext -> //].
61
P: pred T
n: nat
x: T
match pselect (exists x : T, P x) with
| left ex => Some (projT1 (cid ex))
| right _ => None
end = Some x -> P x
61
f9
fb
Px: P x
exists _ : nat,
  match pselect (exists x : T, P x) with
  | left ex => Some (projT1 (cid ex))
  | right _ => None
  end
  by case: pselect => // ex [<- ]; case: cid.
ff
101
by exists 0; case: pselect => // -[]; exists x.
Qed.

Lemma gen_choiceMixin {T : Type} : Choice.mixin_of T.
f2
Proof.
f2 by case: classic. Qed.

Lemma pdegen (P : Prop): P = True \/ P = False.
87
P = True \/ P = False
Proof.
108 by have [p|Np] := pselect P; [left|right]; rewrite propeqE. Qed.

Lemma lem (P : Prop): P \/ ~P.
9b
Proof.
9b by case: (pselect P); tauto. Qed.

(* -------------------------------------------------------------------- *)
Lemma trueE : true = True :> Prop.
true = True
Proof.
10f by rewrite propeqE; split. Qed.

Lemma falseE : false = False :> Prop.
false = False
Proof.
114 by rewrite propeqE; split. Qed.

Lemma propF (P : Prop) : ~ P -> P = False.
87
~ P -> P = False
Proof.
119 by move=> p; rewrite propeqE; tauto. Qed.

Lemma eq_fun T rT (U V : T -> rT) :
  (forall x : T, U x = V x) -> (fun x => U x) = (fun x => V x).
T, rT: Type
U, V: T -> rT
(forall x : T, U x = V x) -> [eta U] = [eta V]
Proof.
11e by move=> /funext->. Qed.

Lemma eq_fun2 T1 T2 rT (U V : T1 -> T2 -> rT) :
  (forall x y, U x y = V x y) -> (fun x y => U x y) = (fun x y => V x y).
T1, T2, rT: Type
U, V: T1 -> T2 -> rT
(forall (x : T1) (y : T2), U x y = V x y) ->
(fun x : T1 => [eta U x]) = (fun x : T1 => [eta V x])
Proof.
126 by move=> UV; rewrite funeq2E => x y; rewrite UV. Qed.

Lemma eq_fun3  T1 T2 T3 rT (U V : T1 -> T2 -> T3 -> rT) :
  (forall x y z, U x y z = V x y z) ->
  (fun x y z => U x y z) = (fun x y z => V x y z).
T1, T2, T3, rT: Type
U, V: T1 -> T2 -> T3 -> rT
(forall (x : T1) (y : T2) (z : T3), U x y z = V x y z) ->
(fun (x : T1) (y : T2) => [eta U x y]) =
(fun (x : T1) (y : T2) => [eta V x y])
Proof.
12e by move=> UV; rewrite funeq3E => x y z; rewrite UV. Qed.

Lemma eq_forall T (U V : T -> Prop) :
  (forall x : T, U x = V x) -> (forall x, U x) = (forall x, V x).
61
U, V: T -> Prop
(forall x : T, U x = V x) ->
(forall x : T, U x) = (forall x : T, V x)
Proof.
136 by move=> e; rewrite propeqE; split=> ??; rewrite (e,=^~e). Qed.

Lemma eq_forall2 T S (U V : forall x : T, S x -> Prop) :
  (forall x y, U x y = V x y) -> (forall x y, U x y) = (forall x y, V x y).
61
S: T -> Type
U, V: forall x : T, S x -> Prop
(forall (x : T) (y : S x), U x y = V x y) ->
(forall (x : T) (y : S x), U x y) =
(forall (x : T) (y : S x), V x y)
Proof.
13d by move=> UV; apply/eq_forall => x; apply/eq_forall. Qed.

Lemma eq_forall3 T S R (U V : forall (x : T) (y : S x), R x y -> Prop) :
  (forall x y z, U x y z = V x y z) ->
  (forall x y z, U x y z) = (forall x y z, V x y z).
61
140
R: forall x : T, S x -> Type
U, V: forall (x : T) (y : S x), R x y -> Prop
(forall (x : T) (y : S x) (z : R x y),
 U x y z = V x y z) ->
(forall (x : T) (y : S x) (z : R x y), U x y z) =
(forall (x : T) (y : S x) (z : R x y), V x y z)
Proof.
145 by move=> UV; apply/eq_forall2 => x y; apply/eq_forall. Qed.

Lemma eq_exists T (U V : T -> Prop) :
  (forall x : T, U x = V x) -> (exists x, U x) = (exists x, V x).
138
(forall x : T, U x = V x) ->
(exists x : T, U x) = (exists x : T, V x)
Proof.
14d
by move=> e; rewrite propeqE; split=> - [] x ?; exists x; rewrite (e,=^~e).
Qed.

Lemma eq_exists2 T S (U V : forall x : T, S x -> Prop) :
  (forall x y, U x y = V x y) -> (exists x y, U x y) = (exists x y, V x y).
13f
(forall (x : T) (y : S x), U x y = V x y) ->
(exists (x : T) (y : S x), U x y) =
(exists (x : T) (y : S x), V x y)
Proof.
152 by move=> UV; apply/eq_exists => x; apply/eq_exists. Qed.

Lemma eq_exists3 T S R (U V : forall (x : T) (y : S x), R x y -> Prop) :
  (forall x y z, U x y z = V x y z) ->
  (exists x y z, U x y z) = (exists x y z, V x y z).
147
(forall (x : T) (y : S x) (z : R x y),
 U x y z = V x y z) ->
(exists (x : T) (y : S x) (z : R x y), U x y z) =
(exists (x : T) (y : S x) (z : R x y), V x y z)
Proof.
157 by move=> UV; apply/eq_exists2 => x y; apply/eq_exists. Qed.

Lemma eq_exist T (P : T -> Prop) (s t : T) (p : P s) (q : P t) :
  s = t -> exist P s p = exist P t q.
61
P: T -> Prop
s, t: T
p: P s
q: P t
s = t -> exist P s p = exist P t q
Proof.
15c by move=> st; case: _ / st in q *; apply/congr1. Qed.

Lemma forall_swap T S (U : forall (x : T) (y : S), Prop) :
   (forall x y, U x y) = (forall y x, U x y).
T, S: Type
U: T -> S -> Prop
(forall (x : T) (y : S), U x y) =
(forall (y : S) (x : T), U x y)
Proof.
166 by rewrite propeqE; split. Qed.

Lemma exists_swap T S (U : forall (x : T) (y : S), Prop) :
   (exists x y, U x y) = (exists y x, U x y).
168
(exists (x : T) (y : S), U x y) =
(exists (y : S) (x : T), U x y)
Proof.
16e by rewrite propeqE; split => -[x [y]]; exists y, x. Qed.

Lemma reflect_eq (P : Prop) (b : bool) : reflect P b -> P = b.
88
b: bool
reflect P b -> P = b
Proof.
173 by rewrite propeqE; exact: rwP. Qed.

Definition asbool (P : Prop) :=
  if pselect P then true else false.

Notation "`[< P >]" := (asbool P) : bool_scope.

Lemma asboolE (P : Prop) : `[<P>] = P :> Prop.
87
`[< P >] = P
Proof.
17a by rewrite propeqE /asbool; case: pselect; split. Qed.

Lemma asboolP (P : Prop) : reflect P `[<P>].
87
reflect P `[< P >]
Proof.
17f by apply: (equivP idP); rewrite asboolE. Qed.

Lemma asboolb (b : bool) : `[< b >] = b.
176
`[< b >] = b
Proof.
184 by apply/asboolP/idP. Qed.

Lemma asboolPn (P : Prop) : reflect (~ P) (~~ `[<P>]).
87
reflect (~ P) (~~ `[< P >])
Proof.
18a by rewrite /asbool; case: pselect=> h; constructor. Qed.

Lemma asboolW (P : Prop) : `[<P>] -> P.
87
`[< P >] -> P
Proof.
18f by case: asboolP. Qed.

(* Shall this be a coercion ?*)
Lemma asboolT (P : Prop) : P -> `[<P>].
87
P -> `[< P >]
Proof.
194 by case: asboolP. Qed.

Lemma asboolF (P : Prop) : ~ P -> `[<P>] = false.
87
~ P -> `[< P >] = false
Proof.
199 by apply/introF/asboolP. Qed.

Lemma eq_opE (T : eqType) (x y : T) : (x == y : Prop) = (x = y).
T: eqType
x, y: T
(x == y : Prop) = (x = y)
Proof.
19e by apply/propext; split=> /eqP. Qed.

Lemma is_true_inj : injective is_true.
injective is_true
Proof.
1a6 by move=> [] []; rewrite ?(trueE, falseE) ?propeqE; tauto. Qed.

Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
e4
Equality.axiom (gen_eq (T:=T))
Proof.
1ab by move=> x y; apply: (iffP (asboolP _)). Qed.
Definition gen_eqMixin {T : Type} := EqMixin (@gen_eqP T).

Canonical arrow_eqType (T : Type) (T' : eqType) :=
  EqType (T -> T') gen_eqMixin.
Canonical arrow_choiceType (T : Type) (T' : choiceType) :=
  ChoiceType (T -> T') gen_choiceMixin.

Definition dep_arrow_eqType (T : Type) (T' : T -> eqType) :=
  EqType (forall x : T, T' x) gen_eqMixin.
Definition dep_arrow_choiceClass (T : Type) (T' : T -> choiceType) :=
  Choice.Class (Equality.class (dep_arrow_eqType T')) gen_choiceMixin.
Definition dep_arrow_choiceType (T : Type) (T' : T -> choiceType) :=
  Choice.Pack (dep_arrow_choiceClass T').

Canonical Prop_eqType := EqType Prop gen_eqMixin.
Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin.

Section classicType.
Variable T : Type.
Definition classicType := T.
Canonical classicType_eqType := EqType classicType gen_eqMixin.
Canonical classicType_choiceType := ChoiceType classicType gen_choiceMixin.
End classicType.
Notation "'{classic' T }" := (classicType T)
 (format "'{classic'  T }") : type_scope.

Section eclassicType.
Variable T : eqType.
Definition eclassicType : Type := T.
Canonical eclassicType_eqType := EqType eclassicType (Equality.class T).
Canonical eclassicType_choiceType := ChoiceType eclassicType gen_choiceMixin.
End eclassicType.
Notation "'{eclassic' T }" := (eclassicType T)
 (format "'{eclassic'  T }") : type_scope.

Definition canonical_of T U (sort : U -> T) := forall (G : T -> Type),
  (forall x', G (sort x')) -> forall x, G x.
Notation canonical_ sort := (@canonical_of _ _ sort).
Notation canonical T E := (@canonical_of T E id).

Lemma canon T U (sort : U -> T) : (forall x, exists y, sort y = x) -> canonical_ sort.
2b
sort: U -> T
(forall x : T, exists y : U, sort y = x) ->
canonical_ sort
Proof.
1b0 by move=> + G Gs x => /(_ x)/cid[x' <-]. Qed.
Arguments canon {T U sort} x.

Lemma Peq : canonical Type eqType.
canonical_ [eta Equality.sort]
Proof.
1b7 by apply: canon => T; exists  [eqType of {classic T}]. Qed.
Lemma Pchoice : canonical Type choiceType.
canonical_ [eta Choice.sort]
Proof.
1bc by apply: canon => T; exists [choiceType of {classic T}]. Qed.
Lemma eqPchoice : canonical eqType choiceType.
canonical_ [eta Choice.eqType]
Proof.
1c1 by apply: canon=> T; exists [choiceType of {eclassic T}]; case: T. Qed.

Lemma not_True : (~ True) = False.
(~ True) = False Proof.
1c6 exact/propext. Qed.
Lemma not_False : (~ False) = True.
(~ False) = True Proof.
1cb by apply/propext; split=> _. Qed.

(* -------------------------------------------------------------------- *)
Lemma asbool_equiv_eq {P Q : Prop} : (P <-> Q) -> `[<P>] = `[<Q>].
23
P <-> Q -> `[< P >] = `[< Q >]
Proof.
1d0 by rewrite -propeqE => ->. Qed.

Lemma asbool_equiv_eqP {P Q : Prop} b : reflect Q b -> (P <-> Q) -> `[<P>] = b.
24
176
reflect Q b -> P <-> Q -> `[< P >] = b
Proof.
1d5 by move=> Q_b [PQ QP]; apply/asboolP/Q_b. Qed.

Lemma asbool_equiv {P Q : Prop} : (P <-> Q) -> (`[<P>] <-> `[<Q>]).
23
P <-> Q -> `[< P >] <-> `[< Q >]
Proof.
1db by move/asbool_equiv_eq->. Qed.

Lemma asbool_eq_equiv {P Q : Prop} : `[<P>] = `[<Q>] -> (P <-> Q).
23
`[< P >] = `[< Q >] -> P <-> Q
Proof.
1e0 by move=> eq; split=> /asboolP; rewrite (eq, =^~ eq) => /asboolP. Qed.

(* -------------------------------------------------------------------- *)
Lemma and_asboolP (P Q : Prop) : reflect (P /\ Q) (`[< P >] && `[< Q >]).
23
reflect (P /\ Q) (`[< P >] && `[< Q >])
Proof.
1e5
apply: (iffP idP); first by case/andP => /asboolP p /asboolP q.
23
P /\ Q -> `[< P >] && `[< Q >]
by case=> /asboolP-> /asboolP->.
Qed.

Lemma and3_asboolP (P Q R : Prop) :
  reflect [/\ P, Q & R] [&& `[< P >], `[< Q >] & `[< R >]].
P, Q, R: Prop
reflect [/\ P, Q & R]
  [&& `[< P >], `[< Q >] & `[< R >]]
Proof.
1ee
apply: (iffP idP); first by case/and3P => /asboolP p /asboolP q /asboolP r.
1f0
[/\ P, Q & R] -> [&& `[< P >], `[< Q >] & `[< R >]]
by case => /asboolP -> /asboolP -> /asboolP ->.
Qed.

Lemma or_asboolP (P Q : Prop) : reflect (P \/ Q) (`[< P >] || `[< Q >]).
23
reflect (P \/ Q) (`[< P >] || `[< Q >])
Proof.
1f9
apply: (iffP idP); first by case/orP=> /asboolP; [left | right].
23
P \/ Q -> `[< P >] || `[< Q >]
by case=> /asboolP-> //=; rewrite orbT.
Qed.

Lemma or3_asboolP (P Q R : Prop) :
  reflect [\/ P, Q | R] [|| `[< P >], `[< Q >] | `[< R >]].
1f0
reflect [\/ P, Q | R]
  [|| `[< P >], `[< Q >] | `[< R >]]
Proof.
202
apply: (iffP idP); last by case=> [| |] /asboolP -> //=; rewrite !orbT.
1f0
[|| `[< P >], `[< Q >] | `[< R >]] -> [\/ P, Q | R]
by case/orP=> [/asboolP p|/orP[]/asboolP]; [exact:Or31|exact:Or32|exact:Or33].
Qed.

Lemma asbool_neg {P : Prop} : `[<~ P>] = ~~ `[<P>].
87
`[< ~ P >] = ~~ `[< P >]
Proof.
20b by apply/idP/asboolPn=> [/asboolP|/asboolT]. Qed.

Lemma asbool_or {P Q : Prop} : `[<P \/ Q>] = `[<P>] || `[<Q>].
23
`[< P \/ Q >] = `[< P >] || `[< Q >]
Proof.
210 exact: (asbool_equiv_eqP (or_asboolP _ _)). Qed.

Lemma asbool_and {P Q : Prop} : `[<P /\ Q>] = `[<P>] && `[<Q>].
23
`[< P /\ Q >] = `[< P >] && `[< Q >]
Proof.
215 exact: (asbool_equiv_eqP (and_asboolP _ _)). Qed.

(* -------------------------------------------------------------------- *)
Lemma imply_asboolP {P Q : Prop} : reflect (P -> Q) (`[<P>] ==> `[<Q>]).
23
reflect (P -> Q) (`[< P >] ==> `[< Q >])
Proof.
21a
apply: (iffP implyP)=> [PQb /asboolP/PQb/asboolW //|].
23
(P -> Q) -> `[< P >] -> `[< Q >]
by move=> PQ /asboolP/PQ/asboolT.
Qed.

Lemma asbool_imply {P Q : Prop} : `[<P -> Q>] = `[<P>] ==> `[<Q>].
23
`[< P -> Q >] = `[< P >] ==> `[< Q >]
Proof.
223 exact: (asbool_equiv_eqP imply_asboolP). Qed.

Lemma imply_asboolPn (P Q : Prop) : reflect (P /\ ~ Q) (~~ `[<P -> Q>]).
23
reflect (P /\ ~ Q) (~~ `[< P -> Q >])
Proof.
228
apply: (iffP idP).
23
~~ `[< P -> Q >] -> P /\ ~ Q
23
P /\ ~ Q -> ~~ `[< P -> Q >]
by rewrite asbool_imply negb_imply -asbool_neg => /and_asboolP.
23
232
by move/and_asboolP; rewrite asbool_neg -negb_imply asbool_imply.
Qed.

(* -------------------------------------------------------------------- *)
Lemma forall_asboolP {T : Type} (P : T -> Prop) :
  reflect (forall x, `[<P x>]) (`[<forall x, P x>]).
61
15f
reflect (forall x : T, `[< P x >])
  `[< forall x : T, P x >]
Proof.
237
apply: (iffP idP); first by move/asboolP=> Px x; apply/asboolP.
239
(forall x : T, `[< P x >]) -> `[< forall x : T, P x >]
by move=> Px; apply/asboolP=> x; apply/asboolP.
Qed.

Lemma exists_asboolP {T : Type} (P : T -> Prop) :
  reflect (exists x, `[<P x>]) (`[<exists x, P x>]).
239
reflect (exists x : T, `[< P x >])
  `[< exists x : T, P x >]
Proof.
241
apply: (iffP idP); first by case/asboolP=> x Px; exists x; apply/asboolP.
239
(exists x : T, `[< P x >]) -> `[< exists x : T, P x >]
by case=> x bPx; apply/asboolP; exists x; apply/asboolP.
Qed.

(* -------------------------------------------------------------------- *)

Lemma notT (P : Prop) : P = False -> ~ P.
87
P = False -> ~ P Proof.
24a by move->. Qed.

Lemma contrapT P : ~ ~ P -> P.
87
~ ~ P -> P
Proof.
24f
by move/asboolPn=> nnb; apply/asboolP; apply: contraR nnb => /asboolPn /asboolP.
Qed.

Lemma notTE (P : Prop) : (~ P) -> P = False.
119
Proof.11c by case: (pdegen P)=> ->. Qed.

Lemma notFE (P : Prop) : (~ P) = False -> P.
87
(~ P) = False -> P
Proof.
255 move/notT; exact: contrapT. Qed.

Lemma notK : involutive not.
involutive not
Proof.
25a
move=> P; case: (pdegen P)=> ->; last by apply: notTE; intuition.
87
(~ ~ True) = True
by rewrite [~ True]notTE //; case: (pdegen (~ False)) => // /notFE.
Qed.

Lemma contra_notP (Q P : Prop) : (~ Q -> P) -> ~ P -> Q.
Q, P: Prop
(~ Q -> P) -> ~ P -> Q
Proof.
263
move=> cb /asboolPn nb; apply/asboolP.
266
cb: ~ Q -> P
nb: ~~ `[< P >]
`[< Q >]
by apply: contraR nb => /asboolP /cb /asboolP.
Qed.

Lemma contraPP (Q P : Prop) : (~ Q -> ~ P) -> P -> Q.
265
(~ Q -> ~ P) -> P -> Q
Proof.
271
move=> cb /asboolP hb; apply/asboolP.
266
cb: ~ Q -> ~ P
hb: `[< P >]
26f
by apply: contraLR hb => /asboolP /cb /asboolPn.
Qed.

Lemma contra_notT b (P : Prop) : (~~ b -> P) -> ~ P -> b.
176
88
(~~ b -> P) -> ~ P -> b
Proof.
27c by move=> bP; apply: contra_notP => /negP. Qed.

Lemma contraPT (P : Prop) b : (~~ b -> ~ P) -> P -> b.
175
(~~ b -> ~ P) -> P -> b
Proof.
282 by move=> /contra_notT; rewrite notK. Qed.

Lemma contraTP b (Q : Prop) : (~ Q -> ~~ b) -> b -> Q.
176
Q: Prop
(~ Q -> ~~ b) -> b -> Q
Proof.
287 by move=> QB; apply: contraPP => /QB/negP. Qed.

Lemma contraNP (P : Prop) (b : bool) : (~ P -> b) -> ~~ b -> P.
175
(~ P -> b) -> ~~ b -> P
Proof.
28e by move=> /contra_notP + /negP => /[apply]. Qed.

Lemma contra_neqP (T : eqType) (x y : T) P : (~ P -> x = y) -> x != y -> P.
1a1
1a2
88
(~ P -> x = y) -> x != y -> P
Proof.
293 by move=> Pxy; apply: contraNP => /Pxy/eqP. Qed.

Lemma contra_eqP (T : eqType) (x y : T) (Q : Prop) : (~ Q -> x != y) -> x = y -> Q.
1a1
1a2
28a
(~ Q -> x != y) -> x = y -> Q
Proof.
299 by move=> Qxy /eqP; apply: contraTP. Qed.

Lemma wlog_neg P : (~ P -> P) -> P.
87
(~ P -> P) -> P
Proof.
29f by move=> ?; case: (pselect P). Qed.

Lemma not_inj : injective not.
injective not Proof.
2a4 exact: can_inj notK. Qed.
Lemma notLR P Q : (P = ~ Q) -> (~ P) = Q.
23
P = (~ Q) -> (~ P) = Q Proof.
2a9 exact: canLR notK. Qed.

Lemma notRL P Q : (~ P) = Q -> P = ~ Q.
23
(~ P) = Q -> P = (~ Q) Proof.
2ae exact: canRL notK. Qed.

Lemma iff_notr (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q).
23
(P <-> ~ Q) <-> (~ P <-> Q)
Proof.
2b3 by split=> [/propext ->|/propext <-]; rewrite notK. Qed.

Lemma iff_not2 (P Q : Prop) : (~ P <-> ~ Q) <-> (P <-> Q).
23
(~ P <-> ~ Q) <-> (P <-> Q)
Proof.
2b8 by split=> [/iff_notr|PQ]; [|apply/iff_notr]; rewrite notK. Qed.

(* -------------------------------------------------------------------- *)
(* assia : let's see if we need the simplpred machinery. In any case, we sould
   first try definitions + appropriate Arguments setting to see whether these
   can replace the canonical structures machinery. *)

Definition predp T := T -> Prop.

Identity Coercion fun_of_pred : predp >-> Funclass.

Definition relp T := T -> predp T.

Identity Coercion fun_of_rel : rel >-> Funclass.

Notation xpredp0 := (fun _ => False).
Notation xpredpT := (fun _ => True).
Notation xpredpI := (fun (p1 p2 : predp _) x => p1 x /\ p2 x).
Notation xpredpU := (fun (p1 p2 : predp _) x => p1 x \/ p2 x).
Notation xpredpC := (fun (p : predp _) x => ~ p x).
Notation xpredpD := (fun (p1 p2 : predp _) x => ~ p2 x /\ p1 x).
Notation xpreimp := (fun f (p : predp _) x => p (f x)).
Notation xrelpU := (fun (r1 r2 : relp _) x y => r1 x y \/ r2 x y).

(* -------------------------------------------------------------------- *)
Definition pred0p (T : Type) (P : predp T) : bool := `[<P =1 xpredp0>].
Prenex Implicits pred0p.

Lemma pred0pP  (T : Type) (P : predp T) : reflect (P =1 xpredp0) (pred0p P).
61
P: predp T
reflect (P =1 xpredp0) (pred0p P)
Proof.
2bd by apply: (iffP (asboolP _)). Qed.

(* -------------------------------------------------------------------- *)
Lemma forallp_asboolPn {T} {P : T -> Prop} :
  reflect (forall x : T, ~ P x) (~~ `[<exists x : T, P x>]).
239
reflect (forall x : T, ~ P x)
  (~~ `[< exists x : T, P x >])
Proof.
2c4
apply: (iffP idP)=> [/asboolPn NP x Px|NP].
61
15f
NP: ~ (exists x : T, P x)
fb
100
False
61
15f
NP: forall x : T, ~ P x
~~ `[< exists x : T, P x >]
by apply/NP; exists x.
2d0
2d2 by apply/asboolP=> -[x]; apply/NP.
Qed.

Lemma existsp_asboolPn {T} {P : T -> Prop} :
  reflect (exists x : T, ~ P x) (~~ `[<forall x : T, P x>]).
239
reflect (exists x : T, ~ P x)
  (~~ `[< forall x : T, P x >])
Proof.
2d7
apply: (iffP idP); last by case=> x NPx; apply/asboolPn=> /(_ x).
239
~~ `[< forall x : T, P x >] -> exists x : T, ~ P x
move/asboolPn=> NP; apply/asboolP/negbNE/asboolPn=> h.
61
15f
NP: ~ (forall x : T, P x)
h: ~ (exists x : T, ~ P x)
2cd
by apply/NP=> x; apply/asboolP/negbNE/asboolPn=> NPx; apply/h; exists x.
Qed.

Lemma asbool_forallNb {T : Type} (P : pred T) :
  `[< forall x : T, ~~ (P x) >] = ~~ `[< exists x : T, P x >].
61
f9
`[< forall x : T, ~~ P x >] =
~~ `[< exists x : T, P x >]
Proof.
2e6
apply: (asbool_equiv_eqP forallp_asboolPn);
  by split=> h x; apply/negP/h.
Qed.

Lemma asbool_existsNb {T : Type} (P : pred T) :
  `[< exists x : T, ~~ (P x) >] = ~~ `[< forall x : T, P x >].
2e8
`[< exists x : T, ~~ P x >] =
~~ `[< forall x : T, P x >]
Proof.
2ec
apply: (asbool_equiv_eqP existsp_asboolPn);
  by split=> -[x h]; exists x; apply/negP.
Qed.

Lemma not_implyP (P Q : Prop) : ~ (P -> Q) <-> P /\ ~ Q.
23
~ (P -> Q) <-> P /\ ~ Q
Proof.
2f1
split=> [/asboolP|[p nq pq]]; [|exact/nq/pq].
23
`[< ~ (P -> Q) >] -> P /\ ~ Q
by rewrite asbool_neg => /imply_asboolPn.
Qed.

Lemma not_andP (P Q : Prop) : ~ (P /\ Q) <-> ~ P \/ ~ Q.
23
~ (P /\ Q) <-> ~ P \/ ~ Q
Proof.
2fa
split => [/asboolPn|[|]]; try by apply: contra_not => -[].
23
~~ `[< P /\ Q >] -> ~ P \/ ~ Q
by rewrite asbool_and negb_and => /orP[]/asboolPn; [left|right].
Qed.

Lemma not_and3P (P Q R : Prop) : ~ [/\ P, Q & R] <-> [\/ ~ P, ~ Q | ~ R].
1f0
~ [/\ P, Q & R] <-> [\/ ~ P, ~ Q | ~ R]
Proof.
303
split=> [/and3_asboolP|/or3_asboolP].
1f0
~~ [&& `[< P >], `[< Q >] & `[< R >]] ->
[\/ ~ P, ~ Q | ~ R]
1f0
[|| `[< ~ P >], `[< ~ Q >] | `[< ~ R >]] ->
~ [/\ P, Q & R]
by rewrite 2!negb_and -3!asbool_neg => /or3_asboolP.
1f0
30d
by rewrite 3!asbool_neg -2!negb_and => /and3_asboolP.
Qed.

Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q.
23
~ (P \/ Q) <-> ~ P /\ ~ Q
Proof.
312
split; [apply: contra_notP => /not_andP|apply: contraPnot => AB; apply/not_andP];
  by rewrite 2!notK.
Qed.

Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q).
23
(~ (P -> Q)) = (P /\ ~ Q)
Proof.
317 by rewrite propeqE not_implyP. Qed.

Lemma orC (P Q : Prop) : (P \/ Q) = (Q \/ P).
23
(P \/ Q) = (Q \/ P)
Proof.
31c by rewrite propeqE; split=> [[]|[]]; [right|left|right|left]. Qed.

Lemma orA : associative or.
associative or
Proof.
321 by move=> P Q R; rewrite propeqE; split=> [|]; tauto. Qed.

Lemma andC (P Q : Prop) : (P /\ Q) = (Q /\ P).
23
(P /\ Q) = (Q /\ P)
Proof.
326 by rewrite propeqE; split=> [[]|[]]. Qed.

Lemma andA : associative and.
associative and
Proof.
32b by move=> P Q R; rewrite propeqE; split=> [|]; tauto. Qed.

Lemma forallNE {T} (P : T -> Prop) : (forall x, ~ P x) = ~ exists x, P x.
239
(forall x : T, ~ P x) = (~ (exists x : T, P x))
Proof.
330
by rewrite propeqE; split => [fP [x /fP]//|nexP x Px]; apply: nexP; exists x.
Qed.

Lemma existsNE {T} (P : T -> Prop) : (exists x, ~ P x) = ~ forall x, P x.
239
(exists x : T, ~ P x) = (~ (forall x : T, P x))
Proof.
335
rewrite propeqE; split=> [[x Px] aP //|NaP].
61
15f
NaP: ~ (forall x : T, P x)
exists x : T, ~ P x
by apply: contrapT; rewrite -forallNE => aP; apply: NaP => x; apply: contrapT.
Qed.

Lemma existsNP T (P : T -> Prop) : (exists x, ~ P x) <-> ~ forall x, P x.
239
(exists x : T, ~ P x) <-> ~ (forall x : T, P x)
Proof.
340 by rewrite existsNE. Qed.

Lemma not_existsP T (P : T -> Prop) : (exists x, P x) <-> ~ forall x, ~ P x.
239
(exists x : T, P x) <-> ~ (forall x : T, ~ P x)
Proof.
345 by rewrite forallNE notK. Qed.

Lemma forallNP T (P : T -> Prop) : (forall x, ~ P x) <-> ~ exists x, P x.
239
(forall x : T, ~ P x) <-> ~ (exists x : T, P x)
Proof.
34a by rewrite forallNE. Qed.

Lemma not_forallP T (P : T -> Prop) : (forall x, P x) <-> ~ exists x, ~ P x.
239
(forall x : T, P x) <-> ~ (exists x : T, ~ P x)
Proof.
34f by rewrite existsNE notK. Qed.

Lemma exists2P T (P Q : T -> Prop) :
  (exists2 x, P x & Q x) <-> exists x, P x /\ Q x.
60
(exists2 x : T, P x & Q x) <->
(exists x : T, P x /\ Q x)
Proof.
354 by split=> [[x ? ?] | [x []]]; exists x. Qed.

Lemma not_exists2P T (P Q : T -> Prop) :
  (exists2 x, P x & Q x) <-> ~ forall x, ~ P x \/ ~ Q x.
60
(exists2 x : T, P x & Q x) <->
~ (forall x : T, ~ P x \/ ~ Q x)
Proof.
359
rewrite exists2P not_existsP.
60
~ (forall x : T, ~ (P x /\ Q x)) <->
~ (forall x : T, ~ P x \/ ~ Q x)
by split; apply: contra_not => PQx x;  apply/not_andP; apply: PQx.
Qed.

Lemma forall2NP T (P Q : T -> Prop) :
  (forall x, ~ P x \/ ~ Q x) <-> ~ (exists2 x, P x & Q x).
60
(forall x : T, ~ P x \/ ~ Q x) <->
~ (exists2 x : T, P x & Q x)
Proof.
362
split=> [PQ [t Pt Qt]|PQ t]; first by have [] := PQ t.
61
62
PQ: ~ (exists2 x : T, P x & Q x)
t: T
~ P t \/ ~ Q t
by rewrite -not_andP => -[Pt Qt]; apply PQ; exists t.
Qed.

Lemma forallPNP T (P Q : T -> Prop) :
  (forall x, P x -> ~ Q x) <-> ~ (exists2 x, P x & Q x).
60
(forall x : T, P x -> ~ Q x) <->
~ (exists2 x : T, P x & Q x)
Proof.
36e
split=> [PQ [t Pt Qt]|PQ t]; first by have [] := PQ t.
369
P t -> ~ Q t
by move=> Pt Qt; apply: PQ; exists t.
Qed.

Lemma existsPNP T (P Q : T -> Prop) :
  (exists2 x, P x & ~ Q x) <-> ~ (forall x, P x -> Q x).
60
(exists2 x : T, P x & ~ Q x) <->
~ (forall x : T, P x -> Q x)
Proof.
377
split=> [[x Px NQx] /(_ x Px)//|]; apply: contra_notP => + x Px.
61
62
fb
100
~ (exists2 x : T, P x & ~ Q x) -> Q x
by apply: contra_notP => NQx; exists x.
Qed.

Lemma forallp_asboolPn2 {T} {P Q : T -> Prop} :
  reflect (forall x : T, ~ P x \/ ~ Q x) (~~ `[<exists2 x : T, P x & Q x>]).
60
reflect (forall x : T, ~ P x \/ ~ Q x)
  (~~ `[< exists2 x : T, P x & Q x >])
Proof.
381
apply: (iffP idP)=> [/asboolPn NP x|NP].
61
62
NP: ~ (exists2 x : T, P x & Q x)
fb
~ P x \/ ~ Q x
61
62
NP: forall x : T, ~ P x \/ ~ Q x
~~ `[< exists2 x : T, P x & Q x >]
  by move/forallPNP : NP => /(_ x)/and_rec/not_andP.
38d
38f
by apply/asboolP=> -[x Px Qx]; have /not_andP := NP x; exact.
Qed.

Module FunOrder.
Section FunOrder.
Import Order.TTheory.
Variables (aT : Type) (d : unit) (T : porderType d).
Implicit Types f g h : aT -> T.

Lemma fun_display : unit.
aT: Type
d: unit
T: porderType d
unit Proof.
394 exact: tt. Qed.

Definition lef f g := `[< forall x, (f x <= g x)%O >].
Local Notation "f <= g" := (lef f g).

Definition ltf f g := `[< (forall x, (f x <= g x)%O) /\ exists x, f x != g x >].
Local Notation "f < g" := (ltf f g).

Lemma ltf_def f g : (f < g) = (g != f) && (f <= g).
397
398
399
f, g: aT -> T
(f < g) = (g != f) && (f <= g)
Proof.
39d
apply/idP/andP => [fg|[gf fg]]; [split|apply/asboolP; split; [exact/asboolP|]].
397
398
399
3a0
fg: f < g
g != f
3a6
f <= g
397
398
399
3a0
gf: g != f
fg: f <= g
exists x : aT, f x != g x
-
3a4 by apply/eqP => gf; move: fg => /asboolP[fg] [x /eqP]; apply; rewrite gf.
3a6
3ab
3ac
-
3b3 apply/asboolP => x; rewrite le_eqVlt; move/asboolP : fg => [fg [y gfy]].
397
398
399
3a0
x: aT
fg: forall x : aT, (f x <= g x)%O
y: aT
gfy: f y != g y
(f x == g x) || (f x < g x)%O
3b5
  by have [//|gfx /=] := boolP (f x == g x); rewrite lt_neqAle gfx /= fg.
3ad
3b0
-
3c1 apply/not_existsP => h.
397
398
399
3a0
3ae
3af
h: forall x : aT, ~ f x != g x
2cd
  have : f =1 g by move=> x; have /negP/negPn/eqP := h x.
3c7
f =1 g -> False
  by rewrite -funeqE; apply/nesym/eqP.
Qed.

Fact lef_refl : reflexive lef.
396
reflexive lef Proof.
3ce by move=> f; apply/asboolP => x. Qed.

Fact lef_anti : antisymmetric lef.
396
antisymmetric lef
Proof.
3d3
move=> f g => /andP[/asboolP fg /asboolP gf]; rewrite funeqE => x.
397
398
399
3a0
3bc
gf: forall x : aT, (g x <= f x)%O
3bb
f x = g x
by apply/eqP; rewrite eq_le fg gf.
Qed.

Fact lef_trans : transitive lef.
396
transitive lef
Proof.
3de
move=> g f h /asboolP fg /asboolP gh; apply/asboolP => x.
397
398
399
g, f, h: aT -> T
3bc
gh: forall x : aT, (g x <= h x)%O
3bb
(f x <= h x)%O
by rewrite (le_trans (fg x)).
Qed.

Definition porderMixin :=
  @LePOrderMixin _ lef ltf ltf_def lef_refl lef_anti lef_trans.

Canonical porderType := POrderType fun_display (aT -> T) porderMixin.

End FunOrder.

Section FunLattice.
Import Order.TTheory.
Variables (aT : Type) (d : unit) (T : latticeType d).
Implicit Types f g h : aT -> T.

Definition meetf f g := fun x => Order.meet (f x) (g x).
Definition joinf f g := fun x => Order.join (f x) (g x).

Lemma meetfC : commutative meetf.
397
398
T: latticeType d
commutative meetf
Proof.
3ea move=> f g; apply/funext => x; exact: meetC. Qed.

Lemma joinfC : commutative joinf.
3ec
commutative joinf
Proof.
3f1 move=> f g; apply/funext => x; exact: joinC. Qed.

Lemma meetfA : associative meetf.
3ec
associative meetf
Proof.
3f6 move=> f g h; apply/funext => x; exact: meetA. Qed.

Lemma joinfA : associative joinf.
3ec
associative joinf
Proof.
3fb move=> f g h; apply/funext => x; exact: joinA. Qed.

Lemma joinfKI g f : meetf f (joinf f g) = f.
397
398
3ed
g, f: aT -> T
meetf f (joinf f g) = f
Proof.
400 apply/funext => x; exact: joinKI. Qed.

Lemma meetfKU g f : joinf f (meetf f g) = f.
402
joinf f (meetf f g) = f
Proof.
407 apply/funext => x; exact: meetKU. Qed.

Lemma lef_meet f g : (f <= g)%O = (meetf f g == f).
397
398
3ed
3a0
(f <= g)%O = (meetf f g == f)
Proof.
40c
apply/idP/idP => [/asboolP f_le_g|/eqP <-].
397
398
3ed
3a0
f_le_g: forall x : aT, (f x <= g x)%O
meetf f g == f
40e
(meetf f g <= g)%O
-
412 apply/eqP/funext => x; exact/meet_l/f_le_g.
40e
419
-
41c apply/asboolP => x; exact: leIr.
Qed.

Definition latticeMixin :=
  LatticeMixin meetfC joinfC meetfA joinfA joinfKI meetfKU lef_meet.

Canonical latticeType := LatticeType (aT -> T) latticeMixin.

End FunLattice.
Module Exports.
Canonical porderType.
Ignoring canonical projection to forall _, _ by
Order.POrder.sort in porderType: redundant with
porderType
[redundant-canonical-projection,typechecker]
Canonical latticeType.
Ignoring canonical projection to forall _, _ by
Order.Lattice.sort in latticeType: redundant with
latticeType
[redundant-canonical-projection,typechecker]
End Exports.
End FunOrder.
Export FunOrder.Exports.

Lemma lefP (aT : Type) d (T : porderType d) (f g : aT -> T) :
  reflect (forall x, (f x <= g x)%O) (f <= g)%O.
39f
reflect (forall x : aT, (f x <= g x)%O) (f <= g)%O
Proof.
422 by apply: (iffP idP) => [fg|fg]; [exact/asboolP | apply/asboolP]. Qed.

Lemma meetfE (aT : Type) d (T : latticeType d) (f g : aT -> T) x :
  ((f `&` g) x = f x `&` g x)%O.
397
398
3ed
3a0
3bb
(f `&` g)%O x = (f x `&` g x)%O
Proof.
427 by []. Qed.

Lemma joinfE (aT : Type) d (T : latticeType d) (f g : aT -> T) x :
  ((f `|` g) x = f x `|` g x)%O.
429
(f `|` g)%O x = (f x `|` g x)%O
Proof.
42d by []. Qed.

Lemma iterfS {T} (f : T -> T) (n : nat) : iter n.+1 f = f \o iter n f.
61
f: T -> T
fa
iter n.+1 f = f \o iter n f
Proof.
432 by []. Qed.

Lemma iterfSr {T} (f : T -> T) (n : nat) : iter n.+1 f = iter n f \o f.
434
iter n.+1 f = iter n f \o f
Proof.
439 by apply/funeqP => ?; rewrite iterSr. Qed.

Lemma iter0 {T} (f : T -> T) : iter 0 f = id.
61
435
iter 0 f = id
Proof.
43e by []. Qed.