Skip to content
Snippets Groups Projects
Commit e40ecd39 authored by François Clément's avatar François Clément
Browse files

Mv stuff around (reorganize sections per properties). 

Rename cancel_id -> can_equiv.
Add and prove comp_id, can_id.
parent 5e2bb9c0
No related branches found
No related tags found
No related merge requests found
Pipeline #7167 waiting for manual action
Stage: test
Hide whitespace changes
Inline Side-by-side
FEM/Compl/Function_compl.v
+ 142
− 139
View file @ e40ecd39
......@@ -120,25 +120,19 @@ Proof. intros [x1] HT2 [h]; contradict HT2; apply (inhabits (h x1)). Qed.
End Inhabited_Facts.
Section Swap_Def.
Section Image_preimage_Facts0.
Context {T1 T2 T3 : Type}.
Variable f : T1 -> T2 -> T3.
Definition swap : T2 -> T1 -> T3 := fun x2 x1 => f x1 x2.
End Swap_Def.
Section Swap_Facts.
Context {T1 T2 : Type}.
Context {T1 T2 T3 : Type}.
Variable f : T1 -> T2 -> T3.
Variable f : T1 -> T2.
Lemma swap_invol : swap (swap f) = f.
Proof. easy. Qed.
Lemma im_dec : forall x2, { x1 | f x1 = x2 } + { forall x1, f x1 <> x2 }.
Proof.
intros x2; destruct (in_dec (fun x2 => exists x1, f x1 = x2) x2) as [H1 | H1];
[left; apply ex_EX | right; apply not_ex_all_not]; easy.
Qed.
End Swap_Facts.
End Image_preimage_Facts0.
Section Image_preimage_Facts1.
......@@ -202,145 +196,116 @@ Qed.
End Image_preimage_Facts3.
Section Range_Def.
Section Comp_Facts1.
Context {T1 T2 : Type}.
Context {T1 T2 T3 T4 : Type}.
Variable f : T1 -> T2.
Variable g : T2 -> T3.
Variable h : T3 -> T4.
Definition Rg : T2 -> Prop := image f fullset.
Lemma comp_correct : forall x1, (g \o f) x1 = g (f x1).
Proof. easy. Qed.
(* There is an alternate form: "forall x2, exists x1, x2 = f x1", but we choose
the one compatible with cancel, eg. when "x1" is "g x2" for some "g".
Note that one can rewrite "x2" with both. *)
Definition surjective : Prop := forall x2, exists x1, f x1 = x2.
Lemma comp_assoc : h \o (g \o f) = (h \o g) \o f.
Proof. easy. Qed.
End Range_Def.
End Comp_Facts1.
Section Range_Facts1.
Section Comp_Facts2.
Context {T1 T2 : Type}.
Context {f : T1 -> T2}.
Variable f : T1 -> T2.
Lemma Rg_correct : forall {x2} x1, f x1 = x2 -> Rg f x2.
Proof. move=> x2 x1 <-; easy. Qed.
Lemma comp_id_l : id \o f = f.
Proof. easy. Qed.
Lemma Rg_ex : forall {x2}, Rg f x2 <-> exists x1, f x1 = x2.
Proof. intros; split; [intros [x1 _]; exists x1 | move=> [x1 <-]]; easy. Qed.
Lemma comp_id_r : f \o id = f.
Proof. easy. Qed.
Lemma Rg_compl : forall {x2}, ~ Rg f x2 <-> forall x1, f x1 <> x2.
Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.
Lemma comp_id : forall {T : Type}, id \o id = (id : T -> T).
Proof. easy. Qed.
Lemma Rg_full_equiv : Rg f = fullset <-> incl fullset (Rg f).
Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.
End Comp_Facts2.
Lemma surj_correct : incl fullset (Rg f) -> surjective f.
Proof. intros Hf y; destruct (Hf y) as [x Hx]; [| exists 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.
Section Comp_Facts3.
Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
Context {T1 T2 T3 : Type}.
Context {f : T2 -> T3}.
Hypothesis Hf : injective f.
Lemma surj_can_uniq_r :
forall {g h : T2 -> T1}, 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 comp_inj_r : forall {g h : T1 -> T2}, f \o g = f \o h -> g = h.
Proof. move=>> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
End Range_Facts1.
End Comp_Facts3.
Section Range_Facts2.
Section Fun_Def.
Context {T1 T2 T3 : Type}.
Context {f : T1 -> T2}.
Context {g : T2 -> T3}.
Lemma preimage_Rg : preimage f (Rg f) = fullset.
Proof. apply preimage_of_image_full. Qed.
Definition swap (f : T1 -> T2 -> T3) : T2 -> T1 -> T3 := fun x2 x1 => f x1 x2.
Lemma Rg_comp : Rg (g \o f) = image g (Rg f).
Proof.
apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
intros _ [_ [x1 _]]; apply: Im; easy.
Qed.
Definition Rg (f : T1 -> T2) : T2 -> Prop := image f fullset.
End Range_Facts2.
(* There is an alternate form: "forall x2, exists x1, x2 = f x1", but we choose
the one compatible with cancel, eg. when "x1" is "g x2" for some "g".
Note that one can rewrite "x2" with both. *)
Definition surjective (f : T1 -> T2) : Prop := forall x2, exists x1, f x1 = x2.
End Fun_Def.
Section Comp_Facts1.
Context {T1 T2 T3 T4 : Type}.
Variable f : T1 -> T2.
Variable g : T2 -> T3.
Variable h : T3 -> T4.
Section Swap_Facts.
Lemma comp_correct : forall x1, (g \o f) x1 = g (f x1).
Proof. easy. Qed.
Context {T1 T2 T3 : Type}.
Variable f : T1 -> T2 -> T3.
Lemma comp_assoc : h \o (g \o f) = (h \o g) \o f.
Lemma swap_invol : swap (swap f) = f.
Proof. easy. Qed.
End Comp_Facts1.
End Swap_Facts.
Section Comp_Facts2.
Section Range_Facts.
Context {T1 T2 : Type}.
Context {T1 T2 T3 : Type}.
Context {f : T1 -> T2}.
Context {g : T2 -> T1}.
Lemma cancel_id : 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; exists (g x1); easy. Qed.
End Comp_Facts2.
Section Comp_Facts3.
Context {T1 T2 : Type}.
Variable f : T1 -> T2.
Lemma comp_id_l : id \o f = f.
Proof. easy. Qed.
Context {g : T2 -> T3}.
Lemma comp_id_r : f \o id = f.
Proof. easy. Qed.
Lemma Rg_correct : forall {x2} x1, f x1 = x2 -> Rg f x2.
Proof. move=> x2 x1 <-; easy. Qed.
End Comp_Facts3.
Lemma Rg_ex : forall {x2}, Rg f x2 <-> exists x1, f x1 = x2.
Proof. intros; split; [intros [x1 _]; exists x1 | move=> [x1 <-]]; easy. Qed.
Lemma Rg_compl : forall {x2}, ~ Rg f x2 <-> forall x1, f x1 <> x2.
Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.
Section Comp_Facts4.
Lemma Rg_full_equiv : Rg f = fullset <-> incl fullset (Rg f).
Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.
Context {T1 T2 T3 : Type}.
Context {f : T2 -> T3}.
Hypothesis Hf : injective f.
Lemma preimage_Rg : preimage f (Rg f) = fullset.
Proof. apply preimage_of_image_full. Qed.
Lemma comp_inj_r : forall {g h : T1 -> T2}, f \o g = f \o h -> g = h.
Proof. move=>> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
Lemma Rg_comp : Rg (g \o f) = image g (Rg f).
Proof.
apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
intros _ [_ [x1 _]]; apply: Im; easy.
Qed.
End Comp_Facts4.
End Range_Facts.
Section Injective_Facts.
Section Inj_Facts.
Context {T1 T2 : Type}.
Context {f : T1 -> T2}.
Lemma fun_from_empty_is_inj : ~ inhabited T1 -> injective f.
Proof. move=>> HT1 x1; contradict HT1; easy. Qed.
Lemma inj_contra : injective f -> forall x1 y1, x1 <> y1 -> f x1 <> f y1.
Proof. intros Hf x1 y1; rewrite -contra_equiv; apply Hf. Qed.
......@@ -354,43 +319,91 @@ Proof. split; [apply inj_contra | apply inj_contra_rev]. Qed.
Lemma inj_equiv : injective f -> forall x1 y1, f x1 = f y1 <-> x1 = y1.
Proof. intros Hf x1 y1; split; [apply Hf | apply f_equal]. Qed.
End Injective_Facts.
Lemma inj_has_left_inv : inhabited T1 -> injective f <-> exists g, cancel f g.
Proof.
intros [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
exists (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; exists x1]; easy.
Qed.
End Inj_Facts.
Section Inj_surj_bij_Facts1.
Section Surj_Facts.
Context {T1 T2 : Type}.
Context {f : T1 -> T2}.
Lemma fun_from_empty_is_inj :
forall (f : T1 -> T2), ~ inhabited T1 -> injective f.
Proof. move=>> HT1 x1; contradict HT1; easy. Qed.
Lemma surj_correct : incl fullset (Rg f) -> surjective f.
Proof. intros Hf y; destruct (Hf y) as [x Hx]; [| exists 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 im_dec :
forall (f : T1 -> T2) x2, { x1 | f x1 = x2 } + { forall x1, f x1 <> x2 }.
Lemma surj_equiv : surjective f <-> Rg f = fullset.
Proof.
intros f x2; destruct (in_dec (fun x2 => exists x1, f x1 = x2) x2) as [H1 | H1];
[left; apply ex_EX | right; apply not_ex_all_not]; easy.
split; [apply surj_rev | intros Hf; apply surj_correct; rewrite Hf]; easy.
Qed.
Lemma inj_has_left_inv :
forall {f : T1 -> T2}, inhabited T1 -> injective f <-> exists g, cancel f g.
Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
Lemma surj_id : forall {T : Type}, surjective (id : T -> T).
Proof. intros T x; exists x; easy. Qed.
End Surj_Facts.
Section Can_Facts1.
Context {T1 T2 : Type}.
Context {f : T1 -> T2}.
Context {g : T2 -> T1}.
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; exists (g x1); easy. Qed.
Lemma can_id : forall {T : Type}, cancel (id : T -> T) id.
Proof. easy. Qed.
End Can_Facts1.
Section Can_Facts2.
Context {T1 T2 : Type}.
Context {f : T1 -> T2}.
Lemma surj_can_uniq_r :
forall {g h : T2 -> T1}, surjective f -> cancel f g -> cancel f h -> g = h.
Proof.
intros f [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
exists (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; exists x1]; easy.
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 :
forall {f : T1 -> T2}, surjective f <-> exists g, cancel g f.
Lemma surj_has_right_inv : surjective f <-> exists g, cancel g f.
Proof.
intros; apply iff_sym; split; [intros [g Hg]; eapply can_surj, Hg |].
apply iff_sym; split; [intros [g Hg]; apply: can_surj Hg |].
intros Hf; destruct (choice _ Hf) as [g Hg]; exists g; easy.
Qed.
End Can_Facts2.
Section Bij_Facts.
Context {T1 T2 : Type}.
Lemma bij_surj : forall (f : T1 -> T2), bijective f -> surjective f.
Proof. intros f [g _ H] x2; exists (g x2); rewrite H; easy. Qed.
......@@ -416,20 +429,10 @@ intros x1 y1 H1; destruct (Hf (f x1)) as [x2 [Hx2a Hx2b]].
rewrite -(Hx2b x1); [apply Hx2b, eq_sym |]; easy.
Qed.
End Inj_surj_bij_Facts1.
Section Inj_surj_bij_Facts2.
Context {T : Type}.
Lemma surj_id : surjective (@id T).
Proof. intros x; exists x; easy. Qed.
Lemma bij_id : bijective (@id T).
Proof. apply bij_equiv; split; [apply inj_id | apply surj_id]. Qed.
Lemma bij_id : forall {T : Type}, bijective (id : T -> T).
Proof. intros; apply (Bijective can_id); easy. Qed.
End Inj_surj_bij_Facts2.
End Bij_Facts.
Section Inverse_Def.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment