Library Ssreflect.ssrbool
Require Import ssreflect ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "~~ b" (at level 35, right associativity).
Reserved Notation "b ==> c" (at level 55, right associativity).
Reserved Notation "b1 (+) b2" (at level 50, left associativity).
Reserved Notation "x \in A"
(at level 70, format "'[hv' x '/ ' \in A ']'", no associativity).
Reserved Notation "x \notin A"
(at level 70, format "'[hv' x '/ ' \notin A ']'", no associativity).
Reserved Notation "p1 =i p2"
(at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity).
Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing).
Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format
"'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format
"'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 ']' '/ ' & P4 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format
"'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'").
Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing).
Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format
"'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'").
Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format
"'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'").
Reserved Notation "[ && b1 & c ]" (at level 0, only parsing).
Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format
"'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'").
Reserved Notation "[ || b1 | c ]" (at level 0, only parsing).
Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format
"'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'").
Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing).
Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format
"'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'").
Reserved Notation "[ 'pred' : T => E ]" (at level 0, format
"'[hv' [ 'pred' : T => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x => E ]" (at level 0, x at level 8, format
"'[hv' [ 'pred' x => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x : T => E ]" (at level 0, x at level 8, format
"'[hv' [ 'pred' x : T => '/ ' E ] ']'").
Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format
"'[hv' [ 'rel' x y => '/ ' E ] ']'").
Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format
"'[hv' [ 'rel' x y : T => '/ ' E ] ']'").
Delimit Scope bool_scope with B.
Open Scope bool_scope.
Definition addb b := if b then negb else id.
Notation "~~ b" := (negb b) : bool_scope.
Notation "b ==> c" := (implb b c) : bool_scope.
Notation "b1 (+) b2" := (addb b1 b2) : bool_scope.
Coercion is_true : bool >-> Sortclass.
Lemma prop_congr : ∀ b b' : bool, b = b' → b = b' :> Prop.
Proof. by move⇒ b b' →. Qed.
Ltac prop_congr := apply: prop_congr.
Lemma is_true_true : true. Proof. by []. Qed.
Lemma not_false_is_true : ¬ false. Proof. by []. Qed.
Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
Hint Resolve is_true_true not_false_is_true is_true_locked_true.
Definition isT := is_true_true.
Definition notF := not_false_is_true.
Lemma negbT b : b = false → ~~ b. Proof. by case: b. Qed.
Lemma negbTE b : ~~ b → b = false. Proof. by case: b. Qed.
Lemma negbF b : (b : bool) → ~~ b = false. Proof. by case: b. Qed.
Lemma negbFE b : ~~ b = false → b. Proof. by case: b. Qed.
Lemma negbK : involutive negb. Proof. by case. Qed.
Lemma negbNE b : ~~ ~~ b → b. Proof. by case: b. Qed.
Lemma negb_inj : injective negb. Proof. exact: can_inj negbK. Qed.
Lemma negbLR b c : b = ~~ c → ~~ b = c. Proof. exact: canLR negbK. Qed.
Lemma negbRL b c : ~~ b = c → b = ~~ c. Proof. exact: canRL negbK. Qed.
Lemma contra (c b : bool) : (c → b) → ~~ b → ~~ c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraNN := contra.
Lemma contraL (c b : bool) : (c → ~~ b) → b → ~~ c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraTN := contraL.
Lemma contraR (c b : bool) : (~~ c → b) → ~~ b → c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraNT := contraR.
Lemma contraLR (c b : bool) : (~~ c → ~~ b) → b → c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraTT := contraLR.
Lemma contraT b : (~~ b → false) → b. Proof. by case: b ⇒ // →. Qed.
Lemma wlog_neg b : (~~ b → b) → b. Proof. by case: b ⇒ // →. Qed.
Lemma contraFT (c b : bool) : (~~ c → b) → b = false → c.
Proof. by move/contraR⇒ notb_c /negbT. Qed.
Lemma contraFN (c b : bool) : (c → b) → b = false → ~~ c.
Proof. by move/contra⇒ notb_notc /negbT. Qed.
Lemma contraTF (c b : bool) : (c → ~~ b) → b → c = false.
Proof. by move/contraL⇒ b_notc /b_notc/negbTE. Qed.
Lemma contraNF (c b : bool) : (c → b) → ~~ b → c = false.
Proof. by move/contra⇒ notb_notc /notb_notc/negbTE. Qed.
Lemma contraFF (c b : bool) : (c → b) → b = false → c = false.
Proof. by move/contraFN⇒ bF_notc /bF_notc/negbTE. Qed.
Coercion isSome T (u : option T) := if u is Some _ then true else false.
Coercion is_inl A B (u : A + B) := if u is inl _ then true else false.
Coercion is_left A B (u : {A} + {B}) := if u is left _ then true else false.
Coercion is_inleft A B (u : A + {B}) := if u is inleft _ then true else false.
Prenex Implicits isSome is_inl is_left is_inleft.
Definition decidable P := {P} + {¬ P}.
Section BoolIf.
Variables (A B : Type) (x : A) (f : A → B) (b : bool) (vT vF : A).
CoInductive if_spec (not_b : Prop) : bool → A → Set :=
| IfSpecTrue of b : if_spec not_b true vT
| IfSpecFalse of not_b : if_spec not_b false vF.
Lemma ifP : if_spec (b = false) b (if b then vT else vF).
Proof. by case def_b: b; constructor. Qed.
Lemma ifPn : if_spec (~~ b) b (if b then vT else vF).
Proof. by case def_b: b; constructor; rewrite ?def_b. Qed.
Lemma ifT : b → (if b then vT else vF) = vT. Proof. by move→. Qed.
Lemma ifF : b = false → (if b then vT else vF) = vF. Proof. by move→. Qed.
Lemma ifN : ~~ b → (if b then vT else vF) = vF. Proof. by move/negbTE→. Qed.
Lemma if_same : (if b then vT else vT) = vT.
Proof. by case b. Qed.
Lemma if_neg : (if ~~ b then vT else vF) = if b then vF else vT.
Proof. by case b. Qed.
Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
Proof. by case b. Qed.
Lemma if_arg (fT fF : A → B) :
(if b then fT else fF) x = if b then fT x else fF x.
Proof. by case b. Qed.
Definition if_expr := if b then vT else vF.
Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed.
End BoolIf.
Inductive reflect (P : Prop) : bool → Set :=
| ReflectT of P : reflect P true
| ReflectF of ¬ P : reflect P false.
Section ReflectCore.
Variables (P Q : Prop) (b c : bool).
Hypothesis Hb : reflect P b.
Lemma introNTF : (if c then ¬ P else P) → ~~ b = c.
Proof. by case c; case Hb. Qed.
Lemma introTF : (if c then P else ¬ P) → b = c.
Proof. by case c; case Hb. Qed.
Lemma elimNTF : ~~ b = c → if c then ¬ P else P.
Proof. by move <-; case Hb. Qed.
Lemma elimTF : b = c → if c then P else ¬ P.
Proof. by move <-; case Hb. Qed.
Lemma equivPif : (Q → P) → (P → Q) → if b then Q else ¬ Q.
Proof. by case Hb; auto. Qed.
Lemma xorPif : Q ∨ P → ¬ (Q ∧ P) → if b then ¬ Q else Q.
Proof. by case Hb ⇒ [? _ H ? | ? H _]; case: H. Qed.
End ReflectCore.
Section ReflectNegCore.
Variables (P Q : Prop) (b c : bool).
Hypothesis Hb : reflect P (~~ b).
Lemma introTFn : (if c then ¬ P else P) → b = c.
Proof. by move/(introNTF Hb) <-; case b. Qed.
Lemma elimTFn : b = c → if c then ¬ P else P.
Proof. by move <-; apply: (elimNTF Hb); case b. Qed.
Lemma equivPifn : (Q → P) → (P → Q) → if b then ¬ Q else Q.
Proof. rewrite -if_neg; exact: equivPif. Qed.
Lemma xorPifn : Q ∨ P → ¬ (Q ∧ P) → if b then Q else ¬ Q.
Proof. rewrite -if_neg; exact: xorPif. Qed.
End ReflectNegCore.
Section Reflect.
Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (~~ b')).
Lemma introT : P → b. Proof. exact: introTF true _. Qed.
Lemma introF : ¬ P → b = false. Proof. exact: introTF false _. Qed.
Lemma introN : ¬ P → ~~ b. Proof. exact: introNTF true _. Qed.
Lemma introNf : P → ~~ b = false. Proof. exact: introNTF false _. Qed.
Lemma introTn : ¬ P → b'. Proof. exact: introTFn true _. Qed.
Lemma introFn : P → b' = false. Proof. exact: introTFn false _. Qed.
Lemma elimT : b → P. Proof. exact: elimTF true _. Qed.
Lemma elimF : b = false → ¬ P. Proof. exact: elimTF false _. Qed.
Lemma elimN : ~~ b → ¬P. Proof. exact: elimNTF true _. Qed.
Lemma elimNf : ~~ b = false → P. Proof. exact: elimNTF false _. Qed.
Lemma elimTn : b' → ¬ P. Proof. exact: elimTFn true _. Qed.
Lemma elimFn : b' = false → P. Proof. exact: elimTFn false _. Qed.
Lemma introP : (b → Q) → (~~ b → ¬ Q) → reflect Q b.
Proof. by case b; constructor; auto. Qed.
Lemma iffP : (P → Q) → (Q → P) → reflect Q b.
Proof. by case: Pb; constructor; auto. Qed.
Lemma equivP : (P ↔ Q) → reflect Q b.
Proof. by case; exact: iffP. Qed.
Lemma sumboolP (decQ : decidable Q) : reflect Q decQ.
Proof. by case: decQ; constructor. Qed.
Lemma appP : reflect Q b → P → Q.
Proof. by move⇒ Qb; move/introT; case: Qb. Qed.
Lemma sameP : reflect P c → b = c.
Proof. case; [exact: introT | exact: introF]. Qed.
Lemma decPcases : if b then P else ¬ P. Proof. by case Pb. Qed.
Definition decP : decidable P. by case: b decPcases; [left | right]. Defined.
Lemma rwP : P ↔ b. Proof. by split; [exact: introT | exact: elimT]. Qed.
Lemma rwP2 : reflect Q b → (P ↔ Q).
Proof. by move⇒ Qb; split⇒ ?; [exact: appP | apply: elimT; case: Qb]. Qed.
CoInductive alt_spec : bool → Type :=
| AltTrue of P : alt_spec true
| AltFalse of ~~ b : alt_spec false.
Lemma altP : alt_spec b.
Proof. by case def_b: b / Pb; constructor; rewrite ?def_b. Qed.
End Reflect.
Hint View for move/ elimTF|3 elimNTF|3 elimTFn|3 introT|2 introTn|2 introN|2.
Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2.
Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
Coercion elimT : reflect >-> Funclass.
Definition unless condition property := (property → condition) → condition.
Lemma bind_unless C P {Q} : unless C P → unless (unless C Q) P.
Proof. by move⇒ haveP suffPQ suffQ; apply: haveP ⇒ /suffPQ; exact. Qed.
Lemma unless_contra b C : (~~ b → C) → unless C b.
Proof. by case: b ⇒ [_ haveC | haveC _]; exact: haveC. Qed.
Definition classically P : Prop := ∀ b : bool, (P → b) → b.
Lemma classicP : ∀ P : Prop, classically P ↔ ¬ ¬ P.
Proof.
move⇒ P; split⇒ [cP nP | nnP [] // nP]; last by case nnP; move/nP.
by have: P → false; [move/nP | move/cP].
Qed.
Lemma classic_bind : ∀ P Q,
(P → classically Q) → (classically P → classically Q).
Proof. by move⇒ P Q IH IH_P b IH_Q; apply: IH_P; move/IH; exact. Qed.
Lemma classic_EM : ∀ P, classically (decidable P).
Proof.
by move⇒ P [] // IH; apply IH; right ⇒ ?; apply: notF (IH _); left.
Qed.
Lemma classic_imply : ∀ P Q, (P → classically Q) → classically (P → Q).
Proof.
move⇒ P Q IH [] // notPQ; apply notPQ; move/IH⇒ hQ; case: notF.
by apply: hQ ⇒ hQ; case: notF; exact: notPQ.
Qed.
Lemma classic_pick : ∀ T P,
classically ({x : T | P x} + (∀ x, ¬ P x)).
Proof.
move⇒ T P [] // IH; apply IH; right⇒ x Px; case: notF.
by apply: IH; left; ∃ x.
Qed.
Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3.
Inductive and4 (P1 P2 P3 P4 : Prop) : Prop := And4 of P1 & P2 & P3 & P4.
Inductive and5 (P1 P2 P3 P4 P5 : Prop) : Prop :=
And5 of P1 & P2 & P3 & P4 & P5.
Inductive or3 (P1 P2 P3 : Prop) : Prop := Or31 of P1 | Or32 of P2 | Or33 of P3.
Inductive or4 (P1 P2 P3 P4 : Prop) : Prop :=
Or41 of P1 | Or42 of P2 | Or43 of P3 | Or44 of P4.
Notation "[ /\ P1 & P2 ]" := (and P1 P2) (only parsing) : type_scope.
Notation "[ /\ P1 , P2 & P3 ]" := (and3 P1 P2 P3) : type_scope.
Notation "[ /\ P1 , P2 , P3 & P4 ]" := (and4 P1 P2 P3 P4) : type_scope.
Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" := (and5 P1 P2 P3 P4 P5) : type_scope.
Notation "[ \/ P1 | P2 ]" := (or P1 P2) (only parsing) : type_scope.
Notation "[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3) : type_scope.
Notation "[ \/ P1 , P2 , P3 | P4 ]" := (or4 P1 P2 P3 P4) : type_scope.
Notation "[ && b1 & c ]" := (b1 && c) (only parsing) : bool_scope.
Notation "[ && b1 , b2 , .. , bn & c ]" := (b1 && (b2 && .. (bn && c) .. ))
: bool_scope.
Notation "[ || b1 | c ]" := (b1 || c) (only parsing) : bool_scope.
Notation "[ || b1 , b2 , .. , bn | c ]" := (b1 || (b2 || .. (bn || c) .. ))
: bool_scope.
Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
(b1 ==> (b2 ==> .. (bn ==> c) .. )) : bool_scope.
Notation "[ ==> b1 => c ]" := (b1 ==> c) (only parsing) : bool_scope.
Section AllAnd.
Variables (T : Type) (P1 P2 P3 P4 P5 : T → Prop).
Local Notation a P := (∀ x, P x).
Lemma all_and2 (hP : ∀ x, [/\ P1 x & P2 x]) : [/\ a P1 & a P2].
Proof. by split⇒ x; case: (hP x). Qed.
Lemma all_and3 (hP : ∀ x, [/\ P1 x, P2 x & P3 x]) :
[/\ a P1, a P2 & a P3].
Proof. by split⇒ x; case: (hP x). Qed.
Lemma all_and4 (hP : ∀ x, [/\ P1 x, P2 x, P3 x & P4 x]) :
[/\ a P1, a P2, a P3 & a P4].
Proof. by split⇒ x; case: (hP x). Qed.
Lemma all_and5 (hP : ∀ x, [/\ P1 x, P2 x, P3 x, P4 x & P5 x]) :
[/\ a P1, a P2, a P3, a P4 & a P5].
Proof. by split⇒ x; case: (hP x). Qed.
End AllAnd.
Lemma pair_andP P Q : P ∧ Q ↔ P × Q. Proof. by split; case. Qed.
Section ReflectConnectives.
Variable b1 b2 b3 b4 b5 : bool.
Lemma idP : reflect b1 b1.
Proof. by case b1; constructor. Qed.
Lemma boolP : alt_spec b1 b1 b1.
Proof. exact: (altP idP). Qed.
Lemma idPn : reflect (~~ b1) (~~ b1).
Proof. by case b1; constructor. Qed.
Lemma negP : reflect (¬ b1) (~~ b1).
Proof. by case b1; constructor; auto. Qed.
Lemma negPn : reflect b1 (~~ ~~ b1).
Proof. by case b1; constructor. Qed.
Lemma negPf : reflect (b1 = false) (~~ b1).
Proof. by case b1; constructor. Qed.
Lemma andP : reflect (b1 ∧ b2) (b1 && b2).
Proof. by case b1; case b2; constructor⇒ //; case. Qed.
Lemma and3P : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3].
Proof. by case b1; case b2; case b3; constructor; try by case. Qed.
Lemma and4P : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4].
Proof. by case b1; case b2; case b3; case b4; constructor; try by case. Qed.
Lemma and5P : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5].
Proof.
by case b1; case b2; case b3; case b4; case b5; constructor; try by case.
Qed.
Lemma orP : reflect (b1 ∨ b2) (b1 || b2).
Proof. by case b1; case b2; constructor; auto; case. Qed.
Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3].
Proof.
case b1; first by constructor; constructor 1.
case b2; first by constructor; constructor 2.
case b3; first by constructor; constructor 3.
by constructor; case.
Qed.
Lemma or4P : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4].
Proof.
case b1; first by constructor; constructor 1.
case b2; first by constructor; constructor 2.
case b3; first by constructor; constructor 3.
case b4; first by constructor; constructor 4.
by constructor; case.
Qed.
Lemma nandP : reflect (~~ b1 ∨ ~~ b2) (~~ (b1 && b2)).
Proof. by case b1; case b2; constructor; auto; case; auto. Qed.
Lemma norP : reflect (~~ b1 ∧ ~~ b2) (~~ (b1 || b2)).
Proof. by case b1; case b2; constructor; auto; case; auto. Qed.
Lemma implyP : reflect (b1 → b2) (b1 ==> b2).
Proof. by case b1; case b2; constructor; auto. Qed.
End ReflectConnectives.
Implicit Arguments idP [b1].
Implicit Arguments idPn [b1].
Implicit Arguments negP [b1].
Implicit Arguments negPn [b1].
Implicit Arguments negPf [b1].
Implicit Arguments andP [b1 b2].
Implicit Arguments and3P [b1 b2 b3].
Implicit Arguments and4P [b1 b2 b3 b4].
Implicit Arguments and5P [b1 b2 b3 b4 b5].
Implicit Arguments orP [b1 b2].
Implicit Arguments or3P [b1 b2 b3].
Implicit Arguments or4P [b1 b2 b3 b4].
Implicit Arguments nandP [b1 b2].
Implicit Arguments norP [b1 b2].
Implicit Arguments implyP [b1 b2].
Prenex Implicits idP idPn negP negPn negPf.
Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
Lemma andTb : left_id true andb. Proof. by []. Qed.
Lemma andFb : left_zero false andb. Proof. by []. Qed.
Lemma andbT : right_id true andb. Proof. by case. Qed.
Lemma andbF : right_zero false andb. Proof. by case. Qed.
Lemma andbb : idempotent andb. Proof. by case. Qed.
Lemma andbC : commutative andb. Proof. by do 2!case. Qed.
Lemma andbA : associative andb. Proof. by do 3!case. Qed.
Lemma andbCA : left_commutative andb. Proof. by do 3!case. Qed.
Lemma andbAC : right_commutative andb. Proof. by do 3!case. Qed.
Lemma andbACA : interchange andb andb. Proof. by do 4!case. Qed.
Lemma orTb : ∀ b, true || b. Proof. by []. Qed.
Lemma orFb : left_id false orb. Proof. by []. Qed.
Lemma orbT : ∀ b, b || true. Proof. by case. Qed.
Lemma orbF : right_id false orb. Proof. by case. Qed.
Lemma orbb : idempotent orb. Proof. by case. Qed.
Lemma orbC : commutative orb. Proof. by do 2!case. Qed.
Lemma orbA : associative orb. Proof. by do 3!case. Qed.
Lemma orbCA : left_commutative orb. Proof. by do 3!case. Qed.
Lemma orbAC : right_commutative orb. Proof. by do 3!case. Qed.
Lemma orbACA : interchange orb orb. Proof. by do 4!case. Qed.
Lemma andbN b : b && ~~ b = false. Proof. by case: b. Qed.
Lemma andNb b : ~~ b && b = false. Proof. by case: b. Qed.
Lemma orbN b : b || ~~ b = true. Proof. by case: b. Qed.
Lemma orNb b : ~~ b || b = true. Proof. by case: b. Qed.
Lemma andb_orl : left_distributive andb orb. Proof. by do 3!case. Qed.
Lemma andb_orr : right_distributive andb orb. Proof. by do 3!case. Qed.
Lemma orb_andl : left_distributive orb andb. Proof. by do 3!case. Qed.
Lemma orb_andr : right_distributive orb andb. Proof. by do 3!case. Qed.
Lemma andb_idl (a b : bool) : (b → a) → a && b = b.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma andb_idr (a b : bool) : (a → b) → a && b = a.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma andb_id2l (a b c : bool) : (a → b = c) → a && b = a && c.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma andb_id2r (a b c : bool) : (b → a = c) → a && b = c && b.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma orb_idl (a b : bool) : (a → b) → a || b = b.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma orb_idr (a b : bool) : (b → a) → a || b = a.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma orb_id2l (a b c : bool) : (~~ a → b = c) → a || b = a || c.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma orb_id2r (a b c : bool) : (~~ b → a = c) → a || b = c || b.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma negb_and (a b : bool) : ~~ (a && b) = ~~ a || ~~ b.
Proof. by case: a; case: b. Qed.
Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b.
Proof. by case: a; case: b. Qed.
Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed.
Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed.
Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed.
Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed.
Lemma implybT b : b ==> true. Proof. by case: b. Qed.
Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed.
Lemma implyFb b : false ==> b. Proof. by []. Qed.
Lemma implyTb b : (true ==> b) = b. Proof. by []. Qed.
Lemma implybb b : b ==> b. Proof. by case: b. Qed.
Lemma negb_imply a b : ~~ (a ==> b) = a && ~~ b.
Proof. by case: a; case: b. Qed.
Lemma implybE a b : (a ==> b) = ~~ a || b.
Proof. by case: a; case: b. Qed.
Lemma implyNb a b : (~~ a ==> b) = a || b.
Proof. by case: a; case: b. Qed.
Lemma implybN a b : (a ==> ~~ b) = (b ==> ~~ a).
Proof. by case: a; case: b. Qed.
Lemma implybNN a b : (~~ a ==> ~~ b) = b ==> a.
Proof. by case: a; case: b. Qed.
Lemma implyb_idl (a b : bool) : (~~ a → b) → (a ==> b) = b.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma implyb_idr (a b : bool) : (b → ~~ a) → (a ==> b) = ~~ a.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma implyb_id2l (a b c : bool) : (a → b = c) → (a ==> b) = (a ==> c).
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma addFb : left_id false addb. Proof. by []. Qed.
Lemma addbF : right_id false addb. Proof. by case. Qed.
Lemma addbb : self_inverse false addb. Proof. by case. Qed.
Lemma addbC : commutative addb. Proof. by do 2!case. Qed.
Lemma addbA : associative addb. Proof. by do 3!case. Qed.
Lemma addbCA : left_commutative addb. Proof. by do 3!case. Qed.
Lemma addbAC : right_commutative addb. Proof. by do 3!case. Qed.
Lemma addbACA : interchange addb addb. Proof. by do 4!case. Qed.
Lemma andb_addl : left_distributive andb addb. Proof. by do 3!case. Qed.
Lemma andb_addr : right_distributive andb addb. Proof. by do 3!case. Qed.
Lemma addKb : left_loop id addb. Proof. by do 2!case. Qed.
Lemma addbK : right_loop id addb. Proof. by do 2!case. Qed.
Lemma addIb : left_injective addb. Proof. by do 3!case. Qed.
Lemma addbI : right_injective addb. Proof. by do 3!case. Qed.
Lemma addTb b : true (+) b = ~~ b. Proof. by []. Qed.
Lemma addbT b : b (+) true = ~~ b. Proof. by case: b. Qed.
Lemma addbN a b : a (+) ~~ b = ~~ (a (+) b).
Proof. by case: a; case: b. Qed.
Lemma addNb a b : ~~ a (+) b = ~~ (a (+) b).
Proof. by case: a; case: b. Qed.
Lemma addbP a b : reflect (~~ a = b) (a (+) b).
Proof. by case: a; case: b; constructor. Qed.
Implicit Arguments addbP [a b].
Ltac bool_congr :=
match goal with
| |- (?X1 && ?X2 = ?X3) ⇒ first
[ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry
| case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ]
| |- (?X1 || ?X2 = ?X3) ⇒ first
[ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry
| case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ]
| |- (?X1 (+) ?X2 = ?X3) ⇒
symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry
| |- (~~ ?X1 = ?X2) ⇒ congr 1 negb
end.
Definition pred T := T → bool.
Identity Coercion fun_of_pred : pred >-> Funclass.
Definition rel T := T → pred T.
Identity Coercion fun_of_rel : rel >-> Funclass.
Notation xpred0 := (fun _ ⇒ false).
Notation xpredT := (fun _ ⇒ true).
Notation xpredI := (fun (p1 p2 : pred _) x ⇒ p1 x && p2 x).
Notation xpredU := (fun (p1 p2 : pred _) x ⇒ p1 x || p2 x).
Notation xpredC := (fun (p : pred _) x ⇒ ~~ p x).
Notation xpredD := (fun (p1 p2 : pred _) x ⇒ ~~ p2 x && p1 x).
Notation xpreim := (fun f (p : pred _) x ⇒ p (f x)).
Notation xrelU := (fun (r1 r2 : rel _) x y ⇒ r1 x y || r2 x y).
Section Predicates.
Variables T : Type.
Definition subpred (p1 p2 : pred T) := ∀ x, p1 x → p2 x.
Definition subrel (r1 r2 : rel T) := ∀ x y, r1 x y → r2 x y.
Definition simpl_pred := simpl_fun T bool.
Definition applicative_pred := pred T.
Definition collective_pred := pred T.
Definition SimplPred (p : pred T) : simpl_pred := SimplFun p.
Coercion pred_of_simpl (p : simpl_pred) : pred T := fun_of_simpl p.
Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred :=
fun_of_simpl p.
Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred :=
fun x ⇒ (let: SimplFun f := p in fun _ ⇒ f x) x.
Definition pred0 := SimplPred xpred0.
Definition predT := SimplPred xpredT.
Definition predI p1 p2 := SimplPred (xpredI p1 p2).
Definition predU p1 p2 := SimplPred (xpredU p1 p2).
Definition predC p := SimplPred (xpredC p).
Definition predD p1 p2 := SimplPred (xpredD p1 p2).
Definition preim rT f (d : pred rT) := SimplPred (xpreim f d).
Definition simpl_rel := simpl_fun T (pred T).
Definition SimplRel (r : rel T) : simpl_rel := [fun x ⇒ r x].
Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y ⇒ r x y.
Definition relU r1 r2 := SimplRel (xrelU r1 r2).
Lemma subrelUl r1 r2 : subrel r1 (relU r1 r2).
Proof. by move⇒ *; apply/orP; left. Qed.
Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
Proof. by move⇒ *; apply/orP; right. Qed.
CoInductive mem_pred := Mem of pred T.
Definition isMem pT topred mem := mem = (fun p : pT ⇒ Mem [eta topred p]).
Structure predType := PredType {
pred_sort :> Type;
topred : pred_sort → pred T;
_ : {mem | isMem topred mem}
}.
Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ (erefl _)).
Canonical predPredType := Eval hnf in @mkPredType (pred T) id.
Canonical simplPredType := Eval hnf in mkPredType pred_of_simpl.
Canonical boolfunPredType := Eval hnf in @mkPredType (T → bool) id.
Coercion pred_of_mem mp : pred_sort predPredType := let: Mem p := mp in [eta p].
Canonical memPredType := Eval hnf in mkPredType pred_of_mem.
Definition clone_pred U :=
fun pT & pred_sort pT → U ⇒
fun a mP (pT' := @PredType U a mP) & phant_id pT' pT ⇒ pT'.
End Predicates.
Implicit Arguments pred0 [T].
Implicit Arguments predT [T].
Prenex Implicits pred0 predT predI predU predC predD preim relU.
Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T ⇒ E%B))
(at level 0, format "[ 'pred' : T | E ]") : fun_scope.
Notation "[ 'pred' x | E ]" := (SimplPred (fun x ⇒ E%B))
(at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope.
Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ]
(at level 0, x ident, format "[ 'pred' x | E1 & E2 ]") : fun_scope.
Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T ⇒ E%B))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'pred' x : T | E1 & E2 ]" := [pred x : T | E1 && E2 ]
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y ⇒ E%B))
(at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T ⇒ E%B))
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id)
(at level 0, format "[ 'predType' 'of' T ]") : form_scope.
Notation pred_class := (pred_sort (predPredType _)).
Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T.
Definition predArgType := Type.
Bind Scope type_scope with predArgType.
Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.
Notation "{ : T }" := (T%type : predArgType)
(at level 0, format "{ : T }") : type_scope.
Definition mem T (pT : predType T) : pT → mem_pred T :=
nosimpl (let: PredType _ _ (exist mem _) := pT return pT → _ in mem).
Definition in_mem T x mp := nosimpl pred_of_mem T mp x.
Prenex Implicits mem.
Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp].
Definition eq_mem T p1 p2 := ∀ x : T, in_mem x p1 = in_mem x p2.
Definition sub_mem T p1 p2 := ∀ x : T, in_mem x p1 → in_mem x p2.
Typeclasses Opaque eq_mem.
Lemma sub_refl T (p : mem_pred T) : sub_mem p p. Proof. by []. Qed.
Implicit Arguments sub_refl [[T] [p]].
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \notin A" := (~~ (x \in A)) : bool_scope.
Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B))
(at level 0, A, B at level 69,
format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope.
Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A)))
(at level 0, only parsing) : fun_scope.
Notation "[ 'rel' 'of' fA ]" := (fun x ⇒ [mem (fA x)])
(at level 0, format "[ 'rel' 'of' fA ]") : fun_scope.
Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B])
(at level 0, format "[ 'predI' A & B ]") : fun_scope.
Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B])
(at level 0, format "[ 'predU' A & B ]") : fun_scope.
Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B])
(at level 0, format "[ 'predD' A & B ]") : fun_scope.
Notation "[ 'predC' A ]" := (predC [mem A])
(at level 0, format "[ 'predC' A ]") : fun_scope.
Notation "[ 'preim' f 'of' A ]" := (preim f [mem A])
(at level 0, format "[ 'preim' f 'of' A ]") : fun_scope.
Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A]
(at level 0, x ident, format "[ 'pred' x 'in' A ]") : fun_scope.
Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E]
(at level 0, x ident, format "[ 'pred' x 'in' A | E ]") : fun_scope.
Notation "[ 'pred' x 'in' A | E1 & E2 ]" := [pred x | x \in A & E1 && E2 ]
(at level 0, x ident,
format "[ 'pred' x 'in' A | E1 & E2 ]") : 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 "[ '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 "[ '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 "[ '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 "[ 'rel' x y 'in' A ]") : fun_scope.
Section simpl_mem.
Variables (T : Type) (pT : predType T).
Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT).
Structure manifest_applicative_pred p := ManifestApplicativePred {
manifest_applicative_pred_value :> pred T;
_ : manifest_applicative_pred_value = p
}.
Definition ApplicativePred p := ManifestApplicativePred (erefl p).
Canonical applicative_pred_applicative sp :=
ApplicativePred (applicative_pred_of_simpl sp).
Structure manifest_simpl_pred p := ManifestSimplPred {
manifest_simpl_pred_value :> simpl_pred T;
_ : manifest_simpl_pred_value = SimplPred p
}.
Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
Structure manifest_mem_pred p := ManifestMemPred {
manifest_mem_pred_value :> mem_pred T;
_ : manifest_mem_pred_value= Mem [eta p]
}.
Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _).
Structure applicative_mem_pred p :=
ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp :=
@ApplicativeMemPred ap mp.
Lemma mem_topred (pp : pT) : mem (topred pp) = mem pp.
Proof. by rewrite /mem; case: pT pp ⇒ T1 app1 [mem1 /= ->]. Qed.
Lemma topredE x (pp : pT) : topred pp x = (x \in pp).
Proof. by rewrite -mem_topred. Qed.
Lemma app_predE x p (ap : manifest_applicative_pred p) : ap x = (x \in p).
Proof. by case: ap ⇒ _ /= →. Qed.
Lemma in_applicative x p (amp : applicative_mem_pred p) : in_mem x amp = p x.
Proof. by case: amp ⇒ [[_ /= ->]]. Qed.
Lemma in_collective x p (msp : manifest_simpl_pred p) :
(x \in collective_pred_of_simpl msp) = p x.
Proof. by case: msp ⇒ _ /= →. Qed.
Lemma in_simpl x p (msp : manifest_simpl_pred p) :
in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x.
Proof. by case: msp ⇒ _ /= →. Qed.
Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x.
Proof. by []. Qed.
Lemma simpl_predE p : SimplPred p =1 p.
Proof. by []. Qed.
Definition inE := (in_applicative, in_simpl, simpl_predE).
Lemma mem_simpl sp : mem sp = sp :> pred T.
Proof. by []. Qed.
Definition memE := mem_simpl.
Lemma mem_mem (pp : pT) : (mem (mem pp) = mem pp) × (mem [mem pp] = mem pp).
Proof. by rewrite -mem_topred. Qed.
End simpl_mem.
CoInductive qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
fun x ⇒ let: Qualifier p := q in p x.
Implicit Arguments has_quality [T].
Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
Notation "x \is A" := (x \in has_quality 0 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \is A ']'") : bool_scope.
Notation "x \is 'a' A" := (x \in has_quality 1 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \is 'a' A ']'") : bool_scope.
Notation "x \is 'an' A" := (x \in has_quality 2 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \is 'an' A ']'") : bool_scope.
Notation "x \isn't A" := (x \notin has_quality 0 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \isn't A ']'") : bool_scope.
Notation "x \isn't 'a' A" := (x \notin has_quality 1 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \isn't 'a' A ']'") : bool_scope.
Notation "x \isn't 'an' A" := (x \notin has_quality 2 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \isn't 'an' A ']'") : bool_scope.
Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x ⇒ P%B))
(at level 0, x at level 99,
format "'[hv' [ 'qualify' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' x : T | P ]" := (Qualifier 0 (fun x : T ⇒ P%B))
(at level 0, x at level 99, only parsing) : form_scope.
Notation "[ 'qualify' 'a' x | P ]" := (Qualifier 1 (fun x ⇒ P%B))
(at level 0, x at level 99,
format "'[hv' [ 'qualify' 'a' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' 'a' x : T | P ]" := (Qualifier 1 (fun x : T ⇒ P%B))
(at level 0, x at level 99, only parsing) : form_scope.
Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x ⇒ P%B))
(at level 0, x at level 99,
format "'[hv' [ 'qualify' 'an' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T ⇒ P%B))
(at level 0, x at level 99, only parsing) : form_scope.
Section KeyPred.
Variable T : Type.
CoInductive pred_key (p : predPredType T) := DefaultPredKey.
Variable p : predPredType T.
Structure keyed_pred (k : pred_key p) :=
PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}.
Variable k : pred_key p.
Definition KeyedPred := @PackKeyedPred k p (frefl _).
Variable k_p : keyed_pred k.
Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed.
Canonical keyed_mem :=
@PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE.
Canonical keyed_mem_simpl :=
@PackKeyedPred k (pred_of_simpl (mem k_p)) keyed_predE.
End KeyPred.
Notation "x \i 'n' S" := (x \in @unkey_pred _ S _ _)
(at level 70, format "'[hv' x '/ ' \i 'n' S ']'") : bool_scope.
Section KeyedQualifier.
Variables (T : Type) (n : nat) (q : qualifier n T).
Structure keyed_qualifier (k : pred_key q) :=
PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
Variables (k : pred_key q) (k_q : keyed_qualifier k).
Fact keyed_qualifier_suproof : unkey_qualifier k_q =i q.
Proof. by case: k_q ⇒ /= _ →. Qed.
Canonical keyed_qualifier_keyed := PackKeyedPred k keyed_qualifier_suproof.
End KeyedQualifier.
Notation "x \i 's' A" := (x \i n has_quality 0 A)
(at level 70, format "'[hv' x '/ ' \i 's' A ']'") : bool_scope.
Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A)
(at level 70, format "'[hv' x '/ ' \i 's' 'a' A ']'") : bool_scope.
Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A)
(at level 70, format "'[hv' x '/ ' \i 's' 'an' A ']'") : bool_scope.
Module DefaultKeying.
Canonical default_keyed_pred T p := KeyedPred (@DefaultPredKey T p).
Canonical default_keyed_qualifier T n (q : qualifier n T) :=
KeyedQualifier (DefaultPredKey q).
End DefaultKeying.
Lemma all_tag_cond_dep I T (C : pred I) U :
(∀ x, T x) → (∀ x, C x → {y : T x & U x y}) →
{f : ∀ x, T x & ∀ x, C x → U x (f x)}.
Proof.
move⇒ f0 fP; apply: all_tag (fun x y ⇒ C x → U x y) _ ⇒ x.
by case Cx: (C x); [case/fP: Cx ⇒ y; ∃ y | ∃ (f0 x)].
Qed.
Lemma all_tag_cond I T (C : pred I) U :
T → (∀ x, C x → {y : T & U x y}) →
{f : I → T & ∀ x, C x → U x (f x)}.
Proof. by move⇒ y0; apply: all_tag_cond_dep. Qed.
Lemma all_sig_cond_dep I T (C : pred I) P :
(∀ x, T x) → (∀ x, C x → {y : T x | P x y}) →
{f : ∀ x, T x | ∀ x, C x → P x (f x)}.
Proof. by move⇒ f0 /(all_tag_cond_dep f0)[f]; ∃ f. Qed.
Lemma all_sig_cond I T (C : pred I) P :
T → (∀ x, C x → {y : T | P x y}) →
{f : I → T | ∀ x, C x → P x (f x)}.
Proof. by move⇒ y0; apply: all_sig_cond_dep. Qed.
Section RelationProperties.
Variable T : Type.
Variable R : rel T.
Definition total := ∀ x y, R x y || R y x.
Definition transitive := ∀ y x z, R x y → R y z → R x z.
Definition symmetric := ∀ x y, R x y = R y x.
Definition antisymmetric := ∀ x y, R x y && R y x → x = y.
Definition pre_symmetric := ∀ x y, R x y → R y x.
Lemma symmetric_from_pre : pre_symmetric → symmetric.
Proof. move⇒ symR x y; apply/idP/idP; exact: symR. Qed.
Definition reflexive := ∀ x, R x x.
Definition irreflexive := ∀ x, R x x = false.
Definition left_transitive := ∀ x y, R x y → R x =1 R y.
Definition right_transitive := ∀ x y, R x y → R^~ x =1 R^~ y.
Section PER.
Hypotheses (symR : symmetric) (trR : transitive).
Lemma sym_left_transitive : left_transitive.
Proof. by move⇒ x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR. Qed.
Lemma sym_right_transitive : right_transitive.
Proof. by move⇒ x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed.
End PER.
Definition equivalence_rel := ∀ x y z, R z z × (R x y → R x z = R y z).
Lemma equivalence_relP : equivalence_rel ↔ reflexive ∧ left_transitive.
Proof.
split⇒ [eqiR | [Rxx trR] x y z]; last by split⇒ [|/trR->].
by split⇒ [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)].
Qed.
End RelationProperties.
Lemma rev_trans T (R : rel T) : transitive R → transitive (fun x y ⇒ R y x).
Proof. by move⇒ trR x y z Ryx Rzy; exact: trR Rzy Ryx. Qed.
Notation Local "{ 'all1' P }" := (∀ x, P x : Prop) (at level 0).
Notation Local "{ 'all2' P }" := (∀ x y, P x y : Prop) (at level 0).
Notation Local "{ 'all3' P }" := (∀ x y z, P x y z: Prop) (at level 0).
Notation Local ph := (phantom _).
Section LocalProperties.
Variables T1 T2 T3 : Type.
Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
Notation Local ph := (phantom Prop).
Definition prop_for (x : T1) P & ph {all1 P} := P x.
Lemma forE x P phP : @prop_for x P phP = P x. Proof. by []. Qed.
Definition prop_in1 P & ph {all1 P} :=
∀ x, in_mem x d1 → P x.
Definition prop_in11 P & ph {all2 P} :=
∀ x y, in_mem x d1 → in_mem y d2 → P x y.
Definition prop_in2 P & ph {all2 P} :=
∀ x y, in_mem x d1 → in_mem y d1 → P x y.
Definition prop_in111 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d2 → in_mem z d3 → P x y z.
Definition prop_in12 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d2 → in_mem z d2 → P x y z.
Definition prop_in21 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d1 → in_mem z d2 → P x y z.
Definition prop_in3 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d1 → in_mem z d1 → P x y z.
Variable f : T1 → T2.
Definition prop_on1 Pf P & phantom T3 (Pf f) & ph {all1 P} :=
∀ x, in_mem (f x) d2 → P x.
Definition prop_on2 Pf P & phantom T3 (Pf f) & ph {all2 P} :=
∀ x y, in_mem (f x) d2 → in_mem (f y) d2 → P x y.
End LocalProperties.
Definition inPhantom := Phantom Prop.
Definition onPhantom T P (x : T) := Phantom Prop (P x).
Definition bijective_in aT rT (d : mem_pred aT) (f : aT → rT) :=
exists2 g, prop_in1 d (inPhantom (cancel f g))
& prop_on1 d (Phantom _ (cancel g)) (onPhantom (cancel g) f).
Definition bijective_on aT rT (cd : mem_pred rT) (f : aT → rT) :=
exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g)
& prop_in1 cd (inPhantom (cancel g f)).
Notation "{ 'for' x , P }" :=
(prop_for x (inPhantom P))
(at level 0, format "{ 'for' x , P }") : type_scope.
Notation "{ 'in' d , P }" :=
(prop_in1 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d , P }") : type_scope.
Notation "{ 'in' d1 & d2 , P }" :=
(prop_in11 (mem d1) (mem d2) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 , P }") : type_scope.
Notation "{ 'in' d & , P }" :=
(prop_in2 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d & , P }") : type_scope.
Notation "{ 'in' d1 & d2 & d3 , P }" :=
(prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope.
Notation "{ 'in' d1 & & d3 , P }" :=
(prop_in21 (mem d1) (mem d3) (inPhantom P))
(at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope.
Notation "{ 'in' d1 & d2 & , P }" :=
(prop_in12 (mem d1) (mem d2) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope.
Notation "{ 'in' d & & , P }" :=
(prop_in3 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d & & , P }") : type_scope.
Notation "{ 'on' cd , P }" :=
(prop_on1 (mem cd) (inPhantom P) (inPhantom P))
(at level 0, format "{ 'on' cd , P }") : type_scope.
Notation "{ 'on' cd & , P }" :=
(prop_on2 (mem cd) (inPhantom P) (inPhantom P))
(at level 0, format "{ 'on' cd & , P }") : type_scope.
Notation "{ 'on' cd , P & g }" :=
(prop_on1 (mem cd) (Phantom (_ → Prop) P) (onPhantom P g))
(at level 0, format "{ 'on' cd , P & g }") : type_scope.
Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f)
(at level 0, f at level 8,
format "{ 'in' d , 'bijective' f }") : type_scope.
Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f)
(at level 0, f at level 8,
format "{ 'on' cd , 'bijective' f }") : type_scope.
Section LocalGlobal.
Variables T1 T2 T3 : predArgType.
Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3).
Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3).
Variables (f f' : T1 → T2) (g : T2 → T1) (h : T3).
Variables (P1 : T1 → Prop) (P2 : T1 → T2 → Prop).
Variable P3 : T1 → T2 → T3 → Prop.
Variable Q1 : (T1 → T2) → T1 → Prop.
Variable Q1l : (T1 → T2) → T3 → T1 → Prop.
Variable Q2 : (T1 → T2) → T1 → T1 → Prop.
Hypothesis sub1 : sub_mem d1 d1'.
Hypothesis sub2 : sub_mem d2 d2'.
Hypothesis sub3 : sub_mem d3 d3'.
Lemma in1W : {all1 P1} → {in D1, {all1 P1}}.
Proof. by move⇒ ? ?. Qed.
Lemma in2W : {all2 P2} → {in D1 & D2, {all2 P2}}.
Proof. by move⇒ ? ?. Qed.
Lemma in3W : {all3 P3} → {in D1 & D2 & D3, {all3 P3}}.
Proof. by move⇒ ? ?. Qed.
Lemma in1T : {in T1, {all1 P1}} → {all1 P1}.
Proof. by move⇒ ? ?; auto. Qed.
Lemma in2T : {in T1 & T2, {all2 P2}} → {all2 P2}.
Proof. by move⇒ ? ?; auto. Qed.
Lemma in3T : {in T1 & T2 & T3, {all3 P3}} → {all3 P3}.
Proof. by move⇒ ? ?; auto. Qed.
Lemma sub_in1 (Ph : ph {all1 P1}) : prop_in1 d1' Ph → prop_in1 d1 Ph.
Proof. move⇒ allP x /sub1; exact: allP. Qed.
Lemma sub_in11 (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph → prop_in11 d1 d2 Ph.
Proof. move⇒ allP x1 x2 /sub1 d1x1 /sub2; exact: allP. Qed.
Lemma sub_in111 (Ph : ph {all3 P3}) :
prop_in111 d1' d2' d3' Ph → prop_in111 d1 d2 d3 Ph.
Proof. by move⇒ allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP. Qed.
Let allQ1 f'' := {all1 Q1 f''}.
Let allQ1l f'' h' := {all1 Q1l f'' h'}.
Let allQ2 f'' := {all2 Q2 f''}.
Lemma on1W : allQ1 f → {on D2, allQ1 f}. Proof. by move⇒ ? ?. Qed.
Lemma on1lW : allQ1l f h → {on D2, allQ1l f & h}. Proof. by move⇒ ? ?. Qed.
Lemma on2W : allQ2 f → {on D2 &, allQ2 f}. Proof. by move⇒ ? ?. Qed.
Lemma on1T : {on T2, allQ1 f} → allQ1 f. Proof. by move⇒ ? ?; auto. Qed.
Lemma on1lT : {on T2, allQ1l f & h} → allQ1l f h.
Proof. by move⇒ ? ?; auto. Qed.
Lemma on2T : {on T2 &, allQ2 f} → allQ2 f.
Proof. by move⇒ ? ?; auto. Qed.
Lemma subon1 (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) :
prop_on1 d2' Phf Ph → prop_on1 d2 Phf Ph.
Proof. by move⇒ allQ x /sub2; exact: allQ. Qed.
Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) :
prop_on1 d2' Phf Ph → prop_on1 d2 Phf Ph.
Proof. by move⇒ allQ x /sub2; exact: allQ. Qed.
Lemma subon2 (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) :
prop_on2 d2' Phf Ph → prop_on2 d2 Phf Ph.
Proof. by move⇒ allQ x y /sub2⇒ d2fx /sub2; exact: allQ. Qed.
Lemma can_in_inj : {in D1, cancel f g} → {in D1 &, injective f}.
Proof. by move⇒ fK x y /fK{2}<- /fK{2}<- →. Qed.
Lemma canLR_in x y : {in D1, cancel f g} → y \in D1 → x = f y → g x = y.
Proof. by move⇒ fK D1y ->; rewrite fK. Qed.
Lemma canRL_in x y : {in D1, cancel f g} → x \in D1 → f x = y → x = g y.
Proof. by move⇒ fK D1x <-; rewrite fK. Qed.
Lemma on_can_inj : {on D2, cancel f & g} → {on D2 &, injective f}.
Proof. by move⇒ fK x y /fK{2}<- /fK{2}<- →. Qed.
Lemma canLR_on x y : {on D2, cancel f & g} → f y \in D2 → x = f y → g x = y.
Proof. by move⇒ fK D2fy ->; rewrite fK. Qed.
Lemma canRL_on x y : {on D2, cancel f & g} → f x \in D2 → f x = y → x = g y.
Proof. by move⇒ fK D2fx <-; rewrite fK. Qed.
Lemma inW_bij : bijective f → {in D1, bijective f}.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma onW_bij : bijective f → {on D2, bijective f}.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma inT_bij : {in T1, bijective f} → bijective f.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma onT_bij : {on T2, bijective f} → bijective f.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma sub_in_bij (D1' : pred T1) :
{subset D1 ≤ D1'} → {in D1', bijective f} → {in D1, bijective f}.
Proof.
by move⇒ subD [g' fK g'K]; ∃ g' ⇒ x; move/subD; [exact: fK | exact: g'K].
Qed.
Lemma subon_bij (D2' : pred T2) :
{subset D2 ≤ D2'} → {on D2', bijective f} → {on D2, bijective f}.
Proof.
by move⇒ subD [g' fK g'K]; ∃ g' ⇒ x; move/subD; [exact: fK | exact: g'K].
Qed.
End LocalGlobal.
Lemma sub_in2 T d d' (P : T → T → Prop) :
sub_mem d d' → ∀ Ph : ph {all2 P}, prop_in2 d' Ph → prop_in2 d Ph.
Proof. by move⇒ /= sub_dd'; exact: sub_in11. Qed.
Lemma sub_in3 T d d' (P : T → T → T → Prop) :
sub_mem d d' → ∀ Ph : ph {all3 P}, prop_in3 d' Ph → prop_in3 d Ph.
Proof. by move⇒ /= sub_dd'; exact: sub_in111. Qed.
Lemma sub_in12 T1 T d1 d1' d d' (P : T1 → T → T → Prop) :
sub_mem d1 d1' → sub_mem d d' →
∀ Ph : ph {all3 P}, prop_in12 d1' d' Ph → prop_in12 d1 d Ph.
Proof. by move⇒ /= sub1 sub; exact: sub_in111. Qed.
Lemma sub_in21 T T3 d d' d3 d3' (P : T → T → T3 → Prop) :
sub_mem d d' → sub_mem d3 d3' →
∀ Ph : ph {all3 P}, prop_in21 d' d3' Ph → prop_in21 d d3 Ph.
Proof. by move⇒ /= sub sub3; exact: sub_in111. Qed.
Lemma equivalence_relP_in T (R : rel T) (A : pred T) :
{in A & &, equivalence_rel R}
↔ {in A, reflexive R} ∧ {in A &, ∀ x y, R x y → {in A, R x =1 R y}}.
Proof.
split⇒ [eqiR | [Rxx trR] x y z *]; last by split⇒ [|/trR→ //]; exact: Rxx.
by split⇒ [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)].
Qed.
Section MonoHomoMorphismTheory.
Variables (aT rT sT : Type) (f : aT → rT) (g : rT → aT).
Variables (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).
Lemma monoW : {mono f : x / aP x >-> rP x} → {homo f : x / aP x >-> rP x}.
Proof. by move⇒ hf x ax; rewrite hf. Qed.
Lemma mono2W :
{mono f : x y / aR x y >-> rR x y} → {homo f : x y / aR x y >-> rR x y}.
Proof. by move⇒ hf x y axy; rewrite hf. Qed.
Hypothesis fgK : cancel g f.
Lemma homoRL :
{homo f : x y / aR x y >-> rR x y} → ∀ x y, aR (g x) y → rR x (f y).
Proof. by move⇒ Hf x y /Hf; rewrite fgK. Qed.
Lemma homoLR :
{homo f : x y / aR x y >-> rR x y} → ∀ x y, aR x (g y) → rR (f x) y.
Proof. by move⇒ Hf x y /Hf; rewrite fgK. Qed.
Lemma homo_mono :
{homo f : x y / aR x y >-> rR x y} → {homo g : x y / rR x y >-> aR x y} →
{mono g : x y / rR x y >-> aR x y}.
Proof.
move⇒ mf mg x y; case: (boolP (rR _ _))=> [/mg //|].
by apply: contraNF⇒ /mf; rewrite !fgK.
Qed.
Lemma monoLR :
{mono f : x y / aR x y >-> rR x y} → ∀ x y, rR (f x) y = aR x (g y).
Proof. by move⇒ mf x y; rewrite -{1}[y]fgK mf. Qed.
Lemma monoRL :
{mono f : x y / aR x y >-> rR x y} → ∀ x y, rR x (f y) = aR (g x) y.
Proof. by move⇒ mf x y; rewrite -{1}[x]fgK mf. Qed.
Lemma can_mono :
{mono f : x y / aR x y >-> rR x y} → {mono g : x y / rR x y >-> aR x y}.
Proof. by move⇒ mf x y /=; rewrite -mf !fgK. Qed.
End MonoHomoMorphismTheory.
Section MonoHomoMorphismTheory_in.
Variables (aT rT sT : predArgType) (f : aT → rT) (g : rT → aT).
Variable (aD : pred aT).
Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).
Notation rD := [pred x | g x \in aD].
Lemma monoW_in :
{in aD &, {mono f : x y / aR x y >-> rR x y}} →
{in aD &, {homo f : x y / aR x y >-> rR x y}}.
Proof. by move⇒ hf x y hx hy axy; rewrite hf. Qed.
Lemma mono2W_in :
{in aD, {mono f : x / aP x >-> rP x}} →
{in aD, {homo f : x / aP x >-> rP x}}.
Proof. by move⇒ hf x hx ax; rewrite hf. Qed.
Hypothesis fgK_on : {on aD, cancel g & f}.
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)}.
Proof. by move⇒ Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed.
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}.
Proof. by move⇒ Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed.
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}}.
Proof.
move⇒ mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact.
by apply: contraNF⇒ /mf; rewrite !fgK_on //; apply.
Qed.
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)}.
Proof. by move⇒ mf x y hx hy; rewrite -{1}[y]fgK_on // mf. Qed.
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}.
Proof. by move⇒ mf x y hx hy; rewrite -{1}[x]fgK_on // mf. Qed.
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}}.
Proof. by move⇒ mf x y hx hy /=; rewrite -mf // !fgK_on. Qed.
End MonoHomoMorphismTheory_in.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "~~ b" (at level 35, right associativity).
Reserved Notation "b ==> c" (at level 55, right associativity).
Reserved Notation "b1 (+) b2" (at level 50, left associativity).
Reserved Notation "x \in A"
(at level 70, format "'[hv' x '/ ' \in A ']'", no associativity).
Reserved Notation "x \notin A"
(at level 70, format "'[hv' x '/ ' \notin A ']'", no associativity).
Reserved Notation "p1 =i p2"
(at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity).
Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing).
Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format
"'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format
"'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 ']' '/ ' & P4 ] ']'").
Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format
"'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'").
Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing).
Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format
"'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'").
Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format
"'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'").
Reserved Notation "[ && b1 & c ]" (at level 0, only parsing).
Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format
"'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'").
Reserved Notation "[ || b1 | c ]" (at level 0, only parsing).
Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format
"'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'").
Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing).
Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format
"'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'").
Reserved Notation "[ 'pred' : T => E ]" (at level 0, format
"'[hv' [ 'pred' : T => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x => E ]" (at level 0, x at level 8, format
"'[hv' [ 'pred' x => '/ ' E ] ']'").
Reserved Notation "[ 'pred' x : T => E ]" (at level 0, x at level 8, format
"'[hv' [ 'pred' x : T => '/ ' E ] ']'").
Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format
"'[hv' [ 'rel' x y => '/ ' E ] ']'").
Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format
"'[hv' [ 'rel' x y : T => '/ ' E ] ']'").
Delimit Scope bool_scope with B.
Open Scope bool_scope.
Definition addb b := if b then negb else id.
Notation "~~ b" := (negb b) : bool_scope.
Notation "b ==> c" := (implb b c) : bool_scope.
Notation "b1 (+) b2" := (addb b1 b2) : bool_scope.
Coercion is_true : bool >-> Sortclass.
Lemma prop_congr : ∀ b b' : bool, b = b' → b = b' :> Prop.
Proof. by move⇒ b b' →. Qed.
Ltac prop_congr := apply: prop_congr.
Lemma is_true_true : true. Proof. by []. Qed.
Lemma not_false_is_true : ¬ false. Proof. by []. Qed.
Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
Hint Resolve is_true_true not_false_is_true is_true_locked_true.
Definition isT := is_true_true.
Definition notF := not_false_is_true.
Lemma negbT b : b = false → ~~ b. Proof. by case: b. Qed.
Lemma negbTE b : ~~ b → b = false. Proof. by case: b. Qed.
Lemma negbF b : (b : bool) → ~~ b = false. Proof. by case: b. Qed.
Lemma negbFE b : ~~ b = false → b. Proof. by case: b. Qed.
Lemma negbK : involutive negb. Proof. by case. Qed.
Lemma negbNE b : ~~ ~~ b → b. Proof. by case: b. Qed.
Lemma negb_inj : injective negb. Proof. exact: can_inj negbK. Qed.
Lemma negbLR b c : b = ~~ c → ~~ b = c. Proof. exact: canLR negbK. Qed.
Lemma negbRL b c : ~~ b = c → b = ~~ c. Proof. exact: canRL negbK. Qed.
Lemma contra (c b : bool) : (c → b) → ~~ b → ~~ c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraNN := contra.
Lemma contraL (c b : bool) : (c → ~~ b) → b → ~~ c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraTN := contraL.
Lemma contraR (c b : bool) : (~~ c → b) → ~~ b → c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraNT := contraR.
Lemma contraLR (c b : bool) : (~~ c → ~~ b) → b → c.
Proof. by case: b ⇒ //; case: c. Qed.
Definition contraTT := contraLR.
Lemma contraT b : (~~ b → false) → b. Proof. by case: b ⇒ // →. Qed.
Lemma wlog_neg b : (~~ b → b) → b. Proof. by case: b ⇒ // →. Qed.
Lemma contraFT (c b : bool) : (~~ c → b) → b = false → c.
Proof. by move/contraR⇒ notb_c /negbT. Qed.
Lemma contraFN (c b : bool) : (c → b) → b = false → ~~ c.
Proof. by move/contra⇒ notb_notc /negbT. Qed.
Lemma contraTF (c b : bool) : (c → ~~ b) → b → c = false.
Proof. by move/contraL⇒ b_notc /b_notc/negbTE. Qed.
Lemma contraNF (c b : bool) : (c → b) → ~~ b → c = false.
Proof. by move/contra⇒ notb_notc /notb_notc/negbTE. Qed.
Lemma contraFF (c b : bool) : (c → b) → b = false → c = false.
Proof. by move/contraFN⇒ bF_notc /bF_notc/negbTE. Qed.
Coercion isSome T (u : option T) := if u is Some _ then true else false.
Coercion is_inl A B (u : A + B) := if u is inl _ then true else false.
Coercion is_left A B (u : {A} + {B}) := if u is left _ then true else false.
Coercion is_inleft A B (u : A + {B}) := if u is inleft _ then true else false.
Prenex Implicits isSome is_inl is_left is_inleft.
Definition decidable P := {P} + {¬ P}.
Section BoolIf.
Variables (A B : Type) (x : A) (f : A → B) (b : bool) (vT vF : A).
CoInductive if_spec (not_b : Prop) : bool → A → Set :=
| IfSpecTrue of b : if_spec not_b true vT
| IfSpecFalse of not_b : if_spec not_b false vF.
Lemma ifP : if_spec (b = false) b (if b then vT else vF).
Proof. by case def_b: b; constructor. Qed.
Lemma ifPn : if_spec (~~ b) b (if b then vT else vF).
Proof. by case def_b: b; constructor; rewrite ?def_b. Qed.
Lemma ifT : b → (if b then vT else vF) = vT. Proof. by move→. Qed.
Lemma ifF : b = false → (if b then vT else vF) = vF. Proof. by move→. Qed.
Lemma ifN : ~~ b → (if b then vT else vF) = vF. Proof. by move/negbTE→. Qed.
Lemma if_same : (if b then vT else vT) = vT.
Proof. by case b. Qed.
Lemma if_neg : (if ~~ b then vT else vF) = if b then vF else vT.
Proof. by case b. Qed.
Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
Proof. by case b. Qed.
Lemma if_arg (fT fF : A → B) :
(if b then fT else fF) x = if b then fT x else fF x.
Proof. by case b. Qed.
Definition if_expr := if b then vT else vF.
Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed.
End BoolIf.
Inductive reflect (P : Prop) : bool → Set :=
| ReflectT of P : reflect P true
| ReflectF of ¬ P : reflect P false.
Section ReflectCore.
Variables (P Q : Prop) (b c : bool).
Hypothesis Hb : reflect P b.
Lemma introNTF : (if c then ¬ P else P) → ~~ b = c.
Proof. by case c; case Hb. Qed.
Lemma introTF : (if c then P else ¬ P) → b = c.
Proof. by case c; case Hb. Qed.
Lemma elimNTF : ~~ b = c → if c then ¬ P else P.
Proof. by move <-; case Hb. Qed.
Lemma elimTF : b = c → if c then P else ¬ P.
Proof. by move <-; case Hb. Qed.
Lemma equivPif : (Q → P) → (P → Q) → if b then Q else ¬ Q.
Proof. by case Hb; auto. Qed.
Lemma xorPif : Q ∨ P → ¬ (Q ∧ P) → if b then ¬ Q else Q.
Proof. by case Hb ⇒ [? _ H ? | ? H _]; case: H. Qed.
End ReflectCore.
Section ReflectNegCore.
Variables (P Q : Prop) (b c : bool).
Hypothesis Hb : reflect P (~~ b).
Lemma introTFn : (if c then ¬ P else P) → b = c.
Proof. by move/(introNTF Hb) <-; case b. Qed.
Lemma elimTFn : b = c → if c then ¬ P else P.
Proof. by move <-; apply: (elimNTF Hb); case b. Qed.
Lemma equivPifn : (Q → P) → (P → Q) → if b then ¬ Q else Q.
Proof. rewrite -if_neg; exact: equivPif. Qed.
Lemma xorPifn : Q ∨ P → ¬ (Q ∧ P) → if b then Q else ¬ Q.
Proof. rewrite -if_neg; exact: xorPif. Qed.
End ReflectNegCore.
Section Reflect.
Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (~~ b')).
Lemma introT : P → b. Proof. exact: introTF true _. Qed.
Lemma introF : ¬ P → b = false. Proof. exact: introTF false _. Qed.
Lemma introN : ¬ P → ~~ b. Proof. exact: introNTF true _. Qed.
Lemma introNf : P → ~~ b = false. Proof. exact: introNTF false _. Qed.
Lemma introTn : ¬ P → b'. Proof. exact: introTFn true _. Qed.
Lemma introFn : P → b' = false. Proof. exact: introTFn false _. Qed.
Lemma elimT : b → P. Proof. exact: elimTF true _. Qed.
Lemma elimF : b = false → ¬ P. Proof. exact: elimTF false _. Qed.
Lemma elimN : ~~ b → ¬P. Proof. exact: elimNTF true _. Qed.
Lemma elimNf : ~~ b = false → P. Proof. exact: elimNTF false _. Qed.
Lemma elimTn : b' → ¬ P. Proof. exact: elimTFn true _. Qed.
Lemma elimFn : b' = false → P. Proof. exact: elimTFn false _. Qed.
Lemma introP : (b → Q) → (~~ b → ¬ Q) → reflect Q b.
Proof. by case b; constructor; auto. Qed.
Lemma iffP : (P → Q) → (Q → P) → reflect Q b.
Proof. by case: Pb; constructor; auto. Qed.
Lemma equivP : (P ↔ Q) → reflect Q b.
Proof. by case; exact: iffP. Qed.
Lemma sumboolP (decQ : decidable Q) : reflect Q decQ.
Proof. by case: decQ; constructor. Qed.
Lemma appP : reflect Q b → P → Q.
Proof. by move⇒ Qb; move/introT; case: Qb. Qed.
Lemma sameP : reflect P c → b = c.
Proof. case; [exact: introT | exact: introF]. Qed.
Lemma decPcases : if b then P else ¬ P. Proof. by case Pb. Qed.
Definition decP : decidable P. by case: b decPcases; [left | right]. Defined.
Lemma rwP : P ↔ b. Proof. by split; [exact: introT | exact: elimT]. Qed.
Lemma rwP2 : reflect Q b → (P ↔ Q).
Proof. by move⇒ Qb; split⇒ ?; [exact: appP | apply: elimT; case: Qb]. Qed.
CoInductive alt_spec : bool → Type :=
| AltTrue of P : alt_spec true
| AltFalse of ~~ b : alt_spec false.
Lemma altP : alt_spec b.
Proof. by case def_b: b / Pb; constructor; rewrite ?def_b. Qed.
End Reflect.
Hint View for move/ elimTF|3 elimNTF|3 elimTFn|3 introT|2 introTn|2 introN|2.
Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2.
Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
Coercion elimT : reflect >-> Funclass.
Definition unless condition property := (property → condition) → condition.
Lemma bind_unless C P {Q} : unless C P → unless (unless C Q) P.
Proof. by move⇒ haveP suffPQ suffQ; apply: haveP ⇒ /suffPQ; exact. Qed.
Lemma unless_contra b C : (~~ b → C) → unless C b.
Proof. by case: b ⇒ [_ haveC | haveC _]; exact: haveC. Qed.
Definition classically P : Prop := ∀ b : bool, (P → b) → b.
Lemma classicP : ∀ P : Prop, classically P ↔ ¬ ¬ P.
Proof.
move⇒ P; split⇒ [cP nP | nnP [] // nP]; last by case nnP; move/nP.
by have: P → false; [move/nP | move/cP].
Qed.
Lemma classic_bind : ∀ P Q,
(P → classically Q) → (classically P → classically Q).
Proof. by move⇒ P Q IH IH_P b IH_Q; apply: IH_P; move/IH; exact. Qed.
Lemma classic_EM : ∀ P, classically (decidable P).
Proof.
by move⇒ P [] // IH; apply IH; right ⇒ ?; apply: notF (IH _); left.
Qed.
Lemma classic_imply : ∀ P Q, (P → classically Q) → classically (P → Q).
Proof.
move⇒ P Q IH [] // notPQ; apply notPQ; move/IH⇒ hQ; case: notF.
by apply: hQ ⇒ hQ; case: notF; exact: notPQ.
Qed.
Lemma classic_pick : ∀ T P,
classically ({x : T | P x} + (∀ x, ¬ P x)).
Proof.
move⇒ T P [] // IH; apply IH; right⇒ x Px; case: notF.
by apply: IH; left; ∃ x.
Qed.
Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3.
Inductive and4 (P1 P2 P3 P4 : Prop) : Prop := And4 of P1 & P2 & P3 & P4.
Inductive and5 (P1 P2 P3 P4 P5 : Prop) : Prop :=
And5 of P1 & P2 & P3 & P4 & P5.
Inductive or3 (P1 P2 P3 : Prop) : Prop := Or31 of P1 | Or32 of P2 | Or33 of P3.
Inductive or4 (P1 P2 P3 P4 : Prop) : Prop :=
Or41 of P1 | Or42 of P2 | Or43 of P3 | Or44 of P4.
Notation "[ /\ P1 & P2 ]" := (and P1 P2) (only parsing) : type_scope.
Notation "[ /\ P1 , P2 & P3 ]" := (and3 P1 P2 P3) : type_scope.
Notation "[ /\ P1 , P2 , P3 & P4 ]" := (and4 P1 P2 P3 P4) : type_scope.
Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" := (and5 P1 P2 P3 P4 P5) : type_scope.
Notation "[ \/ P1 | P2 ]" := (or P1 P2) (only parsing) : type_scope.
Notation "[ \/ P1 , P2 | P3 ]" := (or3 P1 P2 P3) : type_scope.
Notation "[ \/ P1 , P2 , P3 | P4 ]" := (or4 P1 P2 P3 P4) : type_scope.
Notation "[ && b1 & c ]" := (b1 && c) (only parsing) : bool_scope.
Notation "[ && b1 , b2 , .. , bn & c ]" := (b1 && (b2 && .. (bn && c) .. ))
: bool_scope.
Notation "[ || b1 | c ]" := (b1 || c) (only parsing) : bool_scope.
Notation "[ || b1 , b2 , .. , bn | c ]" := (b1 || (b2 || .. (bn || c) .. ))
: bool_scope.
Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
(b1 ==> (b2 ==> .. (bn ==> c) .. )) : bool_scope.
Notation "[ ==> b1 => c ]" := (b1 ==> c) (only parsing) : bool_scope.
Section AllAnd.
Variables (T : Type) (P1 P2 P3 P4 P5 : T → Prop).
Local Notation a P := (∀ x, P x).
Lemma all_and2 (hP : ∀ x, [/\ P1 x & P2 x]) : [/\ a P1 & a P2].
Proof. by split⇒ x; case: (hP x). Qed.
Lemma all_and3 (hP : ∀ x, [/\ P1 x, P2 x & P3 x]) :
[/\ a P1, a P2 & a P3].
Proof. by split⇒ x; case: (hP x). Qed.
Lemma all_and4 (hP : ∀ x, [/\ P1 x, P2 x, P3 x & P4 x]) :
[/\ a P1, a P2, a P3 & a P4].
Proof. by split⇒ x; case: (hP x). Qed.
Lemma all_and5 (hP : ∀ x, [/\ P1 x, P2 x, P3 x, P4 x & P5 x]) :
[/\ a P1, a P2, a P3, a P4 & a P5].
Proof. by split⇒ x; case: (hP x). Qed.
End AllAnd.
Lemma pair_andP P Q : P ∧ Q ↔ P × Q. Proof. by split; case. Qed.
Section ReflectConnectives.
Variable b1 b2 b3 b4 b5 : bool.
Lemma idP : reflect b1 b1.
Proof. by case b1; constructor. Qed.
Lemma boolP : alt_spec b1 b1 b1.
Proof. exact: (altP idP). Qed.
Lemma idPn : reflect (~~ b1) (~~ b1).
Proof. by case b1; constructor. Qed.
Lemma negP : reflect (¬ b1) (~~ b1).
Proof. by case b1; constructor; auto. Qed.
Lemma negPn : reflect b1 (~~ ~~ b1).
Proof. by case b1; constructor. Qed.
Lemma negPf : reflect (b1 = false) (~~ b1).
Proof. by case b1; constructor. Qed.
Lemma andP : reflect (b1 ∧ b2) (b1 && b2).
Proof. by case b1; case b2; constructor⇒ //; case. Qed.
Lemma and3P : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3].
Proof. by case b1; case b2; case b3; constructor; try by case. Qed.
Lemma and4P : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4].
Proof. by case b1; case b2; case b3; case b4; constructor; try by case. Qed.
Lemma and5P : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5].
Proof.
by case b1; case b2; case b3; case b4; case b5; constructor; try by case.
Qed.
Lemma orP : reflect (b1 ∨ b2) (b1 || b2).
Proof. by case b1; case b2; constructor; auto; case. Qed.
Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3].
Proof.
case b1; first by constructor; constructor 1.
case b2; first by constructor; constructor 2.
case b3; first by constructor; constructor 3.
by constructor; case.
Qed.
Lemma or4P : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4].
Proof.
case b1; first by constructor; constructor 1.
case b2; first by constructor; constructor 2.
case b3; first by constructor; constructor 3.
case b4; first by constructor; constructor 4.
by constructor; case.
Qed.
Lemma nandP : reflect (~~ b1 ∨ ~~ b2) (~~ (b1 && b2)).
Proof. by case b1; case b2; constructor; auto; case; auto. Qed.
Lemma norP : reflect (~~ b1 ∧ ~~ b2) (~~ (b1 || b2)).
Proof. by case b1; case b2; constructor; auto; case; auto. Qed.
Lemma implyP : reflect (b1 → b2) (b1 ==> b2).
Proof. by case b1; case b2; constructor; auto. Qed.
End ReflectConnectives.
Implicit Arguments idP [b1].
Implicit Arguments idPn [b1].
Implicit Arguments negP [b1].
Implicit Arguments negPn [b1].
Implicit Arguments negPf [b1].
Implicit Arguments andP [b1 b2].
Implicit Arguments and3P [b1 b2 b3].
Implicit Arguments and4P [b1 b2 b3 b4].
Implicit Arguments and5P [b1 b2 b3 b4 b5].
Implicit Arguments orP [b1 b2].
Implicit Arguments or3P [b1 b2 b3].
Implicit Arguments or4P [b1 b2 b3 b4].
Implicit Arguments nandP [b1 b2].
Implicit Arguments norP [b1 b2].
Implicit Arguments implyP [b1 b2].
Prenex Implicits idP idPn negP negPn negPf.
Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
Lemma andTb : left_id true andb. Proof. by []. Qed.
Lemma andFb : left_zero false andb. Proof. by []. Qed.
Lemma andbT : right_id true andb. Proof. by case. Qed.
Lemma andbF : right_zero false andb. Proof. by case. Qed.
Lemma andbb : idempotent andb. Proof. by case. Qed.
Lemma andbC : commutative andb. Proof. by do 2!case. Qed.
Lemma andbA : associative andb. Proof. by do 3!case. Qed.
Lemma andbCA : left_commutative andb. Proof. by do 3!case. Qed.
Lemma andbAC : right_commutative andb. Proof. by do 3!case. Qed.
Lemma andbACA : interchange andb andb. Proof. by do 4!case. Qed.
Lemma orTb : ∀ b, true || b. Proof. by []. Qed.
Lemma orFb : left_id false orb. Proof. by []. Qed.
Lemma orbT : ∀ b, b || true. Proof. by case. Qed.
Lemma orbF : right_id false orb. Proof. by case. Qed.
Lemma orbb : idempotent orb. Proof. by case. Qed.
Lemma orbC : commutative orb. Proof. by do 2!case. Qed.
Lemma orbA : associative orb. Proof. by do 3!case. Qed.
Lemma orbCA : left_commutative orb. Proof. by do 3!case. Qed.
Lemma orbAC : right_commutative orb. Proof. by do 3!case. Qed.
Lemma orbACA : interchange orb orb. Proof. by do 4!case. Qed.
Lemma andbN b : b && ~~ b = false. Proof. by case: b. Qed.
Lemma andNb b : ~~ b && b = false. Proof. by case: b. Qed.
Lemma orbN b : b || ~~ b = true. Proof. by case: b. Qed.
Lemma orNb b : ~~ b || b = true. Proof. by case: b. Qed.
Lemma andb_orl : left_distributive andb orb. Proof. by do 3!case. Qed.
Lemma andb_orr : right_distributive andb orb. Proof. by do 3!case. Qed.
Lemma orb_andl : left_distributive orb andb. Proof. by do 3!case. Qed.
Lemma orb_andr : right_distributive orb andb. Proof. by do 3!case. Qed.
Lemma andb_idl (a b : bool) : (b → a) → a && b = b.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma andb_idr (a b : bool) : (a → b) → a && b = a.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma andb_id2l (a b c : bool) : (a → b = c) → a && b = a && c.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma andb_id2r (a b c : bool) : (b → a = c) → a && b = c && b.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma orb_idl (a b : bool) : (a → b) → a || b = b.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma orb_idr (a b : bool) : (b → a) → a || b = a.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma orb_id2l (a b c : bool) : (~~ a → b = c) → a || b = a || c.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma orb_id2r (a b c : bool) : (~~ b → a = c) → a || b = c || b.
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma negb_and (a b : bool) : ~~ (a && b) = ~~ a || ~~ b.
Proof. by case: a; case: b. Qed.
Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b.
Proof. by case: a; case: b. Qed.
Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed.
Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed.
Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed.
Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed.
Lemma implybT b : b ==> true. Proof. by case: b. Qed.
Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed.
Lemma implyFb b : false ==> b. Proof. by []. Qed.
Lemma implyTb b : (true ==> b) = b. Proof. by []. Qed.
Lemma implybb b : b ==> b. Proof. by case: b. Qed.
Lemma negb_imply a b : ~~ (a ==> b) = a && ~~ b.
Proof. by case: a; case: b. Qed.
Lemma implybE a b : (a ==> b) = ~~ a || b.
Proof. by case: a; case: b. Qed.
Lemma implyNb a b : (~~ a ==> b) = a || b.
Proof. by case: a; case: b. Qed.
Lemma implybN a b : (a ==> ~~ b) = (b ==> ~~ a).
Proof. by case: a; case: b. Qed.
Lemma implybNN a b : (~~ a ==> ~~ b) = b ==> a.
Proof. by case: a; case: b. Qed.
Lemma implyb_idl (a b : bool) : (~~ a → b) → (a ==> b) = b.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma implyb_idr (a b : bool) : (b → ~~ a) → (a ==> b) = ~~ a.
Proof. by case: a; case: b ⇒ // →. Qed.
Lemma implyb_id2l (a b c : bool) : (a → b = c) → (a ==> b) = (a ==> c).
Proof. by case: a; case: b; case: c ⇒ // →. Qed.
Lemma addFb : left_id false addb. Proof. by []. Qed.
Lemma addbF : right_id false addb. Proof. by case. Qed.
Lemma addbb : self_inverse false addb. Proof. by case. Qed.
Lemma addbC : commutative addb. Proof. by do 2!case. Qed.
Lemma addbA : associative addb. Proof. by do 3!case. Qed.
Lemma addbCA : left_commutative addb. Proof. by do 3!case. Qed.
Lemma addbAC : right_commutative addb. Proof. by do 3!case. Qed.
Lemma addbACA : interchange addb addb. Proof. by do 4!case. Qed.
Lemma andb_addl : left_distributive andb addb. Proof. by do 3!case. Qed.
Lemma andb_addr : right_distributive andb addb. Proof. by do 3!case. Qed.
Lemma addKb : left_loop id addb. Proof. by do 2!case. Qed.
Lemma addbK : right_loop id addb. Proof. by do 2!case. Qed.
Lemma addIb : left_injective addb. Proof. by do 3!case. Qed.
Lemma addbI : right_injective addb. Proof. by do 3!case. Qed.
Lemma addTb b : true (+) b = ~~ b. Proof. by []. Qed.
Lemma addbT b : b (+) true = ~~ b. Proof. by case: b. Qed.
Lemma addbN a b : a (+) ~~ b = ~~ (a (+) b).
Proof. by case: a; case: b. Qed.
Lemma addNb a b : ~~ a (+) b = ~~ (a (+) b).
Proof. by case: a; case: b. Qed.
Lemma addbP a b : reflect (~~ a = b) (a (+) b).
Proof. by case: a; case: b; constructor. Qed.
Implicit Arguments addbP [a b].
Ltac bool_congr :=
match goal with
| |- (?X1 && ?X2 = ?X3) ⇒ first
[ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry
| case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ]
| |- (?X1 || ?X2 = ?X3) ⇒ first
[ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry
| case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ]
| |- (?X1 (+) ?X2 = ?X3) ⇒
symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry
| |- (~~ ?X1 = ?X2) ⇒ congr 1 negb
end.
Definition pred T := T → bool.
Identity Coercion fun_of_pred : pred >-> Funclass.
Definition rel T := T → pred T.
Identity Coercion fun_of_rel : rel >-> Funclass.
Notation xpred0 := (fun _ ⇒ false).
Notation xpredT := (fun _ ⇒ true).
Notation xpredI := (fun (p1 p2 : pred _) x ⇒ p1 x && p2 x).
Notation xpredU := (fun (p1 p2 : pred _) x ⇒ p1 x || p2 x).
Notation xpredC := (fun (p : pred _) x ⇒ ~~ p x).
Notation xpredD := (fun (p1 p2 : pred _) x ⇒ ~~ p2 x && p1 x).
Notation xpreim := (fun f (p : pred _) x ⇒ p (f x)).
Notation xrelU := (fun (r1 r2 : rel _) x y ⇒ r1 x y || r2 x y).
Section Predicates.
Variables T : Type.
Definition subpred (p1 p2 : pred T) := ∀ x, p1 x → p2 x.
Definition subrel (r1 r2 : rel T) := ∀ x y, r1 x y → r2 x y.
Definition simpl_pred := simpl_fun T bool.
Definition applicative_pred := pred T.
Definition collective_pred := pred T.
Definition SimplPred (p : pred T) : simpl_pred := SimplFun p.
Coercion pred_of_simpl (p : simpl_pred) : pred T := fun_of_simpl p.
Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred :=
fun_of_simpl p.
Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred :=
fun x ⇒ (let: SimplFun f := p in fun _ ⇒ f x) x.
Definition pred0 := SimplPred xpred0.
Definition predT := SimplPred xpredT.
Definition predI p1 p2 := SimplPred (xpredI p1 p2).
Definition predU p1 p2 := SimplPred (xpredU p1 p2).
Definition predC p := SimplPred (xpredC p).
Definition predD p1 p2 := SimplPred (xpredD p1 p2).
Definition preim rT f (d : pred rT) := SimplPred (xpreim f d).
Definition simpl_rel := simpl_fun T (pred T).
Definition SimplRel (r : rel T) : simpl_rel := [fun x ⇒ r x].
Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y ⇒ r x y.
Definition relU r1 r2 := SimplRel (xrelU r1 r2).
Lemma subrelUl r1 r2 : subrel r1 (relU r1 r2).
Proof. by move⇒ *; apply/orP; left. Qed.
Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
Proof. by move⇒ *; apply/orP; right. Qed.
CoInductive mem_pred := Mem of pred T.
Definition isMem pT topred mem := mem = (fun p : pT ⇒ Mem [eta topred p]).
Structure predType := PredType {
pred_sort :> Type;
topred : pred_sort → pred T;
_ : {mem | isMem topred mem}
}.
Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ (erefl _)).
Canonical predPredType := Eval hnf in @mkPredType (pred T) id.
Canonical simplPredType := Eval hnf in mkPredType pred_of_simpl.
Canonical boolfunPredType := Eval hnf in @mkPredType (T → bool) id.
Coercion pred_of_mem mp : pred_sort predPredType := let: Mem p := mp in [eta p].
Canonical memPredType := Eval hnf in mkPredType pred_of_mem.
Definition clone_pred U :=
fun pT & pred_sort pT → U ⇒
fun a mP (pT' := @PredType U a mP) & phant_id pT' pT ⇒ pT'.
End Predicates.
Implicit Arguments pred0 [T].
Implicit Arguments predT [T].
Prenex Implicits pred0 predT predI predU predC predD preim relU.
Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T ⇒ E%B))
(at level 0, format "[ 'pred' : T | E ]") : fun_scope.
Notation "[ 'pred' x | E ]" := (SimplPred (fun x ⇒ E%B))
(at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope.
Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ]
(at level 0, x ident, format "[ 'pred' x | E1 & E2 ]") : fun_scope.
Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T ⇒ E%B))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'pred' x : T | E1 & E2 ]" := [pred x : T | E1 && E2 ]
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y ⇒ E%B))
(at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T ⇒ E%B))
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id)
(at level 0, format "[ 'predType' 'of' T ]") : form_scope.
Notation pred_class := (pred_sort (predPredType _)).
Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T.
Definition predArgType := Type.
Bind Scope type_scope with predArgType.
Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.
Notation "{ : T }" := (T%type : predArgType)
(at level 0, format "{ : T }") : type_scope.
Definition mem T (pT : predType T) : pT → mem_pred T :=
nosimpl (let: PredType _ _ (exist mem _) := pT return pT → _ in mem).
Definition in_mem T x mp := nosimpl pred_of_mem T mp x.
Prenex Implicits mem.
Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp].
Definition eq_mem T p1 p2 := ∀ x : T, in_mem x p1 = in_mem x p2.
Definition sub_mem T p1 p2 := ∀ x : T, in_mem x p1 → in_mem x p2.
Typeclasses Opaque eq_mem.
Lemma sub_refl T (p : mem_pred T) : sub_mem p p. Proof. by []. Qed.
Implicit Arguments sub_refl [[T] [p]].
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \notin A" := (~~ (x \in A)) : bool_scope.
Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B))
(at level 0, A, B at level 69,
format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope.
Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A)))
(at level 0, only parsing) : fun_scope.
Notation "[ 'rel' 'of' fA ]" := (fun x ⇒ [mem (fA x)])
(at level 0, format "[ 'rel' 'of' fA ]") : fun_scope.
Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B])
(at level 0, format "[ 'predI' A & B ]") : fun_scope.
Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B])
(at level 0, format "[ 'predU' A & B ]") : fun_scope.
Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B])
(at level 0, format "[ 'predD' A & B ]") : fun_scope.
Notation "[ 'predC' A ]" := (predC [mem A])
(at level 0, format "[ 'predC' A ]") : fun_scope.
Notation "[ 'preim' f 'of' A ]" := (preim f [mem A])
(at level 0, format "[ 'preim' f 'of' A ]") : fun_scope.
Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A]
(at level 0, x ident, format "[ 'pred' x 'in' A ]") : fun_scope.
Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E]
(at level 0, x ident, format "[ 'pred' x 'in' A | E ]") : fun_scope.
Notation "[ 'pred' x 'in' A | E1 & E2 ]" := [pred x | x \in A & E1 && E2 ]
(at level 0, x ident,
format "[ 'pred' x 'in' A | E1 & E2 ]") : 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 "[ '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 "[ '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 "[ '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 "[ 'rel' x y 'in' A ]") : fun_scope.
Section simpl_mem.
Variables (T : Type) (pT : predType T).
Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT).
Structure manifest_applicative_pred p := ManifestApplicativePred {
manifest_applicative_pred_value :> pred T;
_ : manifest_applicative_pred_value = p
}.
Definition ApplicativePred p := ManifestApplicativePred (erefl p).
Canonical applicative_pred_applicative sp :=
ApplicativePred (applicative_pred_of_simpl sp).
Structure manifest_simpl_pred p := ManifestSimplPred {
manifest_simpl_pred_value :> simpl_pred T;
_ : manifest_simpl_pred_value = SimplPred p
}.
Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
Structure manifest_mem_pred p := ManifestMemPred {
manifest_mem_pred_value :> mem_pred T;
_ : manifest_mem_pred_value= Mem [eta p]
}.
Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _).
Structure applicative_mem_pred p :=
ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp :=
@ApplicativeMemPred ap mp.
Lemma mem_topred (pp : pT) : mem (topred pp) = mem pp.
Proof. by rewrite /mem; case: pT pp ⇒ T1 app1 [mem1 /= ->]. Qed.
Lemma topredE x (pp : pT) : topred pp x = (x \in pp).
Proof. by rewrite -mem_topred. Qed.
Lemma app_predE x p (ap : manifest_applicative_pred p) : ap x = (x \in p).
Proof. by case: ap ⇒ _ /= →. Qed.
Lemma in_applicative x p (amp : applicative_mem_pred p) : in_mem x amp = p x.
Proof. by case: amp ⇒ [[_ /= ->]]. Qed.
Lemma in_collective x p (msp : manifest_simpl_pred p) :
(x \in collective_pred_of_simpl msp) = p x.
Proof. by case: msp ⇒ _ /= →. Qed.
Lemma in_simpl x p (msp : manifest_simpl_pred p) :
in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x.
Proof. by case: msp ⇒ _ /= →. Qed.
Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x.
Proof. by []. Qed.
Lemma simpl_predE p : SimplPred p =1 p.
Proof. by []. Qed.
Definition inE := (in_applicative, in_simpl, simpl_predE).
Lemma mem_simpl sp : mem sp = sp :> pred T.
Proof. by []. Qed.
Definition memE := mem_simpl.
Lemma mem_mem (pp : pT) : (mem (mem pp) = mem pp) × (mem [mem pp] = mem pp).
Proof. by rewrite -mem_topred. Qed.
End simpl_mem.
CoInductive qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
fun x ⇒ let: Qualifier p := q in p x.
Implicit Arguments has_quality [T].
Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
Notation "x \is A" := (x \in has_quality 0 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \is A ']'") : bool_scope.
Notation "x \is 'a' A" := (x \in has_quality 1 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \is 'a' A ']'") : bool_scope.
Notation "x \is 'an' A" := (x \in has_quality 2 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \is 'an' A ']'") : bool_scope.
Notation "x \isn't A" := (x \notin has_quality 0 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \isn't A ']'") : bool_scope.
Notation "x \isn't 'a' A" := (x \notin has_quality 1 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \isn't 'a' A ']'") : bool_scope.
Notation "x \isn't 'an' A" := (x \notin has_quality 2 A)
(at level 70, no associativity,
format "'[hv' x '/ ' \isn't 'an' A ']'") : bool_scope.
Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x ⇒ P%B))
(at level 0, x at level 99,
format "'[hv' [ 'qualify' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' x : T | P ]" := (Qualifier 0 (fun x : T ⇒ P%B))
(at level 0, x at level 99, only parsing) : form_scope.
Notation "[ 'qualify' 'a' x | P ]" := (Qualifier 1 (fun x ⇒ P%B))
(at level 0, x at level 99,
format "'[hv' [ 'qualify' 'a' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' 'a' x : T | P ]" := (Qualifier 1 (fun x : T ⇒ P%B))
(at level 0, x at level 99, only parsing) : form_scope.
Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x ⇒ P%B))
(at level 0, x at level 99,
format "'[hv' [ 'qualify' 'an' x | '/ ' P ] ']'") : form_scope.
Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T ⇒ P%B))
(at level 0, x at level 99, only parsing) : form_scope.
Section KeyPred.
Variable T : Type.
CoInductive pred_key (p : predPredType T) := DefaultPredKey.
Variable p : predPredType T.
Structure keyed_pred (k : pred_key p) :=
PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}.
Variable k : pred_key p.
Definition KeyedPred := @PackKeyedPred k p (frefl _).
Variable k_p : keyed_pred k.
Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed.
Canonical keyed_mem :=
@PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE.
Canonical keyed_mem_simpl :=
@PackKeyedPred k (pred_of_simpl (mem k_p)) keyed_predE.
End KeyPred.
Notation "x \i 'n' S" := (x \in @unkey_pred _ S _ _)
(at level 70, format "'[hv' x '/ ' \i 'n' S ']'") : bool_scope.
Section KeyedQualifier.
Variables (T : Type) (n : nat) (q : qualifier n T).
Structure keyed_qualifier (k : pred_key q) :=
PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
Variables (k : pred_key q) (k_q : keyed_qualifier k).
Fact keyed_qualifier_suproof : unkey_qualifier k_q =i q.
Proof. by case: k_q ⇒ /= _ →. Qed.
Canonical keyed_qualifier_keyed := PackKeyedPred k keyed_qualifier_suproof.
End KeyedQualifier.
Notation "x \i 's' A" := (x \i n has_quality 0 A)
(at level 70, format "'[hv' x '/ ' \i 's' A ']'") : bool_scope.
Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A)
(at level 70, format "'[hv' x '/ ' \i 's' 'a' A ']'") : bool_scope.
Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A)
(at level 70, format "'[hv' x '/ ' \i 's' 'an' A ']'") : bool_scope.
Module DefaultKeying.
Canonical default_keyed_pred T p := KeyedPred (@DefaultPredKey T p).
Canonical default_keyed_qualifier T n (q : qualifier n T) :=
KeyedQualifier (DefaultPredKey q).
End DefaultKeying.
Lemma all_tag_cond_dep I T (C : pred I) U :
(∀ x, T x) → (∀ x, C x → {y : T x & U x y}) →
{f : ∀ x, T x & ∀ x, C x → U x (f x)}.
Proof.
move⇒ f0 fP; apply: all_tag (fun x y ⇒ C x → U x y) _ ⇒ x.
by case Cx: (C x); [case/fP: Cx ⇒ y; ∃ y | ∃ (f0 x)].
Qed.
Lemma all_tag_cond I T (C : pred I) U :
T → (∀ x, C x → {y : T & U x y}) →
{f : I → T & ∀ x, C x → U x (f x)}.
Proof. by move⇒ y0; apply: all_tag_cond_dep. Qed.
Lemma all_sig_cond_dep I T (C : pred I) P :
(∀ x, T x) → (∀ x, C x → {y : T x | P x y}) →
{f : ∀ x, T x | ∀ x, C x → P x (f x)}.
Proof. by move⇒ f0 /(all_tag_cond_dep f0)[f]; ∃ f. Qed.
Lemma all_sig_cond I T (C : pred I) P :
T → (∀ x, C x → {y : T | P x y}) →
{f : I → T | ∀ x, C x → P x (f x)}.
Proof. by move⇒ y0; apply: all_sig_cond_dep. Qed.
Section RelationProperties.
Variable T : Type.
Variable R : rel T.
Definition total := ∀ x y, R x y || R y x.
Definition transitive := ∀ y x z, R x y → R y z → R x z.
Definition symmetric := ∀ x y, R x y = R y x.
Definition antisymmetric := ∀ x y, R x y && R y x → x = y.
Definition pre_symmetric := ∀ x y, R x y → R y x.
Lemma symmetric_from_pre : pre_symmetric → symmetric.
Proof. move⇒ symR x y; apply/idP/idP; exact: symR. Qed.
Definition reflexive := ∀ x, R x x.
Definition irreflexive := ∀ x, R x x = false.
Definition left_transitive := ∀ x y, R x y → R x =1 R y.
Definition right_transitive := ∀ x y, R x y → R^~ x =1 R^~ y.
Section PER.
Hypotheses (symR : symmetric) (trR : transitive).
Lemma sym_left_transitive : left_transitive.
Proof. by move⇒ x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR. Qed.
Lemma sym_right_transitive : right_transitive.
Proof. by move⇒ x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed.
End PER.
Definition equivalence_rel := ∀ x y z, R z z × (R x y → R x z = R y z).
Lemma equivalence_relP : equivalence_rel ↔ reflexive ∧ left_transitive.
Proof.
split⇒ [eqiR | [Rxx trR] x y z]; last by split⇒ [|/trR->].
by split⇒ [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)].
Qed.
End RelationProperties.
Lemma rev_trans T (R : rel T) : transitive R → transitive (fun x y ⇒ R y x).
Proof. by move⇒ trR x y z Ryx Rzy; exact: trR Rzy Ryx. Qed.
Notation Local "{ 'all1' P }" := (∀ x, P x : Prop) (at level 0).
Notation Local "{ 'all2' P }" := (∀ x y, P x y : Prop) (at level 0).
Notation Local "{ 'all3' P }" := (∀ x y z, P x y z: Prop) (at level 0).
Notation Local ph := (phantom _).
Section LocalProperties.
Variables T1 T2 T3 : Type.
Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
Notation Local ph := (phantom Prop).
Definition prop_for (x : T1) P & ph {all1 P} := P x.
Lemma forE x P phP : @prop_for x P phP = P x. Proof. by []. Qed.
Definition prop_in1 P & ph {all1 P} :=
∀ x, in_mem x d1 → P x.
Definition prop_in11 P & ph {all2 P} :=
∀ x y, in_mem x d1 → in_mem y d2 → P x y.
Definition prop_in2 P & ph {all2 P} :=
∀ x y, in_mem x d1 → in_mem y d1 → P x y.
Definition prop_in111 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d2 → in_mem z d3 → P x y z.
Definition prop_in12 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d2 → in_mem z d2 → P x y z.
Definition prop_in21 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d1 → in_mem z d2 → P x y z.
Definition prop_in3 P & ph {all3 P} :=
∀ x y z, in_mem x d1 → in_mem y d1 → in_mem z d1 → P x y z.
Variable f : T1 → T2.
Definition prop_on1 Pf P & phantom T3 (Pf f) & ph {all1 P} :=
∀ x, in_mem (f x) d2 → P x.
Definition prop_on2 Pf P & phantom T3 (Pf f) & ph {all2 P} :=
∀ x y, in_mem (f x) d2 → in_mem (f y) d2 → P x y.
End LocalProperties.
Definition inPhantom := Phantom Prop.
Definition onPhantom T P (x : T) := Phantom Prop (P x).
Definition bijective_in aT rT (d : mem_pred aT) (f : aT → rT) :=
exists2 g, prop_in1 d (inPhantom (cancel f g))
& prop_on1 d (Phantom _ (cancel g)) (onPhantom (cancel g) f).
Definition bijective_on aT rT (cd : mem_pred rT) (f : aT → rT) :=
exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g)
& prop_in1 cd (inPhantom (cancel g f)).
Notation "{ 'for' x , P }" :=
(prop_for x (inPhantom P))
(at level 0, format "{ 'for' x , P }") : type_scope.
Notation "{ 'in' d , P }" :=
(prop_in1 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d , P }") : type_scope.
Notation "{ 'in' d1 & d2 , P }" :=
(prop_in11 (mem d1) (mem d2) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 , P }") : type_scope.
Notation "{ 'in' d & , P }" :=
(prop_in2 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d & , P }") : type_scope.
Notation "{ 'in' d1 & d2 & d3 , P }" :=
(prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope.
Notation "{ 'in' d1 & & d3 , P }" :=
(prop_in21 (mem d1) (mem d3) (inPhantom P))
(at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope.
Notation "{ 'in' d1 & d2 & , P }" :=
(prop_in12 (mem d1) (mem d2) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope.
Notation "{ 'in' d & & , P }" :=
(prop_in3 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d & & , P }") : type_scope.
Notation "{ 'on' cd , P }" :=
(prop_on1 (mem cd) (inPhantom P) (inPhantom P))
(at level 0, format "{ 'on' cd , P }") : type_scope.
Notation "{ 'on' cd & , P }" :=
(prop_on2 (mem cd) (inPhantom P) (inPhantom P))
(at level 0, format "{ 'on' cd & , P }") : type_scope.
Notation "{ 'on' cd , P & g }" :=
(prop_on1 (mem cd) (Phantom (_ → Prop) P) (onPhantom P g))
(at level 0, format "{ 'on' cd , P & g }") : type_scope.
Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f)
(at level 0, f at level 8,
format "{ 'in' d , 'bijective' f }") : type_scope.
Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f)
(at level 0, f at level 8,
format "{ 'on' cd , 'bijective' f }") : type_scope.
Section LocalGlobal.
Variables T1 T2 T3 : predArgType.
Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3).
Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3).
Variables (f f' : T1 → T2) (g : T2 → T1) (h : T3).
Variables (P1 : T1 → Prop) (P2 : T1 → T2 → Prop).
Variable P3 : T1 → T2 → T3 → Prop.
Variable Q1 : (T1 → T2) → T1 → Prop.
Variable Q1l : (T1 → T2) → T3 → T1 → Prop.
Variable Q2 : (T1 → T2) → T1 → T1 → Prop.
Hypothesis sub1 : sub_mem d1 d1'.
Hypothesis sub2 : sub_mem d2 d2'.
Hypothesis sub3 : sub_mem d3 d3'.
Lemma in1W : {all1 P1} → {in D1, {all1 P1}}.
Proof. by move⇒ ? ?. Qed.
Lemma in2W : {all2 P2} → {in D1 & D2, {all2 P2}}.
Proof. by move⇒ ? ?. Qed.
Lemma in3W : {all3 P3} → {in D1 & D2 & D3, {all3 P3}}.
Proof. by move⇒ ? ?. Qed.
Lemma in1T : {in T1, {all1 P1}} → {all1 P1}.
Proof. by move⇒ ? ?; auto. Qed.
Lemma in2T : {in T1 & T2, {all2 P2}} → {all2 P2}.
Proof. by move⇒ ? ?; auto. Qed.
Lemma in3T : {in T1 & T2 & T3, {all3 P3}} → {all3 P3}.
Proof. by move⇒ ? ?; auto. Qed.
Lemma sub_in1 (Ph : ph {all1 P1}) : prop_in1 d1' Ph → prop_in1 d1 Ph.
Proof. move⇒ allP x /sub1; exact: allP. Qed.
Lemma sub_in11 (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph → prop_in11 d1 d2 Ph.
Proof. move⇒ allP x1 x2 /sub1 d1x1 /sub2; exact: allP. Qed.
Lemma sub_in111 (Ph : ph {all3 P3}) :
prop_in111 d1' d2' d3' Ph → prop_in111 d1 d2 d3 Ph.
Proof. by move⇒ allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP. Qed.
Let allQ1 f'' := {all1 Q1 f''}.
Let allQ1l f'' h' := {all1 Q1l f'' h'}.
Let allQ2 f'' := {all2 Q2 f''}.
Lemma on1W : allQ1 f → {on D2, allQ1 f}. Proof. by move⇒ ? ?. Qed.
Lemma on1lW : allQ1l f h → {on D2, allQ1l f & h}. Proof. by move⇒ ? ?. Qed.
Lemma on2W : allQ2 f → {on D2 &, allQ2 f}. Proof. by move⇒ ? ?. Qed.
Lemma on1T : {on T2, allQ1 f} → allQ1 f. Proof. by move⇒ ? ?; auto. Qed.
Lemma on1lT : {on T2, allQ1l f & h} → allQ1l f h.
Proof. by move⇒ ? ?; auto. Qed.
Lemma on2T : {on T2 &, allQ2 f} → allQ2 f.
Proof. by move⇒ ? ?; auto. Qed.
Lemma subon1 (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) :
prop_on1 d2' Phf Ph → prop_on1 d2 Phf Ph.
Proof. by move⇒ allQ x /sub2; exact: allQ. Qed.
Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) :
prop_on1 d2' Phf Ph → prop_on1 d2 Phf Ph.
Proof. by move⇒ allQ x /sub2; exact: allQ. Qed.
Lemma subon2 (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) :
prop_on2 d2' Phf Ph → prop_on2 d2 Phf Ph.
Proof. by move⇒ allQ x y /sub2⇒ d2fx /sub2; exact: allQ. Qed.
Lemma can_in_inj : {in D1, cancel f g} → {in D1 &, injective f}.
Proof. by move⇒ fK x y /fK{2}<- /fK{2}<- →. Qed.
Lemma canLR_in x y : {in D1, cancel f g} → y \in D1 → x = f y → g x = y.
Proof. by move⇒ fK D1y ->; rewrite fK. Qed.
Lemma canRL_in x y : {in D1, cancel f g} → x \in D1 → f x = y → x = g y.
Proof. by move⇒ fK D1x <-; rewrite fK. Qed.
Lemma on_can_inj : {on D2, cancel f & g} → {on D2 &, injective f}.
Proof. by move⇒ fK x y /fK{2}<- /fK{2}<- →. Qed.
Lemma canLR_on x y : {on D2, cancel f & g} → f y \in D2 → x = f y → g x = y.
Proof. by move⇒ fK D2fy ->; rewrite fK. Qed.
Lemma canRL_on x y : {on D2, cancel f & g} → f x \in D2 → f x = y → x = g y.
Proof. by move⇒ fK D2fx <-; rewrite fK. Qed.
Lemma inW_bij : bijective f → {in D1, bijective f}.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma onW_bij : bijective f → {on D2, bijective f}.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma inT_bij : {in T1, bijective f} → bijective f.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma onT_bij : {on T2, bijective f} → bijective f.
Proof. by case⇒ g' fK g'K; ∃ g' ⇒ × ? *; auto. Qed.
Lemma sub_in_bij (D1' : pred T1) :
{subset D1 ≤ D1'} → {in D1', bijective f} → {in D1, bijective f}.
Proof.
by move⇒ subD [g' fK g'K]; ∃ g' ⇒ x; move/subD; [exact: fK | exact: g'K].
Qed.
Lemma subon_bij (D2' : pred T2) :
{subset D2 ≤ D2'} → {on D2', bijective f} → {on D2, bijective f}.
Proof.
by move⇒ subD [g' fK g'K]; ∃ g' ⇒ x; move/subD; [exact: fK | exact: g'K].
Qed.
End LocalGlobal.
Lemma sub_in2 T d d' (P : T → T → Prop) :
sub_mem d d' → ∀ Ph : ph {all2 P}, prop_in2 d' Ph → prop_in2 d Ph.
Proof. by move⇒ /= sub_dd'; exact: sub_in11. Qed.
Lemma sub_in3 T d d' (P : T → T → T → Prop) :
sub_mem d d' → ∀ Ph : ph {all3 P}, prop_in3 d' Ph → prop_in3 d Ph.
Proof. by move⇒ /= sub_dd'; exact: sub_in111. Qed.
Lemma sub_in12 T1 T d1 d1' d d' (P : T1 → T → T → Prop) :
sub_mem d1 d1' → sub_mem d d' →
∀ Ph : ph {all3 P}, prop_in12 d1' d' Ph → prop_in12 d1 d Ph.
Proof. by move⇒ /= sub1 sub; exact: sub_in111. Qed.
Lemma sub_in21 T T3 d d' d3 d3' (P : T → T → T3 → Prop) :
sub_mem d d' → sub_mem d3 d3' →
∀ Ph : ph {all3 P}, prop_in21 d' d3' Ph → prop_in21 d d3 Ph.
Proof. by move⇒ /= sub sub3; exact: sub_in111. Qed.
Lemma equivalence_relP_in T (R : rel T) (A : pred T) :
{in A & &, equivalence_rel R}
↔ {in A, reflexive R} ∧ {in A &, ∀ x y, R x y → {in A, R x =1 R y}}.
Proof.
split⇒ [eqiR | [Rxx trR] x y z *]; last by split⇒ [|/trR→ //]; exact: Rxx.
by split⇒ [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)].
Qed.
Section MonoHomoMorphismTheory.
Variables (aT rT sT : Type) (f : aT → rT) (g : rT → aT).
Variables (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).
Lemma monoW : {mono f : x / aP x >-> rP x} → {homo f : x / aP x >-> rP x}.
Proof. by move⇒ hf x ax; rewrite hf. Qed.
Lemma mono2W :
{mono f : x y / aR x y >-> rR x y} → {homo f : x y / aR x y >-> rR x y}.
Proof. by move⇒ hf x y axy; rewrite hf. Qed.
Hypothesis fgK : cancel g f.
Lemma homoRL :
{homo f : x y / aR x y >-> rR x y} → ∀ x y, aR (g x) y → rR x (f y).
Proof. by move⇒ Hf x y /Hf; rewrite fgK. Qed.
Lemma homoLR :
{homo f : x y / aR x y >-> rR x y} → ∀ x y, aR x (g y) → rR (f x) y.
Proof. by move⇒ Hf x y /Hf; rewrite fgK. Qed.
Lemma homo_mono :
{homo f : x y / aR x y >-> rR x y} → {homo g : x y / rR x y >-> aR x y} →
{mono g : x y / rR x y >-> aR x y}.
Proof.
move⇒ mf mg x y; case: (boolP (rR _ _))=> [/mg //|].
by apply: contraNF⇒ /mf; rewrite !fgK.
Qed.
Lemma monoLR :
{mono f : x y / aR x y >-> rR x y} → ∀ x y, rR (f x) y = aR x (g y).
Proof. by move⇒ mf x y; rewrite -{1}[y]fgK mf. Qed.
Lemma monoRL :
{mono f : x y / aR x y >-> rR x y} → ∀ x y, rR x (f y) = aR (g x) y.
Proof. by move⇒ mf x y; rewrite -{1}[x]fgK mf. Qed.
Lemma can_mono :
{mono f : x y / aR x y >-> rR x y} → {mono g : x y / rR x y >-> aR x y}.
Proof. by move⇒ mf x y /=; rewrite -mf !fgK. Qed.
End MonoHomoMorphismTheory.
Section MonoHomoMorphismTheory_in.
Variables (aT rT sT : predArgType) (f : aT → rT) (g : rT → aT).
Variable (aD : pred aT).
Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT).
Notation rD := [pred x | g x \in aD].
Lemma monoW_in :
{in aD &, {mono f : x y / aR x y >-> rR x y}} →
{in aD &, {homo f : x y / aR x y >-> rR x y}}.
Proof. by move⇒ hf x y hx hy axy; rewrite hf. Qed.
Lemma mono2W_in :
{in aD, {mono f : x / aP x >-> rP x}} →
{in aD, {homo f : x / aP x >-> rP x}}.
Proof. by move⇒ hf x hx ax; rewrite hf. Qed.
Hypothesis fgK_on : {on aD, cancel g & f}.
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)}.
Proof. by move⇒ Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed.
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}.
Proof. by move⇒ Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed.
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}}.
Proof.
move⇒ mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact.
by apply: contraNF⇒ /mf; rewrite !fgK_on //; apply.
Qed.
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)}.
Proof. by move⇒ mf x y hx hy; rewrite -{1}[y]fgK_on // mf. Qed.
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}.
Proof. by move⇒ mf x y hx hy; rewrite -{1}[x]fgK_on // mf. Qed.
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}}.
Proof. by move⇒ mf x y hx hy /=; rewrite -mf // !fgK_on. Qed.
End MonoHomoMorphismTheory_in.