Library mathcomp.analysis.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.
--------------------------------------------------------------------
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 asboolMathematical 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.
Declare Scope box_scope.
Declare Scope quant_scope.
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.
_ : ∀ (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)}.
_ : ∀ (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 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.
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.
Arguments canon {T U sort} x.
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 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.
Arguments canon {T U sort} x.
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 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 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 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>]).
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 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.
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.