From 5213a3603dbea542f60bf70e7f642e735f5f22a7 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 11:30:46 +0100
Subject: [PATCH] Fold new notations.

---
 Algebra/Finite_dim/Finite_dim_MS_basis_R.v    |  8 +++----
 .../Finite_dim/Finite_dim_MS_lin_indep_R.v    |  4 ++--
 Algebra/ModuleSpace/ModuleSpace_lin_comb.v    | 16 ++++++-------
 Algebra/Monoid/Monoid_FF.v                    |  2 +-
 Algebra/Monoid/Monomial_order.v               | 24 +++++++++----------
 FEM/multi_index.v                             |  4 ++--
 FEM/poly_LagPd1_ref.v                         |  2 +-
 FEM/poly_Pdk.v                                | 12 +++++-----
 8 files changed, 36 insertions(+), 36 deletions(-)

diff --git a/Algebra/Finite_dim/Finite_dim_MS_basis_R.v b/Algebra/Finite_dim/Finite_dim_MS_basis_R.v
index fcfed23d..dfbb159b 100644
--- a/Algebra/Finite_dim/Finite_dim_MS_basis_R.v
+++ b/Algebra/Finite_dim/Finite_dim_MS_basis_R.v
@@ -307,9 +307,9 @@ apply lin_span_inclF; easy.
 intros i; destruct (classic (exists j, B i = C j)) as [[j Hj] | Hi'].
 rewrite Hj; apply lin_span_inclF_diag.
 specialize (not_ex_all_not _ _ Hi'); simpl; intros Hi; clear Hi'.
-assert (H : lin_dep (insertF ord_max (B i) C)).
+assert (H : lin_dep (insertFmax (B i) C)).
   move: (Nat.lt_irrefl m) => H Hi'; contradict H.
-  apply Hm2; exists (insertF ord_max (B i) C); split; try easy.
+  apply Hm2; exists (insertFmax (B i) C); split; try easy.
   apply insertF_monot_invalF_l; try easy; exists i; easy.
 destruct (lin_dep_insertF_rev _ HC2 H) as [L]; easy.
 Qed.
@@ -374,7 +374,7 @@ assert (H1 : basis PE (concatF Bf C)).
   split; [rewrite (lin_gen_equiv _ Bg)// | easy].
   apply concatF_lub_inclF, lin_span_inclF; try rewrite -Hg; easy.
   intros ig; apply lin_dep_insertF_rev with ord_max; try easy.
-  specialize (Hm2 (insertF ord_max (Bg ig) C)).
+  specialize (Hm2 (insertFmax (Bg ig) C)).
   unfold lin_dep; contradict Hm2; repeat split.
   1,2: intros j; destruct (ord_eq_dec j ord_max) as [Hj | Hj];
     [rewrite insertF_correct_l// | rewrite insertF_correct_r//].
@@ -576,7 +576,7 @@ assert (HC3 : basis PE1 C).
   intros x Hx.
   apply (lin_dep_insertF_rev ord0); try easy.
   specialize (Hn1b n1.+1); apply (proj1 contra_equiv) in Hn1b; auto with arith.
-  rewrite not_ex_all_not_equiv in Hn1b; specialize (Hn1b (insertF ord0 x C)).
+  rewrite not_ex_all_not_equiv in Hn1b; specialize (Hn1b (insertF0 x C)).
   rewrite not_and_equiv -imp_or_equiv in Hn1b; apply Hn1b.
   apply insertF_monot_inclF; easy.
   (* . *)
diff --git a/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v b/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
index f6de9623..3f849d9c 100644
--- a/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
+++ b/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
@@ -328,13 +328,13 @@ rewrite (lc_skipF ord0) HL scal_zero_l plus_zero_l; easy.
 destruct (nextF_rev _ _ HL) as [j0 Hj0]; rewrite zeroF in Hj0; clear HL.
 generalize (HC j0); rewrite (lc_skipF ord0); intros HCj0.
 apply axpy_equiv_R in HCj0; try easy; rewrite -lc_scal_l in HCj0.
-pose (L0 := skipF j0 (L ord0)); pose (L1 := skipF ord0 L);
+pose (L0 := skipF j0 (L ord0)); pose (L1 := skipF0 L);
     pose (L2 := skipT ord0 j0 L).
 pose (M0 := scal (/ L ord0 j0) L0);
     pose (M1 i j := - (M0 j * L1 i j0) + L2 i j).
 pose (D j := skipF j0 C j - scal (M0 j) (C j0)).
 assert (HD : lin_dep D).
-  apply (IHn (skipF ord0 B) _ M1); intros; unfold D, skipF.
+  apply (IHn (skipF0 B) _ M1); intros; unfold D, skipF.
   symmetry; rewrite -plus_minus_r_equiv HC (lc_skipF ord0).
   rewrite HCj0 scal_minus_r -lc_scal_l 2!scal_assoc mult_comm_R.
   rewrite -plus_assoc -lc_opp_l -lc_plus_l -inv_eq_R; easy.
diff --git a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
index 6d7e3f02..609434cb 100644
--- a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
+++ b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
@@ -387,9 +387,9 @@ Lemma lc_liftF_S_l :
   forall {n} L1 (B : 'E^n),
     lin_comb (liftF_S L1) B = lin_comb L1 (castF_1pS (concatF 0 B)).
 Proof.
-intros n L1 B; pose (B1 := insertF ord0 0 B).
+intros n L1 B; pose (B1 := insertF0 0 B).
 assert (HB1a : B1 ord0 = 0) by now unfold B1; rewrite insertF_correct_l.
-assert (HB1b : skipF ord0 B1 = B) by apply skipF_insertF.
+assert (HB1b : skipF0 B1 = B) by apply skipF_insertF.
 rewrite -skipF_first -{1}HB1b -lc_skip_zero_r// -insertF_concatF_0; easy.
 Qed.
 
@@ -397,9 +397,9 @@ Lemma lc_liftF_S_r :
   forall {n} L (B1 : 'E^n.+1),
     lin_comb L (liftF_S B1) = lin_comb (castF_1pS (concatF 0 L)) B1.
 Proof.
-intros n L B1; pose (L1 := insertF ord0 0 L).
+intros n L B1; pose (L1 := insertF0 0 L).
 assert (HL1a : L1 ord0 = 0) by now unfold L1; rewrite insertF_correct_l.
-assert (HL1b : skipF ord0 L1 = L) by apply skipF_insertF.
+assert (HL1b : skipF0 L1 = L) by apply skipF_insertF.
 rewrite -skipF_first -{1}HL1b -lc_skip_zero_l// -insertF_concatF_0; easy.
 Qed.
 
@@ -407,9 +407,9 @@ Lemma lc_widenF_S_l :
   forall {n} L1 (B : 'E^n),
     lin_comb (widenF_S L1) B = lin_comb L1 (castF_p1S (concatF B 0)).
 Proof.
-intros n L1 B; pose (B1 := insertF ord_max 0 B).
+intros n L1 B; pose (B1 := insertFmax 0 B).
 assert (HB1a : B1 ord_max = 0) by now unfold B1; rewrite insertF_correct_l.
-assert (HB1b : skipF ord_max B1 = B) by apply skipF_insertF.
+assert (HB1b : skipFmax B1 = B) by apply skipF_insertF.
 rewrite -skipF_last -{1}HB1b -lc_skip_zero_r// -insertF_concatF_max; easy.
 Qed.
 
@@ -417,9 +417,9 @@ Lemma lc_widenF_S_r :
   forall {n} L (B1 : 'E^n.+1),
     lin_comb L (widenF_S B1) = lin_comb (castF_p1S (concatF L 0)) B1.
 Proof.
-intros n L B1; pose (L1 := insertF ord_max 0 L).
+intros n L B1; pose (L1 := insertFmax 0 L).
 assert (HL1a : L1 ord_max = 0) by now unfold L1; rewrite insertF_correct_l.
-assert (HL1b : skipF ord_max L1 = L) by apply skipF_insertF.
+assert (HL1b : skipFmax L1 = L) by apply skipF_insertF.
 rewrite -skipF_last -{1}HL1b -lc_skip_zero_l// -insertF_concatF_max; easy.
 Qed.
 
diff --git a/Algebra/Monoid/Monoid_FF.v b/Algebra/Monoid/Monoid_FF.v
index db4f3f30..e780f5d8 100644
--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -287,7 +287,7 @@ Proof. intros; rewrite skipF_replaceF; easy. Qed.
 
 Lemma skipF_itemF_0:
   forall (n : nat) (i0 : 'I_n.+1) (H:i0 <> ord0) (x : G),
-   skipF ord0 (itemF n.+1 i0 x) = itemF n (lower_S H) x.
+   skipF0 (itemF n.+1 i0 x) = itemF n (lower_S H) x.
 Proof.
 intros n i0 x H; rewrite skipF_first; unfold liftF_S; extF j.
 case (ord_eq_dec (lift_S j) i0); intros H1.
diff --git a/Algebra/Monoid/Monomial_order.v b/Algebra/Monoid/Monomial_order.v
index abb08009..db8694b6 100644
--- a/Algebra/Monoid/Monomial_order.v
+++ b/Algebra/Monoid/Monomial_order.v
@@ -832,7 +832,7 @@ rewrite !lex_S; rewrite !fct_plus_eq; intros [[H2 H3] | [H2 H3]].
 left; split;
     [contradict H2; apply plus_compat_r | apply H1 with (x ord0)]; easy.
 right; split;
-    [apply HG2 with (x ord0) | apply IHn with (skipF ord0 x)]; easy.
+    [apply HG2 with (x ord0) | apply IHn with (skipF0 x)]; easy.
 Qed.
 
 (* The proof uses the plus regularity hypothesis HG2. *)
@@ -845,7 +845,7 @@ rewrite !colex_S; rewrite !fct_plus_eq; intros [[H2 H3] | [H2 H3]].
 left; split;
     [contradict H2; apply plus_compat_r | apply H1 with (x ord_max)]; easy.
 right; split;
-    [apply HG2 with (x ord_max) | apply IHn with (skipF ord_max x)]; easy.
+    [apply HG2 with (x ord_max) | apply IHn with (skipFmax x)]; easy.
 Qed.
 
 (* The proof depends on the plus regularity hypothesis HG2. *)
@@ -1761,7 +1761,7 @@ Lemma grlex_S :
     sum x <> sum y /\ R (sum x) (sum y) \/
     sum x = sum y /\ x ord0 <> y ord0 /\ R (x ord0) (y ord0) \/
     sum x = sum y /\ x ord0 = y ord0 /\
-            grlex R (skipF ord0 x) (skipF ord0 y).
+            grlex R (skipF0 x) (skipF0 y).
 Proof.
 intros; unfold graded at 1; rewrite lex_S and_or_l;
 do 2 apply or_iff_compat_l; split; intros [H1 [H2 H3]];
@@ -1775,7 +1775,7 @@ Lemma grcolex_S :
     sum x <> sum y /\ R (sum x) (sum y) \/
     sum x = sum y /\ x ord_max <> y ord_max /\ R (x ord_max) (y ord_max) \/
     sum x = sum y /\ x ord_max = y ord_max /\
-            grcolex R (skipF ord_max x) (skipF ord_max y).
+            grcolex R (skipFmax x) (skipFmax y).
 Proof.
 intros; unfold graded at 1; rewrite colex_S and_or_l.
 do 2 apply or_iff_compat_l; split; intros [H1 [H2 H3]];
@@ -1789,7 +1789,7 @@ Lemma grsymlex_S :
     sum x <> sum y /\ R (sum x) (sum y) \/
     sum x = sum y /\ y ord0 <> x ord0 /\ R (y ord0) (x ord0) \/
     sum x = sum y /\ y ord0 = x ord0 /\
-            grsymlex R (skipF ord0 x) (skipF ord0 y).
+            grsymlex R (skipF0 x) (skipF0 y).
 Proof.
 intros; unfold graded at 1; rewrite symlex_S and_or_l.
 do 2 (apply or_iff_compat; [easy |]); split; intros [H1 [H2 H3]];
@@ -1807,7 +1807,7 @@ Lemma grsymlex_S_mo :
     monomial_order R ->
     grsymlex R x y <->
     sum x <> sum y /\ R (sum x) (sum y) \/
-    sum x = sum y /\ grsymlex R (skipF ord0 x) (skipF ord0 y).
+    sum x = sum y /\ grsymlex R (skipF0 x) (skipF0 y).
 Proof.
 intros R n x y HR.
 assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R).
@@ -1831,7 +1831,7 @@ Lemma grevlex_S :
     sum x <> sum y /\ R (sum x) (sum y) \/
     sum x = sum y /\ y ord_max <> x ord_max /\ R (y ord_max) (x ord_max) \/
     sum x = sum y /\ y ord_max = x ord_max /\
-            grevlex R (skipF ord_max x) (skipF ord_max y).
+            grevlex R (skipFmax x) (skipFmax y).
 Proof.
 intros; unfold graded at 1; rewrite revlex_S and_or_l.
 do 2 (apply or_iff_compat; [easy |]); split; intros [H1 [H2 H3]];
@@ -1845,7 +1845,7 @@ Lemma grevlex_S_mo :
     monomial_order R ->
     grevlex R x y <->
     sum x <> sum y /\ R (sum x) (sum y) \/
-    sum x = sum y /\ grevlex R (skipF ord_max x) (skipF ord_max y).
+    sum x = sum y /\ grevlex R (skipFmax x) (skipFmax y).
 Proof.
 intros R n x y HR.
 assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R).
@@ -1944,7 +1944,7 @@ Lemma grlex_lt_S :
     grlex_lt x y <->
     (sum x < sum y)%coq_nat \/
     sum x = sum y /\ (x ord0 < y ord0)%coq_nat \/
-    sum x = sum y /\ x ord0 = y ord0 /\ grlex_lt (skipF ord0 x) (skipF ord0 y).
+    sum x = sum y /\ x ord0 = y ord0 /\ grlex_lt (skipF0 x) (skipF0 y).
 Proof.
 intros; rewrite grlex_S//; apply or_iff_compat;
     [| apply or_iff_compat_r, and_iff_compat_l]; apply br_and_neq_id; easy.
@@ -1956,7 +1956,7 @@ Lemma grcolex_lt_S :
     (sum x < sum y)%coq_nat \/
     sum x = sum y /\ (x ord_max < y ord_max)%coq_nat \/
     sum x = sum y /\ x ord_max = y ord_max /\
-            grcolex_lt (skipF ord_max x) (skipF ord_max y).
+            grcolex_lt (skipFmax x) (skipFmax y).
 Proof.
 intros; rewrite grcolex_S//; apply or_iff_compat;
     [| apply or_iff_compat_r, and_iff_compat_l]; apply br_and_neq_id; easy.
@@ -1966,7 +1966,7 @@ Lemma grsymlex_lt_S :
   forall {n : nat} (x y : 'nat^n.+1),
     grsymlex_lt x y <->
     (sum x < sum y)%coq_nat \/
-    sum x = sum y /\ grsymlex_lt (skipF ord0 x) (skipF ord0 y).
+    sum x = sum y /\ grsymlex_lt (skipF0 x) (skipF0 y).
 Proof.
 intros; rewrite grsymlex_S_mo//; apply or_iff_compat_r, br_and_neq_id; easy.
 Qed.
@@ -1975,7 +1975,7 @@ Lemma grevlex_lt_S :
   forall {n : nat} (x y : 'nat^n.+1),
     grevlex_lt x y <->
     (sum x < sum y)%coq_nat \/
-    sum x = sum y /\ grevlex_lt (skipF ord_max x) (skipF ord_max y).
+    sum x = sum y /\ grevlex_lt (skipFmax x) (skipFmax y).
 Proof.
 intros; rewrite grevlex_S_mo//; apply or_iff_compat_r, br_and_neq_id; easy.
 Qed.
diff --git a/FEM/multi_index.v b/FEM/multi_index.v
index 46b878a3..35cfcca0 100644
--- a/FEM/multi_index.v
+++ b/FEM/multi_index.v
@@ -97,7 +97,7 @@ Definition Slice_fun {d n:nat} (u:nat) (a:'I_n -> 'nat^d) : 'I_n -> 'nat^d.+1
    := mapF (Slice_op u) a.
 
 Lemma Slice_fun_skipF0: forall {d n} u (a:'I_n -> 'nat^d.+1) i,
-   skipF ord0 (Slice_fun u a i) = a i.
+   skipF0 (Slice_fun u a i) = a i.
 Proof.
 intros d n u a i.
 unfold Slice_fun; rewrite mapF_correct; unfold Slice_op.
@@ -634,7 +634,7 @@ Context {d k : nat}.
  Function #f<SUP>d</SUP><SUB>{k,0}</SUB>.<BR>#
  See also Rem 1499, p. 70. *)
 Definition inj_CSdk : 'I_(pbinom d k).+1 -> 'nat^d.+1 :=
-  fun idk => insertF ord0 (k - sum (Adk d k idk))%coq_nat (Adk d k idk).
+  fun idk => insertF0 (k - sum (Adk d k idk))%coq_nat (Adk d k idk).
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
diff --git a/FEM/poly_LagPd1_ref.v b/FEM/poly_LagPd1_ref.v
index 95d4f664..bde3697d 100644
--- a/FEM/poly_LagPd1_ref.v
+++ b/FEM/poly_LagPd1_ref.v
@@ -494,7 +494,7 @@ exists q; split; [easy |]; fun_ext x_ref.
 rewrite Hp3 fct_mult_eq (LagPd1_ref_S ord_max_not_0).
 rewrite -(plus_zero_l (x_ref (lower_S _) * _)); repeat f_equal; [| easy].
 pose (y_ref := widenF_S x_ref); fold y_ref;
-    rewrite -(Hp2 (insertF ord_max 0 y_ref)).
+    rewrite -(Hp2 (insertFmax 0 y_ref)).
 rewrite Hp3 widenF_S_insertF_max insertF_correct_l// mult_zero_l plus_zero_r//.
 rewrite Hface_ref_equiv (LagPd1_ref_S ord_max_not_0) insertF_correct_l; easy.
 Qed.
diff --git a/FEM/poly_Pdk.v b/FEM/poly_Pdk.v
index 4102cf7b..c25606e1 100644
--- a/FEM/poly_Pdk.v
+++ b/FEM/poly_Pdk.v
@@ -323,7 +323,7 @@ rewrite -sum_ind_r H plus_zero_r; apply Adk_sum.
 (* monôme avec ord_max *)
 exists (fun=> 0).
 pose (jSdk:=Adk_inv d.+1 k
-        (replaceF ord_max
+        (replaceFmax
                   (Adk d.+1 k.+1 iSdSk ord_max).-1 (Adk d.+1 k.+1 iSdSk))).
 exists (powF_P (Adk d.+1 k jSdk)).
 split; try split.
@@ -349,7 +349,7 @@ rewrite Nat.add_1_r Nat.succ_pred_pos; auto with zarith.
 rewrite powF_P_replaceF_l; easy.
 apply Nat.add_le_mono_l with (Adk d.+1 k.+1 iSdSk ord_max).
 replace (_ + _)%coq_nat with (Adk d.+1 k.+1 iSdSk ord_max +
-  sum (replaceF ord_max (Adk d.+1 k.+1 iSdSk ord_max).-1 (Adk d.+1 k.+1 iSdSk))); try easy.
+  sum (replaceFmax (Adk d.+1 k.+1 iSdSk ord_max).-1 (Adk d.+1 k.+1 iSdSk))); try easy.
 rewrite sum_replaceF.
 replace (_ + _) with
    ((Adk d.+1 k.+1 iSdSk ord_max).-1 + sum (Adk d.+1 k.+1 iSdSk))%coq_nat; try easy.
@@ -894,7 +894,7 @@ Definition narrow_ord_max := fun {n:nat} (f:'R^n.+1 -> R) (x:'R^n) =>
    f (castF (eq_sym (addn1_sym n)) (concatF x (singleF 0))).
 
 Lemma narrow_ord_max_correct : forall {n:nat} f,
-   (forall (x:'R^n.+1) y, f x = f (replaceF ord_max y x)) ->
+   (forall (x:'R^n.+1) y, f x = f (replaceFmax y x)) ->
    (forall x:'R^n.+1, f x = narrow_ord_max f (widenF_S x)).
 Proof.
 intros n f H x; rewrite (H x 0).
@@ -911,7 +911,7 @@ Qed.
 
 Lemma narrow_ord_max_Derive_multii :
    forall {n} (f:'R^n.+1->R) i j (H: i<> ord_max),
-   (forall (x:'R^n.+1) y, f x = f (replaceF ord_max y x)) ->
+   (forall (x:'R^n.+1) y, f x = f (replaceFmax y x)) ->
     (narrow_ord_max (Derive_multii i j f)) =
        Derive_multii (narrow_S H) j (narrow_ord_max f).
 Proof.
@@ -937,7 +937,7 @@ f_equal; apply ord_inj; now simpl.
 Qed.
 
 Lemma DeriveF_part_scal_fun : forall {n} i (alpha:'nat^n.+1) (Hi: i<>ord_max) (g1:R->R) (g2: 'R^n.+1 -> R),
-  (forall (x:'R^n.+1) y, g2 x = g2 (replaceF ord_max y x)) ->
+  (forall (x:'R^n.+1) y, g2 x = g2 (replaceFmax y x)) ->
   DeriveF_part alpha i (fun x:'R^n.+1 => g1 (x ord_max) * g2 x)
      = (fun x:'R^n.+1 => g1 (x ord_max)
           * DeriveF_part (widenF_S alpha) (narrow_S Hi) (narrow_ord_max g2) (widenF_S x)).
@@ -988,7 +988,7 @@ Qed.
 
 Lemma DeriveF_ind_r_scal_fun : forall {n} (alpha : 'nat^n.+1) f (g1:R->R) (g2: 'R^n.+1 -> R),
    (forall (x:'R^n.+1), Derive_alp alpha ord_max f x = g1 (x ord_max) * g2 x) ->
-   (forall (x:'R^n.+1) y, g2 x = g2 (replaceF ord_max y x)) ->
+   (forall (x:'R^n.+1) y, g2 x = g2 (replaceFmax y x)) ->
    DeriveF alpha f = fun x => g1 (x ord_max) * DeriveF (widenF_S alpha) (narrow_ord_max g2) (widenF_S x).
 Proof.
 intros n alpha f g1 g2 H1 H2.
-- 
GitLab