From 3d044d8fc4ce3da0ea75d3c363a2043f30240289 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 16:09:25 +0100
Subject: [PATCH] Make filter_{,n}eqF{_gen,}, split_eqF{_gen,} abbreviations.
 Mv stuff around.

---
 Algebra/Monoid/Monoid_FF.v |  27 ++--
 Subsets/Finite_family.v    | 261 ++++++++++++++++++-------------------
 2 files changed, 142 insertions(+), 146 deletions(-)

diff --git a/Algebra/Monoid/Monoid_FF.v b/Algebra/Monoid/Monoid_FF.v
index 6bf70163..3617362b 100644
--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -93,21 +93,18 @@ 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 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)) *)
+Notation insert0F := (insertF^~ 0).
+Notation replace0F := (replaceF^~ 0).
+
+Notation unfun0F := (unfunF^~ 0).
+Notation maskP0F := (maskPF^~ 0).
+
+Notation filter0F_gen A B := (filter_eqF_gen 0 A B).
+Notation filter0F A := (filter_eqF 0 A).
+Notation filter_n0F_gen A B := (filter_neqF_gen 0 A B).
+Notation filter_n0F A := (filter_neqF 0 A).
+Notation split0F_gen A B := (split_eqF_gen 0 A B).
+Notation split0F A := (split_eqF 0 A).
 
 
 Section Monoid_FF_Def.
diff --git a/Subsets/Finite_family.v b/Subsets/Finite_family.v
index 8d79d272..3b473668 100644
--- a/Subsets/Finite_family.v
+++ b/Subsets/Finite_family.v
@@ -601,20 +601,6 @@ Definition map2F {n} (f : E -> F -> G) : 'E^n -> 'F^n -> 'G^n :=
 End FF_ops_Def1.
 
 
-Notation eqxF0 := (eqxF ord0).
-Notation eqxFmax := (eqxF ord_max).
-Notation neqxF0 := (neqxF ord0).
-Notation neqxFmax := (neqxF ord_max).
-
-Notation insertF0 := (insertF ord0).
-Notation insertFmax := (insertF ord_max).
-Notation skipF0 := (skipF ord0).
-Notation skipFmax := (skipF ord_max).
-
-Notation replaceF0 := (replaceF ord0).
-Notation replaceFmax := (replaceF ord_max).
-
-
 Section FF_ops_Def2.
 
 Context {E F G : Type}.
@@ -631,34 +617,30 @@ Definition compF {n} : '(F -> G)^n -> '(E -> F)^n -> '(E -> G)^n :=
 End FF_ops_Def2.
 
 
