From 324770b36aba93bced5ff21ee06640e8e05038f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sun, 9 Mar 2025 14:04:26 +0100
Subject: [PATCH] Make {filter0F,filter_n0F,split0F}{,_gen} abbreviations.
 Generalize {filter0F,filter_n0F}_correct into filter_{,n}eqF_correct. Rm now
 useless specific results.

---
 Algebra/AffineSpace/AffineSpace_baryc.v    |  2 +-
 Algebra/ModuleSpace/ModuleSpace_lin_comb.v | 12 +--
 Algebra/Monoid/Monoid_FF.v                 | 96 +++++-----------------
 Subsets/Finite_family.v                    |  7 ++
 4 files changed, 36 insertions(+), 81 deletions(-)

diff --git a/Algebra/AffineSpace/AffineSpace_baryc.v b/Algebra/AffineSpace/AffineSpace_baryc.v
index 4e3bd5b2..124baffc 100644
--- a/Algebra/AffineSpace/AffineSpace_baryc.v
+++ b/Algebra/AffineSpace/AffineSpace_baryc.v
@@ -582,7 +582,7 @@ eexists; exists (scal (/ sum (filter_n0F L)) (filter_n0F L)),
 2: apply filterPF_invalF.
 intros; rewrite fct_scal_r_eq scal_eq_K. apply mult_not_zero_l.
 apply inv_invertible; rewrite -invertible_sum_equiv//.
-apply filter_n0F_correct.
+apply filter_neqF_correct.
 Qed.
 
 Lemma baryc_constF :
diff --git a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
index 5abf8036..de1d92e1 100644
--- a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
+++ b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
@@ -608,8 +608,8 @@ Lemma lc_filter_n0F_l :
     lin_comb (filter_n0F L) (filter_n0F_gen L B) = lin_comb L B.
 Proof.
 intros n L B; rewrite -(lc_split0F_l L) -(plus_zero_l (lin_comb _ _)).
-rewrite split0F_correct split0F_gen_correct lc_concatF; f_equal.
-rewrite lc_zero_compat_l// filter0F_correct//.
+rewrite lc_concatF; f_equal; rewrite lc_zero_compat_l//.
+apply filter0F_correct.
 Qed.
 
 Lemma lc_filter_n0F_l_ex :
@@ -618,7 +618,7 @@ Lemma lc_filter_n0F_l_ex :
 Proof.
 intros n L B'; exists (unfun0F filterP_ord B').
 rewrite -(lc_filter_n0F_l L); f_equal.
-rewrite filter_n0F_gen_eq_funF funF_unfunF; [easy | apply filterP_ord_inj].
+rewrite filter_neqF_gen_eq_funF funF_unfunF; [easy | apply filterP_ord_inj].
 Qed.
 
 Lemma lc_filter_n0F_r :
@@ -626,8 +626,8 @@ Lemma lc_filter_n0F_r :
     lin_comb (filter_n0F_gen B L) (filter_n0F B) = lin_comb L B.
 Proof.
 intros n L B; rewrite -(lc_split0F_r L) -(plus_zero_l (lin_comb _ _)).
-rewrite split0F_correct split0F_gen_correct lc_concatF; f_equal.
-rewrite lc_zero_compat_r// filter0F_correct//.
+rewrite lc_concatF; f_equal; rewrite lc_zero_compat_r//.
+apply filter0F_correct.
 Qed.
 
 Lemma lc_filter_n0F_r_ex :
@@ -636,7 +636,7 @@ Lemma lc_filter_n0F_r_ex :
 Proof.
 intros n B L'; exists (unfun0F filterP_ord L').
 rewrite -(lc_filter_n0F_r _ B); f_equal.
-rewrite filter_n0F_gen_eq_funF funF_unfunF; [easy | apply filterP_ord_inj].
+rewrite filter_neqF_gen_eq_funF funF_unfunF; [easy | apply filterP_ord_inj].
 Qed.
 
 Lemma lc_unfun0F :
diff --git a/Algebra/Monoid/Monoid_FF.v b/Algebra/Monoid/Monoid_FF.v
index cca22e6d..4a01c039 100644
--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -93,10 +93,21 @@ Proof. apply FT0m_eq; easy. Qed.
 End Monoid_FF_0_R_Facts.
 
 
