Library Subsets.Function

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Additional definitions and results about functions. This complements module ssrfun from the Coq standard library.

Description

Subsets of the type U are represented by their belonging function, of type U Prop.
Many properties are tautologies, and can be found on Wikipedia: https://en.wikipedia.org/wiki/List_of_set_identities_and_relations

Additional support for functional extensionality

Provide more results, including equivalence results to enable the use of the rewrite tactic.

Support for functions from/to types that are inhabited or not

Additional support for image/preimage

Additional support for the composition of functions

  • comp_inj_r states the condition for composition to be injective wrt its second (right) argument.

Additional support for injective/surjective/bijective functions

  • im_dec is a decidability result stating that any element of the output type of any function is either in its image/range or not;
  • {inj,surj}_has_left_inv states that injective (resp. surjective) functions have a left (resp. right) inverse.

Support for the inverse of bijective functions

  • bij_EX states the strong existence of the (left and right) inverse of any bijective function;
  • f_inv Hf is the inverse of a function from any proof Hf of its bijectivity.
The inverse of any bijective function is unique and bijective. Involutive functions are the bijective functions equal to their inverse.

Used logic axioms

Usage

This module may be used through the import of Subsets.Subsets, Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Requisite Require Import ssr.

From Logic Require Import logic_compl.
From Subsets Require Import Subset Subset_dec.
From Subsets Require Import Subset_finite Subset_seq Subset_any.

Section Base_Def0.

Context {U1 U2 : Type}.
Variable f g : U1 U2.
Definition same_fun : Prop := x, f x = g x.

Variable A1 : U1 Prop. Variable A2 : U2 Prop.
Inductive image : U2 Prop := Im : x1, A1 x1 image (f x1).

Definition image_ex : U2 Prop := fun x2 x1, A1 x1 x2 = f x1.

Definition preimage : U1 Prop := fun x1A2 (f x1).

End Base_Def0.

Section Base_Def1.

Definition pt_eval {U1 : Type} (U2 : Type) (x1 : U1) : (U1 U2) U2 :=
  fun ff x1.

Context {U1 U2 U3 : Type}.

Definition swap (f : U1 U2 U3) : U2 U1 U3 := fun x2 x1f x1 x2.

Definition Rg (f : U1 U2) : U2 Prop := image f fullset.

Definition surjective (f : U1 U2) : Prop := x2, x1, f x1 = x2.

End Base_Def1.

Section Prop_Facts0.

Context {U1 U2 : Type}.
Facts about same_fun.
It is an equivalence binary relation.


Lemma same_fun_sym : (f g : U1 U2), same_fun f g same_fun g f.
Proof. easy. Qed.

Lemma same_fun_trans :
   (f g h : U1 U2), same_fun f g same_fun g h same_fun f h.
Proof. intros f g h H1 H2 x; now rewrite (H1 x). Qed.


Lemma fun_ext_equiv : {f g : U1 U2}, f = g same_fun f g.
Proof. intros; split; [apply: fun_ext_rev | apply fun_ext]. Qed.

Lemma fun_ext_contra :
   {f g : U1 U2}, f g x1, f x1 g x1.
Proof.
intros f g; rewrite contra_not_l_equiv not_ex_not_all_equiv; apply fun_ext.
Qed.

Lemma fun_ext_contra_rev :
   {f g : U1 U2}, ( x1, f x1 g x1) f g.
Proof.
intros f g; rewrite contra_not_r_equiv not_ex_not_all_equiv; apply fun_ext_rev.
Qed.

Lemma fun_ext_contra_equiv :
   {f g : U1 U2}, f g x1, f x1 g x1.
Proof. intros; split; [apply fun_ext_contra | apply fun_ext_contra_rev]. Qed.

End Prop_Facts0.

Ltac fun_unfold :=
  repeat unfold
    same_fun,
    preimage.
Ltac fun_auto :=
  fun_unfold; subset_auto.

Ltac fun_ext_auto x :=
  apply fun_ext; intros x; fun_auto.

Section Inhabited_Facts.

Context {U1 U2 : Type}.

Lemma fun_to_nonempty_compat : inhabited U2 inhabited (U1 U2).
Proof. intros [x2]; apply (inhabits (fun x2)). Qed.

