From c78596096ee1129db5b4a74a9ee093ec83e739dd 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 23:35:35 +0100
Subject: [PATCH] Cosmetics.
---
Algebra/AffineSpace/AffineSpace_aff_map.v | 2 +-
Algebra/Finite_dim/Finite_dim_AS_def.v | 2 +-
Algebra/Monoid/Monoid_FF.v | 8 ++++----
Algebra/Monoid/Monoid_morphism.v | 2 +-
Algebra/Monoid/Monoid_sum.v | 2 +-
Algebra/Monoid/Monomial_order.v | 12 ++++++------
Algebra/Ring/Ring_sub.v | 2 +-
FEM/poly_LagPd1.v | 4 ++--
8 files changed, 17 insertions(+), 17 deletions(-)
diff --git a/Algebra/AffineSpace/AffineSpace_aff_map.v b/Algebra/AffineSpace/AffineSpace_aff_map.v
index 488e53f7..3eb0fc8e 100644
--- a/Algebra/AffineSpace/AffineSpace_aff_map.v
+++ b/Algebra/AffineSpace/AffineSpace_aff_map.v
@@ -563,7 +563,7 @@ Lemma fct_lm_ms_eq :
forall {f : E1 -> E2} O1 u1, fct_lm f O1 u1 = f (O1 + u1) - f O1.
Proof. unfold fct_lm; intros; rewrite ms_vect_eq ms_transl_eq; easy. Qed.
-Lemma fct_lm_ms_eq_ex:
+Lemma fct_lm_ms_eq_ex :
forall {f lf : E1 -> E2},
lin_map lf ->
lf = fct_lm f 0 <-> exists c2, f = lf + (fun=> c2).
diff --git a/Algebra/Finite_dim/Finite_dim_AS_def.v b/Algebra/Finite_dim/Finite_dim_AS_def.v
index dbc8f368..cc1a28e0 100644
--- a/Algebra/Finite_dim/Finite_dim_AS_def.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_def.v
@@ -191,7 +191,7 @@ Lemma has_aff_dim_EX :
forall PE n, has_aff_dim PE n -> { A : 'E^n.+1 | aff_basis PE A }.
Proof. move=>> H; apply ex_EX; induction H as [A H]; exists A; easy. Qed.
-Lemma has_aff_dim_ex:
+Lemma has_aff_dim_ex :
forall PE n, (exists A : 'E^n.+1, aff_basis PE A) -> has_aff_dim PE n.
Proof. move=>> [A HA]. apply (Aff_dim _ _ A HA). Qed.
diff --git a/Algebra/Monoid/Monoid_FF.v b/Algebra/Monoid/Monoid_FF.v
index 3617362b..d41e31e4 100644
--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -200,9 +200,9 @@ Lemma skipF_itemF_diag :
forall n i0 (x : G), skipF i0 (itemF n.+1 i0 x) = 0.
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.
+Lemma skipF_itemF_0 :
+ forall (n : nat) (i0 : 'I_n.+1) (H : i0 <> ord0) (x : G),
+ 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.
@@ -501,7 +501,7 @@ Lemma lastF_zero_compat :
(forall i : 'I_(n1 + n2), (n1 <= i)%coq_nat -> A i = 0) -> lastF A = 0.
Proof. move=>>; erewrite <- lastF_zero; apply lastF_compat. Qed.
-Lemma splitF_zero_compat:
+Lemma splitF_zero_compat :
forall {n1 n2} (A : 'G^(n1 + n2)), A = 0 -> firstF A = 0 /\ lastF A = 0.
Proof. move=>>; apply splitF_compat. Qed.
diff --git a/Algebra/Monoid/Monoid_morphism.v b/Algebra/Monoid/Monoid_morphism.v
index c0844517..f5c86722 100644
--- a/Algebra/Monoid/Monoid_morphism.v
+++ b/Algebra/Monoid/Monoid_morphism.v
@@ -293,7 +293,7 @@ Section Monoid_Morphism_Sum_Facts3.
Context {G1 G2 : AbelianMonoid}.
Context {T : Type}.
-Lemma sum_compF_r:
+Lemma sum_compF_r :
forall {n} (u : G1 -> G2) (f : '(T -> G1)^n),
morphism_m u -> sum (compF_r u f) = u \o sum f.
Proof.
diff --git a/Algebra/Monoid/Monoid_sum.v b/Algebra/Monoid/Monoid_sum.v
index 4546e586..316c7721 100644
--- a/Algebra/Monoid/Monoid_sum.v
+++ b/Algebra/Monoid/Monoid_sum.v
@@ -410,7 +410,7 @@ Section Sum_Facts3.
Context {G : AbelianMonoid}.
Context {T1 T2 : Type}.
-Lemma sum_compF_l:
+Lemma sum_compF_l :
forall {n} (u : '(T2 -> G)^n) (f : T1 -> T2), sum (compF_l u f) = sum u \o f.
Proof.
intros; fun_ext;
diff --git a/Algebra/Monoid/Monomial_order.v b/Algebra/Monoid/Monomial_order.v
index db8694b6..e4f15602 100644
--- a/Algebra/Monoid/Monomial_order.v
+++ b/Algebra/Monoid/Monomial_order.v
@@ -1756,7 +1756,7 @@ Hypothesis HG2 : @plus_is_reg_r G.
(* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grlex_S :
- forall R {n} (x y :'G^n.+1),
+ forall R {n} (x y : 'G^n.+1),
grlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/
sum x = sum y /\ x ord0 <> y ord0 /\ R (x ord0) (y ord0) \/
@@ -1770,7 +1770,7 @@ Qed.
(* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grcolex_S :
- forall R {n} (x y :'G^n.+1),
+ forall R {n} (x y : 'G^n.+1),
grcolex R x y <->
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) \/
@@ -1784,7 +1784,7 @@ Qed.
(* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grsymlex_S :
- forall R {n} (x y :'G^n.+1),
+ forall R {n} (x y : 'G^n.+1),
grsymlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/
sum x = sum y /\ y ord0 <> x ord0 /\ R (y ord0) (x ord0) \/
@@ -1803,7 +1803,7 @@ Proof. tauto. Qed.
(* The proof depends on the equality decidability hypothesis HG1,
and the plus regularity hypothesis HG2. *)
Lemma grsymlex_S_mo :
- forall R {n} (x y :'G^n.+1),
+ forall R {n} (x y : 'G^n.+1),
monomial_order R ->
grsymlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/
@@ -1826,7 +1826,7 @@ Qed.
(* The proof depends on the plus regularity hypothesis HG2. *)
Lemma grevlex_S :
- forall R {n} (x y :'G^n.+1),
+ forall R {n} (x y : 'G^n.+1),
grevlex R x y <->
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) \/
@@ -1841,7 +1841,7 @@ Qed.
(* The proof depends on the equality decidability hypothesis HG1,
and the plus regularity hypothesis HG2. *)
Lemma grevlex_S_mo :
- forall R {n} (x y :'G^n.+1),
+ forall R {n} (x y : 'G^n.+1),
monomial_order R ->
grevlex R x y <->
sum x <> sum y /\ R (sum x) (sum y) \/
diff --git a/Algebra/Ring/Ring_sub.v b/Algebra/Ring/Ring_sub.v
index 574ee8c1..f4923f25 100644
--- a/Algebra/Ring/Ring_sub.v
+++ b/Algebra/Ring/Ring_sub.v
@@ -308,7 +308,7 @@ Definition sub_mult (x y : PK_g) : PK_g :=
Definition sub_one : PK_g := mk_sub (cr_one HPK : PK 1).
-Lemma sub_mult_assoc:
+Lemma sub_mult_assoc :
forall x y z, sub_mult x (sub_mult y z) = sub_mult (sub_mult x y) z.
Proof. intros; apply val_inj, mult_assoc. Qed.
diff --git a/FEM/poly_LagPd1.v b/FEM/poly_LagPd1.v
index aa01d303..54eb192e 100644
--- a/FEM/poly_LagPd1.v
+++ b/FEM/poly_LagPd1.v
@@ -295,7 +295,7 @@ Section T_geom_permutF_Facts.
Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}.
-Hypothesis Hvtx: aff_indep_ms vtx.
+Hypothesis Hvtx : aff_indep_ms vtx.
Context {pi_d : 'I_[d.+1]}.
Hypothesis Hpi_d : injective pi_d.
@@ -342,7 +342,7 @@ Section T_geom_transpF_Facts.
Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}.
-Hypothesis Hvtx: aff_indep_ms vtx.
+Hypothesis Hvtx : aff_indep_ms vtx.
Lemma LagPd1_eq_transpF :
forall i0 j, LagPd1 Hvtx j =
--
GitLab