-Notation insert0F := (insertF ^~ 0). (* : 'I_n.+1 -> 'G^n -> 'G^n.+1 *)
-Notation replace0F := (replaceF ^~ 0). (* : 'I_n -> 'G^n -> 'G^n *)
-Notation unfun0F := (unfunF ^~ 0). (* : 'I_{n1,n2} -> 'G^n1 -> 'G^n2 *)
-Notation maskP0F := (maskPF ^~ 0). (* : 'Prop^n -> 'G^n -> 'G^n *)
+Notation insert0F := (insertF^~ 0). (* : 'I_n.+1 -> 'G^n -> 'G^n.+1 *)
+Notation replace0F := (replaceF^~ 0). (* : 'I_n -> 'G^n -> 'G^n *)
+
+Notation unfun0F := (unfunF^~ 0). (* : 'I_{n1,n2} -> 'G^n1 -> 'G^n2 *)
+Notation maskP0F := (maskPF^~ 0). (* : 'Prop^n -> 'G^n -> 'G^n *)
+
+Notation filter0F_gen := (filter_eqF_gen 0). (* forall (u : 'G^n), 'T^n -> 'T^(lenPF (eqF u 0)) *)
+Notation filter0F := (filter_eqF 0). (* forall (u : 'G^n), 'G^(lenPF (eqF u 0)) *)
+Notation filter_n0F_gen := (filter_neqF_gen 0). (* forall (u : 'G^n), 'T^n -> 'T^(lenPF (neqF u 0)) *)
+Notation filter_n0F := (filter_neqF 0). (* forall (u : 'G^n), 'G^(lenPF (neqF u 0)) *)
+
+Notation split0F_gen := (split_eqF_gen 0). (* forall (u : 'G^n),
+    'T^n -> 'T^(lenPF (eqF u 0) + lenPF (fun i => ~ eqF u 0 i)) *)
+Notation split0F := (split_eqF 0). (* forall (u : 'G^n),
+    'G^(lenPF (eqF u 0) + lenPF (fun i : 'I_n => ~ eqF u 0 i)) *)
 
 
 Section Monoid_FF_Def.
@@ -108,29 +119,6 @@ Context {G : AbelianMonoid}.
 
 Definition itemF n i0 x : 'G^n := replaceF i0 x 0.
 
-Definition filter0F_gen {T : Type} {n} :
-    forall (u : 'G^n), 'T^n -> 'T^(lenPF (eqF u 0)) :=
-  fun u v => filter_eqF_gen 0 u v.
-
-Definition filter0F {n} : forall (u : 'G^n), 'G^(lenPF (eqF u 0)) :=
-  fun u => filter_eqF 0 u.
-
-Definition filter_n0F_gen {T : Type} {n} :
-    forall (u : 'G^n), 'T^n -> 'T^(lenPF (neqF u 0)) :=
-  fun u v => filter_neqF_gen 0 u v.
-
-Definition filter_n0F {n} : forall (u : 'G^n), 'G^(lenPF (neqF u 0)) :=
-  fun u => filter_neqF 0 u.
-
-Definition split0F_gen {T : Type} {n} :
-    forall (u : 'G^n),
-      'T^n -> 'T^(lenPF (eqF u 0) + lenPF (fun i => ~ eqF u 0 i)) :=
-  fun u v => split_eqF_gen 0 u v.
-
-Definition split0F {n} : forall (u : 'G^n),
-    'G^(lenPF (eqF u 0) + lenPF (fun i : 'I_n => ~ eqF u 0 i)) :=
-  fun u => split_eqF 0 u.
-
 Definition squeezeF {n} (i0 i1 : 'I_n.+1) : 'G^n.+1 -> 'G^n :=
   fun u => skipF i1 (replaceF i0 (u i0 + u i1) u).
 
@@ -145,32 +133,14 @@ Context {G : AbelianMonoid}.
 
 Lemma itemF_correct_l :
   forall n {i0 i} (x : G), i = i0 -> itemF n i0 x i = x.
-Proof. move=>>; unfold itemF; apply replaceF_correct_l. Qed.
+Proof. move=>>; apply replaceF_correct_l. Qed.
 
 Lemma itemF_correct_r :
   forall n {i0 i} (x : G), i <> i0 -> itemF n i0 x i = 0.
 Proof. intros; unfold itemF; rewrite replaceF_correct_r; easy. Qed.
 
 Lemma filter0F_correct : forall {n} (u : 'G^n), filter0F u = 0.
-Proof.
-intros n u; extF; unfold filter0F, filter0F_gen.
-apply (filterP_ord_correct (fun i => u i = 0)).
-Qed.
-
-Lemma filter_n0F_correct : forall {n} (u : 'G^n) i, filter_n0F u i <> 0.
-Proof.
-intros n u i; unfold filter0F, filter0F_gen.
-apply (filterP_ord_correct (fun i => u i <> 0)).
-Qed.
-
-Lemma split0F_gen_correct :
-  forall {T : Type} {n} (u : 'G^n) (v : 'T^n),
-    split0F_gen u v = concatF (filter0F_gen u v) (filter_n0F_gen u v).
-Proof. easy. Qed.
-
-Lemma split0F_correct :
-  forall {n} (u : 'G^n), split0F u = concatF (filter0F u) (filter_n0F u).
-Proof. easy. Qed.
+Proof. intros; extF; apply filter_eqF_correct. Qed.
 
 Lemma squeezeF_correct_l :
   forall {n i0 i1} (Hi : i0 <> i1) (u : 'G^n.+1),
@@ -349,25 +319,8 @@ Proof. move=> f Hf =>>; rewrite mapF_replaceF Hf; easy. Qed.
 
 (** Properties of operators [filter0F]/[filter_n0F]/[split0F]. *)
 
-Lemma filter0F_eq_gen_funF :
-  forall {H : Type} {n} (u : 'G^n) (v : 'H^n),
-    filter0F_gen u v = funF filterP_ord v.
-Proof. easy. Qed.
-
-Lemma filter0F_eq_funF :
-  forall {n} (u : 'G^n), filter0F u = funF filterP_ord u.
-Proof. easy. Qed.
-
-Lemma filter_n0F_gen_eq_funF :
-  forall {H : Type} {n} (u : 'G^n) (v : 'H^n),
-    filter_n0F_gen u v = funF filterP_ord v.
-Proof. easy. Qed.
-
-Lemma filter_n0F_eq_funF :
-  forall {n} (u : 'G^n), filter_n0F u = funF filterP_ord u.
-Proof. easy. Qed.
-
-(* Unused.
+(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
+ Unused.
 Lemma len_n0F_concatF_l :
   forall {n1 n2} (u1 : 'G^n1) {u2 : 'G^n2},
     u2 = 0 ->
@@ -410,10 +363,7 @@ Lemma filter_n0F_gen_unfun0F :
     filter_n0F_gen (unfun0F f u1) (unfun0F f v1) =
       castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
         (filter_n0F_gen (permutF q1 u1) (permutF q1 v1))).
-Proof.
-intros; unfold filter_n0F_gen;
-    rewrite filter_neqF_gen_unfunF; apply castF_eq_l.
-Qed.
+Proof. intros; rewrite filter_neqF_gen_unfunF; apply castF_eq_l. Qed.
 
 Lemma filter_n0F_gen_unfun0F_l :
   forall {H : AbelianMonoid} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
@@ -425,7 +375,7 @@ Lemma filter_n0F_gen_unfun0F_l :
       castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
         (filter_n0F_gen (permutF q1 u1) (permutF q1 (funF f u2)))).
 Proof.
-intros; unfold filter_n0F_gen; rewrite filter_neqF_gen_unfunF_l;
+intros; rewrite filter_neqF_gen_unfunF_l;
     [apply castF_eq_l | apply inhabited_m].
 Qed.
 
@@ -437,9 +387,7 @@ Lemma filter_n0F_unfun0F :
     filter_n0F (unfun0F f u1) =
       castF (len_n0F_unfun0F Hf) (castF (lenPF_permutF Hq1b)
         (filter_n0F (permutF q1 u1))).
-Proof.
-intros; unfold filter_n0F; rewrite filter_neqF_unfunF; apply castF_eq_l.
-Qed.
+Proof. intros; rewrite filter_neqF_unfunF; apply castF_eq_l. Qed.
 
 End Monoid_FF_Facts2.
 
diff --git a/Subsets/Finite_family.v b/Subsets/Finite_family.v
index ff78350c..8d79d272 100644
--- a/Subsets/Finite_family.v
+++ b/Subsets/Finite_family.v
@@ -1041,6 +1041,13 @@ Lemma compF_correct :
   forall {n} (f : '(F -> G)^n) (g : '(E -> F)^n), compF f g = fun i => f i \o g i.
 Proof. easy. Qed.
 
+Lemma filter_eqF_correct : forall {n} x0 (A : 'E^n) i, filter_eqF x0 A i = x0.
+Proof. intros n x0 A i; apply (filterP_ord_correct (fun i => A i = x0)). Qed.
+
+Lemma filter_neqF_correct :
+  forall {n} x0 (A : 'E^n) i, filter_neqF x0 A i <> x0.
+Proof. intros n x0 A i; apply (filterP_ord_correct (fun i => A i <> x0)). Qed.
+
 End FF_ops_Facts0.
 
 
-- 
GitLab