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.
Additional definitions and results about functions.
This complements module ssrfun from the Coq standard library.
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
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.
Brief description
Description
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
- fun_from_empty is the only function from an empty type to another type, empty or not;
- fun_from_empty_is_inj states that it is injective;
- fun_to_empty_is_empty states that there is no function from a nonempty type to an empty one.
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.
Used logic axioms
- fun_ext, an alias for functional_extensionality.
- unique_choice;
- choice;
- ex_EX, an alias for constructive_indefinite_description.
Usage
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 x1 ⇒ A2 (f x1).
End Base_Def0.
Section Base_Def1.
Definition pt_eval {U1 : Type} (U2 : Type) (x1 : U1) : (U1 → U2) → U2 :=
fun f ⇒ f x1.
Context {U1 U2 U3 : Type}.
Definition swap (f : U1 → U2 → U3) : U2 → U1 → U3 := fun x2 x1 ⇒ f 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.
move⇒ Hf /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. move⇒ Hf /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 n ⇒ image 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 n ⇒ image 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 n ⇒ image 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 n ⇒ image 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 _ : U1 ⇒ x2) 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 n ⇒ preimage 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 n ⇒ preimage f (A2 n)) N.
Proof. intros; subset_ext_auto. Qed.
Lemma preimage_union_seq_distr :
∀ A2,
preimage f (union_seq A2) = union_seq (fun n ⇒ preimage f (A2 n)).
Proof. intros; subset_ext_auto. Qed.
Lemma preimage_inter_seq_distr :
∀ A2,
preimage f (inter_seq A2) = inter_seq (fun n ⇒ preimage 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. move⇒ x2 x1 <-; easy. Qed.
Lemma Rg_ext : ∀ (g : U1 → U2), same_fun f g → Rg f = Rg g.
Proof. move⇒ g /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. move⇒ Hf 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 x2 ⇒ match im_dec f x2 with
| inleft H1 ⇒ proj1_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 x1 ⇒ f 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.