Library mathcomp.ssreflect.ssrbool

From mathcomp Require Import ssreflect ssrfun.
From Coq Require Export ssrbool.

Local additions: {pred T} == a type convertible to pred T but that presents the pred_sort coercion class. PredType toP == the predType structure for toP : A -> pred T. relpre f r == the preimage of r by f, simplifying to r (f x) (f y). > These will become part of the core SSReflect library with Coq 8.11. This file also anticipates a v8.11 change in the definition of simpl_pred to T -> simpl_pred T. This change ensures that inE expands the definition of r : simpl_rel along with the \in, when rewriting in y \in r x.
This file also anticipates v8.13 additions as well as a generalization in the statments of `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, monoRL_in, and can_mono_in.
v8.11 addtions

Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0,
  format "{ 'pred' T }") : type_scope.

Lemma simpl_pred_sortE T (p : pred T) : (SimplPred p : {pred T}) =1 p.
Definition inE := (inE, simpl_pred_sortE).

Definition PredType : ∀ T pT, (pT → pred T) → predType T.
Defined.

Definition simpl_rel T := T → simpl_pred T.
Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x ⇒ SimplPred (r x).
Coercion rel_of_simpl_rel T (sr : simpl_rel T) : rel T := sr.

Required to avoid an incompatible format warning with coq-8.12
Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'").

Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y ⇒ E%B)) (at level 0,
  x ident, y ident, format "'[hv' [ 'rel' x y | '/ ' E ] ']'") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T ⇒ E%B))
  (only parsing) : fun_scope.
Notation "[ 'rel' x y 'in' A & B | E ]" :=
  [rel x y | (x \in A) && (y \in B) && E] (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'") : fun_scope.
Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)]
  (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y 'in' A & B ] ']'") : fun_scope.
Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E]
  (at level 0, x ident, y ident,
  format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'") : fun_scope.
Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0,
  x ident, y ident, format "'[hv' [ 'rel' x y 'in' A ] ']'") : fun_scope.

Notation xrelpre := (fun f (r : rel _) x y ⇒ r (f x) (f y)).
Definition relpre {T rT} (f : T → rT) (r : rel rT) :=
  [rel x y | r (f x) (f y)].

v8.13 addtions

Section HomoMonoMorphismFlip.
Variables (aT rT : Type) (aR : rel aT) (rR : rel rT) (f : aT → rT).
Variable (aD aD' : {pred aT}).

Lemma homo_sym : {homo f : x y / aR x y >-> rR x y} →
  {homo f : y x / aR x y >-> rR x y}.

Lemma mono_sym : {mono f : x y / aR x y >-> rR x y} →
  {mono f : y x / aR x y >-> rR x y}.

Lemma homo_sym_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} →
  {in aD &, {homo f : y x / aR x y >-> rR x y}}.

Lemma mono_sym_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} →
  {in aD &, {mono f : y x / aR x y >-> rR x y}}.

Lemma homo_sym_in11 : {in aD & aD', {homo f : x y / aR x y >-> rR x y}} →
  {in aD' & aD, {homo f : y x / aR x y >-> rR x y}}.

Lemma mono_sym_in11 : {in aD & aD', {mono f : x y / aR x y >-> rR x y}} →
  {in aD' & aD, {mono f : y x / aR x y >-> rR x y}}.

End HomoMonoMorphismFlip.

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.

v8.13 addtions

Section CancelOn.

Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
Variables (f : aT → rT) (g : rT → aT).

Lemma onW_can : cancel g f → {on aD, cancel g & f}.

Lemma onW_can_in : {in rD, cancel g f} → {in rD, {on aD, cancel g & f}}.

Lemma in_onW_can : cancel g f → {in rD, {on aD, cancel g & f}}.

Lemma onS_can : (∀ x, g x \in aD) → {on aD, cancel g & f} → cancel g f.

Lemma onS_can_in : {homo g : x / x \in rD >-> x \in aD} →
  {in rD, {on aD, cancel g & f}} → {in rD, cancel g f}.

Lemma in_onS_can : (∀ x, g x \in aD) →
  {in rT, {on aD, cancel g & f}} → cancel g f.

End CancelOn.

Section MonoHomoMorphismTheory_in.

Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
Variables (f : aT → rT) (g : rT → aT) (aR : rel aT) (rR : rel rT).

Hypothesis fgK : {in rD, {on aD, cancel g & f}}.
Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}.

Lemma homoRL_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y}} →
  {in rD & aD, ∀ x y, aR (g x) y → rR x (f y)}.

Lemma homoLR_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y}} →
  {in aD & rD, ∀ x y, aR x (g y) → rR (f x) y}.

Lemma homo_mono_in :
    {in aD &, {homo f : x y / aR x y >-> rR x y}} →
    {in rD &, {homo g : x y / rR x y >-> aR x y}} →
  {in rD &, {mono g : x y / rR x y >-> aR x y}}.

Lemma monoLR_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} →
  {in aD & rD, ∀ x y, rR (f x) y = aR x (g y)}.

Lemma monoRL_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} →
  {in rD & aD, ∀ x y, rR x (f y) = aR (g x) y}.

Lemma can_mono_in :
    {in aD &, {mono f : x y / aR x y >-> rR x y}} →
  {in rD &, {mono g : x y / rR x y >-> aR x y}}.

End MonoHomoMorphismTheory_in.

Section inj_can_sym_in_on.
Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
Variables (f : aT → rT) (g : rT → aT).

Lemma inj_can_sym_in_on :
    {homo f : x / x \in aD >-> x \in rD} → {in aD, {on rD, cancel f & g}} →
  {in rD &, {on aD &, injective g}} → {in rD, {on aD, cancel g & f}}.

Lemma inj_can_sym_on : {in aD, cancel f g} →
  {on aD &, injective g} → {on aD, cancel g & f}.

Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} → {on rD, cancel f & g} →
  {in rD &, injective g} → {in rD, cancel g f}.

End inj_can_sym_in_on.

additional contra lemmas involving [P,Q : Prop]

Section Contra.
Implicit Types (P Q : Prop) (b : bool).

Lemma contra_not P Q : (Q → P) → (¬ P → ¬ Q).

Lemma contraPnot P Q : (Q → ¬ P) → (P → ¬ Q).

Lemma contraTnot b P : (P → ~~ b) → (b → ¬ P).

Lemma contraNnot P b : (P → b) → (~~ b → ¬ P).

Lemma contraPT P b : (~~ b → ¬ P) → P → b.

Lemma contra_notT P b : (~~ b → P) → ¬ P → b.

Lemma contra_notN P b : (b → P) → ¬ P → ~~ b.

Lemma contraPN P b : (b → ¬ P) → (P → ~~ b).

Lemma contraFnot P b : (P → b) → b = false → ¬ P.

Lemma contraPF P b : (b → ¬ P) → P → b = false.

Lemma contra_notF P b : (b → P) → ¬ P → b = false.
End Contra.

v8.14 addtions

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.