-Section FF_ops_Def2.
-
-Context {E : Type}.
-
-Definition filter_eqF_gen {F : Type} {n} (x0 : E) :
-    forall (A : 'E^n), 'F^n -> 'F^(lenPF (eqF A x0)) :=
-  fun A B => filterPF (eqF A x0) B.
-
-Definition filter_eqF {n} (x0 : E) :
-  forall (A : 'E^n), 'E^(lenPF (eqF A x0)) := fun A => filter_eqF_gen x0 A A.
-
-Definition filter_neqF_gen {F : Type} {n} (x0 : E) :
-    forall (A : 'E^n), 'F^n -> 'F^(lenPF (neqF A x0)) :=
-  fun A B => filterPF (neqF A x0) B.
-
-Definition filter_neqF {n} (x0 : E) :
-  forall (A : 'E^n), 'E^(lenPF (neqF A x0)) := fun A => filter_neqF_gen x0 A A.
+Notation eqxF0 := (eqxF ord0).
+Notation eqxFmax := (eqxF ord_max).
+Notation neqxF0 := (neqxF ord0).
+Notation neqxFmax := (neqxF ord_max).
 
-Definition split_eqF_gen {F : Type} {n} (x0 : E) :
-    forall (A : 'E^n),
-      'F^n -> 'F^(lenPF (eqF A x0) + lenPF (fun i => ~ eqF A x0 i)) :=
-  fun A B => splitPF (eqF A x0) B.
+Notation insertF0 := (insertF ord0).
+Notation insertFmax := (insertF ord_max).
+Notation skipF0 := (skipF ord0).
+Notation skipFmax := (skipF ord_max).
 
-Definition split_eqF {n} (x0 : E) :
-    forall (A : 'E^n), 'E^(lenPF (eqF A x0) + lenPF (fun i => ~ eqF A x0 i)) :=
-  fun A => split_eqF_gen x0 A A.
+Notation replaceF0 := (replaceF ord0).
+Notation replaceFmax := (replaceF ord_max).
 
-End FF_ops_Def2.
+Notation filter_eqF_gen x0 A B := (filterPF (eqF A x0) B).
+  (* forall (A : 'E^n), 'F^n -> 'F^(lenPF (eqF A x0)) *)
+Notation filter_eqF x0 A := (filter_eqF_gen x0 A A). (* forall (A : 'E^n), 'E^(lenPF (eqF A x0)) *)
+Notation filter_neqF_gen x0 A B := (filterPF (neqF A x0) B).
+  (* forall (A : 'E^n), 'F^n -> 'F^(lenPF (neqF A x0)) *)
+Notation filter_neqF x0 A := (filter_neqF_gen x0 A A). (* forall (A : 'E^n), 'E^(lenPF (neqF A x0)) *)
+Notation split_eqF_gen x0 A B := (splitPF (eqF A x0) B).
+  (* forall (A : 'E^n),
+      'F^n -> 'F^(lenPF (eqF A x0) + lenPF (fun i => ~ eqF A x0 i)) *)
+Notation split_eqF x0 A := (split_eqF_gen x0 A A).
+  (* forall (A : 'E^n), 'E^(lenPF (eqF A x0) + lenPF (fun i => ~ eqF A x0 i)) *)
 
 
 Section FF_ops_Facts0.
@@ -4600,7 +4582,7 @@ Qed.
 End PermutF_Facts2.
 
 
-Section FilterPF_Facts1.
+Section FilterPF_Facts0.
 
 (** Definition and properties of [filterP_f_ord]. *)
 
@@ -4653,30 +4635,17 @@ Proof.
 move=>> Hp1; apply (filterP_f_ord_comp _ Hp1), (extendPF_permutF _ Hp1).
 Qed.
 
-Context {E : Type}.
-
-(** Properties of operators [lenPF]/[filterPF]/[splitPF]. *)
+End FilterPF_Facts0.
 
-Lemma filterPF_eq_funF :
-  forall {n} (P : 'Prop^n) (A : 'E^n), filterPF P A = funF filterP_ord A.
-Proof. easy. Qed.
 
-Lemma filter_eqF_gen_eq_funF :
-  forall {F : Type} {n} x0 (A : 'E^n) (B : 'F^n),
-    filter_eqF_gen x0 A B = funF filterP_ord B.
-Proof. easy. Qed.
+Section FilterPF_Facts1.
 
-Lemma filter_eqF_eq_funF :
-  forall {n} x0 (A : 'E^n), filter_eqF x0 A = funF filterP_ord A.
-Proof. easy. Qed.
+Context {E : Type}.
 
-Lemma filter_neqF_gen_eq_funF :
-  forall {F : Type} {n} x0 (A : 'E^n) (B : 'F^n),
-    filter_neqF_gen x0 A B = funF filterP_ord B.
-Proof. easy. Qed.
+(** Properties of operators [lenPF]/[filterPF]. *)
 
-Lemma filter_neqF_eq_funF :
-  forall {n} x0 (A : 'E^n), filter_neqF x0 A = funF filterP_ord A.
+Lemma filterPF_eq_funF :
+  forall {n} (P : 'Prop^n) (A : 'E^n), filterPF P A = funF filterP_ord A.
 Proof. easy. Qed.
 
 Lemma filterPF_nil :
@@ -5119,34 +5088,7 @@ Section FilterPF_Facts2.
 
 Context {E : Type}.
 
-(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
- Unused.
-Lemma len_neqF_concatF_l :
-  forall {n1 n2} (A1 : 'E^n1) {A2 : 'E^n2} {x0},
-    A2 = constF n2 x0 ->
-    lenPF (neqF (concatF A1 A2) x0) = lenPF (neqF A1 x0).
-Proof.
-Aglopted.
-
-Lemma filter_neqF_concatF_l :
-  forall {n1 n2} (A1 : 'E^n1) {A2 : 'E^n2} {x0} (HA2 : A2 = constF n2 x0),
-    filter_neqF (concatF A1 A2) x0 =
-      castF (eq_sym (len_neqF_concatF_l A1 HA2)) (filter_neqF A1 x0).
-Proof.
-Aglopted.
-
-Lemma len_neqF_concatF_r :
-  forall {n1 n2} {A1 : 'E^n1} {x0}, A1 = constF n1 x0 -> forall (A2 : 'E^n2),
-    lenPF (neqF (concatF A1 A2) x0) = lenPF (neqF A2 x0).
-Proof.
-Aglopted.
-
-Lemma filter_neqF_concatF_r :
-  forall {n1 n2} {A1 : 'E^n1} {x0} (HA1 : A1 = constF n1 x0) (A2 : 'E^n2),
-    filter_neqF (concatF A1 A2) x0 =
-      castF (eq_sym (len_neqF_concatF_r HA1 A2)) (filter_neqF A2 x0).
-Proof.
-Aglopted.*)
+(** More properties of operators [lenPF]/[filterPF]. *)
 
 Lemma lenPF_firstF_in :
   forall {n1 n2} {P : 'I_(n1 + n2) -> Prop},
@@ -5306,6 +5248,14 @@ rewrite (filterP_f_ord_correct_alt _ (incrF_inj Hf) HP) -(comp_correct _ f).
 rewrite (filterP_ord_w_incrF Hf HP); easy.
 Qed.
 
+Lemma len_neqF_funF :
+  forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
+    injective f -> incl (neqF A2 x0) (Rg f) ->
+    lenPF (neqF (funF f A2) x0) = lenPF (neqF A2 x0).
+Proof.
+move=>> Hf HA2; apply (lenPF_extendPF Hf), (extendPF_funF_neqF_equiv Hf); easy.
+Qed.
+
 Lemma filterPF_funF :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} {P1 : 'Prop^n1} {P2 : 'Prop^n2}
       {i0} (HP0 : P2 (f i0)) {A2 : 'F^n2},
@@ -5317,14 +5267,98 @@ unfold filterPF, funF; f_equal.
 rewrite filterP_f_ord_correct; easy.
 Qed.
 
-Lemma len_neqF_funF :
-  forall {n1 n2} {f : 'I_{n1,n2}} {A2 : 'E^n2} {x0},
-    injective f -> incl (neqF A2 x0) (Rg f) ->
-    lenPF (neqF (funF f A2) x0) = lenPF (neqF A2 x0).
+Lemma len_neqF_unfunF :
+  forall {n1 n2} {f : 'I_{n1,n2}} {x0} {A1 : 'E^n1},
+    injective f -> lenPF (neqF A1 x0) = lenPF (neqF (unfunF f x0 A1) x0).
 Proof.
-move=>> Hf HA2; apply (lenPF_extendPF Hf), (extendPF_funF_neqF_equiv Hf); easy.
+move=>> Hf; apply (lenPF_extendPF Hf), (extendPF_unfunF_neqF _ _ Hf).
+Qed.
+
+Lemma filterPF_unfunF :
+  forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
+      {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop} (HP : extendPF f P1 P2)
+      x0 {A1 : 'F^n1} i1,
+    P1 i1 ->
+    let q1 := proj1_sig (injF_restr_bij_EX Hf) in
+    let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
+    let Hq1b := bij_inj Hq1a in
+    filterPF P2 (unfunF f x0 A1) =
+      castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hq1b)
+        (filterPF (permutF q1 P1) (permutF q1 A1))).
+Proof.
+intros F n1 n2 f Hf P1 P2 HP x0 A1 i1 HP1 q1 Hq1a Hq1b.
+pose (Hq1c := proj2 (proj2_sig (injF_restr_bij_EX Hf)));
+    pose (p1 := f_inv Hq1a); fold q1 in Hq1a, Hq1b, Hq1c.
+assert (HP1' : P1 (q1 (p1 i1))) by now unfold p1; rewrite f_inv_can_r.
+assert (HP2 : P2 (f i1))
+    by now rewrite (extendPF_unfunF_rev Hf HP) (unfunF_correct_l _ i1).
+assert (HP2' : P2 (f (q1 (p1 i1)))) by now rewrite f_inv_can_r.
+(* *)
+rewrite (filterPF_permutF HP1' Hq1b) -{2}(funF_unfunF x0 Hf A1).
+rewrite (filterPF_funF HP2' Hf HP).
+extF; unfold castF, funF; f_equal.
+rewrite -(filterP_f_ord_comp_l HP1' Hq1b).
+rewrite (filterP_f_ord_w_incrF Hq1c (extendPF_incrF Hf HP)).
+rewrite 2!cast_ord_comp cast_ord_id; easy.
 Qed.
 
+End FilterPF_Facts2.
+
+
+Section FilterPF_Facts3.
+
+Context {E : Type}.
+
+(** Properties of operators [filter_eqF_gen]/[filter_eqF], and
+ [filter_neqF_gen]/[filter_neqF]. *)
+
+Lemma filter_eqF_gen_eq_funF :
+  forall {F : Type} {n} x0 (A : 'E^n) (B : 'F^n),
+    filter_eqF_gen x0 A B = funF filterP_ord B.
+Proof. easy. Qed.
+
+Lemma filter_eqF_eq_funF :
+  forall {n} x0 (A : 'E^n), filter_eqF x0 A = funF filterP_ord A.
+Proof. easy. Qed.
+
+Lemma filter_neqF_gen_eq_funF :
+  forall {F : Type} {n} x0 (A : 'E^n) (B : 'F^n),
+    filter_neqF_gen x0 A B = funF filterP_ord B.
+Proof. easy. Qed.
+
+Lemma filter_neqF_eq_funF :
+  forall {n} x0 (A : 'E^n), filter_neqF x0 A = funF filterP_ord A.
+Proof. easy. Qed.
+
+(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
+ Unused.
+Lemma len_neqF_concatF_l :
+  forall {n1 n2} (A1 : 'E^n1) {A2 : 'E^n2} {x0},
+    A2 = constF n2 x0 ->
+    lenPF (neqF (concatF A1 A2) x0) = lenPF (neqF A1 x0).
+Proof.
+Aglopted.
+
+Lemma filter_neqF_concatF_l :
+  forall {n1 n2} (A1 : 'E^n1) {A2 : 'E^n2} {x0} (HA2 : A2 = constF n2 x0),
+    filter_neqF (concatF A1 A2) x0 =
+      castF (eq_sym (len_neqF_concatF_l A1 HA2)) (filter_neqF A1 x0).
+Proof.
+Aglopted.
+
+Lemma len_neqF_concatF_r :
+  forall {n1 n2} {A1 : 'E^n1} {x0}, A1 = constF n1 x0 -> forall (A2 : 'E^n2),
+    lenPF (neqF (concatF A1 A2) x0) = lenPF (neqF A2 x0).
+Proof.
+Aglopted.
+
+Lemma filter_neqF_concatF_r :
+  forall {n1 n2} {A1 : 'E^n1} {x0} (HA1 : A1 = constF n1 x0) (A2 : 'E^n2),
+    filter_neqF (concatF A1 A2) x0 =
+      castF (eq_sym (len_neqF_concatF_r HA1 A2)) (filter_neqF A2 x0).
+Proof.
+Aglopted.*)
+
 Lemma filter_neqF_gen_funF :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} {x0} {A2 : 'E^n2} {B2 : 'F^n2}
       {i0} (HP0 : neqF A2 x0 (f i0)),
@@ -5351,7 +5385,7 @@ Lemma filter_neqF_funF :
     filter_neqF x0 (funF f A2) =
       funF (filterP_f_ord f HP0) (filter_neqF x0 A2).
 Proof.
-intros n1 n2 f x0 A2 i0 HP0 Hf HA2; unfold filter_neqF.
+intros n1 n2 f x0 A2 i0 HP0 Hf HA2.
 rewrite (filter_neqF_gen_funF_r x0 HP0)// unfunF_funF//; repeat f_equal.
 extF i2; destruct (im_dec f i2) as [[i1 <-] | Hi2].
 apply maskPF_correct_l; easy.
@@ -5360,41 +5394,6 @@ rewrite -incl_compl_equiv in HA2; specialize (HA2 i2);
 rewrite HA2; [ apply maskPF_correct_r |]; rewrite Rg_compl; easy.
 Qed.
 
-Lemma filterPF_unfunF :
-  forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
-      {P1 : 'I_n1 -> Prop} {P2 : 'I_n2 -> Prop} (HP : extendPF f P1 P2)
-      x0 {A1 : 'F^n1} i1,
-    P1 i1 ->
-    let q1 := proj1_sig (injF_restr_bij_EX Hf) in
-    let Hq1a := proj1 (proj2_sig (injF_restr_bij_EX Hf)) in
-    let Hq1b := bij_inj Hq1a in
-    filterPF P2 (unfunF f x0 A1) =
-      castF (lenPF_extendPF Hf HP) (castF (lenPF_permutF Hq1b)
-        (filterPF (permutF q1 P1) (permutF q1 A1))).
-Proof.
-intros F n1 n2 f Hf P1 P2 HP x0 A1 i1 HP1 q1 Hq1a Hq1b.
-pose (Hq1c := proj2 (proj2_sig (injF_restr_bij_EX Hf)));
-    pose (p1 := f_inv Hq1a); fold q1 in Hq1a, Hq1b, Hq1c.
-assert (HP1' : P1 (q1 (p1 i1))) by now unfold p1; rewrite f_inv_can_r.
-assert (HP2 : P2 (f i1))
-    by now rewrite (extendPF_unfunF_rev Hf HP) (unfunF_correct_l _ i1).
-assert (HP2' : P2 (f (q1 (p1 i1)))) by now rewrite f_inv_can_r.
-(* *)
-rewrite (filterPF_permutF HP1' Hq1b) -{2}(funF_unfunF x0 Hf A1).
-rewrite (filterPF_funF HP2' Hf HP).
-extF; unfold castF, funF; f_equal.
-rewrite -(filterP_f_ord_comp_l HP1' Hq1b).
-rewrite (filterP_f_ord_w_incrF Hq1c (extendPF_incrF Hf HP)).
-rewrite 2!cast_ord_comp cast_ord_id; easy.
-Qed.
-
-Lemma len_neqF_unfunF :
-  forall {n1 n2} {f : 'I_{n1,n2}} {x0} {A1 : 'E^n1},
-    injective f -> lenPF (neqF A1 x0) = lenPF (neqF (unfunF f x0 A1) x0).
-Proof.
-move=>> Hf; apply (lenPF_extendPF Hf), (extendPF_unfunF_neqF _ _ Hf).
-Qed.
-
 Lemma filter_neqF_gen_unfunF :
   forall {F : Type} {n1 n2} {f : 'I_{n1,n2}} (Hf : injective f)
       x0 y0 (A1 : 'E^n1) (B1 : 'F^n1),
@@ -5410,7 +5409,7 @@ destruct (classic (forall i1, A1 i1 = x0)) as [HA1 | HA1].
 apply eqAF_nil; left; apply lenPF0_alt; intuition.
 move: HA1 => /not_all_ex_not_equiv [i0 Hi0].
 move: (extendPF_unfunF_neqF A1 x0 Hf) => HP.
-unfold filter_neqF_gen; rewrite (filterPF_unfunF Hf HP _ i0);
+rewrite (filterPF_unfunF Hf HP _ i0);
     [rewrite !castF_comp; apply castF_eq_r |]; easy.
 Qed.
 
@@ -5439,11 +5438,11 @@ Lemma filter_neqF_unfunF :
       castF (len_neqF_unfunF Hf) (castF (lenPF_permutF Hq1b)
         (filter_neqF x0 (permutF q1 A1))).
 Proof.
-intros; unfold filter_neqF; rewrite filter_neqF_gen_unfunF_l;
+intros; rewrite filter_neqF_gen_unfunF_l;
   [rewrite funF_unfunF; easy | apply (inhabits x0)].
 Qed.
 
-End FilterPF_Facts2.
+End FilterPF_Facts3.
 
 
 Section MapF_Facts.
-- 
GitLab