Lemma fun_to_unit_unit :
   (x2 : U2), unit_type x2 (f : U1 U2), unit_type f.
Proof.
intros x2 H2 f g; apply fun_ext; intro; rewrite (H2 (f _)) (H2 (g _)); easy.
Qed.

Lemma fun_to_is_unit_is_unit : is_unit_type U2 is_unit_type (U1 U2).
Proof.
intros [x2 H2]; apply (is_unit_type_correct (fun _x2)).
apply (fun_to_unit_unit x2); easy.
Qed.

Definition fun_from_empty (H1 : ¬ inhabited U1) : U1 U2.
Proof. intros; contradict H1; easy. Qed.

Lemma fun_from_empty_is_nonempty : ¬ inhabited U1 inhabited (U1 U2).
Proof. intros H1; apply (inhabits (fun_from_empty H1)). Qed.

Lemma fun_from_empty_unit :
  ¬ inhabited U1 (f : U1 U2), unit_type f.
Proof.
rewrite contra_not_l_equiv not_all_ex_not_equiv.
move⇒ [f /not_all_ex_not_equiv [g /fun_ext_contra_equiv [x1 _]]].
apply (inhabits x1).
Qed.

Lemma fun_from_empty_is_unit : ¬ inhabited U1 is_unit_type (U1 U2).
Proof.
intros H1; destruct (fun_from_empty_is_nonempty H1) as [f].
apply (is_unit_type_correct f), fun_from_empty_unit; easy.
Qed.

Lemma fun_to_empty_is_empty :
  inhabited U1 ¬ inhabited U2 ¬ inhabited (U1 U2).
Proof. intros [x1] HU2 [h]; contradict HU2; apply (inhabits (h x1)). Qed.

End Inhabited_Facts.

Section Comp_Facts0.

Facts about composition of functions.

Context {U1 U2 U3 U4 : Type}.
Variable f : U1 U2. Variable g : U2 U3. Variable h : U3 U4.
Lemma comp_correct : x1, (g \o f) x1 = g (f x1).
Proof. easy. Qed.

Lemma comp_assoc : h \o (g \o f) = (h \o g) \o f.
Proof. easy. Qed.

Lemma image_comp :
   A1, image (g \o f) A1 = image g (image f A1).
Proof.
intros A1; apply subset_ext_equiv; split; intros x3 Hx3.
induction Hx3 as [x1 Hx1]; easy.
induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
rewrite -comp_correct; easy.
Qed.

Lemma preimage_comp :
   A3, preimage (g \o f) A3 = preimage f (preimage g A3).
Proof. easy. Qed.

End Comp_Facts0.

Section Comp_Facts1.

Context {U : Type}.
Context {f g : U U}.

Lemma invol_comp :
  f \o g = g \o f involutive f involutive g involutive (f \o g).
Proof. intros H Hf Hg x; rewrite {2}H; simpl; rewrite Hg Hf; easy. Qed.

End Comp_Facts1.

Section Comp_Facts2.

Context {U1 U2 : Type}.
Variable f : U1 U2.

Lemma comp_id_l : id \o f = f.
Proof. easy. Qed.

Lemma comp_id_r : f \o id = f.
Proof. easy. Qed.

Lemma comp_id : {U : Type}, id \o id = (id : U U).
Proof. easy. Qed.

End Comp_Facts2.

Section Comp_Facts3a.

Context {U1 U2 U3 : Type}.
Context {f : U1 U2}.
Context {g h : U2 U3}.

Lemma comp_inj_l : surjective f g \o f = h \o f g = h.
Proof.
moveHf /fun_ext_rev H.
apply fun_ext; intros x2; destruct (Hf x2) as [x1 <-]; apply H.
Qed.

End Comp_Facts3a.

Section Comp_Facts3b.

Context {U1 U2 U3 : Type}.
Context {g h : U1 U2}.
Context {f : U2 U3}.

Lemma comp_inj_r : injective f f \o g = f \o h g = h.
Proof. moveHf /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.

End Comp_Facts3b.

Section Image_Facts0.

Context {U : Type}.
Variable f : U U.
Variable A : U Prop.

Lemma image_id : f = id image f A = A.
Proof.
intros; subst; apply subset_ext_equiv; split;
    intros x Hx; [destruct Hx | apply: Im]; easy.
