Library Subsets.Function_sub

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

Support for restrictions of functions to subsets represented by predicates.

Description

Let f : T1 T2 for any types T1 and T2. Let P1 and P2 respectively be subsets of T1 and T2.
  • same_funS P1 f g states that f and g are equal on P1;
  • RgS P1 f is the range of f restricted to P1 (an alias for image f P1);
  • funS P1 P2 f states that f is a total function from P1 to P2, namely that RgS P1 f is included in P2;
  • injS P1 f states that f is injective on P1 (definition similar to injective);
  • surjS P1 P2 f states that f is surjective from P1 onto P2 (definition similar to surjective);
  • canS P1 f g states that g cancels f on P1, ie it is its left inverse. (definition similar to cancel);
  • involS P1 f states that f is involutive from P1 onto itself, ie it cancels itself on P1;
  • bijS P1 P2 f states that f is bijective from P1 onto P2 (definition similar to bijective);
  • bijS_EX states the strong existence of the (left and right) inverse of any bijective function from a subset onto another;
  • f_invS Hf is the inverse of a function from a subset onto another from any proof Hf of its bijectivity.

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 Function.

Section Fun_sub_Def1.

Context {T1 T2 : Type}.
Variable P1 : T1 Prop.
Variable P2 : T2 Prop.
Variable f : T1 T2.

Definition same_funS (g : T1 T2) : Prop := x1, P1 x1 f x1 = g x1.

Definition RgS : T2 Prop := image f P1.
Definition RgS_gen : T2 Prop := inter P2 RgS.

Definition funS : Prop := incl RgS P2.

Definition injS : Prop :=
   x1 y1, P1 x1 P1 y1 f x1 = f y1 x1 = y1.

Definition surjS : Prop := x2, P2 x2 x1, P1 x1 f x1 = x2.

Variable g : T2 T1.

Definition canS : Prop := x1, P1 x1 g (f x1) = x1.

End Fun_sub_Def1.

Section Fun_sub_Def2.

Context {T : Type}.
Variable P : T Prop.
Variable f : T T.

Definition involS : Prop := canS P f f.

End Fun_sub_Def2.

Section Fun_sub_Def3.

Context {T1 T2 : Type}.
Variable P1 : T1 Prop.
Variable P2 : T2 Prop.
Variable f : T1 T2.

Definition bijS_spec (g : T2 T1) : Prop :=
  funS P1 P2 f funS P2 P1 g canS P1 f g canS P2 g f.

Variant bijS : Prop := BijS_ : g : T2 T1, bijS_spec g bijS.

End Fun_sub_Def3.

Section Fun_sub_Def4.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Definition BijS (g : T2 T1) : bijS_spec P1 P2 f g bijS P1 P2 f :=
  BijS_ P1 P2 f g.

Lemma bijS_ex : ( g, bijS_spec P1 P2 f g) bijS P1 P2 f.
Proof. intros [g Hg]; apply (BijS g Hg). Qed.

Lemma bijS_EX : bijS P1 P2 f { g : T2 T1 | bijS_spec P1 P2 f g }.
Proof. intros Hf; apply ex_EX; destruct Hf as [g Hg]; g; easy. Qed.

End Fun_sub_Def4.

Section Same_funS_Facts.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.

Lemma same_funS_refl : (f : T1 T2), same_funS P1 f f.
Proof. easy. Qed.

Lemma same_funS_sym :
   {f g : T1 T2}, same_funS P1 f g same_funS P1 g f.
Proof. move=>> H x1 Hx1; rewrite H; easy. Qed.

Lemma same_funS_trans :
   g {f h : T1 T2},
    same_funS P1 f g same_funS P1 g h same_funS P1 f h.
Proof. move=>> H1 H2 x1 Hx1; rewrite H1// H2; easy. Qed.

End Same_funS_Facts.

Section RgS_Facts0.

Context {T1 T2 : Type}.
Variable P1 : T1 Prop.
Variable f : T1 T2.

Lemma imS_dec :
   x2, { x1 | P1 x1 f x1 = x2 } + { x1, P1 x1 f x1 x2 }.
Proof.
intros x2; destruct (in_dec (fun x2 x1, P1 x1 f x1 = x2) x2)
    as [H1 | H1]; [left; apply ex_EX; easy | right; intros x1].
rewrite imp_not_r_and_equiv; apply (not_ex_all_not _ _ H1).
Qed.

End RgS_Facts0.

Section RgS_Facts1.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma RgS_eq : RgS P1 f = RgS_gen P1 (RgS P1 f) f.
Proof. apply eq_sym, inter_idem. Qed.

