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.

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.13 additions

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

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 : rTSome (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.