Qed.

End Image_Facts0.

Section Image_Facts1.

Facts about images.

Context {U1 U2 : Type}.
Variable f g : U1 U2.
Lemma image_eq : A1, image f A1 = image_ex f A1.
Proof.
intros; subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1].
x1; easy.
rewrite (proj2 Hx1); easy.
Qed.

Lemma image_ext_fun : A1, same_fun f g image f A1 = image g A1.
Proof.
intros; subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1];
    [rewrite H | rewrite <- H]; easy.
Qed.

Lemma image_ext : A1 B1, same A1 B1 image f A1 = image f B1.
Proof.
intros A1 B1 H.
subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1]; apply Im; apply H; easy.
Qed.

Lemma im_dec : x2, { x1 | f x1 = x2 } + { x1, f x1 x2 }.
Proof.
intros x2; destruct (in_dec (fun x2 x1, f x1 = x2) x2);
    [left; apply ex_EX | right; apply not_ex_all_not]; easy.
Qed.

Lemma image_empty_equiv : A1, empty (image f A1) empty A1.
Proof.
intros A1; split; intros HA1.
intros x1 Hx1; apply (HA1 (f x1)); easy.
intros x2 [x1 Hx1]; apply (HA1 x1); easy.
Qed.

Lemma image_emptyset : image f emptyset = emptyset.
Proof. apply empty_emptyset, image_empty_equiv; easy. Qed.

Lemma image_monot : A1 B1, incl A1 B1 incl (image f A1) (image f B1).
Proof. intros A1 B1 H1 x2 [x1 Hx1]; apply Im, H1; easy. Qed.

Lemma image_union :
   A1 B1, image f (union A1 B1) = union (image f A1) (image f B1).
Proof.
intros A1 B1; apply subset_ext_equiv; split; intros x2.
intros [x1 [Hx1 | Hx1]]; [left | right]; easy.
intros [[x1 Hx1] | [x1 Hx1]]; apply Im; [left | right]; easy.
Qed.

Lemma image_inter :
   A1 B1, incl (image f (inter A1 B1)) (inter (image f A1) (image f B1)).
Proof. intros A1 B1 x2 [x1 Hx1]; split; apply Im, Hx1. Qed.

Lemma image_diff :
   A1 B1, incl (diff (image f A1) (image f B1)) (image f (diff A1 B1)).