Lemma RgS_correct : {x2} x1, P1 x1 f x1 = x2 RgS P1 f x2.
Proof. intros; subst; easy. Qed.

Lemma RgS_ex : {x2}, RgS P1 f x2 x1, P1 x1 f x1 = x2.
Proof.
intros; unfold RgS; rewrite image_eq; split; intros [x1 Hx1]; x1; easy.
Qed.

Lemma RgS_gen_eq : funS P1 P2 f RgS_gen P1 P2 f = RgS P1 f.
Proof. rewrite -inter_right; easy. Qed.

Lemma RgS_gen_correct :
   {x2} x1, P2 x2 P1 x1 f x1 = x2 RgS_gen P1 P2 f x2.
Proof. intros; subst; easy. Qed.

Lemma RgS_gen_ex :
   {P2} {x2},
    RgS_gen P1 P2 f x2 P2 x2 ( x1, P1 x1 f x1 = x2).
Proof. intros; rewrite -RgS_ex; easy. Qed.

End RgS_Facts1.

Section RgS_Facts2.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma RgS_ext : g, same_funS P1 f g RgS P1 f = RgS P1 g.
Proof.
intros g Hg; apply subset_ext_equiv; split; intros x2; rewrite !RgS_ex;
    intros [x1 Hx1]; x1; [rewrite -Hg | rewrite Hg]; easy.
Qed.

Lemma RgS_gen_ext :
   g, same_funS P1 f g RgS_gen P1 P2 f = RgS_gen P1 P2 g.
Proof. unfold RgS_gen; moveg /(RgS_ext g) ->; easy. Qed.

End RgS_Facts2.

Section RgS_Facts3.

