# Library mathcomp.ssreflect.ssrbool

From mathcomp Require Import ssreflect ssrfun.
From Coq Require Export ssrbool.
8.11 addition in Coq but renamed
#[deprecated(since="mathcomp 1.15", note="Use rel_of_simpl instead.")]
Notation rel_of_simpl_rel := rel_of_simpl.
v8.14 addtions
Section LocalGlobal.
Variables T1 T2 T3 : predArgType.
Variables (D1 : {pred T1}) (D2 : {pred T2}).
Variables (f : T1 → T2) (h : T3).
Variable Q1 : (T1 → T2) → T1 → Prop.
Variable Q1l : (T1 → T2) → T3 → T1 → Prop.
Variable Q2 : (T1 → T2) → T1 → T1 → Prop.
Let allQ1 f'' := {all1 Q1 f''}.
Let allQ1l f'' h' := {all1 Q1l f'' h'}.
Let allQ2 f'' := {all2 Q2 f''}.
Lemma in_on1P : {in D1, {on D2, allQ1 f}} ↔
{in [pred x in D1 | f x \in D2], allQ1 f}.
Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} ↔
{in [pred x in D1 | f x \in D2], allQ1l f h}.
Lemma in_on2P : {in D1 &, {on D2 &, allQ2 f}} ↔
{in [pred x in D1 | f x \in D2] &, allQ2 f}.
Lemma on1W_in : {in D1, allQ1 f} → {in D1, {on D2, allQ1 f}}.
Lemma on1lW_in : {in D1, allQ1l f h} → {in D1, {on D2, allQ1l f & h}}.
Lemma on2W_in : {in D1 &, allQ2 f} → {in D1 &, {on D2 &, allQ2 f}}.
Lemma in_on1W : allQ1 f → {in D1, {on D2, allQ1 f}}.
Lemma in_on1lW : allQ1l f h → {in D1, {on D2, allQ1l f & h}}.
Lemma in_on2W : allQ2 f → {in D1 &, {on D2 &, allQ2 f}}.
Lemma on1S : (∀ x, f x \in D2) → {on D2, allQ1 f} → allQ1 f.
Lemma on1lS : (∀ x, f x \in D2) → {on D2, allQ1l f & h} → allQ1l f h.
Lemma on2S : (∀ x, f x \in D2) → {on D2 &, allQ2 f} → allQ2 f.
Lemma on1S_in : {homo f : x / x \in D1 >-> x \in D2} →
{in D1, {on D2, allQ1 f}} → {in D1, allQ1 f}.
Lemma on1lS_in : {homo f : x / x \in D1 >-> x \in D2} →
{in D1, {on D2, allQ1l f & h}} → {in D1, allQ1l f h}.
Lemma on2S_in : {homo f : x / x \in D1 >-> x \in D2} →
{in D1 &, {on D2 &, allQ2 f}} → {in D1 &, allQ2 f}.
Lemma in_on1S : (∀ x, f x \in D2) → {in T1, {on D2, allQ1 f}} → allQ1 f.
Lemma in_on1lS : (∀ x, f x \in D2) →
{in T1, {on D2, allQ1l f & h}} → allQ1l f h.
Lemma in_on2S : (∀ x, f x \in D2) →
{in T1 &, {on D2 &, allQ2 f}} → allQ2 f.
End LocalGlobal.
Arguments in_on1P {T1 T2 D1 D2 f Q1}.
Arguments in_on1lP {T1 T2 T3 D1 D2 f h Q1l}.
Arguments in_on2P {T1 T2 D1 D2 f Q2}.
Arguments on1W_in {T1 T2 D1} D2 {f Q1}.
Arguments on1lW_in {T1 T2 T3 D1} D2 {f h Q1l}.
Arguments on2W_in {T1 T2 D1} D2 {f Q2}.
Arguments in_on1W {T1 T2} D1 D2 {f Q1}.
Arguments in_on1lW {T1 T2 T3} D1 D2 {f h Q1l}.
Arguments in_on2W {T1 T2} D1 D2 {f Q2}.
Arguments on1S {T1 T2} D2 {f Q1}.
Arguments on1lS {T1 T2 T3} D2 {f h Q1l}.
Arguments on2S {T1 T2} D2 {f Q2}.
Arguments on1S_in {T1 T2 D1} D2 {f Q1}.
Arguments on1lS_in {T1 T2 T3 D1} D2 {f h Q1l}.
Arguments on2S_in {T1 T2 D1} D2 {f Q2}.
Arguments in_on1S {T1 T2} D2 {f Q1}.
Arguments in_on1lS {T1 T2 T3} D2 {f h Q1l}.
Arguments in_on2S {T1 T2} D2 {f Q2}.
Section in_sig.
Variables T1 T2 T3 : Type.
Variables (D1 : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}).
Variable P1 : T1 → Prop.
Variable P2 : T1 → T2 → Prop.
Variable P3 : T1 → T2 → T3 → Prop.
Lemma in1_sig : {in D1, {all1 P1}} → ∀ x : sig D1, P1 (sval x).
Lemma in2_sig : {in D1 & D2, {all2 P2}} →
∀ (x : sig D1) (y : sig D2), P2 (sval x) (sval y).
Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} →
∀ (x : sig D1) (y : sig D2) (z : sig D3), P3 (sval x) (sval y) (sval z).
End in_sig.
Arguments in1_sig {T1 D1 P1}.
Arguments in2_sig {T1 T2 D1 D2 P2}.
Arguments in3_sig {T1 T2 T3 D1 D2 D3 P3}.
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].
#[deprecated(since="mathcomp 1.14.0", note="Use mono1W_in instead.")]
Notation mono2W_in := mono1W_in.
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}.