From 30b42da59218e47cbf1326b748117f1c6bb32b48 Mon Sep 17 00:00:00 2001
From: CLEMENT Francois <francois.clement@inria.fr>
Date: Tue, 21 Sep 2021 16:04:09 +0200
Subject: [PATCH] FC: suppress _aux suffixes of (used) definitions, add prime
 suffix to corresponding unsuffixed (unused) lemmas.

---
 Lebesgue/bochner_integral/BInt_Bif.v    |  8 ++--
 Lebesgue/bochner_integral/BInt_LInt_p.v |  6 +--
 Lebesgue/bochner_integral/BInt_sf.v     | 22 +++++-----
 Lebesgue/bochner_integral/Bi_fun.v      |  2 +-
 Lebesgue/bochner_integral/simpl_fun.v   | 56 ++++++++++++-------------
 5 files changed, 47 insertions(+), 47 deletions(-)

diff --git a/Lebesgue/bochner_integral/BInt_Bif.v b/Lebesgue/bochner_integral/BInt_Bif.v
index fc9792e2..f90506e8 100644
--- a/Lebesgue/bochner_integral/BInt_Bif.v
+++ b/Lebesgue/bochner_integral/BInt_Bif.v
@@ -110,8 +110,8 @@ Section BInt_prop.
         clear HI HI'.
         move: limdif => /(lim_seq_ext _ (λ n : nat, BInt_sf μ (s n - s' n)%sf) _ _) => limdif.
         assert (∀ n : nat, (BInt_sf μ (s n) + opp (BInt_sf μ (s' n)))%hy = BInt_sf μ (s n - s' n)%sf).
-            move => n; rewrite BInt_sf_plus_aux.
-            rewrite BInt_sf_scal_aux.
+            move => n; rewrite BInt_sf_plus.
+            rewrite BInt_sf_scal.
             rewrite scal_opp_one => //.
             apply ints.
             apply integrable_sf_scal, ints'.
@@ -361,7 +361,7 @@ Section BInt_op.
         apply (lim_seq_ext (fun n : nat => BInt_sf μ (sf n) + BInt_sf μ (sg n))%hy).
             move => n.
             rewrite eqbf eqbg => /=.
-            rewrite BInt_sf_plus_aux => //.
+            rewrite BInt_sf_plus => //.
             apply: lim_seq_plus.
             pose H := is_lim_seq_BInt (mk_Bif f sf ι isf Hfpw Hfl1);
                 clearbody H; simpl in H; rewrite <-eqbf in H.
@@ -379,7 +379,7 @@ Section BInt_op.
         case: bf => sf ι isf Hfpw Hfl1.
         apply lim_seq_eq.
         apply (lim_seq_ext (fun n : nat => a ⋅ (BInt_sf μ (sf n)))%hy).
-            move => n; rewrite BInt_sf_scal_aux => //.
+            move => n; rewrite BInt_sf_scal => //.
             apply: lim_seq_scal_r.
             pose H := is_lim_seq_BInt (mk_Bif f sf ι isf Hfpw Hfl1);
                 clearbody H; simpl in H.
diff --git a/Lebesgue/bochner_integral/BInt_LInt_p.v b/Lebesgue/bochner_integral/BInt_LInt_p.v
index 90dd8654..306c2a39 100644
--- a/Lebesgue/bochner_integral/BInt_LInt_p.v
+++ b/Lebesgue/bochner_integral/BInt_LInt_p.v
@@ -247,7 +247,7 @@ Section BInt_to_LInt_p.
         apply measurable_gen.
         apply NM_open_neq.
         pose M := proj1_sig (sf_bounded sf).
-        exact (M â‹… (sf_indic_aux _ _ H))%sf.
+        exact (M â‹… (sf_indic _ _ H))%sf.
     Defined.
 
     Lemma pos_shifted_sf : 
@@ -297,10 +297,10 @@ Section BInt_to_LInt_p.
             (‖ minus (BInt_sf μ (sf n + sf_shifter (sf n))%sf) (LInt_p μ (λ x : X, f x + (sf_shifter (sf n) x))) ‖) < ɛ).
         case => N HN.
         exists N => n /HN.
-        rewrite BInt_sf_plus_aux.
+        rewrite BInt_sf_plus.
         unfold sf_shifter.
         case: (sf_bounded (sf n)) => M HM.
-        rewrite BInt_sf_scal_aux.
+        rewrite BInt_sf_scal.
         rewrite BInt_sf_indic.
         simpl.
         rewrite (LInt_p_ext _ _ (fun x => Rbar_plus (f x) (Rbar_mult M (charac (fun x => sf n x ≠ 0) x)))).
diff --git a/Lebesgue/bochner_integral/BInt_sf.v b/Lebesgue/bochner_integral/BInt_sf.v
index 54948e2d..0185e8db 100644
--- a/Lebesgue/bochner_integral/BInt_sf.v
+++ b/Lebesgue/bochner_integral/BInt_sf.v
@@ -82,13 +82,13 @@ Section BInt_sf_indic.
     Open Scope fun_scope.
 
     Lemma BInt_sf_indic (P : X -> Prop) (Ï€_meas : measurable gen P)
-        : BInt_sf μ (sf_indic_aux gen P π_meas) = real (μ P).
+        : BInt_sf μ (sf_indic gen P π_meas) = real (μ P).
     Proof.
         unfold BInt_sf.
-        replace (max_which (sf_indic_aux gen P π_meas)) with 1%nat at 1 
-            by unfold sf_indic_aux => //.
+        replace (max_which (sf_indic gen P π_meas)) with 1%nat at 1 
+            by unfold sf_indic => //.
         rewrite sum_Sn sum_O.
-        case_eq (sf_indic_aux gen P π_meas) => wP vP maxP axP1 axP2 axP3 EqP;
+        case_eq (sf_indic gen P π_meas) => wP vP maxP axP1 axP2 axP3 EqP;
             unfold nth_carrier; rewrite <-EqP => /=.
         rewrite (measure_ext gen μ _ P).
             all : swap 1 2.
@@ -179,7 +179,7 @@ Section BInt_sf_plus.
     Open Scope nat_scope.
     Open Scope sf_scope.
 
-    Lemma BInt_sf_plus_aux {sf_f sf_g : simpl_fun E gen} :
+    Lemma BInt_sf_plus {sf_f sf_g : simpl_fun E gen} :
         integrable_sf μ sf_f -> integrable_sf μ sf_g ->
             BInt_sf μ (sf_f + sf_g) = ((BInt_sf μ sf_f) + (BInt_sf μ sf_g))%hy.
     Proof.
@@ -575,7 +575,7 @@ Section BInt_sf_scal.
     Open Scope nat_scope.
     Open Scope sf_scope.
 
-    Lemma BInt_sf_scal_aux :
+    Lemma BInt_sf_scal :
         ∀ a : R_AbsRing, ∀ sf : simpl_fun E gen,
             BInt_sf μ (a ⋅ sf) = (a ⋅ (BInt_sf μ sf))%hy.
     Proof.
@@ -616,14 +616,14 @@ Section BInt_sf_linearity.
     Open Scope nat_scope.
     Open Scope sf_scope.
 
-    Lemma BInt_sf_lin_aux {sf sg : simpl_fun E gen} :
+    Lemma BInt_sf_lin {sf sg : simpl_fun E gen} :
         ∀ a b : R_AbsRing, integrable_sf μ sf -> integrable_sf μ sg ->
             BInt_sf μ (a ⋅ sf + b ⋅ sg) 
             = ((a ⋅ (BInt_sf μ sf)) + (b ⋅ (BInt_sf μ sg)))%hy.
     Proof.
         move => a b isf isg.
-        do 2 rewrite <-BInt_sf_scal_aux.
-        rewrite BInt_sf_plus_aux => //.
+        do 2 rewrite <-BInt_sf_scal.
+        rewrite BInt_sf_plus => //.
         1, 2 : apply integrable_sf_scal => //.
     Qed.
 
@@ -783,8 +783,8 @@ Section BInt_well_defined.
             rewrite scal_opp_l scal_one.
             rewrite <-Hsfsf'; rewrite plus_opp_r => //.
             assert ((BInt_sf μ sf) + (opp one) ⋅ (BInt_sf μ sf') = (BInt_sf μ sf') + (opp one) ⋅ (BInt_sf μ sf'))%hy as Subgoal.
-                rewrite <-BInt_sf_scal_aux at 1.
-                rewrite <-BInt_sf_plus_aux at 1.
+                rewrite <-BInt_sf_scal at 1.
+                rewrite <-BInt_sf_plus at 1.
                 fold δ; rewrite BInt_sf_zero.
                 rewrite scal_opp_l scal_one plus_opp_r => //.
                 assumption.
diff --git a/Lebesgue/bochner_integral/Bi_fun.v b/Lebesgue/bochner_integral/Bi_fun.v
index 48f9f9b0..5cf8dffe 100644
--- a/Lebesgue/bochner_integral/Bi_fun.v
+++ b/Lebesgue/bochner_integral/Bi_fun.v
@@ -319,7 +319,7 @@ Section Bi_fun_prop.
         unfold ball_norm.
         unfold minus.
         setoid_rewrite <-(scal_opp_one (BInt_sf μ (s p))).
-        rewrite <-BInt_sf_scal_aux, <-BInt_sf_plus_aux.
+        rewrite <-BInt_sf_scal, <-BInt_sf_plus.
         apply RIneq.Rle_lt_trans with (BInt_sf μ (‖(s q) - (s p)‖)%sf).
             apply norm_Bint_sf_le.
         rewrite (BInt_sf_LInt_SFp).
diff --git a/Lebesgue/bochner_integral/simpl_fun.v b/Lebesgue/bochner_integral/simpl_fun.v
index d9dfb81e..58916572 100644
--- a/Lebesgue/bochner_integral/simpl_fun.v
+++ b/Lebesgue/bochner_integral/simpl_fun.v
@@ -133,7 +133,7 @@ Section simpl_fun_indic.
     Open Scope nat_scope.
     Open Scope R_scope.
 
-    Definition sf_indic_aux (P : X -> Prop) :
+    Definition sf_indic (P : X -> Prop) :
         measurable gen P -> simpl_fun R_ModuleSpace gen.
     (* définition *)
         move => Pmeas.
@@ -175,12 +175,12 @@ Section simpl_fun_indic.
             exact Pmeas.
     Defined.
             
-    Lemma sf_indic :
+    Lemma sf_indic' :
         ∀ P : X -> Prop, measurable gen P
             -> is_simpl gen (χ(P): X -> R).
     Proof.
         move => P Pmeas.
-        exists (sf_indic_aux P Pmeas) => x.
+        exists (sf_indic P Pmeas) => x.
         unfold fun_sf, "χ( _ )" => /=.
         case: (excluded_middle_informative (P x)) => //.
     Qed.
@@ -188,7 +188,7 @@ Section simpl_fun_indic.
     Context (μ : measure gen).
 
     Lemma integrable_sf_indic (P : X -> Prop) (Ï€ : measurable gen P) :
-        is_finite (μ P) -> integrable_sf μ (sf_indic_aux P π).
+        is_finite (μ P) -> integrable_sf μ (sf_indic P π).
     Proof.
         move => Pfin n Hn; simpl in *.
             assert (n = O) by lia.
@@ -257,7 +257,7 @@ Section simpl_fun_norm.
 
     Notation "‖ f ‖" := (fun_norm f) (at level 100) : fun_scope.
 
-    Definition sf_norm_aux (sf : simpl_fun E gen) : simpl_fun R_ModuleSpace gen.
+    Definition sf_norm (sf : simpl_fun E gen) : simpl_fun R_ModuleSpace gen.
         case: sf => which val max_which ax1 ax2 ax3.
         pose nval :=
             fun n => norm (val n).
@@ -274,24 +274,24 @@ Section simpl_fun_norm.
     Context {μ : measure gen}.
 
     Lemma integrable_sf_norm {sf : simpl_fun E gen} (isf : integrable_sf μ sf) :
-        integrable_sf μ (sf_norm_aux sf).
+        integrable_sf μ (sf_norm sf).
     Proof.
         unfold integrable_sf in *.
         case_eq sf => wf vf mawf axf1 axf2 axf3 Eqf => /=.
         rewrite Eqf in isf; simpl in isf => //.
     Qed.
 
-    Notation "‖ sf ‖" := (sf_norm_aux sf) (at level 100) : sf_scope.
+    Notation "‖ sf ‖" := (sf_norm sf) (at level 100) : sf_scope.
 
-    Lemma sf_norm :
+    Lemma sf_norm' :
         ∀ f : X -> E, is_simpl gen f -> 
             is_simpl gen (fun_norm f).
     Proof.
         move => f.
         case => sf. case_eq sf => which val max_which ax1 ax2 ax3 Eqsf Eqf.
-        exists (sf_norm_aux sf).
+        exists (sf_norm sf).
         rewrite Eqsf.
-        move => x; unfold fun_sf, sf_norm_aux => /=.
+        move => x; unfold fun_sf, sf_norm => /=.
         simpl in Eqf.
         rewrite Eqf => //.
     Qed.
@@ -309,7 +309,7 @@ Section simpl_fun_norm.
 End simpl_fun_norm.
 
 Notation "‖ f ‖" := (fun_norm f) (at level 100) : fun_scope.
-Notation "‖ sf ‖" := (sf_norm_aux sf) (at level 100) : sf_scope.
+Notation "‖ sf ‖" := (sf_norm sf) (at level 100) : sf_scope.
 
 Section simpl_fun_power.
 
@@ -321,7 +321,7 @@ Section simpl_fun_power.
     Definition fun_power (f : X -> R_NormedModule) (p : posreal) :=
         (fun x => Rpow (f x) p.(pos)).
 
-    Definition sf_power_aux (sf : simpl_fun R_NormedModule gen) (p : RIneq.posreal) : simpl_fun R_NormedModule gen.
+    Definition sf_power (sf : simpl_fun R_NormedModule gen) (p : RIneq.posreal) : simpl_fun R_NormedModule gen.
     case: sf => which val max_which ax1 ax2 ax3.
     pose nval :=
         fun n => Rpow (val n) p.(pos).
@@ -336,7 +336,7 @@ Section simpl_fun_power.
         exact ax3.
     Defined.
 
-    Notation "sf ^ p" := (sf_power_aux sf p).
+    Notation "sf ^ p" := (sf_power sf p).
 
     Lemma fun_sf_power :
         ∀ sf : simpl_fun R_NormedModule gen, ∀ p : RIneq.posreal,
@@ -361,7 +361,7 @@ Section simpl_fun_power.
 End simpl_fun_power.
 
 Notation "f ^ p" := (fun_power f p) : fun_scope.
-Notation "sf '^' p" := (sf_power_aux sf p) : sf_scope.
+Notation "sf '^' p" := (sf_power sf p) : sf_scope.
 
 Section simpl_fun_plus.
 
@@ -380,7 +380,7 @@ Section simpl_fun_plus.
 
     Notation "f + g" := (fun_plus f g) (left associativity, at level 50) : fun_scope. 
 
-    Definition sf_plus_aux (sf sg : simpl_fun E gen) : simpl_fun E gen.
+    Definition sf_plus (sf sg : simpl_fun E gen) : simpl_fun E gen.
         case: sf => wf vf maxf axf1 axf2 axf3.
         case: sg => wg vg maxg axg1 axg2 axg3.
         pose val := fun m =>
@@ -439,16 +439,16 @@ Section simpl_fun_plus.
                 apply measurable_inter_fg with n c => //.
     Defined.
 
-    Notation "sf + sg" := (sf_plus_aux sf sg) (left associativity, at level 50) : sf_scope.
+    Notation "sf + sg" := (sf_plus sf sg) (left associativity, at level 50) : sf_scope.
 
-    Lemma sf_plus :
+    Lemma sf_plus' :
         ∀ f g : X -> E, 
         is_simpl gen f -> is_simpl gen g ->
         is_simpl gen (fun_plus f g).
     Proof.
         move => f g.
         case => sf Eq_sf_f; case => sg Eq_sg_g.
-        exists (sf_plus_aux sf sg).
+        exists (sf_plus sf sg).
         case_eq sf => wf vf maxf axf1 axf2 axf3 Eqf.
         case_eq sg => wg vg maxg axg1 axg2 axg3 Eqg.
         unfold fun_sf => /= x.
@@ -479,7 +479,7 @@ Section simpl_fun_plus.
     Context {μ : measure gen}.
 
     Lemma integrable_sf_plus {sf sg : simpl_fun E gen} : 
-        (integrable_sf μ sf) -> (integrable_sf μ sg) -> (integrable_sf μ (sf_plus_aux sf sg)).
+        (integrable_sf μ sf) -> (integrable_sf μ sg) -> (integrable_sf μ (sf_plus sf sg)).
     Proof.
         unfold integrable_sf.
         move => axf4 axg4.
@@ -595,7 +595,7 @@ Section simpl_fun_plus.
 End simpl_fun_plus.
 
 Notation "f + g" := (fun_plus f g) (left associativity, at level 50) : fun_scope. 
-Notation "sf + sg" := (sf_plus_aux sf sg) (left associativity, at level 50) : sf_scope.
+Notation "sf + sg" := (sf_plus sf sg) (left associativity, at level 50) : sf_scope.
 
 Section simpl_fun_scal.
 
@@ -614,7 +614,7 @@ Section simpl_fun_scal.
 
     Notation "a â‹… g" := (fun_scal a g) (left associativity, at level 45) : fun_scope.
 
-    Definition sf_scal_aux (a : A) (sf : simpl_fun E gen) : simpl_fun E gen.
+    Definition sf_scal (a : A) (sf : simpl_fun E gen) : simpl_fun E gen.
         case: sf => wf vf maxf axf1 axf2 axf3.
         pose val := fun k => scal a (vf k).
         apply (mk_simpl_fun wf val maxf).
@@ -623,16 +623,16 @@ Section simpl_fun_scal.
             exact axf3.
     Defined.
 
-    Notation "a â‹… sf" := (sf_scal_aux a sf) (left associativity, at level 45) : sf_scope.
+    Notation "a â‹… sf" := (sf_scal a sf) (left associativity, at level 45) : sf_scope.
 
-    Lemma sf_scal :
+    Lemma sf_scal' :
         ∀ a : A, ∀ f : X -> E, 
         is_simpl gen f ->
         is_simpl gen (fun_scal a f).
     Proof.
         move => a f.
         case => sf; case_eq sf => wf vf maxf axf1 axf2 axf3 Eqsf => /= Eqf.
-        exists (sf_scal_aux a sf) => x.
+        exists (sf_scal a sf) => x.
         unfold fun_sf, val, which; rewrite Eqsf => /=.
         unfold fun_scal; rewrite Eqf => //.
     Qed.
@@ -650,7 +650,7 @@ Section simpl_fun_scal.
     Context {μ : measure gen}.
 
     Lemma integrable_sf_scal (a : A) {sf : simpl_fun E gen} :
-        integrable_sf μ sf -> integrable_sf μ (sf_scal_aux a sf).
+        integrable_sf μ sf -> integrable_sf μ (sf_scal a sf).
     Proof.
         unfold integrable_sf.
         case: sf => //.
@@ -659,11 +659,11 @@ Section simpl_fun_scal.
 End simpl_fun_scal.
 
 Notation "a â‹… g" := (fun_scal a g) (left associativity, at level 45) : fun_scope.
-Notation "a â‹… sf" := (sf_scal_aux a sf) (left associativity, at level 45) : sf_scope.
+Notation "a â‹… sf" := (sf_scal a sf) (left associativity, at level 45) : sf_scope.
 Notation "- g" := (fun_scal (opp one) g) : fun_scope.
-Notation "- sg" := (sf_scal_aux (opp one) sg) : sf_scope.
+Notation "- sg" := (sf_scal (opp one) sg) : sf_scope.
 Notation "f - g" := (fun_plus f (- g))%fn : fun_scope.
-Notation "sf - sg" := (sf_plus_aux sf (- sg)) : sf_scope.
+Notation "sf - sg" := (sf_plus sf (- sg)) : sf_scope.
 
 Section simpl_fun_bounded.
 
-- 
GitLab