Context {T1 T2 T3 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Context {g : T2 T3}.

Lemma RgS_full : RgS fullset f = Rg f.
Proof. easy. Qed.

Lemma RgS_gen_full_l : RgS_gen fullset P2 f = inter P2 (Rg f).
Proof. easy. Qed.

Lemma RgS_gen_full_r : {P1}, RgS_gen P1 fullset f = RgS P1 f.
Proof. intros; unfold RgS_gen; rewrite inter_full_l; easy. Qed.

Lemma RgS_gen_full : RgS_gen fullset fullset f = Rg f.
Proof. rewrite RgS_gen_full_r RgS_full; easy. Qed.

Lemma RgS_gen_full_equiv : RgS_gen P1 P2 f = P2 incl P2 (RgS P1 f).
Proof. symmetry; apply inter_left. Qed.

Lemma RgS_gen_full_equiv_alt :
  funS P1 P2 f RgS_gen P1 P2 f = P2 RgS P1 f = P2.
Proof. rewrite RgS_gen_full_equiv subset_ext_equiv; easy. Qed.

Lemma RgS_preimage : RgS (preimage f P2) f = inter P2 (Rg f).
Proof. apply image_of_preimage. Qed.

Lemma RgS_preimage_equiv : RgS (preimage f P2) f = P2 incl P2 (Rg f).
Proof. rewrite RgS_preimage -inter_left; easy. Qed.

Lemma RgS_preimage_RgS : RgS (preimage f (RgS P1 f)) f = RgS P1 f.
Proof. apply image_of_preimage_of_image. Qed.

Lemma preimage_RgS : incl P1 (preimage f (RgS P1 f)).
Proof. apply preimage_of_image. Qed.

Lemma preimage_RgS_equiv :
  preimage f (RgS P1 f) = P1 P2, preimage f P2 = P1.
Proof. apply preimage_of_image_equiv. Qed.

Lemma preimage_RgS_preimage :
  preimage f (RgS (preimage f P2) f) = preimage f P2.
Proof. apply preimage_of_image_of_preimage. Qed.

Lemma RgS_comp : RgS P1 (g \o f) = RgS (RgS P1 f) g.
Proof.
apply subset_ext_equiv; split; intros x3;
    [intros [x1 Hx1] | intros [x2 [x1 Hx1]]; fold ((g \o f) x1)]; easy.
Qed.

Lemma Rg_comp_alt : Rg (g \o f) = RgS (Rg f) g.
Proof. apply Rg_comp. Qed.

End RgS_Facts3.

Section FunS_Facts1.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma funS_correct : ( x1, P1 x1 P2 (f x1)) funS P1 P2 f.
Proof. intros Hf _ [x Hx]; auto. Qed.

Lemma funS_rev : funS P1 P2 f x1, P1 x1 P2 (f x1).
Proof. intros Hf x1 Hx1; apply Hf; easy. Qed.

Lemma funS_equiv : funS P1 P2 f x1, P1 x1 P2 (f x1).
Proof. split; [apply funS_rev | apply funS_correct]. Qed.

End FunS_Facts1.

Section FunS_Facts2.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Variable f : T1 T2.
Context {g : T1 T2}.

Lemma funS_ext : same_funS P1 f g funS P1 P2 f funS P1 P2 g.
Proof. moveHg Hf x2; rewrite -(RgS_ext _ Hg); auto. Qed.

End FunS_Facts2.

Section FunS_Facts3.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.

Lemma funS_id : same_funS P f id funS P P f.
Proof. intros Hf _ [y Hy]; rewrite Hf; easy. Qed.

End FunS_Facts3.

Section FunS_Facts4.

Context {T1 T2 : Type}.
Variable P1 : T1 Prop.
Context {P2 : T2 Prop}.
Variable f : T1 T2.

Lemma funS_full_l : {f : T1 T2}, incl (Rg f) P2 funS fullset P2 f.
Proof. easy. Qed.

Lemma funS_full_r : funS P1 fullset f.
Proof. easy. Qed.

Lemma funS_full : funS fullset fullset f.
Proof. easy. Qed.

End FunS_Facts4.

Section FunS_Facts5.

Context {T1 T2 T3 : Type}.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Context {P3 : T3 Prop}.
Context {f : T1 T2}.
Context {g : T2 T3}.

Lemma funS_comp_compat : funS P1 P2 f funS P2 P3 g funS P1 P3 (g \o f).
Proof. rewrite !funS_equiv; intros Hf Hg x1 Hx1; apply Hg; auto. Qed.

End FunS_Facts5.

Section InjS_Facts1.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.

Lemma injS_id : same_funS P f (id : T T) injS P f.
Proof. intros Hf x y Hx Hy; rewrite !Hf; easy. Qed.

End InjS_Facts1.

Section InjS_Facts2.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Variable f : T1 T2.
Context {g : T1 T2}.

Lemma injS_ext : same_funS P1 f g injS P1 f injS P1 g.
Proof. intros Hg Hf x1 y1 Hx1 Hy1; rewrite -!Hg; auto. Qed.

End InjS_Facts2.

Section InjS_Facts3.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {f : T1 T2}.

Lemma injS_contra :
  injS P1 f x1 y1, P1 x1 P1 y1 x1 y1 f x1 f y1.
Proof. intros Hf x1 y1 Hx1 Hy1; rewrite -contra_equiv; auto. Qed.

Lemma injS_contra_rev :
  ( x1 y1, P1 x1 P1 y1 x1 y1 f x1 f y1) injS P1 f.
Proof. intros Hf x1 y1 Hx1 Hy1; rewrite contra_equiv; auto. Qed.

Lemma injS_contra_equiv :
  injS P1 f x1 y1, P1 x1 P1 y1 x1 y1 f x1 f y1.
Proof. split; [apply injS_contra | apply injS_contra_rev]. Qed.

Lemma injS_equiv :
  injS P1 f x1 y1, P1 x1 P1 y1 f x1 = f y1 x1 = y1.
Proof. intros; split; [auto | intro; subst; easy]. Qed.

Lemma inj_S_equiv : injective f injS fullset f.
Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.

End InjS_Facts3.

Section InjS_Facts4.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Context {g h : T2 T1}.

Lemma injS_canS_uniq_l :
  injS P1 f funS P2 P1 g funS P2 P1 h
  canS P2 g f canS P2 h f same_funS P2 g h.
Proof.
intros H1 H2 H3 H4 H5 x2 Hx2; apply H1; [..| rewrite H5; auto];
    [apply H2 | apply H3]; easy.
Qed.

End InjS_Facts4.

Section InjS_Facts5.

Context {T1 T2 T3 : Type}.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Context {f : T1 T2}.

Lemma injS_comp_compat :
   {g : T2 T3},
    funS P1 P2 f injS P1 f injS P2 g injS P1 (g \o f).
Proof.
intros g Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
Qed.

Lemma injS_comp_reg : (g : T2 T3), injS P1 (g \o f) injS P1 f.
Proof.
intros g H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
Qed.

End InjS_Facts5.

Section InjS_Facts6.

Context {T1 T2 T3 : Type}.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Context {g h : T1 T2}.
Context {f : T2 T3}.

Lemma comp_injS_r :
  funS P1 P2 g funS P1 P2 h injS P2 f
  same_funS P1 (f \o g) (f \o h) same_funS P1 g h.
Proof.
moveHg Hh Hf H x1 Hx1; apply Hf, H; [apply Hg | apply Hh |]; easy.
Qed.

End InjS_Facts6.

Section SurjS_Facts1.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.

Lemma surjS_id : same_funS P f (id : T T) surjS P P f.
Proof. intros Hf y Hy; y; auto. Qed.

End SurjS_Facts1.

Section SurjS_Facts1.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma surjS_correct : incl P2 (RgS P1 f) surjS P1 P2 f.
Proof. intros H x2 Hx2; destruct (H x2 Hx2) as [x1 Hx1]; x1; easy. Qed.

Lemma surjS_rev : surjS P1 P2 f RgS_gen P1 P2 f = P2.
Proof.
intros Hf; apply incl_antisym; intros x2 Hx2; [apply Hx2 |].
destruct (Hf _ Hx2) as [x1 Hx1]; apply (RgS_gen_correct x1); easy.
Qed.

End SurjS_Facts1.

Section SurjS_Facts2.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Variable f : T1 T2.
Context {g : T1 T2}.

Lemma surjS_ext : same_funS P1 f g surjS P1 P2 f surjS P1 P2 g.
Proof.
intros Hg Hf x2 Hx2; destruct (Hf x2 Hx2) as [x1 Hx1];
     x1; rewrite -Hg; easy.
Qed.

End SurjS_Facts2.

Section SurjS_Facts3.

Context {T1 T2 : Type}.
Context {f : T1 T2}.

Lemma surj_S_equiv : surjective f surjS fullset fullset f.
Proof.
split; intros Hf.
intros x2 _; destruct (Hf x2) as [x1 Hx1]; x1; easy.
intros x2; destruct (Hf x2) as [x1 Hx1]; [| x1]; easy.
Qed.

End SurjS_Facts3.

Section SurjS_Facts4.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma surjS_RgS_gen_equiv : surjS P1 P2 f RgS_gen P1 P2 f = P2.
Proof.
split; [apply surjS_rev | move⇒ <-; apply surjS_correct, inter_lb_r].
Qed.

Lemma surjS_RgS_equiv_alt : surjS P1 P2 f incl P2 (RgS P1 f).
Proof. rewrite surjS_RgS_gen_equiv; apply RgS_gen_full_equiv. Qed.

Lemma surjS_RgS_equiv : funS P1 P2 f surjS P1 P2 f RgS P1 f = P2.
Proof.
intros Hf; rewrite -(RgS_gen_full_equiv_alt Hf); apply surjS_RgS_gen_equiv.
Qed.

Lemma surjS_RgS : P1 (f : T1 T2), surjS P1 (RgS P1 f) f.
Proof. intros; apply surjS_correct; easy. Qed.

End SurjS_Facts4.

Section SurjS_Facts5.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Context {g h : T2 T1}.

Lemma surjS_canS_uniq_r :
  surjS P1 P2 f canS P1 f g canS P1 f h same_funS P2 g h.
Proof.
intros H1 H2 H3 x2 Hx2; destruct (H1 _ Hx2) as [x1 [Hx1 <-]]; rewrite H3; auto.
Qed.

End SurjS_Facts5.

Section SurjS_Facts6.

Context {T1 T2 T3 : Type}.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Context {P3 : T3 Prop}.
Context {f : T1 T2}.
Context {g : T2 T3}.

Lemma surjS_comp_compat :
  surjS P1 P2 f surjS P2 P3 g surjS P1 P3 (g \o f).
Proof.
intros Hf Hg x3 Hx3;
    destruct (Hg _ Hx3) as [x2 [Hx2a Hx2b]], (Hf _ Hx2a) as [x1 [Hx1a Hx1b]].
x1; split; [| rewrite comp_correct Hx1b]; easy.
Qed.

End SurjS_Facts6.

Section SurjS_Facts7.

Context {T1 T2 T3 : Type}.
Variable P1 : T1 Prop.
Context {P2 : T2 Prop}.
Context {P3 : T3 Prop}.
Variable f : T1 T2.
Context {g : T2 T3}.

Lemma surjS_comp_reg : funS P1 P2 f surjS P1 P3 (g \o f) surjS P2 P3 g.
Proof.
intros Hf H x3 Hx3; destruct (H _ Hx3) as [x1 [Hx1a Hx1b]].
(f x1); split; [apply Hf |]; easy.
Qed.

End SurjS_Facts7.

Section CanS_Facts1.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.

Lemma canS_id_l : same_funS P f (id : T T) canS P f id.
Proof. easy. Qed.

Lemma canS_id_r : same_funS P f (id : T T) canS P id f.
Proof. easy. Qed.

End CanS_Facts1.

Section CanS_Facts2.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f f' : T1 T2}.
Context {g g' : T2 T1}.

Lemma canS_ext_l : same_funS P1 f f' canS P1 f g canS P1 f' g.
Proof. intros Hf H x1 Hx1; rewrite -Hf//; auto. Qed.

Lemma canS_ext_r :
  funS P1 P2 f same_funS P2 g g' canS P1 f g canS P1 f g'.
Proof. intros Hf Hg H x1 Hx1; rewrite -Hg//; [apply H | apply Hf]; easy. Qed.

End CanS_Facts2.

Section CanS_Facts3.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f f' : T1 T2}.
Context {g g' : T2 T1}.

Lemma canS_ext :
  funS P1 P2 f same_funS P1 f f' same_funS P2 g g'
  canS P1 f g canS P1 f' g'.
Proof. moveH1 H2 H3 /(canS_ext_r H1 H3) /(canS_ext_l H2); easy. Qed.

End CanS_Facts3.

Section CanS_Facts4.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma canS_injS : (g : T2 T1), canS P1 f g injS P1 f.
Proof. moveg H x1 y1 Hx1 Hy1 /(f_equal g); rewrite !H; easy. Qed.

Lemma injS_has_left_inv : inhabited T1 injS P1 f g, canS P1 f g.
Proof.
intros [a1]; split; [intros Hf | intros [g Hg]; apply (canS_injS g), Hg].
(fun x2match imS_dec P1 f x2 with
  | inleft H1proj1_sig H1
  | inright _a1
  end).
intros y1 Hy1; destruct (imS_dec P1 f (f y1)) as [[x1 [Hx1 H1]] | H1].
simpl; apply Hf; easy.
contradict H1; rewrite not_all_ex_not_equiv;
     y1; rewrite not_imp_not_r_and_equiv; easy.
Qed.

Lemma canS_surjS :
   (g : T2 T1), funS P2 P1 g canS P2 g f surjS P1 P2 f.
Proof.
intros g Hg H x2 Hx2; (g x2); split; [apply Hg | rewrite H]; easy.
Qed.

Lemma surjS_has_right_inv :
  inhabited T1 surjS P1 P2 f g, funS P2 P1 g canS P2 g f.
Proof.
intros [a1]; split; [| intros [g Hg]; apply (canS_surjS g); easy].
intros Hf; (fun x2match imS_dec P1 f x2 with
  | inleft H1proj1_sig H1
  | inright _a1
  end); split; [intros y1 [x2 Hx2] | intros x2 Hx2];
    (destruct (imS_dec P1 f x2) as [[x1 Hx1] | H1]; [easy |]).
1,2: contradict H1; rewrite not_all_ex_not_equiv;
    destruct (Hf _ Hx2) as [x1 Hx1];
     x1; rewrite not_imp_not_r_and_equiv; easy.
Qed.

End CanS_Facts4.

Section CanS_Facts5.

Context {T1 T2 : Type}.
Variable P1 : T1 Prop.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Context {g : T2 T1}.

Lemma injS_canS_sym :
  funS P1 P2 f funS P2 P1 g injS P2 g canS P1 f g canS P2 g f.
Proof.
intros H1 H2 H3 H4 x2 Hx2;
    apply H3; [apply H1, Im | easy | rewrite H4//]; apply H2; easy.
Qed.

End CanS_Facts5.

Section CanS_Facts6.

Context {T1 T2 T3 : Type}.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Context {f : T1 T2}.
Context {f1 : T2 T1}.
Context {g : T2 T3}.
Context {g1 : T3 T2}.

Lemma canS_comp_compat :
  funS P1 P2 f canS P1 f f1 canS P2 g g1 canS P1 (g \o f) (f1 \o g1).
Proof.
move⇒ /funS_equiv H1 H2 H3 x1 Hx1; rewrite → !comp_correct, H3, H2; auto.
Qed.

End CanS_Facts6.

Section InvolS_Facts.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.

Lemma involS_injS : involS P f injS P f.
Proof. apply canS_injS. Qed.

Lemma involS_bijS : funS P P f involS P f bijS P P f.
Proof. intros; apply (BijS f); repeat split; easy. Qed.

End InvolS_Facts.

Section BijS_Facts1.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.

Lemma bijS_id : same_funS P f (id : T T) bijS P P f.
Proof.
intros; apply (BijS id); repeat split;
    [apply funS_id.. | apply canS_id_l | apply canS_id_r]; easy.
Qed.

End BijS_Facts1.

Section BijS_Facts2.

Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Variable f : T1 T2.
Context {g : T1 T2}.

Lemma bijS_ext : same_funS P1 f g bijS P1 P2 f bijS P1 P2 g.
Proof.
moveHg /bijS_EX [f1 [Hf1 [Hf2 [Hf3 Hf4]]]];
    apply bijS_ex; f1; repeat split; [| easy |..].
apply (funS_ext f), Hf1; easy.
apply (canS_ext_l Hg Hf3).
apply (canS_ext_r Hf2 Hg Hf4).
Qed.

End BijS_Facts2.

Section BijS_Facts3.

Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma bijS_ex_uniq :
  bijS P1 P2 f
  funS P1 P2 f ( x2, P2 x2 ! x1, P1 x1 f x1 = x2).
Proof.
clear HT1; move⇒ [g [H1 [/funS_equiv H2 [H3 H4]]]]; split; [easy |].
intros x2 Hx2; (g x2); repeat split; auto.
movex1 [Hx1 <-]; auto.
Qed.

Lemma bijS_ex_uniq_rev :
  funS P1 P2 f ( x2, P2 x2 ! x1, P1 x1 f x1 = x2)
  bijS P1 P2 f.
Proof.
intros H1 H2.
destruct (choice (fun x2 x1P2 x2 P1 x1 f x1 = x2)) as [g Hg].
  intros x2; destruct (in_dec P2 x2) as [Hx2 | Hx2].
  destruct (H2 x2 Hx2) as [x1 [Hx1a Hx1b]]; x1; easy.
  destruct HT1 as [x1]; x1; easy.
apply (BijS g); repeat split; [easy |..].
intros _ [x2 Hx2]; apply Hg; easy.
2: intros x2 Hx2; apply Hg; easy.
assert (H3 : injS P1 f).
  intros x1 x2 Hx1 Hx2 Hx.
  destruct (H2 (f x1)) as [y1 [Hy1a Hy1b]]; [apply H1; easy |].
  rewrite -(Hy1b x1); [apply Hy1b |]; easy.
rewrite funS_equiv in H1.
intros x1 Hx1; apply H3; try apply Hg; auto.
Qed.

Lemma bijS_ex_uniq_equiv :
  bijS P1 P2 f
  funS P1 P2 f ( x2, P2 x2 ! x1, P1 x1 f x1 = x2).
Proof. split; [apply bijS_ex_uniq | intros; apply bijS_ex_uniq_rev; easy]. Qed.

End BijS_Facts3.

Section BijS_Facts4.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma bijS_RgS : bijS P1 P2 f RgS P1 f = P2.
Proof.
intros [g [Hf [Hg [H1 H2]]]]; apply subset_ext_equiv; split; [easy |].
intros x2 Hx2; rewrite -(H2 _ Hx2); apply Im, Hg; easy.
Qed.

Lemma bijS_funS : bijS P1 P2 f funS P1 P2 f.
Proof. intros [g Hg]; apply Hg. Qed.

Lemma bijS_injS : P2 {f : T1 T2}, bijS P1 P2 f injS P1 f.
Proof.
move=>> [g [Hf [_ [Hg _]]]] x1 y1 Hx1 Hy1 H1;
    rewrite -(Hg x1)// -(Hg y1)// H1; easy.
Qed.

Lemma bijS_surjS : bijS P1 P2 f surjS P1 P2 f.
Proof. move⇒ [g [_ [/funS_equiv Hg [_ Hf]]]] x2 Hx2; (g x2); auto. Qed.

End BijS_Facts4.

Section BijS_Facts5.

Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.

Lemma injS_surjS_bijS :
  funS P1 P2 f injS P1 f surjS P1 P2 f bijS P1 P2 f.
Proof.
moveH1 H2 H3; apply bijS_ex_uniq_rev; [easy.. |].
intros x2 Hx2; destruct (H3 _ Hx2) as [x1 Hx1]; x1; split; [easy |].
intros y1 Hy1; apply H2; [..| apply trans_eq with x2]; easy.
Qed.

Lemma bijS_equiv : bijS P1 P2 f funS P1 P2 f injS P1 f surjS P1 P2 f.
Proof.
split; intros Hf; [split; [apply bijS_funS; easy |] |].
split; [apply (bijS_injS P2) | apply bijS_surjS]; easy.
apply injS_surjS_bijS; easy.
Qed.

End BijS_Facts5.

Section BijS_Facts6.

Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.
Context {P1 : T1 Prop}.
Context {f : T1 T2}.

Lemma bijS_RgS_equiv : bijS P1 (RgS P1 f) f injS P1 f.
Proof.
rewrite bijS_equiv//; split; [easy |].
intros; repeat split; [| | apply surjS_RgS]; easy.
Qed.

Lemma bij_S_equiv : bijective f bijS fullset fullset f.
Proof. rewrite bij_equiv bijS_equiv// inj_S_equiv surj_S_equiv; easy. Qed.

End BijS_Facts6.

Section BijS_Facts7.

Context {T1 T2 T3 : Type}.
Hypothesis HT1 : inhabited T1.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Context {P3 : T3 Prop}.
Context {f : T1 T2}.
Context {g : T2 T3}.

Lemma bijS_spec_comp_compat :
   {f1 g1},
    bijS_spec P1 P2 f f1 bijS_spec P2 P3 g g1
    bijS_spec P1 P3 (g \o f) (f1 \o g1).
Proof.
intros f1 g1 [Hf1 [Hf2 [Hf3 Hf4]]] [Hg1 [Hg2 [Hg3 Hg4]]]; repeat split.
1,2: apply (funS_comp_compat P2); easy.
1,2: apply (canS_comp_compat P2); easy.
Qed.

Lemma bijS_comp_compat : bijS P1 P2 f bijS P2 P3 g bijS P1 P3 (g \o f).
Proof.
intros [f1 Hf] [g1 Hg]; (f1 \o g1); apply bijS_spec_comp_compat; easy.
Qed.

End BijS_Facts7.

Section BijS_Facts8.

Context {T1 T2 T3 : Type}.
Hypothesis HT1 : inhabited T1.
Context {P1 : T1 Prop}.
Variable P2 : T2 Prop.
Variable P3 : T3 Prop.
Context {f : T1 T2}.
Variable g : T2 T3.

Lemma bijS_comp_injS : funS P1 P2 f bijS P1 P3 (g \o f) injS P1 f.
Proof.
intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) ⇒ [_ [H3 _]].
apply injS_comp_reg with g; easy.
Qed.

End BijS_Facts8.

Section BijS_Facts9.

Context {T1 T2 T3 : Type}.
Hypothesis HT1 : inhabited T1.
Variable P1 : T1 Prop.
Context {P2 : T2 Prop}.
Context {P3 : T3 Prop}.
Variable f : T1 T2.
Context {g : T2 T3}.

Lemma bijS_comp_surjS : funS P1 P2 f bijS P1 P3 (g \o f) surjS P2 P3 g.
Proof.
intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) ⇒ [_ [_ H3]].
apply (surjS_comp_reg P1 f); easy.
Qed.

End BijS_Facts9.

Section BijS_FactsA.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Context {g h : T2 T1}.

Lemma bijS_canS_uniq_l :
  bijS P1 P2 f funS P2 P1 g funS P2 P1 h
  canS P2 g f canS P2 h f same_funS P2 g h.
Proof. move⇒ /bijS_injS; apply injS_canS_uniq_l. Qed.

Lemma bijS_canS_uniq_r :
  bijS P1 P2 f canS P1 f g canS P1 f h same_funS P2 g h.
Proof. move⇒ /bijS_surjS; apply surjS_canS_uniq_r. Qed.

End BijS_FactsA.

Section BijS_FactsB.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Context {g : T2 T1}.

Lemma bijS_canS_sym : bijS P1 P2 f canS P1 f g funS P2 P1 g canS P2 g f.
Proof.
intros Hf; move: (bijS_EX Hf) ⇒ [f1 [H1 [H2 [H3 H4]]]]; split.
intros H5; split.
apply: (funS_ext f1 _ H2); apply (bijS_canS_uniq_r Hf H3 H5).
intros x2 Hx2; rewrite (bijS_canS_uniq_r Hf H5 H3); auto.
intros [H5 H6] x1 Hx1; rewrite (bijS_canS_uniq_l Hf H5 H2 H6 H4);
    [apply H3 | apply H1]; easy.
Qed.

Lemma bijS_canS_bijS : canS P1 f g bijS P1 P2 f bijS P2 P1 g.
Proof.
intros Hg Hf; apply bijS_ex; f; repeat split; [.. | easy].
1,3: apply (bijS_canS_sym Hf), Hg.
apply (bijS_funS Hf).
Qed.

End BijS_FactsB.

Section F_invS_Def.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Hypothesis Hf : bijS P1 P2 f.

Definition f_invS : T2 T1 := proj1_sig (bijS_EX Hf).

Lemma f_invS_funS_l : funS P1 P2 f.
Proof. apply (proj2_sig (bijS_EX Hf)). Qed.

Lemma f_invS_funS_r : funS P2 P1 f_invS.
Proof. apply (proj2_sig (bijS_EX Hf)). Qed.

Lemma f_invS_canS_l : canS P1 f f_invS.
Proof. apply (proj2_sig (bijS_EX Hf)). Qed.

Lemma f_invS_canS_r : canS P2 f_invS f.
Proof. apply (proj2_sig (bijS_EX Hf)). Qed.

End F_invS_Def.

Section F_invS_Facts1.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f : T1 T2}.
Hypothesis Hf : bijS P1 P2 f.

Lemma f_invS_uniq_l :
   (g : T2 T1), canS P1 f g same_funS P2 g (f_invS Hf).
Proof. move=>> H; apply (bijS_canS_uniq_r Hf H), f_invS_canS_l. Qed.

Lemma f_invS_uniq_r :
   (g : T2 T1),
    funS P2 P1 g canS P2 g f same_funS P2 g (f_invS Hf).
Proof.
move=>> Hg H; apply: (bijS_canS_uniq_l Hf Hg _ H);
    [apply f_invS_funS_r | apply f_invS_canS_r].
Qed.

Lemma f_invS_bijS : bijS P2 P1 (f_invS Hf).
Proof. apply: (bijS_canS_bijS _ Hf); apply f_invS_canS_l. Qed.

Lemma f_invS_injS : injS P2 (f_invS Hf).
Proof. apply (bijS_injS P1), f_invS_bijS. Qed.

Lemma f_invS_surjS : surjS P2 P1 (f_invS Hf).
Proof. apply bijS_surjS, f_invS_bijS. Qed.

Lemma f_invS_eq_equiv :
   x1 x2, P1 x1 P2 x2 x1 = f_invS Hf x2 f x1 = x2.
Proof.
intros x1 x2 Hx1 Hx2; split.
rewrite -{2}(f_invS_canS_r Hf x2 Hx2); apply f_equal.
rewrite -{2}(f_invS_canS_l Hf x1 Hx1); apply f_equal.
Qed.

Lemma f_invS_neq_equiv :
   x1 x2, P1 x1 P2 x2 x1 f_invS Hf x2 f x1 x2.
Proof. intros; rewrite -iff_not_equiv; apply f_invS_eq_equiv; easy. Qed.

End F_invS_Facts1.

Section F_invS_Facts2.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.
Context {f g : T1 T2}.
Hypothesis Hf : bijS P1 P2 f.
Hypothesis Hg : bijS P1 P2 g.

Lemma f_invS_ext : same_funS P1 f g same_funS P2 (f_invS Hf) (f_invS Hg).
Proof.
intros H x2 Hx2; apply (bijS_injS P2 Hf).
3: rewrite → (H (f_invS Hg _)), !f_invS_canS_r; [easy.. |].
apply (f_invS_funS_r Hf (f_invS Hf x2)); easy.
1,2: apply (f_invS_funS_r Hg (f_invS Hg x2)); easy.
Qed.

Lemma f_invS_invol :
   (Hf1 : bijS P2 P1 (f_invS Hf)), same_funS P1 (f_invS Hf1) f.
Proof. intros; apply same_funS_sym, f_invS_uniq_l, f_invS_canS_r. Qed.

Lemma f_invS_invol_alt : same_funS P1 (f_invS (f_invS_bijS Hf)) f.
Proof. apply f_invS_invol. Qed.

End F_invS_Facts2.

Section F_invS_Facts3.

Context {T : Type}.
Context {P : T Prop}.
Context {f : T T}.
Hypothesis Hf : bijS P P f.

Lemma f_invS_id : involS P f same_funS P (f_invS Hf) f.
Proof.
intros Hf1; apply: (comp_injS_r _ _ _ (bijS_injS _ Hf)).
apply f_invS_funS_r.
apply f_invS_funS_l, Hf.
intros x Hx; rewrite !comp_correct f_invS_canS_r// Hf1; easy.
Qed.

Lemma f_invS_id_rev : same_funS P (f_invS Hf) f involS P f.
Proof. intros H x Hx; rewrite -(H x Hx) f_invS_canS_r; easy. Qed.

Lemma f_invS_id_equiv : same_funS P (f_invS Hf) f involS P f.
Proof. split; [apply f_invS_id_rev | apply f_invS_id]. Qed.

End F_invS_Facts3.