Library Ssreflect.ssrfun
Require Import ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
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.
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.
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 "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 "s `_ i"
(at level 3, i at level 2, left associativity, format "s `_ i").
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).
Reserved Notation "[ 'rec' a0 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
(at level 0).
Section SimplFun.
Variables aT rT : Type.
CoInductive simpl_fun : Type := SimplFun of aT -> rT.
Definition fun_of_simpl := fun f 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].
Definition erefl := refl_equal.
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.
Section ExtensionalEquality.
Variables A B C : Type.
Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x.
Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y.
Lemma frefl : forall f, eqfun f f. Proof. by []. Qed.
Lemma fsym : forall f g, eqfun f g -> eqfun g f. Proof. by move=> f g E x. Qed.
Lemma ftrans : forall f g h, eqfun f g -> eqfun g h -> eqfun f h.
Proof. by move=> f g h eqfg eqgh x; rewrite eqfg. Qed.
Lemma rrefl : forall r, eqrel r r. Proof. by []. Qed.
End ExtensionalEquality.
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 comp (f : B -> A) (g : C -> B) := [fun x => f (g x)].
Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).
Lemma eq_comp : forall f f' g g', f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.
Proof. by move=> f f' g g' Ef Eg x; rewrite /= Eg Ef. Qed.
End Composition.
Notation "[ 'eta' f ]" := (fun x => f x)
(at level 0, format "[ 'eta' f ]") : 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.
Notation "f1 \o f2" := (comp f1 f2) (at level 50) : fun_scope.
Definition idfun T := @id T.
Prenex Implicits idfun.
Section OperationProperties.
Variable T : Type.
Variables zero one: T.
Variable inv : T -> T.
Variables mul add : T -> T -> T.
Notation Local "1" := one.
Notation Local "0" := zero.
Notation Local "x ^-1" := (inv x).
Notation Local "x * y" := (mul x y).
Notation Local "x + y" := (add x y).
Definition left_id := forall x, 1 * x = x.
Definition right_id := forall x, x * 1 = x.
Definition left_inverse := forall x, x^-1 * x = 1.
Definition right_inverse := forall x, x * x^-1 = 1.
Definition self_inverse := forall x, x * x = 1.
Definition idempotent := forall x, x * x = x.
Definition associative := forall x y z, x * (y * z) = x * y * z.
Definition commutative := forall x y, x * y = y * x.
Definition left_commutative := forall x y z, x * (y * z) = y * (x * z).
Definition right_commutative := forall x y z, x * y * z = x * z * y.
Definition left_zero := forall x, 0 * x = 0.
Definition right_zero := forall x, x * 0 = 0.
Definition left_distributive := forall x y z, (x + y) * z = x * z + y * z.
Definition right_distributive := forall x y z, x * (y + z) = x * y + x * z.
End OperationProperties.
Section Morphism.
Variables (aT rT sT : Type) (f : aT -> rT).
Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f 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.
Section Injections.
Variables (rT aT : Type) (f : aT -> rT).
Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.
Definition cancel g := forall x, g (f x) = x.
Definition pcancel g := forall x, g (f x) = Some x.
Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.
Lemma can_pcan : forall g, cancel g -> pcancel (fun y => Some (g y)).
Proof. by move=> g fK x; congr (Some _). Qed.
Lemma pcan_inj : forall g, pcancel g -> injective.
Proof. by move=> g fK x y; move/(congr1 g); rewrite !fK => [[]]. Qed.
Lemma can_inj : forall g, cancel g -> injective.
Proof. by move=> g; move/can_pcan; exact: pcan_inj. Qed.
Lemma canLR : forall g x y, cancel g -> x = f y -> g x = y.
Proof. by move=> g x y fK ->. Qed.
Lemma canRL : forall g x y, cancel g -> f x = y -> x = g y.
Proof. by move=> g x y fK <-. Qed.
End Injections.
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 : forall f', cancel f f' -> injective f' -> cancel f' f.
Proof. move=> f' fK injf' x; exact: injf'. Qed.
Lemma inj_comp : injective f -> injective h -> injective (f \o h).
Proof. move=> injf injh x y; move/injf; exact: injh. Qed.
Lemma can_comp : forall f' h',
cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f').
Proof. by move=> f' h' fK hK x; rewrite /= fK hK. Qed.
Lemma pcan_pcomp : forall f' h',
pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f').
Proof. by move=> f' h' 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 : forall f' g', cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.
Proof. by move=> f' g' fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed.
Lemma inj_can_eq : forall f',
cancel f f' -> injective f' -> cancel g f' -> f =1 g.
Proof. by move=> f' fK injf' gK x; apply: injf'; rewrite fK. Qed.
End InjectionsTheory.
Section Bijections.
Variables (A B : Type) (f : B -> A).
Definition bijective : Prop := exists2 g, cancel f g & cancel g f.
Hypothesis bijf : bijective.
Lemma bij_inj : injective f.
Proof. by case: bijf => [h fK _]; apply: can_inj fK. Qed.
Lemma bij_can_sym : forall f', cancel f' f <-> cancel f f'.
Proof.
move=> f'; 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 : forall f' f'', cancel f f' -> cancel f f'' -> f' =1 f''.
Proof.
by move=> f' f'' 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 -> forall g, f =1 g -> bijective g.
Proof. by move=> [f' fK f'K] g eqfg; exists f'; eapply eq_can; eauto. Qed.
Lemma bij_comp : bijective f -> bijective h -> bijective (f \o h).
Proof.
move=> [f' fK f'K] [h' hK h'K].
by exists (h' \o f' : _ -> _); apply can_comp; auto.
Qed.
Lemma bij_can_bij : bijective f -> forall f', cancel f f' -> bijective f'.
Proof. by move=> bijf; exists 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 exists f. Qed.
End Involutions.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
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.
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.
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 "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 "s `_ i"
(at level 3, i at level 2, left associativity, format "s `_ i").
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).
Reserved Notation "[ 'rec' a0 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"
(at level 0).
Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
(at level 0).
Section SimplFun.
Variables aT rT : Type.
CoInductive simpl_fun : Type := SimplFun of aT -> rT.
Definition fun_of_simpl := fun f 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].
Definition erefl := refl_equal.
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.
Section ExtensionalEquality.
Variables A B C : Type.
Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x.
Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y.
Lemma frefl : forall f, eqfun f f. Proof. by []. Qed.
Lemma fsym : forall f g, eqfun f g -> eqfun g f. Proof. by move=> f g E x. Qed.
Lemma ftrans : forall f g h, eqfun f g -> eqfun g h -> eqfun f h.
Proof. by move=> f g h eqfg eqgh x; rewrite eqfg. Qed.
Lemma rrefl : forall r, eqrel r r. Proof. by []. Qed.
End ExtensionalEquality.
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 comp (f : B -> A) (g : C -> B) := [fun x => f (g x)].
Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).
Lemma eq_comp : forall f f' g g', f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.
Proof. by move=> f f' g g' Ef Eg x; rewrite /= Eg Ef. Qed.
End Composition.
Notation "[ 'eta' f ]" := (fun x => f x)
(at level 0, format "[ 'eta' f ]") : 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.
Notation "f1 \o f2" := (comp f1 f2) (at level 50) : fun_scope.
Definition idfun T := @id T.
Prenex Implicits idfun.
Section OperationProperties.
Variable T : Type.
Variables zero one: T.
Variable inv : T -> T.
Variables mul add : T -> T -> T.
Notation Local "1" := one.
Notation Local "0" := zero.
Notation Local "x ^-1" := (inv x).
Notation Local "x * y" := (mul x y).
Notation Local "x + y" := (add x y).
Definition left_id := forall x, 1 * x = x.
Definition right_id := forall x, x * 1 = x.
Definition left_inverse := forall x, x^-1 * x = 1.
Definition right_inverse := forall x, x * x^-1 = 1.
Definition self_inverse := forall x, x * x = 1.
Definition idempotent := forall x, x * x = x.
Definition associative := forall x y z, x * (y * z) = x * y * z.
Definition commutative := forall x y, x * y = y * x.
Definition left_commutative := forall x y z, x * (y * z) = y * (x * z).
Definition right_commutative := forall x y z, x * y * z = x * z * y.
Definition left_zero := forall x, 0 * x = 0.
Definition right_zero := forall x, x * 0 = 0.
Definition left_distributive := forall x y z, (x + y) * z = x * z + y * z.
Definition right_distributive := forall x y z, x * (y + z) = x * y + x * z.
End OperationProperties.
Section Morphism.
Variables (aT rT sT : Type) (f : aT -> rT).
Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f 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.
Section Injections.
Variables (rT aT : Type) (f : aT -> rT).
Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.
Definition cancel g := forall x, g (f x) = x.
Definition pcancel g := forall x, g (f x) = Some x.
Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.
Lemma can_pcan : forall g, cancel g -> pcancel (fun y => Some (g y)).
Proof. by move=> g fK x; congr (Some _). Qed.
Lemma pcan_inj : forall g, pcancel g -> injective.
Proof. by move=> g fK x y; move/(congr1 g); rewrite !fK => [[]]. Qed.
Lemma can_inj : forall g, cancel g -> injective.
Proof. by move=> g; move/can_pcan; exact: pcan_inj. Qed.
Lemma canLR : forall g x y, cancel g -> x = f y -> g x = y.
Proof. by move=> g x y fK ->. Qed.
Lemma canRL : forall g x y, cancel g -> f x = y -> x = g y.
Proof. by move=> g x y fK <-. Qed.
End Injections.
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 : forall f', cancel f f' -> injective f' -> cancel f' f.
Proof. move=> f' fK injf' x; exact: injf'. Qed.
Lemma inj_comp : injective f -> injective h -> injective (f \o h).
Proof. move=> injf injh x y; move/injf; exact: injh. Qed.
Lemma can_comp : forall f' h',
cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f').
Proof. by move=> f' h' fK hK x; rewrite /= fK hK. Qed.
Lemma pcan_pcomp : forall f' h',
pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f').
Proof. by move=> f' h' 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 : forall f' g', cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.
Proof. by move=> f' g' fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed.
Lemma inj_can_eq : forall f',
cancel f f' -> injective f' -> cancel g f' -> f =1 g.
Proof. by move=> f' fK injf' gK x; apply: injf'; rewrite fK. Qed.
End InjectionsTheory.
Section Bijections.
Variables (A B : Type) (f : B -> A).
Definition bijective : Prop := exists2 g, cancel f g & cancel g f.
Hypothesis bijf : bijective.
Lemma bij_inj : injective f.
Proof. by case: bijf => [h fK _]; apply: can_inj fK. Qed.
Lemma bij_can_sym : forall f', cancel f' f <-> cancel f f'.
Proof.
move=> f'; 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 : forall f' f'', cancel f f' -> cancel f f'' -> f' =1 f''.
Proof.
by move=> f' f'' 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 -> forall g, f =1 g -> bijective g.
Proof. by move=> [f' fK f'K] g eqfg; exists f'; eapply eq_can; eauto. Qed.
Lemma bij_comp : bijective f -> bijective h -> bijective (f \o h).
Proof.
move=> [f' fK f'K] [h' hK h'K].
by exists (h' \o f' : _ -> _); apply can_comp; auto.
Qed.
Lemma bij_can_bij : bijective f -> forall f', cancel f f' -> bijective f'.
Proof. by move=> bijf; exists 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 exists f. Qed.
End Involutions.