Library Ssreflect.ssrfun
Require Import ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Delimit Scope fun_scope with FUN.
Open Scope fun_scope.
Notation "f ^~ y" := (fun x ⇒ f x y)
(at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope.
Notation "@^~ x" := (fun f ⇒ f x)
(at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope.
Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.
Notation "p .1" := (fst p)
(at level 2, left associativity, format "p .1") : pair_scope.
Notation "p .2" := (snd p)
(at level 2, left associativity, format "p .2") : pair_scope.
Coercion pair_of_and P Q (PandQ : P ∧ Q) := (proj1 PandQ, proj2 PandQ).
Definition all_pair I T U (w : ∀ i : I, T i × U i) :=
(fun i ⇒ (w i).1, fun i ⇒ (w i).2).
Reserved Notation "e .[ x ]"
(at level 2, left associativity, format "e .[ x ]").
Reserved Notation "e .[ x1 , x2 , .. , xn ]" (at level 2, left associativity,
format "e '[ ' .[ x1 , '/' x2 , '/' .. , '/' xn ] ']'").
Reserved Notation "s `_ i" (at level 3, i at level 2, left associativity,
format "s `_ i").
Reserved Notation "x ^-1" (at level 3, left associativity, format "x ^-1").
Reserved Notation "x *+ n" (at level 40, left associativity).
Reserved Notation "x *- n" (at level 40, left associativity).
Reserved Notation "x ^+ n" (at level 29, left associativity).
Reserved Notation "x ^- n" (at level 29, left associativity).
Reserved Notation "x *: A" (at level 40).
Reserved Notation "A :* x" (at level 40).
Reserved Notation "A :&: B" (at level 48, left associativity).
Reserved Notation "A :|: B" (at level 52, left associativity).
Reserved Notation "a |: A" (at level 52, left associativity).
Reserved Notation "A :\: B" (at level 50, left associativity).
Reserved Notation "A :\ b" (at level 50, left associativity).
Reserved Notation "<< A >>" (at level 0, format "<< A >>").
Reserved Notation "<[ a ] >" (at level 0, format "<[ a ] >").
Reserved Notation "''C' [ x ]" (at level 8, format "''C' [ x ]").
Reserved Notation "''C_' A [ x ]"
(at level 8, A at level 2, format "''C_' A [ x ]").
Reserved Notation "''C' ( A )" (at level 8, format "''C' ( A )").
Reserved Notation "''C_' B ( A )"
(at level 8, B at level 2, format "''C_' B ( A )").
Reserved Notation "''Z' ( A )" (at level 8, format "''Z' ( A )").
Reserved Notation "''C_' ( A ) [ x ]" (at level 8, only parsing).
Reserved Notation "''C_' ( B ) ( A )" (at level 8, only parsing).
Reserved Notation "m %/ d" (at level 40, no associativity).
Reserved Notation "m %% d" (at level 40, no associativity).
Reserved Notation "m %| d" (at level 70, no associativity).
Reserved Notation "m = n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' = n '/' %[mod d ] ']'").
Reserved Notation "m == n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' == n '/' %[mod d ] ']'").
Reserved Notation "m <> n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' <> n '/' %[mod d ] ']'").
Reserved Notation "m != n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' != n '/' %[mod d ] ']'").
Reserved Notation "a ^` ()" (at level 8, format "a ^` ()").
Reserved Notation "a ^` ( n )" (at level 8, format "a ^` ( n )").
Reserved Notation "`| x |" (at level 0, x at level 99, format "`| x |").
Reserved Notation "x <= y ?= 'iff' c" (at level 70, y, c at next level,
format "x '[hv' <= y '/' ?= 'iff' c ']'").
Reserved Notation "x <= y :> T" (at level 70, y at next level).
Reserved Notation "x >= y :> T" (at level 70, y at next level, only parsing).
Reserved Notation "x < y :> T" (at level 70, y at next level).
Reserved Notation "x > y :> T" (at level 70, y at next level, only parsing).
Reserved Notation "x <= y ?= 'iff' c :> T" (at level 70, y, c at next level,
format "x '[hv' <= y '/' ?= 'iff' c :> T ']'").
Module Option.
Definition apply aT rT (f : aT → rT) x u := if u is Some y then f y else x.
Definition default T := apply (fun x : T ⇒ x).
Definition bind aT rT (f : aT → option rT) := apply f None.
Definition map aT rT (f : aT → rT) := bind (fun x ⇒ Some (f x)).
End Option.
Notation oapp := Option.apply.
Notation odflt := Option.default.
Notation obind := Option.bind.
Notation omap := Option.map.
Notation some := (@Some _) (only parsing).
Notation erefl := refl_equal.
Notation ecast i T e x := (let: erefl in _ = i := e return T in x).
Definition esym := sym_eq.
Definition nesym := sym_not_eq.
Definition etrans := trans_eq.
Definition congr1 := f_equal.
Definition congr2 := f_equal2.
Prenex Implicits esym nesym.
Definition all_equal_to T (x0 : T) := ∀ x, unkeyed x = x0.
Lemma unitE : all_equal_to tt. Proof. by case. Qed.
Structure wrapped T := Wrap {unwrap : T}.
Canonical wrap T x := @Wrap T x.
Prenex Implicits unwrap wrap Wrap.
Reserved Notation "[ 'rec' a0 ]"
(at level 0, format "[ 'rec' a0 ]").
Reserved Notation "[ 'rec' a0 , a1 ]"
(at level 0, format "[ 'rec' a0 , a1 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"
(at level 0,
format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"
(at level 0,
format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
(at level 0,
format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]").
Section SimplFun.
Variables aT rT : Type.
CoInductive simpl_fun := SimplFun of aT → rT.
Definition fun_of_simpl f := fun x ⇒ let: SimplFun lam := f in lam x.
Coercion fun_of_simpl : simpl_fun >-> Funclass.
End SimplFun.
Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T ⇒ E))
(at level 0,
format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x => E ]" := (SimplFun (fun x ⇒ E))
(at level 0, x ident,
format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T ⇒ E))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'fun' x y => E ]" := (fun x ⇒ [fun y ⇒ E])
(at level 0, x ident, y ident,
format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x y : T => E ]" := (fun x : T ⇒ [fun y : T ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T ⇒ [fun y ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' x ( y : T ) => E ]" := (fun x ⇒ [fun y : T ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
(fun x : xT ⇒ [fun y : yT ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Definition SimplFunDelta aT rT (f : aT → aT → rT) := [fun z ⇒ f z z].
Section ExtensionalEquality.
Variables A B C : Type.
Definition eqfun (f g : B → A) : Prop := ∀ x, f x = g x.
Definition eqrel (r s : C → B → A) : Prop := ∀ x y, r x y = s x y.
Lemma frefl f : eqfun f f. Proof. by []. Qed.
Lemma fsym f g : eqfun f g → eqfun g f. Proof. by move⇒ eq_fg x. Qed.
Lemma ftrans f g h : eqfun f g → eqfun g h → eqfun f h.
Proof. by move⇒ eq_fg eq_gh x; rewrite eq_fg. Qed.
Lemma rrefl r : eqrel r r. Proof. by []. Qed.
End ExtensionalEquality.
Typeclasses Opaque eqfun.
Typeclasses Opaque eqrel.
Hint Resolve frefl rrefl.
Notation "f1 =1 f2" := (eqfun f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A))
(at level 70, f2 at next level, A at level 90) : fun_scope.
Notation "f1 =2 f2" := (eqrel f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A))
(at level 70, f2 at next level, A, B at level 90) : fun_scope.
Section Composition.
Variables A B C : Type.
Definition funcomp u (f : B → A) (g : C → B) x := let: tt := u in f (g x).
Definition catcomp u g f := funcomp u f g.
Local Notation comp := (funcomp tt).
Definition pcomp (f : B → option A) (g : C → option B) x := obind f (g x).
Lemma eq_comp f f' g g' : f =1 f' → g =1 g' → comp f g =1 comp f' g'.
Proof. by move⇒ eq_ff' eq_gg' x; rewrite /= eq_gg' eq_ff'. Qed.
End Composition.
Notation comp := (funcomp tt).
Notation "@ 'comp'" := (fun A B C ⇒ @funcomp A B C tt).
Notation "f1 \o f2" := (comp f1 f2)
(at level 50, format "f1 \o '/ ' f2") : fun_scope.
Notation "f1 \; f2" := (catcomp tt f1 f2)
(at level 60, right associativity, format "f1 \; '/ ' f2") : fun_scope.
Notation "[ 'eta' f ]" := (fun x ⇒ f x)
(at level 0, format "[ 'eta' f ]") : fun_scope.
Notation "'fun' => E" := (fun _ ⇒ E) (at level 200, only parsing) : fun_scope.
Notation id := (fun x ⇒ x).
Notation "@ 'id' T" := (fun x : T ⇒ x)
(at level 10, T at level 8, only parsing) : fun_scope.
Definition id_head T u x : T := let: tt := u in x.
Definition explicit_id_key := tt.
Notation idfun := (id_head tt).
Notation "@ 'idfun' T " := (@id_head T explicit_id_key)
(at level 10, T at level 8, format "@ 'idfun' T") : fun_scope.
Definition phant_id T1 T2 v1 v2 := phantom T1 v1 → phantom T2 v2.
Section Tag.
Variables (I : Type) (i : I) (T_ U_ : I → Type).
Definition tag := projS1.
Definition tagged : ∀ w, T_(tag w) := @projS2 I [eta T_].
Definition Tagged x := @existS I [eta T_] i x.
Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 i _ _ := w in i.
Definition tagged2 w : T_(tag2 w) := let: existT2 _ x _ := w in x.
Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ y := w in y.
Definition Tagged2 x y := @existS2 I [eta T_] [eta U_] i x y.
End Tag.
Implicit Arguments Tagged [I i].
Implicit Arguments Tagged2 [I i].
Prenex Implicits tag tagged Tagged tag2 tagged2 tagged2' Tagged2.
Coercion tag_of_tag2 I T_ U_ (w : @sigT2 I T_ U_) :=
Tagged (fun i ⇒ T_ i × U_ i)%type (tagged2 w, tagged2' w).
Lemma all_tag I T U :
(∀ x : I, {y : T x & U x y}) →
{f : ∀ x, T x & ∀ x, U x (f x)}.
Proof. by move⇒ fP; ∃ (fun x ⇒ tag (fP x)) ⇒ x; case: (fP x). Qed.
Lemma all_tag2 I T U V :
(∀ i : I, {y : T i & U i y & V i y}) →
{f : ∀ i, T i & ∀ i, U i (f i) & ∀ i, V i (f i)}.
Proof. by case/all_tag⇒ f /all_pair[]; ∃ f. Qed.
Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").
Section Sig.
Variables (T : Type) (P Q : T → Prop).
Lemma svalP (u : sig P) : P (sval u). Proof. by case: u. Qed.
Definition s2val (u : sig2 P Q) := let: exist2 x _ _ := u in x.
Lemma s2valP u : P (s2val u). Proof. by case: u. Qed.
Lemma s2valP' u : Q (s2val u). Proof. by case: u. Qed.
End Sig.
Prenex Implicits svalP s2val s2valP s2valP'.
Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u).
Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) :=
exist (fun i ⇒ P i ∧ Q i) (s2val u) (conj (s2valP u) (s2valP' u)).
Lemma all_sig I T P :
(∀ x : I, {y : T x | P x y}) →
{f : ∀ x, T x | ∀ x, P x (f x)}.
Proof. by case/all_tag⇒ f; ∃ f. Qed.
Lemma all_sig2 I T P Q :
(∀ x : I, {y : T x | P x y & Q x y}) →
{f : ∀ x, T x | ∀ x, P x (f x) & ∀ x, Q x (f x)}.
Proof. by case/all_sig⇒ f /all_pair[]; ∃ f. Qed.
Section Morphism.
Variables (aT rT sT : Type) (f : aT → rT).
Definition morphism_1 aF rF := ∀ x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := ∀ x y, f (aOp x y) = rOp (f x) (f y).
Definition homomorphism_1 (aP rP : _ → Prop) := ∀ x, aP x → rP (f x).
Definition homomorphism_2 (aR rR : _ → _ → Prop) :=
∀ x y, aR x y → rR (f x) (f y).
Definition monomorphism_1 (aP rP : _ → sT) := ∀ x, rP (f x) = aP x.
Definition monomorphism_2 (aR rR : _ → _ → sT) :=
∀ x y, rR (f x) (f y) = aR x y.
End Morphism.
Notation "{ 'morph' f : x / a >-> r }" :=
(morphism_1 f (fun x ⇒ a) (fun x ⇒ r))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a >-> r }") : type_scope.
Notation "{ 'morph' f : x / a }" :=
(morphism_1 f (fun x ⇒ a) (fun x ⇒ a))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a }") : type_scope.
Notation "{ 'morph' f : x y / a >-> r }" :=
(morphism_2 f (fun x y ⇒ a) (fun x y ⇒ r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a >-> r }") : type_scope.
Notation "{ 'morph' f : x y / a }" :=
(morphism_2 f (fun x y ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a }") : type_scope.
Notation "{ 'homo' f : x / a >-> r }" :=
(homomorphism_1 f (fun x ⇒ a) (fun x ⇒ r))
(at level 0, f at level 99, x ident,
format "{ 'homo' f : x / a >-> r }") : type_scope.
Notation "{ 'homo' f : x / a }" :=
(homomorphism_1 f (fun x ⇒ a) (fun x ⇒ a))
(at level 0, f at level 99, x ident,
format "{ 'homo' f : x / a }") : type_scope.
Notation "{ 'homo' f : x y / a >-> r }" :=
(homomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'homo' f : x y / a >-> r }") : type_scope.
Notation "{ 'homo' f : x y / a }" :=
(homomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'homo' f : x y / a }") : type_scope.
Notation "{ 'homo' f : x y /~ a }" :=
(homomorphism_2 f (fun y x ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'homo' f : x y /~ a }") : type_scope.
Notation "{ 'mono' f : x / a >-> r }" :=
(monomorphism_1 f (fun x ⇒ a) (fun x ⇒ r))
(at level 0, f at level 99, x ident,
format "{ 'mono' f : x / a >-> r }") : type_scope.
Notation "{ 'mono' f : x / a }" :=
(monomorphism_1 f (fun x ⇒ a) (fun x ⇒ a))
(at level 0, f at level 99, x ident,
format "{ 'mono' f : x / a }") : type_scope.
Notation "{ 'mono' f : x y / a >-> r }" :=
(monomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'mono' f : x y / a >-> r }") : type_scope.
Notation "{ 'mono' f : x y / a }" :=
(monomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'mono' f : x y / a }") : type_scope.
Notation "{ 'mono' f : x y /~ a }" :=
(monomorphism_2 f (fun y x ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'mono' f : x y /~ a }") : type_scope.
Section Injections.
Variables (rT aT : Type) (f : aT → rT).
Definition injective := ∀ x1 x2, f x1 = f x2 → x1 = x2.
Definition cancel g := ∀ x, g (f x) = x.
Definition pcancel g := ∀ x, g (f x) = Some x.
Definition ocancel (g : aT → option rT) h := ∀ x, oapp h x (g x) = x.
Lemma can_pcan g : cancel g → pcancel (fun y ⇒ Some (g y)).
Proof. by move⇒ fK x; congr (Some _). Qed.
Lemma pcan_inj g : pcancel g → injective.
Proof. by move⇒ fK x y /(congr1 g); rewrite !fK ⇒ [[]]. Qed.
Lemma can_inj g : cancel g → injective.
Proof. by move/can_pcan; exact: pcan_inj. Qed.
Lemma canLR g x y : cancel g → x = f y → g x = y.
Proof. by move⇒ fK →. Qed.
Lemma canRL g x y : cancel g → f x = y → x = g y.
Proof. by move⇒ fK <-. Qed.
End Injections.
Lemma Some_inj {T} : injective (@Some T). Proof. by move⇒ x y []. Qed.
Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
Proof. by case: y /. Qed.
Lemma etrans_id T x y (eqxy : x = y :> T) : etrans (erefl x) eqxy = eqxy.
Proof. by case: y / eqxy. Qed.
Section InjectionsTheory.
Variables (A B C : Type) (f g : B → A) (h : C → B).
Lemma inj_id : injective (@id A).
Proof. by []. Qed.
Lemma inj_can_sym f' : cancel f f' → injective f' → cancel f' f.
Proof. move⇒ fK injf' x; exact: injf'. Qed.
Lemma inj_comp : injective f → injective h → injective (f \o h).
Proof. move⇒ injf injh x y /injf; exact: injh. Qed.
Lemma can_comp f' h' : cancel f f' → cancel h h' → cancel (f \o h) (h' \o f').
Proof. by move⇒ fK hK x; rewrite /= fK hK. Qed.
Lemma pcan_pcomp f' h' :
pcancel f f' → pcancel h h' → pcancel (f \o h) (pcomp h' f').
Proof. by move⇒ fK hK x; rewrite /pcomp fK /= hK. Qed.
Lemma eq_inj : injective f → f =1 g → injective g.
Proof. by move⇒ injf eqfg x y; rewrite -2!eqfg; exact: injf. Qed.
Lemma eq_can f' g' : cancel f f' → f =1 g → f' =1 g' → cancel g g'.
Proof. by move⇒ fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed.
Lemma inj_can_eq f' : cancel f f' → injective f' → cancel g f' → f =1 g.
Proof. by move⇒ fK injf' gK x; apply: injf'; rewrite fK. Qed.
End InjectionsTheory.
Section Bijections.
Variables (A B : Type) (f : B → A).
CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f.
Hypothesis bijf : bijective.
Lemma bij_inj : injective f.
Proof. by case: bijf ⇒ g fK _; apply: can_inj fK. Qed.
Lemma bij_can_sym f' : cancel f' f ↔ cancel f f'.
Proof.
split⇒ fK; first exact: inj_can_sym fK bij_inj.
by case: bijf ⇒ h _ hK x; rewrite -[x]hK fK.
Qed.
Lemma bij_can_eq f' f'' : cancel f f' → cancel f f'' → f' =1 f''.
Proof.
by move⇒ fK fK'; apply: (inj_can_eq _ bij_inj); apply/bij_can_sym.
Qed.
End Bijections.
Section BijectionsTheory.
Variables (A B C : Type) (f : B → A) (h : C → B).
Lemma eq_bij : bijective f → ∀ g, f =1 g → bijective g.
Proof. by case⇒ f' fK f'K g eqfg; ∃ f'; eapply eq_can; eauto. Qed.
Lemma bij_comp : bijective f → bijective h → bijective (f \o h).
Proof.
by move⇒ [f' fK f'K] [h' hK h'K]; ∃ (h' \o f'); apply: can_comp; auto.
Qed.
Lemma bij_can_bij : bijective f → ∀ f', cancel f f' → bijective f'.
Proof. by move⇒ bijf; ∃ f; first by apply/(bij_can_sym bijf). Qed.
End BijectionsTheory.
Section Involutions.
Variables (A : Type) (f : A → A).
Definition involutive := cancel f f.
Hypothesis Hf : involutive.
Lemma inv_inj : injective f. Proof. exact: can_inj Hf. Qed.
Lemma inv_bij : bijective f. Proof. by ∃ f. Qed.
End Involutions.
Section OperationProperties.
Variables S T R : Type.
Section SopTisR.
Implicit Type op : S → T → R.
Definition left_inverse e inv op := ∀ x, op (inv x) x = e.
Definition right_inverse e inv op := ∀ x, op x (inv x) = e.
Definition left_injective op := ∀ x, injective (op^~ x).
Definition right_injective op := ∀ y, injective (op y).
End SopTisR.
Section SopTisS.
Implicit Type op : S → T → S.
Definition right_id e op := ∀ x, op x e = x.
Definition left_zero z op := ∀ x, op z x = z.
Definition right_commutative op := ∀ x y z, op (op x y) z = op (op x z) y.
Definition left_distributive op add :=
∀ x y z, op (add x y) z = add (op x z) (op y z).
Definition right_loop inv op := ∀ y, cancel (op^~ y) (op^~ (inv y)).
Definition rev_right_loop inv op := ∀ y, cancel (op^~ (inv y)) (op^~ y).
End SopTisS.
Section SopTisT.
Implicit Type op : S → T → T.
Definition left_id e op := ∀ x, op e x = x.
Definition right_zero z op := ∀ x, op x z = z.
Definition left_commutative op := ∀ x y z, op x (op y z) = op y (op x z).
Definition right_distributive op add :=
∀ x y z, op x (add y z) = add (op x y) (op x z).
Definition left_loop inv op := ∀ x, cancel (op x) (op (inv x)).
Definition rev_left_loop inv op := ∀ x, cancel (op (inv x)) (op x).
End SopTisT.
Section SopSisT.
Implicit Type op : S → S → T.
Definition self_inverse e op := ∀ x, op x x = e.
Definition commutative op := ∀ x y, op x y = op y x.
End SopSisT.
Section SopSisS.
Implicit Type op : S → S → S.
Definition idempotent op := ∀ x, op x x = x.
Definition associative op := ∀ x y z, op x (op y z) = op (op x y) z.
Definition interchange op1 op2 :=
∀ x y z t, op1 (op2 x y) (op2 z t) = op2 (op1 x z) (op1 y t).
End SopSisS.
End OperationProperties.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Delimit Scope fun_scope with FUN.
Open Scope fun_scope.
Notation "f ^~ y" := (fun x ⇒ f x y)
(at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope.
Notation "@^~ x" := (fun f ⇒ f x)
(at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope.
Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.
Notation "p .1" := (fst p)
(at level 2, left associativity, format "p .1") : pair_scope.
Notation "p .2" := (snd p)
(at level 2, left associativity, format "p .2") : pair_scope.
Coercion pair_of_and P Q (PandQ : P ∧ Q) := (proj1 PandQ, proj2 PandQ).
Definition all_pair I T U (w : ∀ i : I, T i × U i) :=
(fun i ⇒ (w i).1, fun i ⇒ (w i).2).
Reserved Notation "e .[ x ]"
(at level 2, left associativity, format "e .[ x ]").
Reserved Notation "e .[ x1 , x2 , .. , xn ]" (at level 2, left associativity,
format "e '[ ' .[ x1 , '/' x2 , '/' .. , '/' xn ] ']'").
Reserved Notation "s `_ i" (at level 3, i at level 2, left associativity,
format "s `_ i").
Reserved Notation "x ^-1" (at level 3, left associativity, format "x ^-1").
Reserved Notation "x *+ n" (at level 40, left associativity).
Reserved Notation "x *- n" (at level 40, left associativity).
Reserved Notation "x ^+ n" (at level 29, left associativity).
Reserved Notation "x ^- n" (at level 29, left associativity).
Reserved Notation "x *: A" (at level 40).
Reserved Notation "A :* x" (at level 40).
Reserved Notation "A :&: B" (at level 48, left associativity).
Reserved Notation "A :|: B" (at level 52, left associativity).
Reserved Notation "a |: A" (at level 52, left associativity).
Reserved Notation "A :\: B" (at level 50, left associativity).
Reserved Notation "A :\ b" (at level 50, left associativity).
Reserved Notation "<< A >>" (at level 0, format "<< A >>").
Reserved Notation "<[ a ] >" (at level 0, format "<[ a ] >").
Reserved Notation "''C' [ x ]" (at level 8, format "''C' [ x ]").
Reserved Notation "''C_' A [ x ]"
(at level 8, A at level 2, format "''C_' A [ x ]").
Reserved Notation "''C' ( A )" (at level 8, format "''C' ( A )").
Reserved Notation "''C_' B ( A )"
(at level 8, B at level 2, format "''C_' B ( A )").
Reserved Notation "''Z' ( A )" (at level 8, format "''Z' ( A )").
Reserved Notation "''C_' ( A ) [ x ]" (at level 8, only parsing).
Reserved Notation "''C_' ( B ) ( A )" (at level 8, only parsing).
Reserved Notation "m %/ d" (at level 40, no associativity).
Reserved Notation "m %% d" (at level 40, no associativity).
Reserved Notation "m %| d" (at level 70, no associativity).
Reserved Notation "m = n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' = n '/' %[mod d ] ']'").
Reserved Notation "m == n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' == n '/' %[mod d ] ']'").
Reserved Notation "m <> n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' <> n '/' %[mod d ] ']'").
Reserved Notation "m != n %[mod d ]" (at level 70, n at next level,
format "'[hv ' m '/' != n '/' %[mod d ] ']'").
Reserved Notation "a ^` ()" (at level 8, format "a ^` ()").
Reserved Notation "a ^` ( n )" (at level 8, format "a ^` ( n )").
Reserved Notation "`| x |" (at level 0, x at level 99, format "`| x |").
Reserved Notation "x <= y ?= 'iff' c" (at level 70, y, c at next level,
format "x '[hv' <= y '/' ?= 'iff' c ']'").
Reserved Notation "x <= y :> T" (at level 70, y at next level).
Reserved Notation "x >= y :> T" (at level 70, y at next level, only parsing).
Reserved Notation "x < y :> T" (at level 70, y at next level).
Reserved Notation "x > y :> T" (at level 70, y at next level, only parsing).
Reserved Notation "x <= y ?= 'iff' c :> T" (at level 70, y, c at next level,
format "x '[hv' <= y '/' ?= 'iff' c :> T ']'").
Module Option.
Definition apply aT rT (f : aT → rT) x u := if u is Some y then f y else x.
Definition default T := apply (fun x : T ⇒ x).
Definition bind aT rT (f : aT → option rT) := apply f None.
Definition map aT rT (f : aT → rT) := bind (fun x ⇒ Some (f x)).
End Option.
Notation oapp := Option.apply.
Notation odflt := Option.default.
Notation obind := Option.bind.
Notation omap := Option.map.
Notation some := (@Some _) (only parsing).
Notation erefl := refl_equal.
Notation ecast i T e x := (let: erefl in _ = i := e return T in x).
Definition esym := sym_eq.
Definition nesym := sym_not_eq.
Definition etrans := trans_eq.
Definition congr1 := f_equal.
Definition congr2 := f_equal2.
Prenex Implicits esym nesym.
Definition all_equal_to T (x0 : T) := ∀ x, unkeyed x = x0.
Lemma unitE : all_equal_to tt. Proof. by case. Qed.
Structure wrapped T := Wrap {unwrap : T}.
Canonical wrap T x := @Wrap T x.
Prenex Implicits unwrap wrap Wrap.
Reserved Notation "[ 'rec' a0 ]"
(at level 0, format "[ 'rec' a0 ]").
Reserved Notation "[ 'rec' a0 , a1 ]"
(at level 0, format "[ 'rec' a0 , a1 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]"
(at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"
(at level 0,
format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"
(at level 0,
format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]").
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
(at level 0,
format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]").
Section SimplFun.
Variables aT rT : Type.
CoInductive simpl_fun := SimplFun of aT → rT.
Definition fun_of_simpl f := fun x ⇒ let: SimplFun lam := f in lam x.
Coercion fun_of_simpl : simpl_fun >-> Funclass.
End SimplFun.
Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T ⇒ E))
(at level 0,
format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x => E ]" := (SimplFun (fun x ⇒ E))
(at level 0, x ident,
format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T ⇒ E))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'fun' x y => E ]" := (fun x ⇒ [fun y ⇒ E])
(at level 0, x ident, y ident,
format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x y : T => E ]" := (fun x : T ⇒ [fun y : T ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T ⇒ [fun y ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' x ( y : T ) => E ]" := (fun x ⇒ [fun y : T ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
(fun x : xT ⇒ [fun y : yT ⇒ E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Definition SimplFunDelta aT rT (f : aT → aT → rT) := [fun z ⇒ f z z].
Section ExtensionalEquality.
Variables A B C : Type.
Definition eqfun (f g : B → A) : Prop := ∀ x, f x = g x.
Definition eqrel (r s : C → B → A) : Prop := ∀ x y, r x y = s x y.
Lemma frefl f : eqfun f f. Proof. by []. Qed.
Lemma fsym f g : eqfun f g → eqfun g f. Proof. by move⇒ eq_fg x. Qed.
Lemma ftrans f g h : eqfun f g → eqfun g h → eqfun f h.
Proof. by move⇒ eq_fg eq_gh x; rewrite eq_fg. Qed.
Lemma rrefl r : eqrel r r. Proof. by []. Qed.
End ExtensionalEquality.
Typeclasses Opaque eqfun.
Typeclasses Opaque eqrel.
Hint Resolve frefl rrefl.
Notation "f1 =1 f2" := (eqfun f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A))
(at level 70, f2 at next level, A at level 90) : fun_scope.
Notation "f1 =2 f2" := (eqrel f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A))
(at level 70, f2 at next level, A, B at level 90) : fun_scope.
Section Composition.
Variables A B C : Type.
Definition funcomp u (f : B → A) (g : C → B) x := let: tt := u in f (g x).
Definition catcomp u g f := funcomp u f g.
Local Notation comp := (funcomp tt).
Definition pcomp (f : B → option A) (g : C → option B) x := obind f (g x).
Lemma eq_comp f f' g g' : f =1 f' → g =1 g' → comp f g =1 comp f' g'.
Proof. by move⇒ eq_ff' eq_gg' x; rewrite /= eq_gg' eq_ff'. Qed.
End Composition.
Notation comp := (funcomp tt).
Notation "@ 'comp'" := (fun A B C ⇒ @funcomp A B C tt).
Notation "f1 \o f2" := (comp f1 f2)
(at level 50, format "f1 \o '/ ' f2") : fun_scope.
Notation "f1 \; f2" := (catcomp tt f1 f2)
(at level 60, right associativity, format "f1 \; '/ ' f2") : fun_scope.
Notation "[ 'eta' f ]" := (fun x ⇒ f x)
(at level 0, format "[ 'eta' f ]") : fun_scope.
Notation "'fun' => E" := (fun _ ⇒ E) (at level 200, only parsing) : fun_scope.
Notation id := (fun x ⇒ x).
Notation "@ 'id' T" := (fun x : T ⇒ x)
(at level 10, T at level 8, only parsing) : fun_scope.
Definition id_head T u x : T := let: tt := u in x.
Definition explicit_id_key := tt.
Notation idfun := (id_head tt).
Notation "@ 'idfun' T " := (@id_head T explicit_id_key)
(at level 10, T at level 8, format "@ 'idfun' T") : fun_scope.
Definition phant_id T1 T2 v1 v2 := phantom T1 v1 → phantom T2 v2.
Section Tag.
Variables (I : Type) (i : I) (T_ U_ : I → Type).
Definition tag := projS1.
Definition tagged : ∀ w, T_(tag w) := @projS2 I [eta T_].
Definition Tagged x := @existS I [eta T_] i x.
Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 i _ _ := w in i.
Definition tagged2 w : T_(tag2 w) := let: existT2 _ x _ := w in x.
Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ y := w in y.
Definition Tagged2 x y := @existS2 I [eta T_] [eta U_] i x y.
End Tag.
Implicit Arguments Tagged [I i].
Implicit Arguments Tagged2 [I i].
Prenex Implicits tag tagged Tagged tag2 tagged2 tagged2' Tagged2.
Coercion tag_of_tag2 I T_ U_ (w : @sigT2 I T_ U_) :=
Tagged (fun i ⇒ T_ i × U_ i)%type (tagged2 w, tagged2' w).
Lemma all_tag I T U :
(∀ x : I, {y : T x & U x y}) →
{f : ∀ x, T x & ∀ x, U x (f x)}.
Proof. by move⇒ fP; ∃ (fun x ⇒ tag (fP x)) ⇒ x; case: (fP x). Qed.
Lemma all_tag2 I T U V :
(∀ i : I, {y : T i & U i y & V i y}) →
{f : ∀ i, T i & ∀ i, U i (f i) & ∀ i, V i (f i)}.
Proof. by case/all_tag⇒ f /all_pair[]; ∃ f. Qed.
Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").
Section Sig.
Variables (T : Type) (P Q : T → Prop).
Lemma svalP (u : sig P) : P (sval u). Proof. by case: u. Qed.
Definition s2val (u : sig2 P Q) := let: exist2 x _ _ := u in x.
Lemma s2valP u : P (s2val u). Proof. by case: u. Qed.
Lemma s2valP' u : Q (s2val u). Proof. by case: u. Qed.
End Sig.
Prenex Implicits svalP s2val s2valP s2valP'.
Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u).
Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) :=
exist (fun i ⇒ P i ∧ Q i) (s2val u) (conj (s2valP u) (s2valP' u)).
Lemma all_sig I T P :
(∀ x : I, {y : T x | P x y}) →
{f : ∀ x, T x | ∀ x, P x (f x)}.
Proof. by case/all_tag⇒ f; ∃ f. Qed.
Lemma all_sig2 I T P Q :
(∀ x : I, {y : T x | P x y & Q x y}) →
{f : ∀ x, T x | ∀ x, P x (f x) & ∀ x, Q x (f x)}.
Proof. by case/all_sig⇒ f /all_pair[]; ∃ f. Qed.
Section Morphism.
Variables (aT rT sT : Type) (f : aT → rT).
Definition morphism_1 aF rF := ∀ x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := ∀ x y, f (aOp x y) = rOp (f x) (f y).
Definition homomorphism_1 (aP rP : _ → Prop) := ∀ x, aP x → rP (f x).
Definition homomorphism_2 (aR rR : _ → _ → Prop) :=
∀ x y, aR x y → rR (f x) (f y).
Definition monomorphism_1 (aP rP : _ → sT) := ∀ x, rP (f x) = aP x.
Definition monomorphism_2 (aR rR : _ → _ → sT) :=
∀ x y, rR (f x) (f y) = aR x y.
End Morphism.
Notation "{ 'morph' f : x / a >-> r }" :=
(morphism_1 f (fun x ⇒ a) (fun x ⇒ r))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a >-> r }") : type_scope.
Notation "{ 'morph' f : x / a }" :=
(morphism_1 f (fun x ⇒ a) (fun x ⇒ a))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a }") : type_scope.
Notation "{ 'morph' f : x y / a >-> r }" :=
(morphism_2 f (fun x y ⇒ a) (fun x y ⇒ r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a >-> r }") : type_scope.
Notation "{ 'morph' f : x y / a }" :=
(morphism_2 f (fun x y ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a }") : type_scope.
Notation "{ 'homo' f : x / a >-> r }" :=
(homomorphism_1 f (fun x ⇒ a) (fun x ⇒ r))
(at level 0, f at level 99, x ident,
format "{ 'homo' f : x / a >-> r }") : type_scope.
Notation "{ 'homo' f : x / a }" :=
(homomorphism_1 f (fun x ⇒ a) (fun x ⇒ a))
(at level 0, f at level 99, x ident,
format "{ 'homo' f : x / a }") : type_scope.
Notation "{ 'homo' f : x y / a >-> r }" :=
(homomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'homo' f : x y / a >-> r }") : type_scope.
Notation "{ 'homo' f : x y / a }" :=
(homomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'homo' f : x y / a }") : type_scope.
Notation "{ 'homo' f : x y /~ a }" :=
(homomorphism_2 f (fun y x ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'homo' f : x y /~ a }") : type_scope.
Notation "{ 'mono' f : x / a >-> r }" :=
(monomorphism_1 f (fun x ⇒ a) (fun x ⇒ r))
(at level 0, f at level 99, x ident,
format "{ 'mono' f : x / a >-> r }") : type_scope.
Notation "{ 'mono' f : x / a }" :=
(monomorphism_1 f (fun x ⇒ a) (fun x ⇒ a))
(at level 0, f at level 99, x ident,
format "{ 'mono' f : x / a }") : type_scope.
Notation "{ 'mono' f : x y / a >-> r }" :=
(monomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'mono' f : x y / a >-> r }") : type_scope.
Notation "{ 'mono' f : x y / a }" :=
(monomorphism_2 f (fun x y ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'mono' f : x y / a }") : type_scope.
Notation "{ 'mono' f : x y /~ a }" :=
(monomorphism_2 f (fun y x ⇒ a) (fun x y ⇒ a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'mono' f : x y /~ a }") : type_scope.
Section Injections.
Variables (rT aT : Type) (f : aT → rT).
Definition injective := ∀ x1 x2, f x1 = f x2 → x1 = x2.
Definition cancel g := ∀ x, g (f x) = x.
Definition pcancel g := ∀ x, g (f x) = Some x.
Definition ocancel (g : aT → option rT) h := ∀ x, oapp h x (g x) = x.
Lemma can_pcan g : cancel g → pcancel (fun y ⇒ Some (g y)).
Proof. by move⇒ fK x; congr (Some _). Qed.
Lemma pcan_inj g : pcancel g → injective.
Proof. by move⇒ fK x y /(congr1 g); rewrite !fK ⇒ [[]]. Qed.
Lemma can_inj g : cancel g → injective.
Proof. by move/can_pcan; exact: pcan_inj. Qed.
Lemma canLR g x y : cancel g → x = f y → g x = y.
Proof. by move⇒ fK →. Qed.
Lemma canRL g x y : cancel g → f x = y → x = g y.
Proof. by move⇒ fK <-. Qed.
End Injections.
Lemma Some_inj {T} : injective (@Some T). Proof. by move⇒ x y []. Qed.
Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
Proof. by case: y /. Qed.
Lemma etrans_id T x y (eqxy : x = y :> T) : etrans (erefl x) eqxy = eqxy.
Proof. by case: y / eqxy. Qed.
Section InjectionsTheory.
Variables (A B C : Type) (f g : B → A) (h : C → B).
Lemma inj_id : injective (@id A).
Proof. by []. Qed.
Lemma inj_can_sym f' : cancel f f' → injective f' → cancel f' f.
Proof. move⇒ fK injf' x; exact: injf'. Qed.
Lemma inj_comp : injective f → injective h → injective (f \o h).
Proof. move⇒ injf injh x y /injf; exact: injh. Qed.
Lemma can_comp f' h' : cancel f f' → cancel h h' → cancel (f \o h) (h' \o f').
Proof. by move⇒ fK hK x; rewrite /= fK hK. Qed.
Lemma pcan_pcomp f' h' :
pcancel f f' → pcancel h h' → pcancel (f \o h) (pcomp h' f').
Proof. by move⇒ fK hK x; rewrite /pcomp fK /= hK. Qed.
Lemma eq_inj : injective f → f =1 g → injective g.
Proof. by move⇒ injf eqfg x y; rewrite -2!eqfg; exact: injf. Qed.
Lemma eq_can f' g' : cancel f f' → f =1 g → f' =1 g' → cancel g g'.
Proof. by move⇒ fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed.
Lemma inj_can_eq f' : cancel f f' → injective f' → cancel g f' → f =1 g.
Proof. by move⇒ fK injf' gK x; apply: injf'; rewrite fK. Qed.
End InjectionsTheory.
Section Bijections.
Variables (A B : Type) (f : B → A).
CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f.
Hypothesis bijf : bijective.
Lemma bij_inj : injective f.
Proof. by case: bijf ⇒ g fK _; apply: can_inj fK. Qed.
Lemma bij_can_sym f' : cancel f' f ↔ cancel f f'.
Proof.
split⇒ fK; first exact: inj_can_sym fK bij_inj.
by case: bijf ⇒ h _ hK x; rewrite -[x]hK fK.
Qed.
Lemma bij_can_eq f' f'' : cancel f f' → cancel f f'' → f' =1 f''.
Proof.
by move⇒ fK fK'; apply: (inj_can_eq _ bij_inj); apply/bij_can_sym.
Qed.
End Bijections.
Section BijectionsTheory.
Variables (A B C : Type) (f : B → A) (h : C → B).
Lemma eq_bij : bijective f → ∀ g, f =1 g → bijective g.
Proof. by case⇒ f' fK f'K g eqfg; ∃ f'; eapply eq_can; eauto. Qed.
Lemma bij_comp : bijective f → bijective h → bijective (f \o h).
Proof.
by move⇒ [f' fK f'K] [h' hK h'K]; ∃ (h' \o f'); apply: can_comp; auto.
Qed.
Lemma bij_can_bij : bijective f → ∀ f', cancel f f' → bijective f'.
Proof. by move⇒ bijf; ∃ f; first by apply/(bij_can_sym bijf). Qed.
End BijectionsTheory.
Section Involutions.
Variables (A : Type) (f : A → A).
Definition involutive := cancel f f.
Hypothesis Hf : involutive.
Lemma inv_inj : injective f. Proof. exact: can_inj Hf. Qed.
Lemma inv_bij : bijective f. Proof. by ∃ f. Qed.
End Involutions.
Section OperationProperties.
Variables S T R : Type.
Section SopTisR.
Implicit Type op : S → T → R.
Definition left_inverse e inv op := ∀ x, op (inv x) x = e.
Definition right_inverse e inv op := ∀ x, op x (inv x) = e.
Definition left_injective op := ∀ x, injective (op^~ x).
Definition right_injective op := ∀ y, injective (op y).
End SopTisR.
Section SopTisS.
Implicit Type op : S → T → S.
Definition right_id e op := ∀ x, op x e = x.
Definition left_zero z op := ∀ x, op z x = z.
Definition right_commutative op := ∀ x y z, op (op x y) z = op (op x z) y.
Definition left_distributive op add :=
∀ x y z, op (add x y) z = add (op x z) (op y z).
Definition right_loop inv op := ∀ y, cancel (op^~ y) (op^~ (inv y)).
Definition rev_right_loop inv op := ∀ y, cancel (op^~ (inv y)) (op^~ y).
End SopTisS.
Section SopTisT.
Implicit Type op : S → T → T.
Definition left_id e op := ∀ x, op e x = x.
Definition right_zero z op := ∀ x, op x z = z.
Definition left_commutative op := ∀ x y z, op x (op y z) = op y (op x z).
Definition right_distributive op add :=
∀ x y z, op x (add y z) = add (op x y) (op x z).
Definition left_loop inv op := ∀ x, cancel (op x) (op (inv x)).
Definition rev_left_loop inv op := ∀ x, cancel (op (inv x)) (op x).
End SopTisT.
Section SopSisT.
Implicit Type op : S → S → T.
Definition self_inverse e op := ∀ x, op x x = e.
Definition commutative op := ∀ x y, op x y = op y x.
End SopSisT.
Section SopSisS.
Implicit Type op : S → S → S.
Definition idempotent op := ∀ x, op x x = x.
Definition associative op := ∀ x y z, op x (op y z) = op (op x y) z.
Definition interchange op1 op2 :=
∀ x y z t, op1 (op2 x y) (op2 z t) = op2 (op1 x z) (op1 y t).
End SopSisS.
End OperationProperties.