Library mathcomp.ssreflect.ssrbool
Local additions:
[in A] == the applicative counterpart of a collective predicate A:
[in A] x beta-expands to x \in A. This is similar to
mem A, except that mem A x only simplfies to x \in A.
--> These will become part of the core SSReflect library in later Coq
versions.
For the sake of backwards compatibility, this file also replicates
v8.13-15 additions, including a generalization of the statments of
`homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, and
`can_mono_in`.
v8.15 addtions
Section ReflectCombinators.
Variables (P Q : Prop) (p q : bool).
Hypothesis rP : reflect P p.
Hypothesis rQ : reflect Q q.
Lemma negPP : reflect (¬ P) (~~ p).
Lemma andPP : reflect (P ∧ Q) (p && q).
Lemma orPP : reflect (P ∨ Q) (p || q).
Lemma implyPP : reflect (P → Q) (p ==> q).
End ReflectCombinators.
Arguments negPP {P p}.
Arguments andPP {P Q p q}.
Arguments orPP {P Q p q}.
Arguments implyPP {P Q p q}.
v8.16 additions
pred_oapp T D := [pred x | oapp (mem D) false x]
Lemma mono1W_in (aT rT : predArgType) (f : aT → rT) (aD : {pred aT})
(aP : pred aT) (rP : pred rT) :
{in aD, {mono f : x / aP x >-> rP x}} →
{in aD, {homo f : x / aP x >-> rP x}}.
Arguments mono1W_in [aT rT f aD aP rP].
Set Implicit Arguments.
v8.17 additions
Lemma all_sig2_cond {I T} (C : pred I) P Q :
T → (∀ x, C x → {y : T | P x y & Q x y}) →
{f : I → T | ∀ x, C x → P x (f x) & ∀ x, C x → Q x (f x)}.
Lemma can_in_pcan [rT aT : Type] (A : {pred aT}) [f : aT → rT] [g : rT → aT] :
{in A, cancel f g} → {in A, pcancel f (fun y : rT ⇒ Some (g y))}.
Lemma pcan_in_inj [rT aT : Type] [A : {pred aT}]
[f : aT → rT] [g : rT → option aT] :
{in A, pcancel f g} → {in A &, injective f}.
Lemma in_inj_comp A B C (f : B → A) (h : C → B) (P : pred B) (Q : pred C) :
{in P &, injective f} → {in Q &, injective h} → {homo h : x / Q x >-> P x} →
{in Q &, injective (f \o h)}.
Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
[f : B → A] [h : C → B] [f' : A → B] [h' : B → C] :
{homo h : x / x \in D' >-> x \in D} →
{in D, cancel f f'} → {in D', cancel h h'} →
{in D', cancel (f \o h) (h' \o f')}.
Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
[f : B → A] [h : C → B] [f' : A → option B] [h' : B → option C] :
{homo h : x / x \in D' >-> x \in D} →
{in D, pcancel f f'} → {in D', pcancel h h'} →
{in D', pcancel (f \o h) (obind h' \o f')}.
Definition pred_oapp T (D : {pred T}) : pred (option T) :=
[pred x | oapp (mem D) false x].
Lemma ocan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C})
[f : B → option A] [h : C → option B] [f' : A → B] [h' : B → C] :
{homo h : x / x \in D' >-> x \in pred_oapp D} →
{in D, ocancel f f'} → {in D', ocancel h h'} →
{in D', ocancel (obind f \o h) (h' \o f')}.
Lemma eqbLR (b1 b2 : bool) : b1 = b2 → b1 → b2.
Lemma eqbRL (b1 b2 : bool) : b1 = b2 → b2 → b1.
Lemma homo_mono1 [aT rT : Type] [f : aT → rT] [g : rT → aT]
[aP : pred aT] [rP : pred rT] :
cancel g f →
{homo f : x / aP x >-> rP x} →
{homo g : x / rP x >-> aP x} → {mono g : x / rP x >-> aP x}.
Lemma if_and b1 b2 T (x y : T) :
(if b1 && b2 then x else y) = (if b1 then if b2 then x else y else y).
Lemma if_or b1 b2 T (x y : T) :
(if b1 || b2 then x else y) = (if b1 then x else if b2 then x else y).
Lemma if_implyb b1 b2 T (x y : T) :
(if b1 ==> b2 then x else y) = (if b1 then if b2 then x else y else x).
Lemma if_implybC b1 b2 T (x y : T) :
(if b1 ==> b2 then x else y) = (if b2 then x else if b1 then y else x).
Lemma if_add b1 b2 T (x y : T) :
(if b1 (+) b2 then x else y) = (if b1 then if b2 then y else x else if b2 then x else y).
Future additions
Notation "[ 'in' A ]" := (in_mem^~ (mem A))
(at level 0, format "[ 'in' A ]") : fun_scope.
Notation "[ 'predI' A & B ]" := (predI [in A] [in B]) : fun_scope.
Notation "[ 'predU' A & B ]" := (predU [in A] [in B]) : fun_scope.
Notation "[ 'predD' A & B ]" := (predD [in A] [in B]) : fun_scope.
Notation "[ 'predC' A ]" := (predC [in A]) : fun_scope.
Notation "[ 'preim' f 'of' A ]" := (preim f [in A]) : fun_scope.
Lemma relpre_trans {T' T : Type} {leT : rel T} {f : T' → T} :
transitive leT → transitive (relpre f leT).