Library probsa.util.boolp
(* 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.
(******************************************************************************)
(* 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)*)
(* see lemma lefP. *)
(******************************************************************************)
Set Implicit Arguments.
(* -------------------------------------------------------------------- *)
Axiom functional_extensionality_dep :
∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
(∀ x : A, f x = g x) → f = g.
Axiom propositional_extensionality :
∀ P Q : Prop, P ↔ Q → P = Q.
Axiom constructive_indefinite_description :
∀ (A : Type) (P : A → Prop),
(∃ 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}.
(* -------------------------------------------------------------------- *)
Record mextentionality := {
_ : ∀ (P Q : Prop), (P ↔ Q) → (P = Q);
_ : ∀ {T U : Type} (f g : T → U),
(∀ x, f x = g x) → f = g;
}.
Fact extentionality : mextentionality.
Lemma propext (P Q : Prop) : (P ↔ Q) → (P = Q).
Lemma funext {T U : Type} (f g : T → U) : (f =1 g) → f = g.
Lemma propeqE (P Q : Prop) : (P = Q) = (P ↔ Q).
Lemma propeqP (P Q : Prop) : (P = Q) ↔ (P ↔ Q).
Lemma funeqE {T U : Type} (f g : T → U) : (f = g) = (f =1 g).
Lemma funeq2E {T U V : Type} (f g : T → U → V) : (f = g) = (f =2 g).
Lemma funeq3E {T U V W : Type} (f g : T → U → V → W) :
(f = g) = (∀ x y z, f x y z = g x y z).
Lemma funeqP {T U : Type} (f g : T → U) : (f = g) ↔ (f =1 g).
Lemma funeq2P {T U V : Type} (f g : T → U → V) : (f = g) ↔ (f =2 g).
Lemma funeq3P {T U V W : Type} (f g : T → U → V → W) :
(f = g) ↔ (∀ x y z, f x y z = g x y z).
Lemma predeqE {T} (P Q : T → Prop) : (P = Q) = (∀ x, P x ↔ Q x).
Lemma predeq2E {T U} (P Q : T → U → Prop) :
(P = Q) = (∀ x y, P x y ↔ Q x y).
Lemma predeq3E {T U V} (P Q : T → U → V → Prop) :
(P = Q) = (∀ x y z, P x y z ↔ Q x y z).
Lemma predeqP {T} (A B : T → Prop) : (A = B) ↔ (∀ x, A x ↔ B x).
Lemma predeq2P {T U} (P Q : T → U → Prop) :
(P = Q) ↔ (∀ x y, P x y ↔ Q x y).
Lemma predeq3P {T U V} (P Q : T → U → V → Prop) :
(P = Q) ↔ (∀ x y z, P x y z ↔ Q x y z).
Lemma propT {P : Prop} : P → P = True.
Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.
#[global] Hint Resolve Prop_irrelevance : core.
(* -------------------------------------------------------------------- *)
Record mclassic := {
_ : ∀ (P : Prop), {P} + {¬P};
_ : ∀ T, Choice.mixin_of T
}.
Lemma choice X Y (P : X → Y → Prop) :
(∀ x, ∃ y, P x y) → {f & ∀ x, P x (f x)}.
(* Diaconescu Theorem *)
Theorem EM P : P ∨ ¬ P.
Lemma pselect (P : Prop): {P} + {¬P}.
Lemma pselectT T : (T → False) + T.
Lemma classic : mclassic.
Lemma gen_choiceMixin {T : Type} : Choice.mixin_of T.
Lemma pdegen (P : Prop): P = True ∨ P = False.
Lemma lem (P : Prop): P ∨ ¬P.
(* -------------------------------------------------------------------- *)
Lemma trueE : true = True :> Prop.
Lemma falseE : false = False :> Prop.
Lemma propF (P : Prop) : ¬ P → P = False.
Lemma eq_fun T rT (U V : T → rT) :
(∀ x : T, U x = V x) → (fun x ⇒ U x) = (fun x ⇒ V x).
Lemma eq_fun2 T1 T2 rT (U V : T1 → T2 → rT) :
(∀ x y, U x y = V x y) → (fun x y ⇒ U x y) = (fun x y ⇒ V x y).
Lemma eq_fun3 T1 T2 T3 rT (U V : T1 → T2 → T3 → rT) :
(∀ 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).
Lemma eq_forall T (U V : T → Prop) :
(∀ x : T, U x = V x) → (∀ x, U x) = (∀ x, V x).
Lemma eq_forall2 T S (U V : ∀ x : T, S x → Prop) :
(∀ x y, U x y = V x y) → (∀ x y, U x y) = (∀ x y, V x y).
Lemma eq_forall3 T S R (U V : ∀ (x : T) (y : S x), R x y → Prop) :
(∀ x y z, U x y z = V x y z) →
(∀ x y z, U x y z) = (∀ x y z, V x y z).
Lemma eq_exists T (U V : T → Prop) :
(∀ x : T, U x = V x) → (∃ x, U x) = (∃ x, V x).
Lemma eq_exists2 T S (U V : ∀ x : T, S x → Prop) :
(∀ x y, U x y = V x y) → (∃ x y, U x y) = (∃ x y, V x y).
Lemma eq_exists3 T S R (U V : ∀ (x : T) (y : S x), R x y → Prop) :
(∀ x y z, U x y z = V x y z) →
(∃ x y z, U x y z) = (∃ x y z, V x y z).
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.
Lemma forall_swap T S (U : ∀ (x : T) (y : S), Prop) :
(∀ x y, U x y) = (∀ y x, U x y).
Lemma exists_swap T S (U : ∀ (x : T) (y : S), Prop) :
(∃ x y, U x y) = (∃ y x, U x y).
Lemma reflect_eq (P : Prop) (b : bool) : reflect P b → P = b.
Definition asbool (P : Prop) :=
if pselect P then true else false.
Notation "`[< P >]" := (asbool P) : bool_scope.
Lemma asboolE (P : Prop) : `[<P>] = P :> Prop.
Lemma asboolP (P : Prop) : reflect P `[<P>].
Lemma asboolb (b : bool) : `[< b >] = b.
Lemma asboolPn (P : Prop) : reflect (¬ P) (~~ `[<P>]).
Lemma asboolW (P : Prop) : `[<P>] → P.
(* Shall this be a coercion ?*)
Lemma asboolT (P : Prop) : P → `[<P>].
Lemma asboolF (P : Prop) : ¬ P → `[<P>] = false.
Lemma eq_opE (T : eqType) (x y : T) : (x == y : Prop) = (x = y).
Lemma is_true_inj : injective is_true.
Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
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 (∀ 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) := ∀ (G : T → Type),
(∀ x', G (sort x')) → ∀ 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) : (∀ x, ∃ y, sort y = x) → canonical_ sort.
Lemma Peq : canonical Type eqType.
Lemma Pchoice : canonical Type choiceType.
Lemma eqPchoice : canonical eqType choiceType.
Lemma not_True : (¬ True) = False.
Lemma not_False : (¬ False) = True.
(* -------------------------------------------------------------------- *)
Lemma asbool_equiv_eq {P Q : Prop} : (P ↔ Q) → `[<P>] = `[<Q>].
Lemma asbool_equiv_eqP {P Q : Prop} b : reflect Q b → (P ↔ Q) → `[<P>] = b.
Lemma asbool_equiv {P Q : Prop} : (P ↔ Q) → (`[<P>] ↔ `[<Q>]).
Lemma asbool_eq_equiv {P Q : Prop} : `[<P>] = `[<Q>] → (P ↔ Q).
(* -------------------------------------------------------------------- *)
Lemma and_asboolP (P Q : Prop) : reflect (P ∧ Q) (`[< P >] && `[< Q >]).
Lemma and3_asboolP (P Q R : Prop) :
reflect [/\ P, Q & R] [&& `[< P >], `[< Q >] & `[< R >]].
Lemma or_asboolP (P Q : Prop) : reflect (P ∨ Q) (`[< P >] || `[< Q >]).
Lemma or3_asboolP (P Q R : Prop) :
reflect [\/ P, Q | R] [|| `[< P >], `[< Q >] | `[< R >]].
Lemma asbool_neg {P : Prop} : `[<¬ P>] = ~~ `[<P>].
Lemma asbool_or {P Q : Prop} : `[<P ∨ Q>] = `[<P>] || `[<Q>].
Lemma asbool_and {P Q : Prop} : `[<P ∧ Q>] = `[<P>] && `[<Q>].
(* -------------------------------------------------------------------- *)
Lemma imply_asboolP {P Q : Prop} : reflect (P → Q) (`[<P>] ==> `[<Q>]).
Lemma asbool_imply {P Q : Prop} : `[<P → Q>] = `[<P>] ==> `[<Q>].
Lemma imply_asboolPn (P Q : Prop) : reflect (P ∧ ¬ Q) (~~ `[<P → Q>]).
(* -------------------------------------------------------------------- *)
Lemma forall_asboolP {T : Type} (P : T → Prop) :
reflect (∀ x, `[<P x>]) (`[<∀ x, P x>]).
Lemma exists_asboolP {T : Type} (P : T → Prop) :
reflect (∃ x, `[<P x>]) (`[<∃ x, P x>]).
(* -------------------------------------------------------------------- *)
Lemma notT (P : Prop) : P = False → ¬ P.
Lemma contrapT P : ¬ ¬ P → P.
Lemma notTE (P : Prop) : (¬ P) → P = False.
Lemma notFE (P : Prop) : (¬ P) = False → P.
Lemma notK : involutive not.
Lemma contra_notP (Q P : Prop) : (¬ Q → P) → ¬ P → Q.
Lemma contraPP (Q P : Prop) : (¬ Q → ¬ P) → P → Q.
Lemma contra_notT b (P : Prop) : (~~ b → P) → ¬ P → b.
Lemma contraPT (P : Prop) b : (~~ b → ¬ P) → P → b.
Lemma contraTP b (Q : Prop) : (¬ Q → ~~ b) → b → Q.
Lemma contraNP (P : Prop) (b : bool) : (¬ P → b) → ~~ b → P.
Lemma contra_neqP (T : eqType) (x y : T) P : (¬ P → x = y) → x != y → P.
Lemma contra_eqP (T : eqType) (x y : T) (Q : Prop) : (¬ Q → x != y) → x = y → Q.
Lemma wlog_neg P : (¬ P → P) → P.
Lemma not_inj : injective not.
Lemma notLR P Q : (P = ¬ Q) → (¬ P) = Q.
Lemma notRL P Q : (¬ P) = Q → P = ¬ Q.
Lemma iff_notr (P Q : Prop) : (P ↔ ¬ Q) ↔ (¬ P ↔ Q).
Lemma iff_not2 (P Q : Prop) : (¬ P ↔ ¬ Q) ↔ (P ↔ Q).
(* -------------------------------------------------------------------- *)
(* 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>].
Lemma pred0pP (T : Type) (P : predp T) : reflect (P =1 xpredp0) (pred0p P).
(* -------------------------------------------------------------------- *)
Lemma forallp_asboolPn {T} {P : T → Prop} :
reflect (∀ x : T, ¬ P x) (~~ `[<∃ x : T, P x>]).
Lemma existsp_asboolPn {T} {P : T → Prop} :
reflect (∃ x : T, ¬ P x) (~~ `[<∀ x : T, P x>]).
Lemma asbool_forallNb {T : Type} (P : pred T) :
`[< ∀ x : T, ~~ (P x) >] = ~~ `[< ∃ x : T, P x >].
Lemma asbool_existsNb {T : Type} (P : pred T) :
`[< ∃ x : T, ~~ (P x) >] = ~~ `[< ∀ x : T, P x >].
Lemma not_implyP (P Q : Prop) : ¬ (P → Q) ↔ P ∧ ¬ Q.
Lemma not_andP (P Q : Prop) : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q.
Lemma not_and3P (P Q R : Prop) : ¬ [/\ P, Q & R] ↔ [\/ ¬ P, ¬ Q | ¬ R].
Lemma not_orP (P Q : Prop) : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q.
Lemma not_implyE (P Q : Prop) : (¬ (P → Q)) = (P ∧ ¬ Q).
Lemma orC (P Q : Prop) : (P ∨ Q) = (Q ∨ P).
Lemma orA : associative or.
Lemma andC (P Q : Prop) : (P ∧ Q) = (Q ∧ P).
Lemma andA : associative and.
Lemma forallNE {T} (P : T → Prop) : (∀ x, ¬ P x) = ¬ ∃ x, P x.
Lemma existsNE {T} (P : T → Prop) : (∃ x, ¬ P x) = ¬ ∀ x, P x.
Lemma existsNP T (P : T → Prop) : (∃ x, ¬ P x) ↔ ¬ ∀ x, P x.
Lemma not_existsP T (P : T → Prop) : (∃ x, P x) ↔ ¬ ∀ x, ¬ P x.
Lemma forallNP T (P : T → Prop) : (∀ x, ¬ P x) ↔ ¬ ∃ x, P x.
Lemma not_forallP T (P : T → Prop) : (∀ x, P x) ↔ ¬ ∃ x, ¬ P x.
Lemma exists2P T (P Q : T → Prop) :
(exists2 x, P x & Q x) ↔ ∃ x, P x ∧ Q x.
Lemma not_exists2P T (P Q : T → Prop) :
(exists2 x, P x & Q x) ↔ ¬ ∀ x, ¬ P x ∨ ¬ Q x.
Lemma forall2NP T (P Q : T → Prop) :
(∀ x, ¬ P x ∨ ¬ Q x) ↔ ¬ (exists2 x, P x & Q x).
Lemma forallPNP T (P Q : T → Prop) :
(∀ x, P x → ¬ Q x) ↔ ¬ (exists2 x, P x & Q x).
Lemma existsPNP T (P Q : T → Prop) :
(exists2 x, P x & ¬ Q x) ↔ ¬ (∀ x, P x → Q x).
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.
Definition lef f g := `[< ∀ x, (f x ≤ g x)%O >].
Definition ltf f g := `[< (∀ x, (f x ≤ g x)%O) ∧ ∃ x, f x != g x >].
Lemma ltf_def f g : (f < g) = (g != f) && (f ≤ g).
Fact lef_refl : reflexive lef.
Fact lef_anti : antisymmetric lef.
Fact lef_trans : transitive lef.
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.
Lemma joinfC : commutative joinf.
Lemma meetfA : associative meetf.
Lemma joinfA : associative joinf.
Lemma joinfKI g f : meetf f (joinf f g) = f.
Lemma meetfKU g f : joinf f (meetf f g) = f.
Lemma lef_meet f g : (f ≤ g)%O = (meetf f g == f).
Definition latticeMixin :=
LatticeMixin meetfC joinfC meetfA joinfA joinfKI meetfKU lef_meet.
Canonical latticeType := LatticeType (aT → T) latticeMixin.
End FunLattice.
Module Exports.
Canonical porderType.
Canonical latticeType.
End Exports.
End FunOrder.
Export FunOrder.Exports.
Lemma lefP (aT : Type) d (T : porderType d) (f g : aT → T) :
reflect (∀ x, (f x ≤ g x)%O) (f ≤ g)%O.
Lemma meetfE (aT : Type) d (T : latticeType d) (f g : aT → T) x :
((f `&` g) x = f x `&` g x)%O.
Lemma joinfE (aT : Type) d (T : latticeType d) (f g : aT → T) x :
((f `|` g) x = f x `|` g x)%O.
Lemma iterfS {T} (f : T → T) (n : nat) : iter n.+1 f = f \o iter n f.
Lemma iterfSr {T} (f : T → T) (n : nat) : iter n.+1 f = iter n f \o f.
Lemma iter0 {T} (f : T → T) : iter 0 f = id.
(* -------------------------------------------------------------------- *)
(* Copyright (c) - 2015--2016 - IMDEA Software Institute *)
(* Copyright (c) - 2015--2018 - Inria *)
(* Copyright (c) - 2016--2018 - Polytechnique *)
(* -------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
(******************************************************************************)
(* 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)*)
(* see lemma lefP. *)
(******************************************************************************)
Set Implicit Arguments.
(* -------------------------------------------------------------------- *)
Axiom functional_extensionality_dep :
∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x),
(∀ x : A, f x = g x) → f = g.
Axiom propositional_extensionality :
∀ P Q : Prop, P ↔ Q → P = Q.
Axiom constructive_indefinite_description :
∀ (A : Type) (P : A → Prop),
(∃ 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}.
(* -------------------------------------------------------------------- *)
Record mextentionality := {
_ : ∀ (P Q : Prop), (P ↔ Q) → (P = Q);
_ : ∀ {T U : Type} (f g : T → U),
(∀ x, f x = g x) → f = g;
}.
Fact extentionality : mextentionality.
Lemma propext (P Q : Prop) : (P ↔ Q) → (P = Q).
Lemma funext {T U : Type} (f g : T → U) : (f =1 g) → f = g.
Lemma propeqE (P Q : Prop) : (P = Q) = (P ↔ Q).
Lemma propeqP (P Q : Prop) : (P = Q) ↔ (P ↔ Q).
Lemma funeqE {T U : Type} (f g : T → U) : (f = g) = (f =1 g).
Lemma funeq2E {T U V : Type} (f g : T → U → V) : (f = g) = (f =2 g).
Lemma funeq3E {T U V W : Type} (f g : T → U → V → W) :
(f = g) = (∀ x y z, f x y z = g x y z).
Lemma funeqP {T U : Type} (f g : T → U) : (f = g) ↔ (f =1 g).
Lemma funeq2P {T U V : Type} (f g : T → U → V) : (f = g) ↔ (f =2 g).
Lemma funeq3P {T U V W : Type} (f g : T → U → V → W) :
(f = g) ↔ (∀ x y z, f x y z = g x y z).
Lemma predeqE {T} (P Q : T → Prop) : (P = Q) = (∀ x, P x ↔ Q x).
Lemma predeq2E {T U} (P Q : T → U → Prop) :
(P = Q) = (∀ x y, P x y ↔ Q x y).
Lemma predeq3E {T U V} (P Q : T → U → V → Prop) :
(P = Q) = (∀ x y z, P x y z ↔ Q x y z).
Lemma predeqP {T} (A B : T → Prop) : (A = B) ↔ (∀ x, A x ↔ B x).
Lemma predeq2P {T U} (P Q : T → U → Prop) :
(P = Q) ↔ (∀ x y, P x y ↔ Q x y).
Lemma predeq3P {T U V} (P Q : T → U → V → Prop) :
(P = Q) ↔ (∀ x y z, P x y z ↔ Q x y z).
Lemma propT {P : Prop} : P → P = True.
Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.
#[global] Hint Resolve Prop_irrelevance : core.
(* -------------------------------------------------------------------- *)
Record mclassic := {
_ : ∀ (P : Prop), {P} + {¬P};
_ : ∀ T, Choice.mixin_of T
}.
Lemma choice X Y (P : X → Y → Prop) :
(∀ x, ∃ y, P x y) → {f & ∀ x, P x (f x)}.
(* Diaconescu Theorem *)
Theorem EM P : P ∨ ¬ P.
Lemma pselect (P : Prop): {P} + {¬P}.
Lemma pselectT T : (T → False) + T.
Lemma classic : mclassic.
Lemma gen_choiceMixin {T : Type} : Choice.mixin_of T.
Lemma pdegen (P : Prop): P = True ∨ P = False.
Lemma lem (P : Prop): P ∨ ¬P.
(* -------------------------------------------------------------------- *)
Lemma trueE : true = True :> Prop.
Lemma falseE : false = False :> Prop.
Lemma propF (P : Prop) : ¬ P → P = False.
Lemma eq_fun T rT (U V : T → rT) :
(∀ x : T, U x = V x) → (fun x ⇒ U x) = (fun x ⇒ V x).
Lemma eq_fun2 T1 T2 rT (U V : T1 → T2 → rT) :
(∀ x y, U x y = V x y) → (fun x y ⇒ U x y) = (fun x y ⇒ V x y).
Lemma eq_fun3 T1 T2 T3 rT (U V : T1 → T2 → T3 → rT) :
(∀ 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).
Lemma eq_forall T (U V : T → Prop) :
(∀ x : T, U x = V x) → (∀ x, U x) = (∀ x, V x).
Lemma eq_forall2 T S (U V : ∀ x : T, S x → Prop) :
(∀ x y, U x y = V x y) → (∀ x y, U x y) = (∀ x y, V x y).
Lemma eq_forall3 T S R (U V : ∀ (x : T) (y : S x), R x y → Prop) :
(∀ x y z, U x y z = V x y z) →
(∀ x y z, U x y z) = (∀ x y z, V x y z).
Lemma eq_exists T (U V : T → Prop) :
(∀ x : T, U x = V x) → (∃ x, U x) = (∃ x, V x).
Lemma eq_exists2 T S (U V : ∀ x : T, S x → Prop) :
(∀ x y, U x y = V x y) → (∃ x y, U x y) = (∃ x y, V x y).
Lemma eq_exists3 T S R (U V : ∀ (x : T) (y : S x), R x y → Prop) :
(∀ x y z, U x y z = V x y z) →
(∃ x y z, U x y z) = (∃ x y z, V x y z).
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.
Lemma forall_swap T S (U : ∀ (x : T) (y : S), Prop) :
(∀ x y, U x y) = (∀ y x, U x y).
Lemma exists_swap T S (U : ∀ (x : T) (y : S), Prop) :
(∃ x y, U x y) = (∃ y x, U x y).
Lemma reflect_eq (P : Prop) (b : bool) : reflect P b → P = b.
Definition asbool (P : Prop) :=
if pselect P then true else false.
Notation "`[< P >]" := (asbool P) : bool_scope.
Lemma asboolE (P : Prop) : `[<P>] = P :> Prop.
Lemma asboolP (P : Prop) : reflect P `[<P>].
Lemma asboolb (b : bool) : `[< b >] = b.
Lemma asboolPn (P : Prop) : reflect (¬ P) (~~ `[<P>]).
Lemma asboolW (P : Prop) : `[<P>] → P.
(* Shall this be a coercion ?*)
Lemma asboolT (P : Prop) : P → `[<P>].
Lemma asboolF (P : Prop) : ¬ P → `[<P>] = false.
Lemma eq_opE (T : eqType) (x y : T) : (x == y : Prop) = (x = y).
Lemma is_true_inj : injective is_true.
Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
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 (∀ 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) := ∀ (G : T → Type),
(∀ x', G (sort x')) → ∀ 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) : (∀ x, ∃ y, sort y = x) → canonical_ sort.
Lemma Peq : canonical Type eqType.
Lemma Pchoice : canonical Type choiceType.
Lemma eqPchoice : canonical eqType choiceType.
Lemma not_True : (¬ True) = False.
Lemma not_False : (¬ False) = True.
(* -------------------------------------------------------------------- *)
Lemma asbool_equiv_eq {P Q : Prop} : (P ↔ Q) → `[<P>] = `[<Q>].
Lemma asbool_equiv_eqP {P Q : Prop} b : reflect Q b → (P ↔ Q) → `[<P>] = b.
Lemma asbool_equiv {P Q : Prop} : (P ↔ Q) → (`[<P>] ↔ `[<Q>]).
Lemma asbool_eq_equiv {P Q : Prop} : `[<P>] = `[<Q>] → (P ↔ Q).
(* -------------------------------------------------------------------- *)
Lemma and_asboolP (P Q : Prop) : reflect (P ∧ Q) (`[< P >] && `[< Q >]).
Lemma and3_asboolP (P Q R : Prop) :
reflect [/\ P, Q & R] [&& `[< P >], `[< Q >] & `[< R >]].
Lemma or_asboolP (P Q : Prop) : reflect (P ∨ Q) (`[< P >] || `[< Q >]).
Lemma or3_asboolP (P Q R : Prop) :
reflect [\/ P, Q | R] [|| `[< P >], `[< Q >] | `[< R >]].
Lemma asbool_neg {P : Prop} : `[<¬ P>] = ~~ `[<P>].
Lemma asbool_or {P Q : Prop} : `[<P ∨ Q>] = `[<P>] || `[<Q>].
Lemma asbool_and {P Q : Prop} : `[<P ∧ Q>] = `[<P>] && `[<Q>].
(* -------------------------------------------------------------------- *)
Lemma imply_asboolP {P Q : Prop} : reflect (P → Q) (`[<P>] ==> `[<Q>]).
Lemma asbool_imply {P Q : Prop} : `[<P → Q>] = `[<P>] ==> `[<Q>].
Lemma imply_asboolPn (P Q : Prop) : reflect (P ∧ ¬ Q) (~~ `[<P → Q>]).
(* -------------------------------------------------------------------- *)
Lemma forall_asboolP {T : Type} (P : T → Prop) :
reflect (∀ x, `[<P x>]) (`[<∀ x, P x>]).
Lemma exists_asboolP {T : Type} (P : T → Prop) :
reflect (∃ x, `[<P x>]) (`[<∃ x, P x>]).
(* -------------------------------------------------------------------- *)
Lemma notT (P : Prop) : P = False → ¬ P.
Lemma contrapT P : ¬ ¬ P → P.
Lemma notTE (P : Prop) : (¬ P) → P = False.
Lemma notFE (P : Prop) : (¬ P) = False → P.
Lemma notK : involutive not.
Lemma contra_notP (Q P : Prop) : (¬ Q → P) → ¬ P → Q.
Lemma contraPP (Q P : Prop) : (¬ Q → ¬ P) → P → Q.
Lemma contra_notT b (P : Prop) : (~~ b → P) → ¬ P → b.
Lemma contraPT (P : Prop) b : (~~ b → ¬ P) → P → b.
Lemma contraTP b (Q : Prop) : (¬ Q → ~~ b) → b → Q.
Lemma contraNP (P : Prop) (b : bool) : (¬ P → b) → ~~ b → P.
Lemma contra_neqP (T : eqType) (x y : T) P : (¬ P → x = y) → x != y → P.
Lemma contra_eqP (T : eqType) (x y : T) (Q : Prop) : (¬ Q → x != y) → x = y → Q.
Lemma wlog_neg P : (¬ P → P) → P.
Lemma not_inj : injective not.
Lemma notLR P Q : (P = ¬ Q) → (¬ P) = Q.
Lemma notRL P Q : (¬ P) = Q → P = ¬ Q.
Lemma iff_notr (P Q : Prop) : (P ↔ ¬ Q) ↔ (¬ P ↔ Q).
Lemma iff_not2 (P Q : Prop) : (¬ P ↔ ¬ Q) ↔ (P ↔ Q).
(* -------------------------------------------------------------------- *)
(* 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>].
Lemma pred0pP (T : Type) (P : predp T) : reflect (P =1 xpredp0) (pred0p P).
(* -------------------------------------------------------------------- *)
Lemma forallp_asboolPn {T} {P : T → Prop} :
reflect (∀ x : T, ¬ P x) (~~ `[<∃ x : T, P x>]).
Lemma existsp_asboolPn {T} {P : T → Prop} :
reflect (∃ x : T, ¬ P x) (~~ `[<∀ x : T, P x>]).
Lemma asbool_forallNb {T : Type} (P : pred T) :
`[< ∀ x : T, ~~ (P x) >] = ~~ `[< ∃ x : T, P x >].
Lemma asbool_existsNb {T : Type} (P : pred T) :
`[< ∃ x : T, ~~ (P x) >] = ~~ `[< ∀ x : T, P x >].
Lemma not_implyP (P Q : Prop) : ¬ (P → Q) ↔ P ∧ ¬ Q.
Lemma not_andP (P Q : Prop) : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q.
Lemma not_and3P (P Q R : Prop) : ¬ [/\ P, Q & R] ↔ [\/ ¬ P, ¬ Q | ¬ R].
Lemma not_orP (P Q : Prop) : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q.
Lemma not_implyE (P Q : Prop) : (¬ (P → Q)) = (P ∧ ¬ Q).
Lemma orC (P Q : Prop) : (P ∨ Q) = (Q ∨ P).
Lemma orA : associative or.
Lemma andC (P Q : Prop) : (P ∧ Q) = (Q ∧ P).
Lemma andA : associative and.
Lemma forallNE {T} (P : T → Prop) : (∀ x, ¬ P x) = ¬ ∃ x, P x.
Lemma existsNE {T} (P : T → Prop) : (∃ x, ¬ P x) = ¬ ∀ x, P x.
Lemma existsNP T (P : T → Prop) : (∃ x, ¬ P x) ↔ ¬ ∀ x, P x.
Lemma not_existsP T (P : T → Prop) : (∃ x, P x) ↔ ¬ ∀ x, ¬ P x.
Lemma forallNP T (P : T → Prop) : (∀ x, ¬ P x) ↔ ¬ ∃ x, P x.
Lemma not_forallP T (P : T → Prop) : (∀ x, P x) ↔ ¬ ∃ x, ¬ P x.
Lemma exists2P T (P Q : T → Prop) :
(exists2 x, P x & Q x) ↔ ∃ x, P x ∧ Q x.
Lemma not_exists2P T (P Q : T → Prop) :
(exists2 x, P x & Q x) ↔ ¬ ∀ x, ¬ P x ∨ ¬ Q x.
Lemma forall2NP T (P Q : T → Prop) :
(∀ x, ¬ P x ∨ ¬ Q x) ↔ ¬ (exists2 x, P x & Q x).
Lemma forallPNP T (P Q : T → Prop) :
(∀ x, P x → ¬ Q x) ↔ ¬ (exists2 x, P x & Q x).
Lemma existsPNP T (P Q : T → Prop) :
(exists2 x, P x & ¬ Q x) ↔ ¬ (∀ x, P x → Q x).
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.
Definition lef f g := `[< ∀ x, (f x ≤ g x)%O >].
Definition ltf f g := `[< (∀ x, (f x ≤ g x)%O) ∧ ∃ x, f x != g x >].
Lemma ltf_def f g : (f < g) = (g != f) && (f ≤ g).
Fact lef_refl : reflexive lef.
Fact lef_anti : antisymmetric lef.
Fact lef_trans : transitive lef.
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.
Lemma joinfC : commutative joinf.
Lemma meetfA : associative meetf.
Lemma joinfA : associative joinf.
Lemma joinfKI g f : meetf f (joinf f g) = f.
Lemma meetfKU g f : joinf f (meetf f g) = f.
Lemma lef_meet f g : (f ≤ g)%O = (meetf f g == f).
Definition latticeMixin :=
LatticeMixin meetfC joinfC meetfA joinfA joinfKI meetfKU lef_meet.
Canonical latticeType := LatticeType (aT → T) latticeMixin.
End FunLattice.
Module Exports.
Canonical porderType.
Canonical latticeType.
End Exports.
End FunOrder.
Export FunOrder.Exports.
Lemma lefP (aT : Type) d (T : porderType d) (f g : aT → T) :
reflect (∀ x, (f x ≤ g x)%O) (f ≤ g)%O.
Lemma meetfE (aT : Type) d (T : latticeType d) (f g : aT → T) x :
((f `&` g) x = f x `&` g x)%O.
Lemma joinfE (aT : Type) d (T : latticeType d) (f g : aT → T) x :
((f `|` g) x = f x `|` g x)%O.
Lemma iterfS {T} (f : T → T) (n : nat) : iter n.+1 f = f \o iter n f.
Lemma iterfSr {T} (f : T → T) (n : nat) : iter n.+1 f = iter n f \o f.
Lemma iter0 {T} (f : T → T) : iter 0 f = id.