From a502ec946e73b189c9c8ef87290119dfcfc29284 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 17 Jun 2022 17:31:44 +0200
Subject: [PATCH] WIP: use compose*.

---
 Lebesgue/Set_theory/Set_base.v | 136 +++------------------------------
 1 file changed, 12 insertions(+), 124 deletions(-)

diff --git a/Lebesgue/Set_theory/Set_base.v b/Lebesgue/Set_theory/Set_base.v
index 6c383cfb..2e6cbbe3 100644
--- a/Lebesgue/Set_theory/Set_base.v
+++ b/Lebesgue/Set_theory/Set_base.v
@@ -18,7 +18,7 @@ COPYING file for more details.
 
 From Coq Require Import ClassicalChoice.
 
-Require Import Set_def.
+Require Import Set_def Set_fun.
 
 
 Section Prop_Facts0a.
@@ -105,20 +105,27 @@ Variable A : set U.
 
 (** Correctness results. *)
 
-Lemma lift_trace : forall (B : set U), lift A (trace A B) = inter A B.
+Lemma lift_trace : compose (lift A) (trace A) = inter A.
 Proof.
-intros; apply set_ext_equiv; split; intros x [HAx HBx].
+apply fun_ext; intros B; apply set_ext_equiv; split; intros x [HAx HBx].
 split; auto.
 apply Lft with HAx; easy.
 Qed.
 
-Lemma trace_lift : forall (BA : subset A), trace A (lift A BA) = BA.
+Lemma trace_lift : compose (trace A) (lift A) = id.
 Proof.
-intros; apply set_ext_equiv; split; intros [x HAx] HBx.
+apply fun_ext; intros BA; apply set_ext_equiv; split; intros [x HAx] HBx.
 destruct HBx as [HAx' HBx]; rewrite (proof_irrelevance _ _ HAx'); easy.
 apply Lft with HAx; easy.
 Qed.
 
+Lemma lift_trace_lift : compose3 (lift A) (trace A) (lift A) = lift A.
+Proof.
+unfold compose3; rewrite trace_lift.
+
+intros; rewrite trace_lift; easy.
+Qed.
+
 Lemma lift_trace_lift :
   forall (BA : subset A), lift A (trace A (lift A BA)) = lift A BA.
 Proof.
@@ -2486,83 +2493,11 @@ Qed.
 End Prod_Facts.
 
 
-Section Fun_Facts0.
-
-Context {U1 U2 : Type}.
-
-(** Facts about same_fun. *)
-
-(** It is an equivalence binary relation. *)
-
-(* Useless?
-Lemma same_fun_refl :
-  forall (f : U1 -> U2),
-    same_fun f f.
-Proof.
-easy.
-Qed.
-*)
-
-(* Useful? *)
-Lemma same_fun_sym :
-  forall (f g : U1 -> U2),
-    same_fun f g -> same_fun g f.
-Proof.
-easy.
-Qed.
-
-Lemma same_fun_trans :
-  forall (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.
-
-End Fun_Facts0.
-
-
 Section Fun_Facts1a.
 
 Context {U1 U2 : Type}.
 Variable f : U1 -> U2.
 
-(** Facts about injective*/surjective/bijective. *)
-
-Lemma injective_equiv : injective f <-> injective_alt f.
-Proof.
-split; intros Hf x1 y1 H1; auto.
-destruct (classic (x1 = y1)) as [H2 | H2]; try easy.
-contradict H1; auto.
-Qed.
-
-Lemma bijective_equiv : bijective f <-> bijective_alt f.
-Proof.
-split.
-(* *)
-intros [Hf1 Hf2] x2; destruct (Hf2 x2) as [x1 Hx1]; exists x1; split; try easy.
-intros y1 Hy1; apply Hf1; rewrite Hy1; easy.
-(* *)
-intros Hf; split.
-intros x1 y1 H1; destruct (Hf (f y1)) as [z1 [_ Hz1]]; apply eq_trans with z1;
-  [symmetry | ]; apply Hz1; easy.
-intros x2; destruct (Hf x2) as [x1 [Hx1 _]]; exists x1; easy.
-Qed.
-
-Lemma bijective_equiv_fun :
-  bijective f <->
-  exists g, (forall z1, compose g f z1 = z1) /\ (forall z2, compose f g z2 = z2).
-Proof.
-unfold compose; split.
-(* *)
-intros [Hf1 Hf2]; destruct (choice _ Hf2) as [g Hg].
-exists g; split; try easy.
-intros x1; apply Hf1; rewrite Hg; easy.
-(* *)
-intros [g [Hg1 Hg2]]; split.
-intros x1 y1 H1; rewrite <- (Hg1 x1), <- (Hg1 y1); f_equal; easy.
-intros x2; exists (g x2); auto.
-Qed.
-
 (** Facts about image. *)
 
 Lemma image_empty_equiv :
@@ -2784,50 +2719,3 @@ intros [A2 HA2]; rewrite <- HA2; apply preimage_of_image_of_preimage.
 Qed.
 
 End Fun_Facts2.
-
-
-Section Fun_Facts3.
-
-(** Facts about composition of functions. *)
-
-Context {U1 U2 U3 U4 : Type}.
-Variable f12 : U1 -> U2.
-Variable f23 : U2 -> U3.
-Variable f34 : U3 -> U4.
-
-(* Useful? *)
-Lemma compose_assoc :
-  compose f34 (compose f23 f12) = compose (compose f34 f23) f12.
-Proof.
-easy.
-Qed.
-
-Lemma image_compose_fun :
-  image (compose f23 f12) = fun A1 => image f23 (image f12 A1).
-Proof.
-apply fun_ext; intros A1; apply set_ext_equiv; split; intros x3 Hx3.
-induction Hx3 as [x1 Hx1]; easy.
-induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
-replace (f23 (f12 x1)) with (compose f23 f12 x1); easy.
-Qed.
-
-Lemma image_compose :
-  forall A1, image (compose f23 f12) A1 = image f23 (image f12 A1).
-Proof.
-rewrite image_compose_fun; easy.
-Qed.
-
-(* Useful? *)
-Lemma preimage_compose_fun :
-  preimage (compose f23 f12) = fun A3 => preimage f12 (preimage f23 A3).
-Proof.
-easy.
-Qed.
-
-Lemma preimage_compose :
-  forall A3, preimage (compose f23 f12) A3 = preimage f12 (preimage f23 A3).
-Proof.
-easy.
-Qed.
-
-End Fun_Facts3.
-- 
GitLab