Proof.
intros A1 B1 x2 [[x1 Hx1] Hx2']; apply Im; split; try easy.
intros Hx1'; apply Hx2'; easy.
Qed.

Lemma image_compl :
   A1, incl (diff (image f fullset) (image f A1)) (image f (compl A1)).
Proof. intros; rewrite compl_equiv_def_diff; apply image_diff. Qed.

Lemma image_sym_diff :
   A1 B1,
    incl (sym_diff (image f A1) (image f B1)) (image f (sym_diff A1 B1)).
Proof.
intros; unfold sym_diff; rewrite image_union.
apply union_monot; apply image_diff.
Qed.

Lemma image_union_finite_distr :
   A1 N,
    image f (union_finite A1 N) = union_finite (fun nimage f (A1 n)) N.
Proof.
intros A1 N; apply subset_ext_equiv; split; intros x2.
intros [x1 [n [Hn Hx1]]]; n; split; easy.
intros [n [Hn [x1 Hx1]]]; apply Im; n; easy.
Qed.

Lemma image_inter_finite :
   A1 N,
    incl (image f (inter_finite A1 N))
      (inter_finite (fun nimage f (A1 n)) N).
Proof. intros A1 N x2 [x1 Hx1] n Hn; apply Im, Hx1; easy. Qed.

Lemma image_union_seq_distr :
   A1, image f (union_seq A1) = union_seq (fun nimage f (A1 n)).
Proof.
intros A1; apply subset_ext_equiv; split; intros x2.
intros [x1 [n Hx1]]; n; easy.
intros [n [x1 Hx1]]; apply Im; n; easy.
Qed.

Lemma image_inter_seq :
   A1,
    incl (image f (inter_seq A1)) (inter_seq (fun nimage f (A1 n))).
Proof. intros A1 x2 [x1 Hx1] n; apply Im, Hx1. Qed.

End Image_Facts1.

Section Image_Facts2.

Context {U1 U2 : Type}.
Context {f : U1 U2}.
Context {g : U2 U1}.
Hypothesis H : cancel f g.

Lemma image_can : cancel (image f) (image g).
Proof. move=>>; rewrite -image_comp; apply image_id, fun_ext, H. Qed.

Lemma image_inj : injective (image f).
Proof. intros A1 B1 H1; rewrite -(image_can A1) -(image_can B1) H1; easy. Qed.

End Image_Facts2.

Section Preimage_Facts0.

Context {U : Type}.
Variable f : U U.
Variable A : U Prop.

Lemma preimage_id : f = id preimage f A = A.
Proof. intros; subst; easy. Qed.

End Preimage_Facts0.

Section Preimage_Facts1.

Facts about preimages.

Context {U1 U2 : Type}.
Variable f g : U1 U2.
Lemma preimage_ext_fun :
   A2, same_fun f g preimage f A2 = preimage g A2.
Proof. intros A2 H; fun_ext_auto x1; rewrite (H x1); easy. Qed.

Lemma preimage_ext : A2 B2, same A2 B2 preimage f A2 = preimage f B2.
Proof. intros; subset_ext_auto; fun_auto. Qed.

Lemma preimage_empty_equiv :
   A2, empty (preimage f A2) disj A2 (image f fullset).
Proof.
intros A2; split.
intros HA2 x2 Hx2a Hx2b; induction Hx2b as [x1 Hx1]; apply (HA2 x1); easy.
intros HA2 x1 Hx1; apply (HA2 (f x1)); easy.
Qed.

Lemma preimage_emptyset : preimage f emptyset = emptyset.
Proof. apply empty_emptyset, preimage_empty_equiv; easy. Qed.

Lemma preimage_full_equiv :
   A2, full (preimage f A2) incl (image f fullset) A2.
Proof.
intros A2; split; intros HA2.
intros x2 [x1 Hx1]; apply HA2.
intros x1; apply HA2; easy.
Qed.

Lemma preimage_monot :
   A2 B2, incl A2 B2 incl (preimage f A2) (preimage f B2).
Proof. intros; fun_auto. Qed.

Lemma preimage_compl :
   A2, preimage f (compl A2) = compl (preimage f A2).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_union :
   A2 B2,
    preimage f (union A2 B2) = union (preimage f A2) (preimage f B2).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_inter :
   A2 B2,
    preimage f (inter A2 B2) = inter (preimage f A2) (preimage f B2).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_diff :
   A2 B2,
    preimage f (diff A2 B2) = diff (preimage f A2) (preimage f B2).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_sym_diff :
   A2 B2,
    preimage f (sym_diff A2 B2) = sym_diff (preimage f A2) (preimage f B2).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_cst :
   A2 (x2 : U2), preimage (fun _ : U1x2) A2 = Prop_cst (A2 x2).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_union_finite_distr :
   A2 N,
    preimage f (union_finite A2 N) = union_finite (fun npreimage f (A2 n)) N.
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_inter_finite_distr :
   A2 N,
    preimage f (inter_finite A2 N) = inter_finite (fun npreimage f (A2 n)) N.
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_union_seq_distr :
   A2,
    preimage f (union_seq A2) = union_seq (fun npreimage f (A2 n)).
Proof. intros; subset_ext_auto. Qed.

Lemma preimage_inter_seq_distr :
   A2,
    preimage f (inter_seq A2) = inter_seq (fun npreimage f (A2 n)).
Proof. intros; subset_ext_auto. Qed.

End Preimage_Facts1.

Section Preimage_Facts2.

Context {U1 U2 : Type}.
Context {f : U1 U2}.
Context {g : U2 U1}.
Hypothesis H : cancel f g.

Lemma preimage_can : cancel (preimage g) (preimage f).
Proof. move=>>; rewrite -preimage_comp; apply preimage_id, fun_ext, H. Qed.

Lemma preimage_inj : injective (preimage g).
Proof.
intros A2 B2 H1; rewrite -(preimage_can A2) -(preimage_can B2) H1; easy.
Qed.

End Preimage_Facts2.

Section Image_Preimage_Facts.

Facts about images and preimages.

Context {U1 U2 : Type}.
Variable f : U1 U2.
Lemma image_of_preimage :
   A2, image f (preimage f A2) = inter A2 (image f fullset).
Proof.
intros A2; apply subset_ext; intros x2; split.
intros Hx2; induction Hx2 as [x1 Hx1]; easy.
intros [Hx2 Hx2']; induction Hx2' as [x1 Hx1]; easy.
Qed.

Lemma image_of_preimage_of_image :
   A1, image f (preimage f (image f A1)) = image f A1.
Proof.
intros; rewrite image_of_preimage; apply inter_left, image_monot; easy.
Qed.

Lemma preimage_of_image : A1, incl A1 (preimage f (image f A1)).
Proof. easy. Qed.

Lemma preimage_of_image_full : preimage f (image f fullset) = fullset.
Proof. apply subset_ext_equiv; easy. Qed.

Lemma preimage_of_image_of_preimage :
   A2, preimage f (image f (preimage f A2)) = preimage f A2.
Proof.
intros; rewrite image_of_preimage.
rewrite preimage_inter preimage_of_image_full.
apply inter_full_r.
Qed.

Lemma preimage_of_image_equiv :
   A1, (preimage f (image f A1)) = A1 A2, preimage f A2 = A1.
Proof.
intros A1; split.
intros HA1; (image f A1); easy.
intros [A2 HA2]; rewrite <- HA2; apply preimage_of_image_of_preimage.
Qed.

End Image_Preimage_Facts.

Section Preimage_Facts3.

Context {U1 U2 : Type}.
Context {f : U1 U2}.
Context {g : U2 U1}.
Hypothesis H1 : cancel f g.
Hypothesis H2 : cancel g f.

Lemma preimage_eq : (A2 : U2 Prop), preimage f A2 = image g A2.
Proof.
move=>>; apply (preimage_inj H1); rewrite (preimage_can H2).
apply eq_sym, preimage_of_image_equiv; eexists; apply (preimage_can H2).
Qed.

End Preimage_Facts3.

Section Swap_Facts.

Context {U1 U2 U3 : Type}.
Variable f : U1 U2 U3.

Lemma swap_invol : swap (swap f) = f.
Proof. easy. Qed.

End Swap_Facts.

Section Range_Facts.

Context {U1 U2 U3 : Type}.
Context {f : U1 U2}.

Lemma Rg_correct : {x2} x1, f x1 = x2 Rg f x2.
Proof. movex2 x1 <-; easy. Qed.

Lemma Rg_ext : (g : U1 U2), same_fun f g Rg f = Rg g.
Proof. moveg /fun_ext ->; easy. Qed.

Lemma Rg_ex : {x2}, Rg f x2 x1, f x1 = x2.
Proof. intros; split; [intros [x1 _]; x1 | move⇒ [x1 <-]]; easy. Qed.

Lemma Rg_compl : {x2}, ¬ Rg f x2 x1, f x1 x2.
Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.

Lemma Rg_full_equiv : Rg f = fullset incl fullset (Rg f).
Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.

Lemma preimage_Rg : preimage f (Rg f) = fullset.
Proof. apply preimage_of_image_full. Qed.

Lemma Rg_comp : {g : U2 U3}, Rg (g \o f) = image g (Rg f).
Proof.
intros; apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
intros _ [_ [x1 _]]; apply: Im; easy.
Qed.

End Range_Facts.

Section Inj_Facts.

Context {U1 U2 U3 : Type}.
Context {f : U1 U2}.

Lemma inj_ext :
   {g : U1 U2}, same_fun f g injective f injective g.
Proof. move=>> H Hf; apply (eq_inj Hf H). Qed.

Lemma inj_equiv : injective f x1 y1, f x1 = f y1 x1 = y1.
Proof. intros Hf x1 y1; split; [apply Hf | apply f_equal]. Qed.

Lemma inj_contra : injective f x1 y1, x1 y1 f x1 f y1.
Proof. intros Hf x1 y1; rewrite -contra_equiv; apply Hf. Qed.

Lemma inj_contra_rev : ( x1 y1, x1 y1 f x1 f y1) injective f.
Proof. intros Hf x1 y1; rewrite contra_equiv; apply Hf. Qed.

Lemma inj_contra_equiv :
  injective f x1 y1, x1 y1 f x1 f y1.
Proof. split; [apply inj_contra | apply inj_contra_rev]. Qed.

Lemma inj_comp_compat :
   {g : U2 U3}, injective f injective g injective (g \o f).
Proof. intros; apply inj_comp; easy. Qed.

Lemma inj_comp_reg : (g : U2 U3), injective (g \o f) injective f.
Proof. intros g H; apply (inj_compr H). Qed.

Lemma fun_from_empty_is_inj : ¬ inhabited U1 injective f.
Proof. move=>> HU1 x1; contradict HU1; easy. Qed.

End Inj_Facts.

Section Surj_Facts.

Context {U1 U2 U3 : Type}.
Context {f : U1 U2}.

Lemma surj_correct : incl fullset (Rg f) surjective f.
Proof. intros Hf y; destruct (Hf y) as [x Hx]; [| x]; easy. Qed.

Lemma surj_rev : surjective f Rg f = fullset.
Proof.
intros Hf; apply incl_antisym; intros x2 _;
    [| destruct (Hf x2) as [x1 Hx1]; apply (Rg_correct x1)]; easy.
Qed.

Lemma surj_equiv : surjective f Rg f = fullset.
Proof.
split; [apply surj_rev | intros Hf; apply surj_correct; rewrite Hf]; easy.
Qed.

Lemma surj_equiv_alt : surjective f incl fullset (Rg f).
Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.

Lemma surj_ext :
   {g : U1 U2}, same_fun f g surjective f surjective g.
Proof.
move=>> H Hf; intros x2; destruct (Hf x2) as [x1 Hx1];
     x1; rewrite -H; easy.
Qed.

Lemma surj_comp_compat :
   {g : U2 U3}, surjective f surjective g surjective (g \o f).
Proof.
intros g Hf Hg x3; destruct (Hg x3) as [x2 Hx2], (Hf x2) as [x1 Hx1].
x1; rewrite -Hx2 -Hx1; easy.
Qed.

Lemma surj_comp_reg :
   (g : U2 U3), surjective (g \o f) surjective g.
Proof. intros g H x3; destruct (H x3) as [x1 Hx1]; (f x1); easy. Qed.

Lemma surj_id : {U : Type}, surjective (id : U U).
Proof. intros U x; x; easy. Qed.

End Surj_Facts.

Section Can_Facts1.

Context {U1 U2 : Type}.
Context {f f' : U1 U2}.
Context {g g' : U2 U1}.

Lemma can_ext_l : same_fun f f' cancel f g cancel f' g.
Proof. intros Hf H x1; rewrite -Hf//; auto. Qed.

Lemma can_ext_r : same_fun g g' cancel f g cancel f g'.
Proof. intros Hg H x1; rewrite -Hg; easy. Qed.

End Can_Facts1.

Section Can_Facts2.

Context {U1 U2 : Type}.
Context {f f' : U1 U2}.
Context {g g' : U2 U1}.

Lemma can_ext : same_fun f f' same_fun g g' cancel f g cancel f' g'.
Proof. moveHf Hg /(can_ext_r Hg) /(can_ext_l Hf); easy. Qed.

End Can_Facts2.

Section Can_Facts3.

Context {U1 U2 : Type}.
Context {f : U1 U2}.
Context {g : U2 U1}.

Lemma can_equiv : cancel f g g \o f = id.
Proof. apply iff_sym, fun_ext_equiv. Qed.

Lemma can_surj : cancel g f surjective f.
Proof. intros H x1; (g x1); easy. Qed.

Lemma can_id : {U : Type}, cancel (id : U U) id.
Proof. easy. Qed.

End Can_Facts3.

Section Can_Facts4.

Context {U1 U2 : Type}.
Context {f : U1 U2}.

Lemma inj_can_uniq_l :
   {g h : U2 U1}, injective f cancel g f cancel h f g = h.
Proof. move=>> Hf Hg Hh; apply fun_ext, (inj_can_eq Hg Hf Hh). Qed.

Lemma inj_has_left_inv : inhabited U1 injective f g, cancel f g.
Proof.
intros [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
(fun x2match im_dec f x2 with
  | inleft H1proj1_sig H1
  | inright _a1
  end).
intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
    [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; x1]; easy.
Qed.

Lemma surj_can_uniq_r :
   {g h : U2 U1}, surjective f cancel f g cancel f h g = h.
Proof.
intros g h Hf Hg Hh; apply fun_ext; intros x2.
destruct (Hf x2) as [x1 <-]; rewrite Hh; auto.
Qed.

Lemma surj_has_right_inv : surjective f g, cancel g f.
Proof.
split; [| intros [g Hg]; apply: can_surj Hg].
intros Hf; destruct (choice _ Hf) as [g Hg]; g; easy.
Qed.

End Can_Facts4.

Section Bij_Facts.

Context {U1 U2 U3 : Type}.
Context {f : U1 U2}.

Lemma bij_ex : ( g, cancel f g cancel g f) bijective f.
Proof. intros [g [Hg1 Hg2]]; apply (Bijective Hg1 Hg2). Qed.

Lemma bij_EX : bijective f { g : U2 U1 | cancel f g cancel g f }.
Proof. intros Hf; apply ex_EX; destruct Hf as [g Hg1 Hg2]; g; easy. Qed.

Lemma bij_ext :
   f {g : U1 U2}, same_fun f g bijective f bijective g.
Proof. move=>> H Hf; apply (eq_bij Hf H). Qed.

Lemma bij_surj : bijective f surjective f.
Proof. intros [g _ H] x2; (g x2); rewrite H; easy. Qed.

Lemma inj_surj_ex_uniq :
  injective f surjective f x2, ! x1, f x1 = x2.
Proof.
intros Hf1 Hf2 x2; destruct (Hf2 x2) as [x1 Hx1]; x1; split; [easy |].
intro; rewrite -Hx1; auto.
Qed.

Lemma inj_surj_ex_uniq_rev :
  ( x2, ! x1, f x1 = x2) injective f surjective f.
Proof.
intros Hf; split;
    [| intros x2; destruct (Hf x2) as [x1 [Hx1 _]]; x1; easy].
intros x1 y1 H1; destruct (Hf (f x1)) as [x2 [Hx2a Hx2b]].
rewrite -(Hx2b x1); [apply Hx2b, eq_sym |]; easy.
Qed.

Lemma bij_equiv : bijective f injective f surjective f.
Proof.
split; [intros Hf; split; [apply bij_inj | apply bij_surj]; easy |].
intros [Hf1 Hf2]; destruct (unique_choice (fun x2 x1f x1 = x2)) as [g Hg].
apply (inj_surj_ex_uniq Hf1 Hf2).
apply: (Bijective _ Hg); intro; auto.
Qed.

Lemma bij_ex_uniq : bijective f x2, ! x1, f x1 = x2.
Proof.
rewrite bij_equiv; intros [Hf1 Hf2]; apply (inj_surj_ex_uniq Hf1 Hf2).
Qed.

Lemma bij_ex_uniq_rev : ( x2, ! x1, f x1 = x2) bijective f.
Proof. rewrite bij_equiv; apply inj_surj_ex_uniq_rev. Qed.

Lemma bij_ex_uniq_equiv : bijective f x2, ! x1, f x1 = x2.
Proof. split; [apply bij_ex_uniq | apply bij_ex_uniq_rev]. Qed.

Lemma bij_comp_compat :
   {g : U2 U3}, bijective f bijective g bijective (g \o f).
Proof. intros; apply bij_comp; easy. Qed.

Lemma bij_can_uniq_l :
   {g h : U2 U1}, bijective f cancel g f cancel h f g = h.
Proof. move=>> /bij_inj; apply inj_can_uniq_l. Qed.

Lemma bij_can_uniq_r :
   {g h : U2 U1}, bijective f cancel f g cancel f h g = h.
Proof. move=>> /bij_surj; apply surj_can_uniq_r. Qed.

Lemma bij_id : {U : Type}, bijective (id : U U).
Proof. intros; apply (Bijective can_id); easy. Qed.

End Bij_Facts.

Section Inverse_Def.

Context {U1 U2 : Type}.
Context {f : U1 U2}.
Hypothesis Hf : bijective f.


Definition f_inv : U2 U1 := proj1_sig (bij_EX Hf).

Lemma f_inv_can_l : cancel f f_inv.
Proof. apply (proj2_sig (bij_EX Hf)). Qed.

Lemma f_inv_id_l : f_inv \o f = id.
Proof. apply can_equiv, f_inv_can_l. Qed.

Lemma f_inv_can_r : cancel f_inv f.
Proof. apply (proj2_sig (bij_EX Hf)). Qed.

Lemma f_inv_id_r : f \o f_inv = id.
Proof. apply can_equiv, f_inv_can_r. Qed.

End Inverse_Def.

Section Inverse_Facts1.

Context {U1 U2 : Type}.
Context {f : U1 U2}.
Hypothesis Hf : bijective f.

Lemma f_inv_uniq_l : (g : U2 U1), cancel f g g = f_inv Hf.
Proof. move=>> H; apply (bij_can_uniq_r Hf H), f_inv_can_l. Qed.

Lemma f_inv_uniq_r : (g : U2 U1), cancel g f g = f_inv Hf.
Proof. move=>> H; apply (bij_can_uniq_l Hf H), f_inv_can_r. Qed.

Lemma f_inv_bij : bijective (f_inv Hf).
Proof. apply (bij_can_bij Hf), f_inv_can_l. Qed.

Lemma f_inv_inj : injective (f_inv Hf).
Proof. apply bij_inj, f_inv_bij. Qed.

Lemma f_inv_surj : surjective (f_inv Hf).
Proof. apply bij_surj, f_inv_bij. Qed.

Lemma f_inv_eq_equiv : x1 x2, x1 = f_inv Hf x2 f x1 = x2.
Proof.
intros x1 x2; split.
rewrite -{2}(f_inv_can_r Hf x2); apply f_equal.
rewrite -{2}(f_inv_can_l Hf x1); apply f_equal.
Qed.

Lemma f_inv_neq_equiv : x1 x2, x1 f_inv Hf x2 f x1 x2.
Proof. intros; rewrite -iff_not_equiv; apply f_inv_eq_equiv. Qed.

End Inverse_Facts1.

Section Inverse_Facts2.

Context {U1 U2 : Type}.
Context {f g : U1 U2}.
Hypothesis Hf : bijective f.
Hypothesis Hg : bijective g.

Lemma f_inv_ext : same_fun f g f_inv Hf = f_inv Hg.
Proof.
move⇒ /fun_ext_equiv H; apply (comp_inj_r (bij_inj Hf)).
rewrite {3}H !f_inv_id_r; easy.
Qed.

Lemma f_inv_invol : (Hf1 : bijective (f_inv Hf)), f_inv Hf1 = f.
Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_can_r. Qed.

Lemma f_inv_invol_alt : f_inv (f_inv_bij Hf) = f.
Proof. apply f_inv_invol. Qed.

End Inverse_Facts2.

Section Inverse_Facts3.

Context {U : Type}.
Context {f : U U}.
Hypothesis Hf : bijective f.

Lemma f_inv_id : involutive f f_inv Hf = f.
Proof.
intros; apply (comp_inj_r (bij_inj Hf)).
apply fun_ext; intro; rewrite !comp_correct H f_inv_can_r; easy.
Qed.

Lemma f_inv_id_rev : f_inv Hf = f involutive f.
Proof. intros H x; rewrite -{1}H; apply f_inv_can_l. Qed.

Lemma f_inv_id_equiv : f_inv Hf = f involutive f.
Proof. split; [apply f_inv_id_rev | apply f_inv_id]. Qed.

Lemma f_inv_is_id : f = id f_inv Hf = id.
Proof.
intros; apply (comp_inj_r (bij_inj Hf)); rewrite f_inv_id_r comp_id_r; easy.
Qed.

Lemma f_inv_is_id_rev : f_inv Hf = id f = id.
Proof.
intros; apply (comp_inj_r (bij_inj (f_inv_bij Hf)));
    rewrite f_inv_id_l comp_id_r; easy.
Qed.

Lemma f_inv_is_id_equiv : f_inv Hf = id f = id.
Proof. split; [apply f_inv_is_id_rev | apply f_inv_is_id]. Qed.

End Inverse_Facts3.