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.
Arguments PredType [T pT] toP.

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.
Arguments rel_of_simpl_rel {T} sr x / y : rename.

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.
Arguments homo_sym {aT rT} [aR rR f].
Arguments mono_sym {aT rT} [aR rR f].
Arguments homo_sym_in {aT rT} [aR rR f aD].
Arguments mono_sym_in {aT rT} [aR rR f aD].
Arguments homo_sym_in11 {aT rT} [aR rR f aD aD'].
Arguments mono_sym_in11 {aT rT} [aR rR f aD aD'].

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}.

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.
Arguments onW_can {aT rT} aD {f g}.
Arguments onW_can_in {aT rT} aD {rD f g}.
Arguments in_onW_can {aT rT} aD rD {f g}.
Arguments onS_can {aT rT} aD {f g}.
Arguments onS_can_in {aT rT} aD {rD f g}.
Arguments in_onS_can {aT rT} aD {f g}.

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.
Arguments homoRL_in {aT rT aD rD f g aR rR}.
Arguments homoLR_in {aT rT aD rD f g aR rR}.
Arguments homo_mono_in {aT rT aD rD f g aR rR}.
Arguments monoLR_in {aT rT aD rD f g aR rR}.
Arguments monoRL_in {aT rT aD rD f g aR rR}.
Arguments can_mono_in {aT rT aD rD f g aR rR}.

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.
Arguments inj_can_sym_in_on {aT rT aD rD f g}.
Arguments inj_can_sym_on {aT rT aD f g}.
Arguments inj_can_sym_in {aT rT rD f g}.

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.
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}.