Module mathcomp.classical.boolp
From HB Require Import structures.From mathcomp Require Import all_ssreflect.
From mathcomp Require Import mathcomp_extra.
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
- R. Affeldt, C. Cohen, D. Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. JFR 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}.
Proof.
Record mextensionality := {
_ : 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 extensionality : mextensionality.
Proof.
Lemma propext (P Q : Prop) : (P <-> Q) -> (P = Q).
Proof.
Ltac eqProp := apply: propext; split.
Lemma funext {T U : Type} (f g : T -> U) : (f =1 g) -> f = g.
Proof.
Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q).
Proof.
Lemma propeqP (P Q : Prop) : (P = Q) <-> (P <-> Q).
Proof.
Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g).
Proof.
Lemma funeq2E {T U V : Type} (f g : T -> U -> V) : (f = g) = (f =2 g).
Proof.
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).
Proof.
Lemma funeqP {T U : Type} (f g : T -> U) : (f = g) <-> (f =1 g).
Proof.
Lemma funeq2P {T U V : Type} (f g : T -> U -> V) : (f = g) <-> (f =2 g).
Proof.
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).
Proof.
Lemma predeqE {T} (P Q : T -> Prop) : (P = Q) = (forall x, P x <-> Q x).
Proof.
Lemma predeq2E {T U} (P Q : T -> U -> Prop) :
(P = Q) = (forall x y, P x y <-> Q x y).
Proof.
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).
Proof.
Lemma predeqP {T} (A B : T -> Prop) : (A = B) <-> (forall x, A x <-> B x).
Proof.
Lemma predeq2P {T U} (P Q : T -> U -> Prop) :
(P = Q) <-> (forall x y, P x y <-> Q x y).
Proof.
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).
Proof.
Lemma propT {P : Prop} : P -> P = True.
Proof.
Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.
Proof.
#[global] Hint Resolve Prop_irrelevance : core.Record mclassic := {
_ : forall (P : Prop), {P} + {~P};
_ : forall T, hasChoice T
}.
Lemma choice X Y (P : X -> Y -> Prop) :
(forall x, exists y, P x y) -> {f & forall x, P x (f x)}.
Proof.
Theorem EM P : P \/ ~ P.
Proof.
Lemma pselect (P : Prop): {P} + {~P}.
Proof.
Lemma pselectT T : (T -> False) + T.
Proof.
Lemma classic : mclassic.
Proof.
Lemma gen_choiceMixin (T : Type) : hasChoice T.
Proof.
Lemma lem (P : Prop): P \/ ~P.
Proof.
Lemma trueE : true = True :> Prop.
Proof.
Lemma falseE : false = False :> Prop.
Proof.
Lemma propF (P : Prop) : ~ P -> P = False.
Proof.
Lemma eq_fun T rT (U V : T -> rT) :
(forall x : T, U x = V x) -> (fun x => U x) = (fun x => V x).
Proof.
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).
Proof.
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).
Proof.
Lemma eq_forall T (U V : T -> Prop) :
(forall x : T, U x = V x) -> (forall x, U x) = (forall x, V x).
Proof.
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).
Proof.
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).
Proof.
Lemma eq_exists T (U V : T -> Prop) :
(forall x : T, U x = V x) -> (exists x, U x) = (exists x, V x).
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
Lemma forall_swap T S (U : forall (x : T) (y : S), Prop) :
(forall x y, U x y) = (forall y x, U x y).
Proof.
Lemma exists_swap T S (U : forall (x : T) (y : S), Prop) :
(exists x y, U x y) = (exists y x, U x y).
Proof.
Lemma reflect_eq (P : Prop) (b : bool) : reflect P b -> P = b.
Proof.
Definition asbool (P : Prop) := if pselect P then true else false.
Notation "`[< P >]" := (asbool P) : bool_scope.
Lemma asboolE (P : Prop) : `[<P>] = P :> Prop.
Proof.
Lemma asboolP (P : Prop) : reflect P `[<P>].
Proof.
Lemma asboolb (b : bool) : `[< b >] = b.
Proof.
Lemma asboolPn (P : Prop) : reflect (~ P) (~~ `[<P>]).
Proof.
Lemma asboolW (P : Prop) : `[<P>] -> P.
Proof.
Lemma asboolT (P : Prop) : P -> `[<P>].
Proof.
Lemma asboolF (P : Prop) : ~ P -> `[<P>] = false.
Proof.
Lemma eq_opE (T : eqType) (x y : T) : (x == y : Prop) = (x = y).
Proof.
Lemma is_true_inj : injective is_true.
Proof.
Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
Proof.
Definition gen_eqMixin (T : Type) : hasDecEq T :=hasDecEq.Build T (@gen_eqP T).
HB.instance Definition _ (T : Type) (T' : T -> eqType) :=
gen_eqMixin (forall t : T, T' t).
HB.instance Definition _ (T : Type) (T' : T -> choiceType) :=
gen_choiceMixin (forall t : T, T' t).
HB.instance Definition _ := gen_eqMixin Prop.
HB.instance Definition _ := gen_choiceMixin Prop.
Section classicType.
Variable T : Type.
Definition classicType := T.
HB.instance Definition _ := gen_eqMixin classicType.
HB.instance Definition _ := gen_choiceMixin classicType.
End classicType.
Notation "'{classic' T }" := (classicType T)
(format "'{classic' T }") : type_scope.
Section eclassicType.
Variable T : eqType.
Definition eclassicType : Type := T.
HB.instance Definition _ := Equality.copy eclassicType T.
HB.instance Definition _ := gen_choiceMixin eclassicType.
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.
Proof.
Arguments canon {T U sort} x.Lemma Peq : canonical Type eqType.
Proof.
Lemma Pchoice : canonical Type choiceType.Proof.
Lemma eqPchoice : canonical eqType choiceType.Proof.
Lemma not_True : (~ True) = False. Proof. exact/propext.Lemma not_False : (~ False) = True. Proof. by apply/propext; split=> _.
Lemma asbool_equiv_eq {P Q : Prop} : (P <-> Q) -> `[<P>] = `[<Q>].
Proof.
Lemma asbool_equiv_eqP {P Q : Prop} b : reflect Q b -> (P <-> Q) -> `[<P>] = b.
Proof.
Lemma asbool_equiv {P Q : Prop} : (P <-> Q) -> (`[<P>] <-> `[<Q>]).
Proof.
Lemma asbool_eq_equiv {P Q : Prop} : `[<P>] = `[<Q>] -> (P <-> Q).
Proof.
Lemma and_asboolP (P Q : Prop) : reflect (P /\ Q) (`[< P >] && `[< Q >]).
Proof.
Lemma and3_asboolP (P Q R : Prop) :
reflect [/\ P, Q & R] [&& `[< P >], `[< Q >] & `[< R >]].
Proof.
Lemma or_asboolP (P Q : Prop) : reflect (P \/ Q) (`[< P >] || `[< Q >]).
Proof.
Lemma or3_asboolP (P Q R : Prop) :
reflect [\/ P, Q | R] [|| `[< P >], `[< Q >] | `[< R >]].
Proof.
Lemma asbool_neg {P : Prop} : `[<~ P>] = ~~ `[<P>].
Proof.
Lemma asbool_or {P Q : Prop} : `[<P \/ Q>] = `[<P>] || `[<Q>].
Proof.
Lemma asbool_and {P Q : Prop} : `[<P /\ Q>] = `[<P>] && `[<Q>].
Proof.
Lemma imply_asboolP {P Q : Prop} : reflect (P -> Q) (`[<P>] ==> `[<Q>]).
Proof.
Lemma asbool_imply {P Q : Prop} : `[<P -> Q>] = `[<P>] ==> `[<Q>].
Proof.
Lemma imply_asboolPn (P Q : Prop) : reflect (P /\ ~ Q) (~~ `[<P -> Q>]).
Proof.
Lemma forall_asboolP {T : Type} (P : T -> Prop) :
reflect (forall x, `[<P x>]) (`[<forall x, P x>]).
Proof.
Lemma exists_asboolP {T : Type} (P : T -> Prop) :
reflect (exists x, `[<P x>]) (`[<exists x, P x>]).
Proof.
Variant BoolProp : Prop -> Type :=
| TrueProp : BoolProp True
| FalseProp : BoolProp False.
Lemma PropB P : BoolProp P.
Proof.
Lemma notB : ((~ True) = False) * ((~ False) = True).
Proof.
Lemma andB : left_id True and * right_id True and
* (left_zero False and * right_zero False and * idempotent and).
Proof.
Lemma orB : left_id False or * right_id False or
* (left_zero True or * right_zero True or * idempotent or).
Proof.
Lemma implyB : let imply (P Q : Prop) := P -> Q in
(imply False =1 fun=> True) * (imply^~ False =1 not)
* (left_id True imply * right_zero True imply * self_inverse True imply).
Proof.
Lemma decide_or P Q : P \/ Q -> {P} + {Q}.
Proof.
Lemma notT (P : Prop) : P = False -> ~ P.
Proof.
Lemma contrapT P : ~ ~ P -> P.
Proof.
Lemma notTE (P : Prop) : (~ P) -> P = False. Proof. by case: (PropB P).
Lemma notFE (P : Prop) : (~ P) = False -> P.
Proof.
Lemma notK : involutive not.
Proof.
Lemma contra_notP (Q P : Prop) : (~ Q -> P) -> ~ P -> Q.
Proof.
Lemma contraPP (Q P : Prop) : (~ Q -> ~ P) -> P -> Q.
Proof.
Lemma contra_notT b (P : Prop) : (~~ b -> P) -> ~ P -> b.
Proof.
Lemma contraPT (P : Prop) b : (~~ b -> ~ P) -> P -> b.
Proof.
Lemma contraTP b (Q : Prop) : (~ Q -> ~~ b) -> b -> Q.
Proof.
Lemma contraNP (P : Prop) (b : bool) : (~ P -> b) -> ~~ b -> P.
Proof.
Lemma contra_neqP (T : eqType) (x y : T) P : (~ P -> x = y) -> x != y -> P.
Proof.
Lemma contra_eqP (T : eqType) (x y : T) Q : (~ Q -> x != y) -> x = y -> Q.
Proof.
Lemma contra_leP {disp1} {T1 : porderType disp1} [P : Prop] [x y : T1] :
(~ P -> (x < y)%O) -> (y <= x)%O -> P.
Proof.
Lemma contra_ltP {disp1} {T1 : porderType disp1} [P : Prop] [x y : T1] :
(~ P -> (x <= y)%O) -> (y < x)%O -> P.
Proof.
Lemma wlog_neg P : (~ P -> P) -> P.
Proof.
Lemma not_inj : injective not. Proof. exact: can_inj notK.
Lemma notLR P Q : (P = ~ Q) -> (~ P) = Q. Proof. exact: canLR notK.
Lemma notRL P Q : (~ P) = Q -> P = ~ Q. Proof. exact: canRL notK.
Lemma iff_notr (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q).
Proof.
Lemma iff_not2 (P Q : Prop) : (~ P <-> ~ Q) <-> (P <-> Q).
Proof.
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).
Proof.
Lemma forallp_asboolPn {T} {P : T -> Prop} :
reflect (forall x : T, ~ P x) (~~ `[<exists x : T, P x>]).
Proof.
Lemma existsp_asboolPn {T} {P : T -> Prop} :
reflect (exists x : T, ~ P x) (~~ `[<forall x : T, P x>]).
Proof.
Lemma asbool_forallNb {T : Type} (P : pred T) :
`[< forall x : T, ~~ (P x) >] = ~~ `[< exists x : T, P x >].
Proof.
Lemma asbool_existsNb {T : Type} (P : pred T) :
`[< exists x : T, ~~ (P x) >] = ~~ `[< forall x : T, P x >].
Proof.
Lemma not_implyP (P Q : Prop) : ~ (P -> Q) <-> P /\ ~ Q.
Proof.
Lemma not_andE (P Q : Prop) : (~ (P /\ Q)) = ~ P \/ ~ Q.
Proof.
Lemma not_andP (P Q : Prop) : ~ (P /\ Q) <-> ~ P \/ ~ Q.
Proof.
Lemma not_and3P (P Q R : Prop) : ~ [/\ P, Q & R] <-> [\/ ~ P, ~ Q | ~ R].
Proof.
Lemma notP (P : Prop) : ~ ~ P <-> P.
Proof.
Lemma notE (P : Prop) : (~ ~ P) = P. Proof. by rewrite propeqE notP.
Lemma not_orE (P Q : Prop) : (~ (P \/ Q)) = ~ P /\ ~ Q.
Proof.
Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q.
Proof.
Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q).
Proof.
Lemma implyE (P Q : Prop) : (P -> Q) = (~ P \/ Q).
Proof.
Lemma orC : commutative or.
Proof.
Lemma orA : associative or.
Proof.
Lemma orCA : left_commutative or.
Proof.
Lemma orAC : right_commutative or.
Proof.
Lemma orACA : interchange or or.
Proof.
Lemma orNp P Q : (~ P \/ Q) = (P -> Q).
Proof.
Lemma orpN P Q : (P \/ ~ Q) = (Q -> P)
Proof.
Lemma or3E P Q R : [\/ P, Q | R] = (P \/ Q \/ R).
Proof.
Lemma or4E P Q R S : [\/ P, Q, R | S] = (P \/ Q \/ R \/ S).
Proof.
Lemma andC : commutative and.
Proof.
Lemma andA : associative and.
Proof.
Lemma andCA : left_commutative and.
Proof.
Lemma andAC : right_commutative and.
Proof.
Lemma andACA : interchange and and.
Proof.
Lemma and3E P Q R : [/\ P, Q & R] = (P /\ Q /\ R).
Proof.
Lemma and4E P Q R S : [/\ P, Q, R & S] = (P /\ Q /\ R /\ S).
Proof.
Lemma and5E P Q R S T : [/\ P, Q, R, S & T] = (P /\ Q /\ R /\ S /\ T).
Proof.
Lemma implyNp P Q : (~ P -> Q : Prop) = (P \/ Q).
Proof.
Lemma implypN (P Q : Prop) : (P -> ~ Q) = ~ (P /\ Q).
Proof.
Lemma implyNN P Q : (~ P -> ~ Q) = (Q -> P).
Proof.
Lemma or_andr : right_distributive or and.
Proof.
Lemma or_andl : left_distributive or and.
Proof.
Lemma and_orr : right_distributive and or.
Proof.
Lemma and_orl : left_distributive and or.
Proof.
Lemma forallNE {T} (P : T -> Prop) : (forall x, ~ P x) = ~ exists x, P x.
Proof.
Lemma existsNE {T} (P : T -> Prop) : (exists x, ~ P x) = ~ forall x, P x.
Proof.
Lemma existsNP T (P : T -> Prop) : (exists x, ~ P x) <-> ~ forall x, P x.
Proof.
Lemma not_existsP T (P : T -> Prop) : (exists x, P x) <-> ~ forall x, ~ P x.
Proof.
Lemma forallNP T (P : T -> Prop) : (forall x, ~ P x) <-> ~ exists x, P x.
Proof.
Lemma not_forallP T (P : T -> Prop) : (forall x, P x) <-> ~ exists x, ~ P x.
Proof.
Lemma exists2E A P Q : (exists2 x : A, P x & Q x) = (exists x, P x /\ Q x).
Proof.
Lemma exists2P T (P Q : T -> Prop) :
(exists2 x, P x & Q x) <-> exists x, P x /\ Q x.
Proof.
Lemma not_exists2P T (P Q : T -> Prop) :
(exists2 x, P x & Q x) <-> ~ forall x, ~ P x \/ ~ Q x.
Proof.
Lemma forall2NP T (P Q : T -> Prop) :
(forall x, ~ P x \/ ~ Q x) <-> ~ (exists2 x, P x & Q x).
Proof.
Lemma forallPNP T (P Q : T -> Prop) :
(forall x, P x -> ~ Q x) <-> ~ (exists2 x, P x & Q x).
Proof.
Lemma existsPNP T (P Q : T -> Prop) :
(exists2 x, P x & ~ Q x) <-> ~ (forall x, P x -> Q x).
Proof.
Lemma forallp_asboolPn2 {T} {P Q : T -> Prop} :
reflect (forall x : T, ~ P x \/ ~ Q x) (~~ `[<exists2 x : T, P x & Q x>]).
Proof.
Module FunOrder.
Section FunOrder.
Import Order.TTheory.
Variables (aT : Type) (d : Order.disp_t) (T : porderType d).
Implicit Types f g h : aT -> T.
Lemma fun_display : Order.disp_t. Proof. exact: Order.default_display.
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).
Proof.
Fact lef_refl : reflexive lef. Proof. by move=> f; apply/asboolP => x.
Fact lef_anti : antisymmetric lef.
Proof.
Fact lef_trans : transitive lef.
Proof.
#[export]
HB.instance Definition _ := @Order.isPOrder.Build
fun_display (aT -> T) lef ltf ltf_def lef_refl lef_anti lef_trans.
End FunOrder.
Section FunLattice.
Import Order.TTheory.
Variables (aT : Type) (d : Order.disp_t) (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.
Proof.
Lemma joinfC : commutative joinf.
Proof.
Lemma meetfA : associative meetf.
Proof.
Lemma joinfA : associative joinf.
Proof.
Lemma joinfKI g f : meetf f (joinf f g) = f.
Proof.
Lemma meetfKU g f : joinf f (meetf f g) = f.
Proof.
Lemma lef_meet f g : (f <= g)%O = (meetf f g == f).
Proof.
#[export]
HB.instance Definition _ := Order.POrder_isLattice.Build _ (aT -> T)
meetfC joinfC meetfA joinfA joinfKI meetfKU lef_meet.
End FunLattice.
Module Exports.
HB.reexport.
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.
Proof.
Lemma meetfE (aT : Type) d (T : latticeType d) (f g : aT -> T) x :
((f `&` g) x = f x `&` g x)%O.
Proof.
Lemma joinfE (aT : Type) d (T : latticeType d) (f g : aT -> T) x :
((f `|` g) x = f x `|` g x)%O.
Proof.
Lemma iterfS {T} (f : T -> T) (n : nat) : iter n.+1 f = f \o iter n f.
Proof.
Lemma iterfSr {T} (f : T -> T) (n : nat) : iter n.+1 f = iter n f \o f.
Proof.
Lemma iter0 {T} (f : T -> T) : iter 0 f = id.
Proof.
Section Inhabited.
Variable (T : Type).
Lemma inhabitedE: inhabited T = exists x : T, True.
Proof.
Lemma inhabited_witness: inhabited T -> T.
Proof.
End Inhabited.