Library mathcomp.analysis.boolp
(* --------------------------------------------------------------------
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique
-------------------------------------------------------------------- *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice.
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique
-------------------------------------------------------------------- *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice.
Set Implicit Arguments.
Declare Scope box_scope.
Declare Scope quant_scope.
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.
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 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 predeqE {T} (P Q : T → Prop) : (P = Q) = (∀ x, P x ↔ Q x).
Lemma predeqP {T} (A B : T → Prop) : (A = B) ↔ (∀ x, A x ↔ B 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 propT (P : Prop) : P → P = True.
Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.
_ : ∀ (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 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 predeqE {T} (P Q : T → Prop) : (P = Q) = (∀ x, P x ↔ Q x).
Lemma predeqP {T} (A B : T → Prop) : (A = B) ↔ (∀ x, A x ↔ B 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 propT (P : Prop) : P → P = True.
Lemma Prop_irrelevance (P : Prop) (x y : P) : x = y.
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 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 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.
Definition equality_mixin_of_Type (T : Type) : Equality.mixin_of T :=
EqMixin (fun x y : T ⇒ asboolP (x = y)).
Definition choice_of_Type (T : Type) : choiceType :=
Choice.Pack (Choice.Class (equality_mixin_of_Type T) gen_choiceMixin).
Lemma is_true_inj : injective is_true.
Lemma not_True : (¬ True) = False.
Lemma not_False : (¬ False) = True.
Lemma asboolF (P : Prop) : ¬ P → `[<P>] = false.
Definition equality_mixin_of_Type (T : Type) : Equality.mixin_of T :=
EqMixin (fun x y : T ⇒ asboolP (x = y)).
Definition choice_of_Type (T : Type) : choiceType :=
Choice.Pack (Choice.Class (equality_mixin_of_Type T) gen_choiceMixin).
Lemma is_true_inj : injective is_true.
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 contra_notP (Q P : Prop) : (¬ Q → P) → ¬ P → Q.
Lemma contraPP (Q P : Prop) : (¬ Q → ¬ P) → P → Q.
Lemma contrapT P : ¬ ¬ P → P.
Lemma wlog_neg P : (¬ P → P) → P.
Lemma notT (P : Prop) : P = False → ¬ P.
Lemma notTE (P : Prop) : (¬ P) → P = False.
Lemma notFE (P : Prop) : (¬ P) = False → P.
Lemma notK : involutive not.
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).
Module BoolQuant.
Inductive box := Box of bool.
Bind Scope box_scope with box.
Delimit Scope box_scope with P.
Definition idbox {T : Type} (B : box) := fun (x : T) ⇒ B.
Definition unbox {T : Type} (B : T → box) : bool :=
asbool (∀ x : T, let: Box b := B x in b).
Notation "F ^*" := (Box F) (at level 2).
Notation "F ^~" := (~~ F) (at level 2).
Section Definitions.
Variable T : Type.
Implicit Types (B : box) (x y : T).
Definition quant0p Bp := pred0p (fun x : T ⇒ let: F^* := Bp x x in F).
Inductive box := Box of bool.
Bind Scope box_scope with box.
Delimit Scope box_scope with P.
Definition idbox {T : Type} (B : box) := fun (x : T) ⇒ B.
Definition unbox {T : Type} (B : T → box) : bool :=
asbool (∀ x : T, let: Box b := B x in b).
Notation "F ^*" := (Box F) (at level 2).
Notation "F ^~" := (~~ F) (at level 2).
Section Definitions.
Variable T : Type.
Implicit Types (B : box) (x y : T).
Definition quant0p Bp := pred0p (fun x : T ⇒ let: F^* := Bp x x in F).
The first redundant argument protects the notation from Coq's K-term
display kludge; the second protects it from simpl and /=.
Binding the predicate value rather than projecting it prevents spurious
unfolding of the boolean connectives by unification.
Definition all B x y := let: F^* := B in F^~^*.
Definition all_in C B x y := let: F^* := B in (C ==> F)^~^*.
Definition ex_in C B x y := let: F^* := B in (C && F)^*.
End Definitions.
Notation "`[ x | B ]" := (quant0p (fun x ⇒ B x)) (at level 0, x ident).
Notation "`[ x : T | B ]" := (quant0p (fun x : T ⇒ B x)) (at level 0, x ident).
Module Exports.
Delimit Scope quant_scope with Q. (* Bogus, only used to declare scope. *)
Bind Scope quant_scope with box.
Notation ", F" := F^* (at level 200, format ", '/ ' F") : quant_scope.
Notation "`[ 'forall' x B ]" := `[x | all B]
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' 'forall' x B ] ']'") : bool_scope.
Notation "`[ 'forall' x : T B ]" := `[x : T | all B]
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'forall' ( x | C ) B ]" := `[x | all_in C B]
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'forall' ( x '/ ' | C ) ']' B ] ']'") : bool_scope.
Notation "`[ 'forall' ( x : T | C ) B ]" := `[x : T | all_in C B]
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'forall' x 'in' A B ]" := `[x | all_in (x \in A) B]
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'forall' x '/ ' 'in' A ']' B ] ']'") : bool_scope.
Notation "`[ 'forall' x : T 'in' A B ]" := `[x : T | all_in (x \in A) B]
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation ", 'forall' x B" := `[x | all B]^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' 'forall' x B") : quant_scope.
Notation ", 'forall' x : T B" := `[x : T | all B]^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'forall' ( x | C ) B" := `[x | all_in C B]^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'forall' ( x '/ ' | C ) ']' B") : quant_scope.
Notation ", 'forall' ( x : T | C ) B" := `[x : T | all_in C B]^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'forall' x 'in' A B" := `[x | all_in (x \in A) B]^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'forall' x '/ ' 'in' A ']' B") : bool_scope.
Notation ", 'forall' x : T 'in' A B" := `[x : T | all_in (x \in A) B]^*
(at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'exists' x B ]" := `[x | ex B]^~
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' 'exists' x B ] ']'") : bool_scope.
Notation "`[ 'exists' x : T B ]" := `[x : T | ex B]^~
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'exists' ( x | C ) B ]" := `[x | ex_in C B]^~
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'exists' ( x '/ ' | C ) ']' B ] ']'") : bool_scope.
Notation "`[ 'exists' ( x : T | C ) B ]" := `[x : T | ex_in C B]^~
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'exists' x 'in' A B ]" := `[x | ex_in (x \in A) B]^~
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'exists' x '/ ' 'in' A ']' B ] ']'") : bool_scope.
Notation "`[ 'exists' x : T 'in' A B ]" := `[x : T | ex_in (x \in A) B]^~
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation ", 'exists' x B" := `[x | ex B]^~^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' 'exists' x B") : quant_scope.
Notation ", 'exists' x : T B" := `[x : T | ex B]^~^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'exists' ( x | C ) B" := `[x | ex_in C B]^~^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'exists' ( x '/ ' | C ) ']' B") : quant_scope.
Notation ", 'exists' ( x : T | C ) B" := `[x : T | ex_in C B]^~^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'exists' x 'in' A B" := `[x | ex_in (x \in A) B]^~^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'exists' x '/ ' 'in' A ']' B") : bool_scope.
Notation ", 'exists' x : T 'in' A B" := `[x : T | ex_in (x \in A) B]^~^*
(at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
End Exports.
End BoolQuant.
Export BoolQuant.Exports.
Local Open Scope quant_scope.
Definition all_in C B x y := let: F^* := B in (C ==> F)^~^*.
Definition ex_in C B x y := let: F^* := B in (C && F)^*.
End Definitions.
Notation "`[ x | B ]" := (quant0p (fun x ⇒ B x)) (at level 0, x ident).
Notation "`[ x : T | B ]" := (quant0p (fun x : T ⇒ B x)) (at level 0, x ident).
Module Exports.
Delimit Scope quant_scope with Q. (* Bogus, only used to declare scope. *)
Bind Scope quant_scope with box.
Notation ", F" := F^* (at level 200, format ", '/ ' F") : quant_scope.
Notation "`[ 'forall' x B ]" := `[x | all B]
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' 'forall' x B ] ']'") : bool_scope.
Notation "`[ 'forall' x : T B ]" := `[x : T | all B]
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'forall' ( x | C ) B ]" := `[x | all_in C B]
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'forall' ( x '/ ' | C ) ']' B ] ']'") : bool_scope.
Notation "`[ 'forall' ( x : T | C ) B ]" := `[x : T | all_in C B]
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'forall' x 'in' A B ]" := `[x | all_in (x \in A) B]
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'forall' x '/ ' 'in' A ']' B ] ']'") : bool_scope.
Notation "`[ 'forall' x : T 'in' A B ]" := `[x : T | all_in (x \in A) B]
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation ", 'forall' x B" := `[x | all B]^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' 'forall' x B") : quant_scope.
Notation ", 'forall' x : T B" := `[x : T | all B]^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'forall' ( x | C ) B" := `[x | all_in C B]^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'forall' ( x '/ ' | C ) ']' B") : quant_scope.
Notation ", 'forall' ( x : T | C ) B" := `[x : T | all_in C B]^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'forall' x 'in' A B" := `[x | all_in (x \in A) B]^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'forall' x '/ ' 'in' A ']' B") : bool_scope.
Notation ", 'forall' x : T 'in' A B" := `[x : T | all_in (x \in A) B]^*
(at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'exists' x B ]" := `[x | ex B]^~
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' 'exists' x B ] ']'") : bool_scope.
Notation "`[ 'exists' x : T B ]" := `[x : T | ex B]^~
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'exists' ( x | C ) B ]" := `[x | ex_in C B]^~
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'exists' ( x '/ ' | C ) ']' B ] ']'") : bool_scope.
Notation "`[ 'exists' ( x : T | C ) B ]" := `[x : T | ex_in C B]^~
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation "`[ 'exists' x 'in' A B ]" := `[x | ex_in (x \in A) B]^~
(at level 0, x at level 99, B at level 200,
format "`[ '[hv' '[' 'exists' x '/ ' 'in' A ']' B ] ']'") : bool_scope.
Notation "`[ 'exists' x : T 'in' A B ]" := `[x : T | ex_in (x \in A) B]^~
(at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
Notation ", 'exists' x B" := `[x | ex B]^~^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' 'exists' x B") : quant_scope.
Notation ", 'exists' x : T B" := `[x : T | ex B]^~^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'exists' ( x | C ) B" := `[x | ex_in C B]^~^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'exists' ( x '/ ' | C ) ']' B") : quant_scope.
Notation ", 'exists' ( x : T | C ) B" := `[x : T | ex_in C B]^~^*
(at level 200, x at level 99, B at level 200, only parsing) : quant_scope.
Notation ", 'exists' x 'in' A B" := `[x | ex_in (x \in A) B]^~^*
(at level 200, x at level 99, B at level 200,
format ", '/ ' '[' 'exists' x '/ ' 'in' A ']' B") : bool_scope.
Notation ", 'exists' x : T 'in' A B" := `[x : T | ex_in (x \in A) B]^~^*
(at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
End Exports.
End BoolQuant.
Export BoolQuant.Exports.
Local Open Scope quant_scope.
Section QuantifierCombinators.
Variables (T : Type) (P : pred T) (PP : predp T).
Hypothesis viewP : ∀ x, reflect (PP x) (P x).
Lemma existsPP : reflect (∃ x, PP x) `[∃ x, P x].
Lemma forallPP : reflect (∀ x, PP x) `[∀ x, P x].
End QuantifierCombinators.
Section PredQuantifierCombinators.
Variables (T : Type) (P : pred T).
Lemma existsbP : reflect (∃ x, P x) `[∃ x, P x].
Lemma existsbE : `[∃ x, P x] = `[<∃ x, P x>].
Lemma forallbP : reflect (∀ x, P x) `[∀ x, P x].
Lemma forallbE : `[∀ x, P x] = `[<∀ x, P x>].
End PredQuantifierCombinators.
Variables (T : Type) (P : pred T) (PP : predp T).
Hypothesis viewP : ∀ x, reflect (PP x) (P x).
Lemma existsPP : reflect (∃ x, PP x) `[∃ x, P x].
Lemma forallPP : reflect (∀ x, PP x) `[∀ x, P x].
End QuantifierCombinators.
Section PredQuantifierCombinators.
Variables (T : Type) (P : pred T).
Lemma existsbP : reflect (∃ x, P x) `[∃ x, P x].
Lemma existsbE : `[∃ x, P x] = `[<∃ x, P x>].
Lemma forallbP : reflect (∀ x, P x) `[∀ x, P x].
Lemma forallbE : `[∀ x, P x] = `[<∀ x, P x>].
End PredQuantifierCombinators.
Lemma existsp_asboolP {T} {P : T → Prop} :
reflect (∃ x : T, P x) `[∃ x : T, `[<P x>]].
Lemma forallp_asboolP {T} {P : T → Prop} :
reflect (∀ x : T, P x) `[∀ x : T, `[<P x>]].
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 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 exists2P T (P Q : T → Prop) :
(exists2 x, P x & Q x) ↔ ∃ x, P x ∧ Q x.
reflect (∃ x : T, P x) `[∃ x : T, `[<P x>]].
Lemma forallp_asboolP {T} {P : T → Prop} :
reflect (∀ x : T, P x) `[∀ x : T, `[<P x>]].
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 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 exists2P T (P Q : T → Prop) :
(exists2 x, P x & Q x) ↔ ∃ x, P x ∧ Q x.
Definition xchooseb {T : choiceType} (P : pred T) (h : `[∃ x, P x]) :=
xchoose (existsbP P h).
Lemma xchoosebP {T : choiceType} (P : pred T) (h : `[∃ x, P x]) :
P (xchooseb h).
xchoose (existsbP P h).
Lemma xchoosebP {T : choiceType} (P : pred T) (h : `[∃ x, P x]) :
P (xchooseb h).
FIXME: to be moved