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.
Support for restrictions of functions to subsets represented by predicates.
Let f : T1 → T2 for any types T1 and T2.
Let P1 and P2 respectively be subsets of T1 and T2.
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
- 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
- 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 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; move⇒ g /(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. move⇒ Hg 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.
move⇒ Hg 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. move⇒ H1 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. move⇒ g 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 x2 ⇒ match imS_dec P1 f x2 with
| inleft H1 ⇒ proj1_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 x2 ⇒ match imS_dec P1 f x2 with
| inleft H1 ⇒ proj1_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.
move⇒ Hg /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.
move⇒ x1 [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 x1 ⇒ P2 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.
move⇒ H1 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.