From 399f2e908588447ae70677f356e187590a7aded6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sat, 8 Mar 2025 23:16:26 +0100
Subject: [PATCH] Propagate new API (from Finite_family).
---
Algebra/AffineSpace/AffineSpace_FF.v | 36 ++++-----
Algebra/AffineSpace/AffineSpace_aff_map.v | 6 +-
Algebra/AffineSpace/AffineSpace_baryc.v | 24 +++---
Algebra/Finite_dim/Finite_dim_AS_aff_gen.v | 4 +-
Algebra/Finite_dim/Finite_dim_AS_aff_indep.v | 8 +-
Algebra/Finite_dim/Finite_dim_AS_aff_span.v | 4 +-
Algebra/Finite_dim/Finite_dim_MS_basis_R.v | 8 +-
Algebra/Finite_dim/Finite_dim_MS_lin_indep.v | 18 ++---
.../Finite_dim/Finite_dim_MS_lin_indep_R.v | 18 ++---
Algebra/Group/Group_compl.v | 16 ++--
Algebra/Group/Group_morphism.v | 2 +-
Algebra/ModuleSpace/ModuleSpace_FF_FT.v | 28 +++----
Algebra/ModuleSpace/ModuleSpace_lin_comb.v | 74 +++++++++----------
Algebra/ModuleSpace/ModuleSpace_lin_map.v | 2 +-
Algebra/Ring/Ring_FF_FT.v | 12 +--
Algebra/Ring/Ring_compl.v | 2 +-
Algebra/Ring/Ring_kron.v | 4 +-
Algebra/Ring/Ring_morphism.v | 2 +-
FEM/geom_transf_affine.v | 4 +-
FEM/geometry.v | 8 +-
FEM/monomial.v | 12 +--
FEM/multi_index.v | 6 +-
FEM/poly_LagP1k.v | 2 +-
FEM/poly_LagPd1.v | 4 +-
FEM/poly_LagPd1_ref.v | 8 +-
FEM/poly_Pdk.v | 69 +++++++++--------
26 files changed, 190 insertions(+), 191 deletions(-)
diff --git a/Algebra/AffineSpace/AffineSpace_FF.v b/Algebra/AffineSpace/AffineSpace_FF.v
index 2c090071..3a4cda46 100644
--- a/Algebra/AffineSpace/AffineSpace_FF.v
+++ b/Algebra/AffineSpace/AffineSpace_FF.v
@@ -30,7 +30,7 @@ COPYING file for more details.
- [vectF O A] is the [n]-family of [V] with [i]-th item [vect O (A i)];
- [translF O u] is the [n]-family of [E] with [i]-th item [transl O (u i)];
- [frameF B i0] is the [n]-family [vectF (B i0) (skipF B i0)];
- - [inv_frameF O u i0] is the [n]-family [translF O (insertF u 0 i0)].
+ - [inv_frameF O u i0] is the [n]-family [translF O (insertF i0 0 u)].
* Used logic axioms
@@ -67,9 +67,9 @@ Context {E : AffineSpace V}.
Definition vectF {n} O (A : 'E^n) : 'V^n := mapF (vect O) A.
Definition translF {n} O (u : 'V^n) : 'E^n := mapF (transl O) u.
-Definition frameF {n} (A : 'E^n.+1) i0 : 'V^n := vectF (A i0) (skipF A i0).
+Definition frameF {n} (A : 'E^n.+1) i0 : 'V^n := vectF (A i0) (skipF i0 A).
Definition inv_frameF {n} O (u : 'V^n) i0 : 'E^n.+1 :=
- translF O (insertF u 0 i0).
+ translF O (insertF i0 0 u).
(** Correctness lemmas. *)
@@ -222,7 +222,7 @@ Qed.
Lemma vectF_insertF :
forall {n} O (A : 'E^n) Ai0 i0,
- vectF O (insertF A Ai0 i0) = insertF (vectF O A) (O --> Ai0) i0.
+ vectF O (insertF i0 Ai0 A) = insertF i0 (O --> Ai0) (vectF O A).
Proof.
intros n O A Ai0 i0; extF i; destruct (ord_eq_dec i i0).
rewrite vectF_correct !insertF_correct_l; easy.
@@ -231,7 +231,7 @@ Qed.
Lemma vectF_skipF :
forall {n} O (A : 'E^n.+1) i0,
- vectF O (skipF A i0) = skipF (vectF O A) i0.
+ vectF O (skipF i0 A) = skipF i0 (vectF O A).
Proof.
intros n O A i0; extF j; destruct (lt_dec j i0).
rewrite vectF_correct !skipF_correct_l; easy.
@@ -401,7 +401,7 @@ Qed.
Lemma translF_insertF :
forall {n} (O : E) (u : 'V^n) u0 i0,
- translF O (insertF u u0 i0) = insertF (translF O u) (O +++ u0) i0.
+ translF O (insertF i0 u0 u) = insertF i0 (O +++ u0) (translF O u).
Proof.
intros n O u u0 i0; extF i; destruct (ord_eq_dec i i0).
rewrite translF_correct !insertF_correct_l; easy.
@@ -410,7 +410,7 @@ Qed.
Lemma translF_skipF :
forall {n} (O : E) (u : 'V^n.+1) i0,
- translF O (skipF u i0) = skipF (translF O u) i0.
+ translF O (skipF i0 u) = skipF i0 (translF O u).
Proof.
intros n O A i0; extF j; destruct (lt_dec j i0).
rewrite translF_correct !skipF_correct_l; easy.
@@ -466,12 +466,12 @@ Qed.
Lemma frameF_inj_equiv :
forall {n} (A : 'E^n.+1) i0,
- injective (frameF A i0) <-> injective (skipF A i0).
+ injective (frameF A i0) <-> injective (skipF i0 A).
Proof. move=>>; apply vectF_inj_equiv. Qed.
Lemma inv_frameF_inj_equiv :
forall {n} (O : E) (u : 'V^n) i0,
- injective (skipF (inv_frameF O u i0) i0) <-> injective u.
+ injective (skipF i0 (inv_frameF O u i0)) <-> injective u.
Proof. move=>>; rewrite -frameF_inj_equiv frameF_inv_frameF; easy. Qed.
(* (preimage (transl (A i0)) PE) will be (vectP PE (A i0)) below *)
@@ -488,20 +488,20 @@ Qed.
Lemma frameF_invalF :
forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
A1 i1 = A2 i2 ->
- invalF (skipF A1 i1) (skipF A2 i2) -> invalF (frameF A1 i1) (frameF A2 i2).
+ invalF (skipF i1 A1) (skipF i2 A2) -> invalF (frameF A1 i1) (frameF A2 i2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.
Lemma frameF_invalF_rev :
forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
A1 i1 = A2 i2 ->
- invalF (frameF A1 i1) (frameF A2 i2) -> invalF (skipF A1 i1) (skipF A2 i2).
+ invalF (frameF A1 i1) (frameF A2 i2) -> invalF (skipF i1 A1) (skipF i2 A2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.
Lemma frameF_invalF_equiv :
forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
A1 i1 = A2 i2 ->
invalF (frameF A1 i1) (frameF A2 i2) <->
- invalF (skipF A1 i1) (skipF A2 i2).
+ invalF (skipF i1 A1) (skipF i2 A2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.
Lemma frameF_1 : forall (A : 'E^1), frameF A ord0 = 0.
@@ -533,8 +533,8 @@ Proof. intros; rewrite frameF_2_1 coupleF_0 coupleF_1; easy. Qed.
Lemma frameF_skipF :
forall {n} (A : 'E^n.+2) {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1),
- frameF (skipF A i0) (insert_ord H10) =
- skipF (frameF A i1) (insert_ord H01).
+ frameF (skipF i0 A) (insert_ord H10) =
+ skipF (insert_ord H01) (frameF A i1).
Proof.
intros n A i0 i1 H10 H01; unfold frameF.
rewrite -vectF_skipF (skipF_correct_alt H10); [| apply skip_insert_ord].
@@ -543,8 +543,8 @@ Qed.
Lemma frameF_skipF_alt :
forall {n} (A : 'E^n.+2) {i0 i1} {H10 : i1 <> i0},
- frameF (skipF A i0) (insert_ord H10) =
- skipF (frameF A i1) (insert_ord (not_eq_sym H10)).
+ frameF (skipF i0 A) (insert_ord H10) =
+ skipF (insert_ord (not_eq_sym H10)) (frameF A i1).
Proof. intros; apply frameF_skipF. Qed.
Lemma frameF_permutF :
@@ -602,12 +602,12 @@ Lemma translF_ms_eq :
Proof. intros; extF; rewrite translF_correct ms_transl_eq; easy. Qed.
Lemma frameF_ms_eq :
- forall {n} (A : 'V^n.+1) i0, frameF A i0 = skipF A i0 - constF n (A i0).
+ forall {n} (A : 'V^n.+1) i0, frameF A i0 = skipF i0 A - constF n (A i0).
Proof. intros; unfold frameF; rewrite vectF_ms_eq; easy. Qed.
Lemma inv_frameF_ms_eq :
forall {n} (u : 'V^n) (O : V) i0,
- inv_frameF O u i0 = constF n.+1 O + insertF u 0 i0.
+ inv_frameF O u i0 = constF n.+1 O + insertF i0 0 u.
Proof. intros; unfold inv_frameF; rewrite translF_ms_eq; easy. Qed.
Lemma injF_ms_equiv :
diff --git a/Algebra/AffineSpace/AffineSpace_aff_map.v b/Algebra/AffineSpace/AffineSpace_aff_map.v
index 7ff3bab7..ffcd34e4 100644
--- a/Algebra/AffineSpace/AffineSpace_aff_map.v
+++ b/Algebra/AffineSpace/AffineSpace_aff_map.v
@@ -358,7 +358,7 @@ Context {E : AffineSpace V}.
Lemma insertF_fct_lm :
forall {n} x0 i0,
- fct_lm (fun A : 'E^n => insertF A x0 i0) (constF n x0) =
+ fct_lm (fun A : 'E^n => insertF i0 x0 A) (constF n x0) =
(fun u : 'V^n => insert0F u i0).
Proof.
intros n x0 i0; unfold fct_lm; fun_ext u; extF i.
@@ -369,7 +369,7 @@ rewrite !insertF_correct_r fct_transl_eq constF_correct transl_correct_r; easy.
Qed.
Lemma insertF_am :
- forall {n} x0 i0, aff_map (fun A : 'E^n => insertF A x0 i0).
+ forall {n} x0 i0, aff_map (fun A : 'E^n => insertF i0 x0 A).
Proof.
intros n x0 i0; apply (am_lm (constF _ x0)).
rewrite insertF_fct_lm; apply insert0F_lm.
@@ -755,7 +755,7 @@ Proof. intros; apply lm_am, component_lm. Qed.
Lemma constF_am : forall n, aff_map_ms (@constF E n).
Proof. intros; apply lm_am, constF_lm. Qed.
-Lemma skipF_am : forall {n} i0, aff_map_ms (skipF^~ i0 : 'E^n.+1 -> 'E^n).
+Lemma skipF_am : forall {n} i0, aff_map_ms (skipF i0 : 'E^n.+1 -> 'E^n).
Proof. intros; apply lm_am, skipF_lm. Qed.
Lemma insert0F_am : forall {n} i0, aff_map_ms (fun A : 'E^n => insert0F A i0).
diff --git a/Algebra/AffineSpace/AffineSpace_baryc.v b/Algebra/AffineSpace/AffineSpace_baryc.v
index 31e0a15e..17a731fb 100644
--- a/Algebra/AffineSpace/AffineSpace_baryc.v
+++ b/Algebra/AffineSpace/AffineSpace_baryc.v
@@ -192,7 +192,7 @@ Proof. move=>>; apply ac_permutF, transp_ord_inj. Qed.
Lemma ac_squeezeF :
forall {n} {L} {A : 'E^n.+1} {i0 i1} G,
i1 <> i0 -> A i1 = A i0 ->
- aff_comb L A G -> aff_comb (squeezeF L i0 i1) (skipF A i1) G.
+ aff_comb L A G -> aff_comb (squeezeF L i0 i1) (skipF i1 A) G.
Proof.
move=>> Hi HA HG; unfold aff_comb.
rewrite vectF_skipF lc_squeezeF// !vectF_correct HA; easy.
@@ -362,7 +362,7 @@ Qed.
Lemma transl_lc :
forall {n} i0 (A : E) L (u : 'V^n),
- A +++ lin_comb L u = barycenter (part1F L i0) (insertF (translF A u) A i0).
+ A +++ lin_comb L u = barycenter (part1F L i0) (insertF i0 A (translF A u)).
Proof.
intros n i0 A L u; apply (baryc_orig_equiv A);
rewrite sum_insertF_baryc; [apply invertible_one |].
@@ -372,12 +372,12 @@ Qed.
Lemma baryc_insertF :
forall {n} i0 O (A : 'E^n) L,
- barycenter (part1F L i0) (insertF A O i0) = O +++ lin_comb L (vectF O A).
+ barycenter (part1F L i0) (insertF i0 O A) = O +++ lin_comb L (vectF O A).
Proof. intros; rewrite (transl_lc i0) translF_vectF; easy. Qed.
Lemma vectF_lc :
forall {n} i0 O (A : 'E^n) L,
- lin_comb L (vectF O A) = O --> barycenter (part1F L i0) (insertF A O i0).
+ lin_comb L (vectF O A) = O --> barycenter (part1F L i0) (insertF i0 O A).
Proof.
intros n i0 O A L; apply (transl_l_inj O).
rewrite -(baryc_insertF i0) transl_correct_l; easy.
@@ -386,7 +386,7 @@ Qed.
Lemma vectF_lc_skipF :
forall {n} i0 (A : 'E^n.+1) L,
lin_comb L (vectF (A i0) A) =
- lin_comb (skipF L i0) (vectF (A i0) (skipF A i0)).
+ lin_comb (skipF i0 L) (vectF (A i0) (skipF i0 A)).
Proof.
intros n i0 A L; rewrite (lc_skipF i0) vectF_correct vect_zero
scal_zero_r plus_zero_l; easy.
@@ -413,7 +413,7 @@ Qed.
Lemma baryc_frameF_equiv :
forall {n L} (A : 'E^n.+1) G i0, sum L = 1 ->
- G = barycenter L A <-> A i0 --> G = lin_comb (skipF L i0) (frameF A i0).
+ G = barycenter L A <-> A i0 --> G = lin_comb (skipF i0 L) (frameF A i0).
Proof.
intros n L A G i0 HL.
assert (HL0 : invertible (sum L)) by now apply invertible_eq_one.
@@ -498,7 +498,7 @@ Qed.
Lemma baryc_skip_zero :
forall {n} L (A : 'E^n.+1) i0,
invertible (sum L) -> L i0 = 0 ->
- barycenter L A = barycenter (skipF L i0) (skipF A i0).
+ barycenter L A = barycenter (skipF i0 L) (skipF i0 A).
Proof.
intros n L A i0 HL Hi0; apply baryc_equiv; unfold aff_comb.
rewrite -(plus_zero_l (sum _)) -Hi0 -sum_skipF; easy.
@@ -512,7 +512,7 @@ Qed.
Lemma baryc_insert_zero :
forall {n} L (A : 'E^n) x0 i0,
invertible (sum L) ->
- barycenter L A = barycenter (insertF L 0 i0) (insertF A x0 i0).
+ barycenter L A = barycenter (insertF i0 0 L) (insertF i0 x0 A).
Proof.
intros n L A x0 i0 HL; rewrite (baryc_skip_zero (insertF _ _ _) _ i0).
rewrite !skipF_insertF; easy.
@@ -523,7 +523,7 @@ Qed.
Lemma baryc_squeezeF :
forall {n} {L} {A : 'E^n.+1} {i0 i1},
invertible (sum L) -> i1 <> i0 -> A i1 = A i0 ->
- barycenter L A = barycenter (squeezeF L i0 i1) (skipF A i1).
+ barycenter L A = barycenter (squeezeF L i0 i1) (skipF i1 A).
Proof.
intros n L A i0 i1 HL Hia Hib; apply baryc_equiv.
apply invertible_sum_squeezeF; easy.
@@ -549,10 +549,10 @@ destruct (classic (injective A)) as [HA | HA].
exists n.+1, L, A; repeat split; try apply invalF_refl; easy.
move: HA => /not_all_ex_not [i1 /not_all_ex_not [i0 Hi]].
move: Hi => /not_imp_and_equiv [Hia Hib].
-destruct (Hn (squeezeF L i0 i1) (skipF A i1)) as [m [M [B [H1 [H2 [H3 H4]]]]]];
+destruct (Hn (squeezeF L i0 i1) (skipF i1 A)) as [m [M [B [H1 [H2 [H3 H4]]]]]];
try now apply invertible_sum_squeezeF.
exists m, M, B; repeat split; try easy.
-apply (skipF_monot_r _ _ i1); easy.
+apply (skipF_monot_r i1); easy.
rewrite (baryc_squeezeF _ Hib); easy.
Qed.
@@ -913,7 +913,7 @@ Qed.
Lemma baryc_frameF_ms_eq :
forall {n L} {A : 'E^n.+1} i0, sum L = 1 ->
barycenter_ms L A =
- A i0 + lin_comb (skipF L i0) (skipF A i0 - constF n (A i0)).
+ A i0 + lin_comb (skipF i0 L) (skipF i0 A - constF n (A i0)).
Proof.
intros n L A i0 HL; apply eq_sym, (baryc_frameF_equiv A _ i0 HL).
rewrite frameF_ms_eq; apply: minus_plus_l.
diff --git a/Algebra/Finite_dim/Finite_dim_AS_aff_gen.v b/Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
index f9e3fee2..2d0b7f8d 100644
--- a/Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
@@ -185,7 +185,7 @@ Context {E : ModuleSpace R_Ring}.
Lemma aff_gen_lin_gen_ms_equiv :
forall {PE : E -> Prop} {n} {A : 'E^n.+1} O i0, PE O -> aff_span_ms A O ->
aff_gen_ms PE A <->
- lin_gen (fun u => PE (O + u)) (skipF A i0 - constF n (A i0)).
+ lin_gen (fun u => PE (O + u)) (skipF i0 A - constF n (A i0)).
Proof.
intros PE n A O i0; rewrite -vectP_ms_eq -frameF_ms_eq;
apply (aff_gen_lin_gen_equiv i0).
@@ -194,7 +194,7 @@ Qed.
Lemma lin_gen_aff_gen_ms_equiv :
forall {PE : E -> Prop} {n} {u : 'E^n} (O : E) i0, zero_closed PE ->
lin_gen PE u <->
- aff_gen_ms (fun A => PE (A - O)) (constF n.+1 O + insertF u 0 i0).
+ aff_gen_ms (fun A => PE (A - O)) (constF n.+1 O + insertF i0 0 u).
Proof.
move=>>; rewrite -translP_ms_eq -inv_frameF_ms_eq; apply lin_gen_aff_gen_equiv.
Qed.
diff --git a/Algebra/Finite_dim/Finite_dim_AS_aff_indep.v b/Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
index fe0daece..d6867d43 100644
--- a/Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
@@ -67,7 +67,7 @@ intros L; unfold frameF; rewrite (vectF_change_orig (A i0))
lc_plus_r lc_constF_r scal_opp -vect_sym vectF_skipF.
rewrite -lc_insertF_l (lc_skip_zero_r i0 (vectF_zero_alt _ _)).
move=> /HA /extF_rev HL1.
-assert (HL1a : skipF L (insert_ord (not_eq_sym Hi)) = 0).
+assert (HL1a : skipF (insert_ord (not_eq_sym Hi)) L = 0).
apply skipF_zero_compat; move=> j /skip_insert_ord_neq Hj.
specialize (HL1 (insert_ord Hj)).
rewrite skipF_correct insertF_correct in HL1; easy.
@@ -147,8 +147,8 @@ Qed.
Lemma aff_indep_decomp_uniq_rev :
forall {n} {A : 'E^n.+1}, baryc_injL A -> aff_indep A.
Proof.
-intros n A HA L HL; apply (insertF_inj_l _ _ (1 - sum L) 1 ord0).
-replace (insertF L _ _) with (part1F0 L) by easy; rewrite -itemF_insertF.
+intros n A HA L HL; apply (insertF_inj_l ord0 (1 - sum L) 1).
+replace (insertF _ _ L) with (part1F0 L) by easy; rewrite -itemF_insertF.
assert (H1 : sum (part1F L ord0) = 1) by apply part1F_sum.
assert (H2 : sum (itemF n.+1 1 ord0) = (1 : K)) by now apply sum_itemF.
apply HA; [easy.. |]; apply (vect_l_inj (A ord0)).
@@ -244,7 +244,7 @@ Lemma aff_indep_coupleF_equiv :
Proof. intros; rewrite aff_indep_2_equiv coupleF_0 coupleF_1; easy. Qed.
Lemma aff_indep_skipF :
- forall {n} {A : 'E^n.+2} i0, aff_indep A -> aff_indep (skipF A i0).
+ forall {n} {A : 'E^n.+2} i0, aff_indep A -> aff_indep (skipF i0 A).
Proof.
intros n A i0 HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |].
(* *)
diff --git a/Algebra/Finite_dim/Finite_dim_AS_aff_span.v b/Algebra/Finite_dim/Finite_dim_AS_aff_span.v
index fe176599..9f8e697e 100644
--- a/Algebra/Finite_dim/Finite_dim_AS_aff_span.v
+++ b/Algebra/Finite_dim/Finite_dim_AS_aff_span.v
@@ -340,14 +340,14 @@ Proof. move=>>; apply aff_span_ext. Qed.
Lemma lin_span_aff_span_ms :
forall {n} {u : 'E^n} O i0, lin_span u =
- fun v => aff_span_ms (constF n.+1 O + insertF u 0 i0) (O + v).
+ fun v => aff_span_ms (constF n.+1 O + insertF i0 0 u) (O + v).
Proof.
intros; rewrite -inv_frameF_ms_eq -vectP_ms_eq; apply lin_span_aff_span.
Qed.
Lemma aff_span_lin_span_ms :
forall {n} {A : 'E^n.+1} {O} i0, aff_span_ms A O ->
- aff_span_ms A = fun B => lin_span (skipF A i0 - constF n (A i0)) (B - O).
+ aff_span_ms A = fun B => lin_span (skipF i0 A - constF n (A i0)) (B - O).
Proof.
intros; rewrite -frameF_ms_eq -translP_ms_eq; apply aff_span_lin_span; easy.
Qed.
diff --git a/Algebra/Finite_dim/Finite_dim_MS_basis_R.v b/Algebra/Finite_dim/Finite_dim_MS_basis_R.v
index 23c7b091..fcfed23d 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 C (B i) ord_max)).
+assert (H : lin_dep (insertF ord_max (B i) C)).
move: (Nat.lt_irrefl m) => H Hi'; contradict H.
- apply Hm2; exists (insertF C (B i) ord_max); split; try easy.
+ apply Hm2; exists (insertF ord_max (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 C (Bg ig) ord_max)).
+ specialize (Hm2 (insertF ord_max (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 C x ord0)).
+ rewrite not_ex_all_not_equiv in Hn1b; specialize (Hn1b (insertF ord0 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.v b/Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
index 0ed94004..31831b04 100644
--- a/Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
+++ b/Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
@@ -174,18 +174,18 @@ rewrite concatF_correct_l concat_l_first
Qed.
Lemma lin_dep_insertF_compat :
- forall {n} {B : 'E^n} x0 i0, lin_dep B -> lin_dep (insertF B x0 i0).
+ forall {n} {B : 'E^n} x0 i0, lin_dep B -> lin_dep (insertF i0 x0 B).
Proof.
intros n B x0 i0; rewrite 2!lin_dep_ex; move=> [L [HL /nextF_rev [i Hi]]].
-exists (insertF L 0 i0); split.
+exists (insertF i0 0 L); split.
rewrite lc_insertF scal_zero_l HL plus_zero_l; easy.
apply nextF; exists (skip_ord i0 i); rewrite insertF_correct; easy.
Qed.
Lemma lin_dep_skipF_reg :
- forall {n} {B : 'E^n.+1} i0, lin_dep (skipF B i0) -> lin_dep B.
+ forall {n} {B : 'E^n.+1} i0, lin_dep (skipF i0 B) -> lin_dep B.
Proof.
-intros n B i0; rewrite -{2}(insertF_skipF B i0).
+intros n B i0; rewrite -{2}(insertF_skipF i0 B).
apply lin_dep_insertF_compat.
Qed.
@@ -308,11 +308,11 @@ intros [H1 H2]; eapply lin_dep_concatF_not_disjF; [apply H1 | easy].
Qed.
Lemma lin_indep_insertF_reg :
- forall {n} {B : 'E^n} x0 i0, lin_indep (insertF B x0 i0) -> lin_indep B.
+ forall {n} {B : 'E^n} x0 i0, lin_indep (insertF i0 x0 B) -> lin_indep B.
Proof. move=>>; rewrite contra_equiv; apply lin_dep_insertF_compat. Qed.
Lemma lin_indep_skipF_compat :
- forall {n} {B : 'E^n.+1} i0, lin_indep B -> lin_indep (skipF B i0).
+ forall {n} {B : 'E^n.+1} i0, lin_indep B -> lin_indep (skipF i0 B).
Proof. move=>>; rewrite contra_equiv; apply lin_dep_skipF_reg. Qed.
Lemma lin_indep_not_line :
@@ -423,9 +423,9 @@ Qed.
#<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
Th 6.61, pp. 189-190. (=>) *)
Lemma lin_dep_insertF :
- forall {n} {B : 'E^n} {x0} i0, lin_span B x0 -> lin_dep (insertF B x0 i0).
+ forall {n} {B : 'E^n} {x0} i0, lin_span B x0 -> lin_dep (insertF i0 x0 B).
Proof.
-intros n B x0 i0 [L]; apply lin_dep_ex; exists (insertF L (- 1%K) i0); split.
+intros n B x0 i0 [L]; apply lin_dep_ex; exists (insertF i0 (- 1%K) L); split.
rewrite lc_insertF scal_opp_l scal_one; apply: plus_opp_l.
rewrite -(insertF_zero i0); apply insertF_nextF_compat_r.
apply one_not_zero in HK; contradict HK; apply opp_inj; rewrite opp_zero; easy.
@@ -433,7 +433,7 @@ Qed.
Lemma lin_indep_insertF_rev :
forall {n} {B : 'E^n} {x0} i0,
- lin_indep (insertF B x0 i0) -> ~ lin_span B x0.
+ lin_indep (insertF i0 x0 B) -> ~ lin_span B x0.
Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_insertF. Qed.
End Linear_independent_Facts.
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 9609fa1e..1050c45a 100644
--- a/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
+++ b/Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
@@ -266,7 +266,7 @@ Proof. move=>>; rewrite -contra_equiv; apply lin_indep_coupleF_sym. Qed.
Th 6.61, pp. 189-190. (<=) *)
Lemma lin_dep_insertF_rev :
forall {n} {B : 'E^n} {x0} i0,
- lin_indep B -> lin_dep (insertF B x0 i0) -> lin_span B x0.
+ lin_indep B -> lin_dep (insertF i0 x0 B) -> lin_span B x0.
Proof.
move=> n B x0 i0 HB /lin_dep_ex [L [HL1 HL2]];
rewrite lc_insertF_r in HL1.
@@ -277,7 +277,7 @@ apply HB in HL1; contradict HL2.
apply (extF_zero_skipF _ i0); easy.
(* *)
assert (HL3' : - L i0 <> 0) by now rewrite -opp_zero; apply opp_neq_compat.
-apply lin_span_ex; exists (scal (/ - L i0) (skipF L i0)); symmetry.
+apply lin_span_ex; exists (scal (/ - L i0) (skipF i0 L)); symmetry.
apply (scal_reg_r_R (- L i0)); try easy.
rewrite lc_scal_l scal_assoc scal_opp_l; apply plus_is_zero_l.
apply invertible_equiv_R in HL3'.
@@ -289,7 +289,7 @@ Qed.
Th 6.61, pp. 189-190. (<=>) *)
Lemma lin_dep_insertF_equiv :
forall {n} {B : 'E^n} {x0} i0,
- lin_indep B -> lin_dep (insertF B x0 i0) <-> lin_span B x0.
+ lin_indep B -> lin_dep (insertF i0 x0 B) <-> lin_span B x0.
Proof.
intros; split; [apply lin_dep_insertF_rev; easy |
apply lin_dep_insertF, nonzero_struct_R].
@@ -297,14 +297,14 @@ Qed.
Lemma lin_indep_insertF :
forall {n} {B : 'E^n} {x0} i0,
- lin_indep B -> ~ lin_span B x0 -> lin_indep (insertF B x0 i0).
+ lin_indep B -> ~ lin_span B x0 -> lin_indep (insertF i0 x0 B).
Proof.
move=>> HB; rewrite contra_not_l_equiv; apply lin_dep_insertF_rev; easy.
Qed.
Lemma lin_indep_insertF_equiv :
forall {n} {B : 'E^n} {x0} i0,
- lin_indep B -> lin_indep (insertF B x0 i0) <-> ~ lin_span B x0.
+ lin_indep B -> lin_indep (insertF i0 x0 B) <-> ~ lin_span B x0.
Proof. move=>>; rewrite iff_not_r_equiv; apply lin_dep_insertF_equiv. Qed.
(**
@@ -320,7 +320,7 @@ apply lc_zero_compat_r; extF i; rewrite HC; apply lc_nil.
(* *)
destruct (classic (L ord0 = 0)) as [HL | HL].
(* . *)
-eapply lin_dep_ext; try apply (insertF_skipF _ ord_max).
+eapply lin_dep_ext; try apply (insertF_skipF ord_max).
apply lin_dep_insertF_compat; rewrite skipF_last; eapply IHn; intros j.
unfold widenF_S; rewrite (HC (widen_S j)).
rewrite (lc_skipF ord0) HL scal_zero_l plus_zero_l; easy.
@@ -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 (L ord0) j0); pose (L1 := skipF L ord0);
+pose (L0 := skipF j0 (L ord0)); pose (L1 := skipF ord0 L);
pose (L2 := skipT L ord0 j0).
pose (M0 := scal (/ L ord0 j0) L0);
pose (M1 i j := - (M0 j * L1 i j0) + L2 i j).
-pose (D j := skipF C j0 j - scal (M0 j) (C j0)).
+pose (D j := skipF j0 C j - scal (M0 j) (C j0)).
assert (HD : lin_dep D).
- apply (IHn (skipF B ord0) _ M1); intros; unfold D, skipF.
+ apply (IHn (skipF ord0 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/Group/Group_compl.v b/Algebra/Group/Group_compl.v
index a9481347..bf9a0b86 100644
--- a/Algebra/Group/Group_compl.v
+++ b/Algebra/Group/Group_compl.v
@@ -304,7 +304,7 @@ Lemma concatF_minus :
Proof. intros; rewrite !minus_eq concatF_plus concatF_opp; easy. Qed.
Lemma insertF_opp :
- forall {n} (A : 'G^n) a i0, insertF (- A) (- a) i0 = - insertF A a i0.
+ forall {n} (A : 'G^n) a0 i0, insertF i0 (-a0) (- A) = - insertF i0 a0 A.
Proof.
intros n A a i0; extF i; rewrite fct_opp_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
@@ -313,19 +313,19 @@ Qed.
Lemma insertF_minus :
forall {n} (A B : 'G^n) a0 b0 i0,
- insertF (A - B) (a0 - b0) i0 = insertF A a0 i0 - insertF B b0 i0.
+ insertF i0 (a0 - b0) (A - B) = insertF i0 a0 A - insertF i0 b0 B.
Proof. intros; rewrite !minus_eq insertF_plus insertF_opp; easy. Qed.
-Lemma skipF_opp : forall {n} (A : 'G^n.+1) i0, skipF (- A) i0 = - skipF A i0.
+Lemma skipF_opp : forall {n} (A : 'G^n.+1) i0, skipF i0 (- A) = - skipF i0 A.
Proof. easy. Qed.
Lemma skipF_minus :
- forall {n} (A B : 'G^n.+1) i0, skipF (A - B) i0 = skipF A i0 - skipF B i0.
+ forall {n} (A B : 'G^n.+1) i0, skipF i0 (A - B) = skipF i0 A - skipF i0 B.
Proof. easy. Qed.
Lemma replaceF_opp :
forall {n} (A : 'G^n.+1) a0 i0,
- replaceF (- A) (- a0) i0 = - replaceF A a0 i0.
+ replaceF i0 (- a0) (- A) = - replaceF i0 a0 A.
Proof.
intros n A a0 i0; extF i; rewrite fct_opp_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
@@ -334,7 +334,7 @@ Qed.
Lemma replaceF_minus :
forall {n} (A B : 'G^n.+1) a0 b0 i0,
- replaceF (A - B) (a0 - b0) i0 = replaceF A a0 i0 - replaceF B b0 i0.
+ replaceF i0 (a0 - b0) (A - B) = replaceF i0 a0 A - replaceF i0 b0 B.
Proof. intros; rewrite !minus_eq replaceF_plus replaceF_opp; easy. Qed.
Lemma permutF_opp :
@@ -353,14 +353,14 @@ Lemma sum_squeezeF :
forall {n} (u : 'G^n.+1) {i0 i1}, i1 <> i0 -> sum (squeezeF u i0 i1) = sum u.
Proof.
intros n u i0 i1 Hi.
-apply (plus_reg_l (u i0 + replaceF u (u i0 + u i1) i0 i1)).
+apply (plus_reg_l (u i0 + replaceF i0 (u i0 + u i1) u i1)).
rewrite -plus_assoc -sum_skipF replaceF_correct_r//.
rewrite sum_replaceF; easy.
Qed.
Lemma injF_g_equiv :
forall {n} (u : 'G^n.+1),
- injective u <-> forall i0, ~ inF 0 (skipF u i0 - constF _ (u i0)).
+ injective u <-> forall i0, ~ inF 0 (skipF i0 u - constF _ (u i0)).
Proof.
intros; rewrite -skipF_not_inF_equiv; split;
intros Hu i0 [j Hj]; move: (Hu i0) Hj; rewrite -contra_equiv.
diff --git a/Algebra/Group/Group_morphism.v b/Algebra/Group/Group_morphism.v
index 3eb6ca98..56129aae 100644
--- a/Algebra/Group/Group_morphism.v
+++ b/Algebra/Group/Group_morphism.v
@@ -152,7 +152,7 @@ Proof. easy. Qed.
Lemma constF_mg : forall n, morphism_g (@constF G n).
Proof. easy. Qed.
-Lemma skipF_mg : forall {n} i0, morphism_g (skipF^~ i0 : 'G^n.+1 -> 'G^n).
+Lemma skipF_mg : forall {n} i0, morphism_g (skipF i0 : 'G^n.+1 -> 'G^n).
Proof. easy. Qed.
Lemma insert0F_mg : forall {n} i0, morphism_g (fun A : 'G^n => insert0F A i0).
diff --git a/Algebra/ModuleSpace/ModuleSpace_FF_FT.v b/Algebra/ModuleSpace/ModuleSpace_FF_FT.v
index f6648080..9d20f32c 100644
--- a/Algebra/ModuleSpace/ModuleSpace_FF_FT.v
+++ b/Algebra/ModuleSpace/ModuleSpace_FF_FT.v
@@ -268,8 +268,8 @@ Proof. easy. Qed.
Lemma scalF_insertF :
forall {n} a a0 (u : 'E^n) x0 i0,
- scalF (insertF a a0 i0) (insertF u x0 i0) =
- insertF (scalF a u) (scal a0 x0) i0.
+ scalF (insertF i0 a0 a) (insertF i0 x0 u) =
+ insertF i0 (scal a0 x0) (scalF a u).
Proof.
intros; extF; rewrite scalF_correct; unfold insertF;
destruct (ord_eq_dec _ _); easy.
@@ -277,32 +277,32 @@ Qed.
Lemma scalF_insert2F :
forall {n} a a0 a1 (u : 'E^n) x0 x1 {i0 i1} (H : i1 <> i0),
- scalF (insert2F a a0 a1 H) (insert2F u x0 x1 H) =
- insert2F (scalF a u) (scal a0 x0) (scal a1 x1) H.
+ scalF (insert2F H a0 a1 a) (insert2F H x0 x1 u) =
+ insert2F H (scal a0 x0) (scal a1 x1) (scalF a u).
Proof. intros; rewrite 3!insert2F_correct 2!scalF_insertF; easy. Qed.
Lemma scalF_skipF :
forall {n} a (u : 'E^n.+1) i0,
- scalF (skipF a i0) (skipF u i0) = skipF (scalF a u) i0.
+ scalF (skipF i0 a) (skipF i0 u) = skipF i0 (scalF a u).
Proof. easy. Qed.
Lemma scalF_skip2F :
forall {n} a (u : 'E^n.+2) {i0 i1} (H : i1 <> i0),
- scalF (skip2F a H) (skip2F u H) = skip2F (scalF a u) H.
+ scalF (skip2F H a) (skip2F H u) = skip2F H (scalF a u).
Proof. easy. Qed.
Lemma scalF_replaceF :
forall {n} a a0 (u : 'E^n) x0 i0,
- scalF (replaceF a a0 i0) (replaceF u x0 i0) =
- replaceF (scalF a u) (scal a0 x0) i0.
+ scalF (replaceF i0 a0 a) (replaceF i0 x0 u) =
+ replaceF i0 (scal a0 x0) (scalF a u).
Proof.
intros; rewrite 3!replaceF_equiv_def_skipF scalF_skipF scalF_insertF; easy.
Qed.
Lemma scalF_replace2F :
forall {n} a a0 a1 (u : 'E^n) x0 x1 i0 i1,
- scalF (replace2F a a0 a1 i0 i1) (replace2F u x0 x1 i0 i1) =
- replace2F (scalF a u) (scal a0 x0) (scal a1 x1) i0 i1.
+ scalF (replace2F i0 i1 a0 a1 a) (replace2F i0 i1 x0 x1 u) =
+ replace2F i0 i1 (scal a0 x0) (scal a1 x1) (scalF a u).
Proof. intros; rewrite 2!scalF_replaceF; easy. Qed.
Lemma scalF_permutF :
@@ -367,7 +367,7 @@ Qed.
Lemma scalF_squeezeF :
forall {n} a (u : 'E^n.+1) {i0 i1},
i1 <> i0 -> u i1 = u i0 ->
- scalF (squeezeF a i0 i1) (skipF u i1) = squeezeF (scalF a u) i0 i1.
+ scalF (squeezeF a i0 i1) (skipF i1 u) = squeezeF (scalF a u) i0 i1.
Proof.
intros n a u i0 i1 Hi Hu; extF j.
rewrite scalF_correct; destruct (ord_eq_dec (skip_ord i1 j) i0) as [Hj | Hj].
@@ -460,7 +460,7 @@ Qed.
Lemma insertF_scal :
forall {n} l (A : 'E^n) a0 i0,
- insertF (scal l A) (scal l a0) i0 = scal l insertF A a0 i0.
+ insertF i0 (scal l a0) (scal l A) = scal l insertF i0 a0 A.
Proof.
intros n l A a0 i0; extF i; rewrite !fct_scal_eq;
destruct (ord_eq_dec i i0);
@@ -474,12 +474,12 @@ intros; unfold insert0F at 1; rewrite -{1}(scal_zero_r l) insertF_scal; easy.
Qed.
Lemma skipF_scal :
- forall {n} l (A : 'E^n.+1) i0, skipF (scal l A) i0 = scal l skipF A i0.
+ forall {n} l (A : 'E^n.+1) i0, skipF i0 (scal l A) = scal l skipF i0 A.
Proof. easy. Qed.
Lemma replaceF_scal :
forall {n} l (A : 'E^n.+1) a0 i0,
- replaceF (scal l A) (scal l a0) i0 = scal l replaceF A a0 i0.
+ replaceF i0 (scal l a0) (scal l A) = scal l replaceF i0 a0 A.
Proof.
intros n l A a0 i0; extF i; rewrite !fct_scal_eq;
destruct (ord_eq_dec i i0);
diff --git a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
index f2cffa9d..4ed15273 100644
--- a/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
+++ b/Algebra/ModuleSpace/ModuleSpace_lin_comb.v
@@ -325,35 +325,35 @@ Proof. intros; rewrite lc_splitF firstF_concatF lastF_concatF; easy. Qed.
Lemma lc_skipF :
forall {n} {L} {B : 'E^n.+1} i0,
- lin_comb L B = scal (L i0) (B i0) + lin_comb (skipF L i0) (skipF B i0).
+ lin_comb L B = scal (L i0) (B i0) + lin_comb (skipF i0 L) (skipF i0 B).
Proof. intros n L B i0; unfold lin_comb; rewrite (sum_skipF _ i0); easy. Qed.
Lemma lc_skipF_ex_l :
forall {n} L0 L1 (B : 'E^n.+1) i0,
- exists L, lin_comb L B = scal L0 (B i0) + lin_comb L1 (skipF B i0) /\
- L i0 = L0 /\ skipF L i0 = L1.
+ exists L, lin_comb L B = scal L0 (B i0) + lin_comb L1 (skipF i0 B) /\
+ L i0 = L0 /\ skipF i0 L = L1.
Proof.
-intros n L0 L1 B i0; destruct (skipF_ex L0 L1 i0) as [L [HL0 HL1]].
+intros n L0 L1 B i0; destruct (skipF_ex i0 L0 L1) as [L [HL0 HL1]].
exists L; repeat split; try easy; rewrite -HL0 -HL1; apply lc_skipF.
Qed.
Lemma lc_skipF_ex_r :
forall {n} L u0 (B1 : 'E^n) i0,
- exists B, lin_comb L B = scal (L i0) u0 + lin_comb (skipF L i0) B1 /\
- B i0 = u0 /\ skipF B i0 = B1.
+ exists B, lin_comb L B = scal (L i0) u0 + lin_comb (skipF i0 L) B1 /\
+ B i0 = u0 /\ skipF i0 B = B1.
Proof.
-intros n L u0 B1 i0; destruct (skipF_ex u0 B1 i0) as [B [Hu0 HB1]].
+intros n L u0 B1 i0; destruct (skipF_ex i0 u0 B1) as [B [Hu0 HB1]].
exists B; repeat split; try easy; rewrite -Hu0 -HB1; apply lc_skipF.
Qed.
Lemma lc_one :
forall {n L} {B : 'E^n.+1} i0,
- skipF (scalF L B) i0 = 0 -> lin_comb L B = scal (L i0) (B i0).
+ skipF i0 (scalF L B) = 0 -> lin_comb L B = scal (L i0) (B i0).
Proof. move=>>; rewrite -scalF_correct; apply sum_one. Qed.
Lemma lc_one_l :
forall {n L} {B : 'E^n.+1} i0,
- skipF L i0 = 0 -> lin_comb L B = scal (L i0) (B i0).
+ skipF i0 L = 0 -> lin_comb L B = scal (L i0) (B i0).
Proof.
intros; apply lc_one; rewrite -scalF_skipF.
apply scalF_zero_compat_l; easy.
@@ -361,7 +361,7 @@ Qed.
Lemma lc_one_r :
forall {n L} {B : 'E^n.+1} i0,
- skipF B i0 = 0 -> lin_comb L B = scal (L i0) (B i0).
+ skipF i0 B = 0 -> lin_comb L B = scal (L i0) (B i0).
Proof.
intros; apply lc_one; rewrite -scalF_skipF.
apply scalF_zero_compat_r; easy.
@@ -369,7 +369,7 @@ Qed.
Lemma lc_skip_zero_l :
forall {n L} {B : 'E^n.+1} i0,
- L i0 = 0 -> lin_comb L B = lin_comb (skipF L i0) (skipF B i0).
+ L i0 = 0 -> lin_comb L B = lin_comb (skipF i0 L) (skipF i0 B).
Proof.
intros n L B i0 HL; unfold lin_comb; rewrite (sum_skip_zero i0); try easy.
rewrite scalF_correct HL scal_zero_l; easy.
@@ -377,7 +377,7 @@ Qed.
Lemma lc_skip_zero_r :
forall {n L} {B : 'E^n.+1} i0,
- B i0 = 0 -> lin_comb L B = lin_comb (skipF L i0) (skipF B i0).
+ B i0 = 0 -> lin_comb L B = lin_comb (skipF i0 L) (skipF i0 B).
Proof.
intros n L B i0 HB; unfold lin_comb; rewrite (sum_skip_zero i0); try easy.
rewrite scalF_correct HB scal_zero_r; easy.
@@ -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 B 0 ord0).
+intros n L1 B; pose (B1 := insertF ord0 0 B).
assert (HB1a : B1 ord0 = 0) by now unfold B1; rewrite insertF_correct_l.
-assert (HB1b : skipF B1 ord0 = B) by apply skipF_insertF.
+assert (HB1b : skipF ord0 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 L 0 ord0).
+intros n L B1; pose (L1 := insertF ord0 0 L).
assert (HL1a : L1 ord0 = 0) by now unfold L1; rewrite insertF_correct_l.
-assert (HL1b : skipF L1 ord0 = L) by apply skipF_insertF.
+assert (HL1b : skipF ord0 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 B 0 ord_max).
+intros n L1 B; pose (B1 := insertF ord_max 0 B).
assert (HB1a : B1 ord_max = 0) by now unfold B1; rewrite insertF_correct_l.
-assert (HB1b : skipF B1 ord_max = B) by apply skipF_insertF.
+assert (HB1b : skipF ord_max 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 L 0 ord_max).
+intros n L B1; pose (L1 := insertF ord_max 0 L).
assert (HL1a : L1 ord_max = 0) by now unfold L1; rewrite insertF_correct_l.
-assert (HL1b : skipF L1 ord_max = L) by apply skipF_insertF.
+assert (HL1b : skipF ord_max L1 = L) by apply skipF_insertF.
rewrite -skipF_last -{1}HL1b -lc_skip_zero_l// -insertF_concatF_max; easy.
Qed.
@@ -427,20 +427,20 @@ Lemma lc_skip2F :
forall {n} L (B : 'E^n.+2) {i0 i1} (H : i1 <> i0),
lin_comb L B =
scal (L i0) (B i0) + scal (L i1) (B i1) +
- lin_comb (skip2F L H) (skip2F B H).
+ lin_comb (skip2F H L) (skip2F H B).
Proof.
intros n L B i0 i1 H; unfold lin_comb; rewrite (sum_skip2F _ H); easy.
Qed.
Lemma lc_two :
forall {n L} {B : 'E^n.+2} {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat),
- skip2F (scalF L B) H = 0 ->
+ skip2F H (scalF L B) = 0 ->
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof. move=>>; rewrite -!scalF_correct; apply sum_two. Qed.
Lemma lc_two_l :
forall {n L} {B : 'E^n.+2} {i0 i1} (H : i1 <> i0),
- skip2F L H = 0 ->
+ skip2F H L = 0 ->
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof.
intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F.
@@ -449,7 +449,7 @@ Qed.
Lemma lc_two_r :
forall {n L} {B : 'E^n.+2} {i0 i1} (H : i1 <> i0),
- skip2F B H = 0 ->
+ skip2F H B = 0 ->
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof.
intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F.
@@ -458,32 +458,32 @@ Qed.
Lemma lc_insertF :
forall {n} L (B : 'E^n) a0 x0 i0,
- lin_comb (insertF L a0 i0) (insertF B x0 i0) = scal a0 x0 + lin_comb L B.
+ lin_comb (insertF i0 a0 L) (insertF i0 x0 B) = scal a0 x0 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insertF; apply sum_insertF. Qed.
Lemma lc_insertF_l :
forall {n} L (B : 'E^n.+1) a0 i0,
- lin_comb (insertF L a0 i0) B = scal a0 (B i0) + lin_comb L (skipF B i0).
+ lin_comb (insertF i0 a0 L) B = scal a0 (B i0) + lin_comb L (skipF i0 B).
Proof.
-intros n L B a0 i0; rewrite -{1}(insertF_skipF B i0) lc_insertF; easy.
+intros n L B a0 i0; rewrite -{1}(insertF_skipF i0 B) lc_insertF; easy.
Qed.
Lemma lc_insertF_r :
forall {n} L (B : 'E^n) x0 i0,
- lin_comb L (insertF B x0 i0) = scal (L i0) x0 + lin_comb (skipF L i0) B.
+ lin_comb L (insertF i0 x0 B) = scal (L i0) x0 + lin_comb (skipF i0 L) B.
Proof.
-intros n L B x0 i0; rewrite -{1}(insertF_skipF L i0) lc_insertF; easy.
+intros n L B x0 i0; rewrite -{1}(insertF_skipF i0 L) lc_insertF; easy.
Qed.
Lemma lc_insert2F :
forall {n} L (B : 'E^n) a0 a1 x0 x1 {i0 i1} (H : i1 <> i0),
- lin_comb (insert2F L a0 a1 H) (insert2F B x0 x1 H) =
+ lin_comb (insert2F H a0 a1 L) (insert2F H x0 x1 B) =
scal a0 x0 + scal a1 x1 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insert2F; apply sum_insert2F. Qed.
Lemma lc_replaceF :
forall {n} L (B : 'E^n) a0 x0 i0,
- scal (L i0) (B i0) + lin_comb (replaceF L a0 i0) (replaceF B x0 i0) =
+ scal (L i0) (B i0) + lin_comb (replaceF i0 a0 L) (replaceF i0 x0 B) =
scal a0 x0 + lin_comb L B.
Proof.
intros [| n] L B a0 x0 i0; [destruct i0; easy |].
@@ -494,7 +494,7 @@ Lemma lc_replace2F :
forall {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1},
i1 <> i0 ->
scal (L i0) (B i0) + scal (L i1) (B i1) +
- lin_comb (replace2F L a0 a1 i0 i1) (replace2F B x0 x1 i0 i1) =
+ lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) =
scal a0 x0 + scal a1 x1 + lin_comb L B.
Proof.
intros; unfold lin_comb; rewrite scalF_replace2F -!scalF_correct;
@@ -505,7 +505,7 @@ Lemma lc_replace2F_eq :
forall {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1},
i1 = i0 ->
scal (L i1) (B i1) +
- lin_comb (replace2F L a0 a1 i0 i1) (replace2F B x0 x1 i0 i1) =
+ lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) =
scal a1 x1 + lin_comb L B.
Proof.
intros; unfold lin_comb; rewrite scalF_replace2F -scalF_correct;
@@ -647,7 +647,7 @@ Proof. intros; unfold lin_comb; rewrite scalF_unfun0F sum_unfun0F; easy. Qed.
Lemma lc_squeezeF :
forall {n} L (B : 'E^n.+1) {i0 i1},
i1 <> i0 -> B i1 = B i0 ->
- lin_comb (squeezeF L i0 i1) (skipF B i1) = lin_comb L B.
+ lin_comb (squeezeF L i0 i1) (skipF i1 B) = lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_squeezeF// sum_squeezeF//. Qed.
Lemma lc_concatnF :
@@ -667,7 +667,7 @@ Proof. intros; rewrite -lcT_r; easy. Qed.
Lemma lc_skipTc_r :
forall {n1 n2} L1 (B12 : 'E^{n1,n2.+1}) i20,
- lin_comb L1 (skipTc B12 i20) = skipF (lin_comb L1 B12) i20.
+ lin_comb L1 (skipTc B12 i20) = skipF i20 (lin_comb L1 B12).
Proof. intros; rewrite -sum_skipTc -scalF_skipTc_r; easy. Qed.
Lemma lc_row_r :
@@ -1006,12 +1006,12 @@ Proof. intros; unfold dot_product; rewrite lc_ind_l; easy. Qed.
Lemma dot_product_insertF :
forall {n} (u v : 'K^n) a b i0,
- insertF u a i0 â‹… insertF v b i0 = a * b + u â‹… v.
+ insertF i0 a u â‹… insertF i0 b v = a * b + u â‹… v.
Proof. intros; unfold dot_product; rewrite lc_insertF; easy. Qed.
Lemma dot_product_skipF :
forall {n} (u v : 'K^n.+1) i0,
- u â‹… v = scal (u i0) (v i0) + skipF u i0 â‹… skipF v i0.
+ u â‹… v = scal (u i0) (v i0) + skipF i0 u â‹… skipF i0 v.
Proof. intros; unfold dot_product; apply lc_skipF. Qed.
Lemma dot_product_zero_l : forall {n} (v : 'K^n), 0 â‹… v = 0.
diff --git a/Algebra/ModuleSpace/ModuleSpace_lin_map.v b/Algebra/ModuleSpace/ModuleSpace_lin_map.v
index ca68e5b0..9f579319 100644
--- a/Algebra/ModuleSpace/ModuleSpace_lin_map.v
+++ b/Algebra/ModuleSpace/ModuleSpace_lin_map.v
@@ -221,7 +221,7 @@ Proof. easy. Qed.
Lemma constF_lm : forall n, lin_map (@constF E n).
Proof. easy. Qed.
-Lemma skipF_lm : forall {n} i0, lin_map (skipF^~ i0 : 'E^n.+1 -> 'E^n).
+Lemma skipF_lm : forall {n} i0, lin_map (skipF i0 : 'E^n.+1 -> 'E^n).
Proof. easy. Qed.
Lemma insert0F_lm : forall {n} i0, lin_map (fun A : 'E^n => insert0F A i0).
diff --git a/Algebra/Ring/Ring_FF_FT.v b/Algebra/Ring/Ring_FF_FT.v
index 2ed92121..820d61ac 100644
--- a/Algebra/Ring/Ring_FF_FT.v
+++ b/Algebra/Ring/Ring_FF_FT.v
@@ -195,7 +195,7 @@ Lemma sum_alt_ones_3_invertible : invertible (sum (tripleF 1 (- (1 : K)) 1)).
Proof. rewrite sum_alt_ones_3; apply invertible_one. Qed.
Definition part1F {n} (u : 'K^n) (i0 : 'I_n.+1) : 'K^n.+1 :=
- insertF u (1 - sum u) i0.
+ insertF i0 (1 - sum u) u.
Lemma part1F_correct_0 :
forall {n} (u : 'K^n) i0 i, i = i0 -> part1F u i0 i = 1 - sum u.
@@ -207,14 +207,14 @@ Lemma part1F_correct_S :
Proof. intros; apply insertF_correct_r. Qed.
Lemma part1F_sum : forall {n} (u : 'K^n) i0, sum (part1F u i0) = 1.
-Proof. intros; unfold part1F; rewrite sum_insertF plus_minus_l; easy. Qed.
+Proof. intro; apply sum_insertF_baryc. Qed.
Lemma part1F_Rg :
forall {n} (i0 : 'I_n.+1), Rg (part1F^~ i0) = fun u => sum u = 1.
Proof.
intros n i0; apply subset_ext_equiv; split.
intros _ [v _]; apply part1F_sum.
-intros u Hu; rewrite image_ex; exists (skipF u i0); split; [easy |].
+intros u Hu; rewrite image_ex; exists (skipF i0 u); split; [easy |].
unfold part1F; rewrite -Hu (sum_skipF _ i0) minus_plus_r insertF_skipF; easy.
Qed.
@@ -294,19 +294,19 @@ Qed.
Lemma insertF_mult :
forall {n} (A B : 'K^n) a0 b0 i0,
- insertF (A * B) (a0 * b0) i0 = insertF A a0 i0 * insertF B b0 i0.
+ insertF i0 (a0 * b0) (A * B) = insertF i0 a0 A * insertF i0 b0 B.
Proof.
intros n A B a0 b0 i0; extF i; rewrite fct_mult_eq; destruct (ord_eq_dec i i0);
[rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed.
Lemma skipF_mult :
- forall {n} (A B : 'K^n.+1) i0, skipF (A * B) i0 = skipF A i0 * skipF B i0.
+ forall {n} (A B : 'K^n.+1) i0, skipF i0 (A * B) = skipF i0 A * skipF i0 B.
Proof. easy. Qed.
Lemma replaceF_mult :
forall {n} (A B : 'K^n.+1) a0 b0 i0,
- replaceF (A * B) (a0 * b0) i0 = replaceF A a0 i0 * replaceF B b0 i0.
+ replaceF i0 (a0 * b0) (A * B) = replaceF i0 a0 A * replaceF i0 b0 B.
Proof.
intros n A B a b i0; extF i; rewrite fct_mult_eq; destruct (ord_eq_dec i i0);
[rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
diff --git a/Algebra/Ring/Ring_compl.v b/Algebra/Ring/Ring_compl.v
index c57b7671..48399c64 100644
--- a/Algebra/Ring/Ring_compl.v
+++ b/Algebra/Ring/Ring_compl.v
@@ -564,7 +564,7 @@ Lemma invertible_sum_equiv :
Proof. intros; rewrite sum_filter_n0F; easy. Qed.
Lemma sum_insertF_baryc :
- forall {n} (u : 'K^n) i0, sum (insertF u (1 - sum u) i0) = 1.
+ forall {n} (u : 'K^n) i0, sum (insertF i0 (1 - sum u) u) = 1.
Proof. intros; rewrite sum_insertF plus_minus_l; easy. Qed.
Lemma invertible_sum_squeezeF :
diff --git a/Algebra/Ring/Ring_kron.v b/Algebra/Ring/Ring_kron.v
index b3beba2d..01584a05 100644
--- a/Algebra/Ring/Ring_kron.v
+++ b/Algebra/Ring/Ring_kron.v
@@ -147,14 +147,14 @@ Lemma itemF_kron_eqT :
Proof. intros; extF; apply itemF_kron_eq. Qed.
Lemma kron_skipF_diag_l :
- forall {n} (i : 'I_n.+1), skipF (fun j : 'I_n.+1 => kron K i j) i = 0.
+ forall {n} (i : 'I_n.+1), skipF i (fun j : 'I_n.+1 => kron K i j) = 0.
Proof.
intros n i; apply skipF_zero_compat; intros j Hj.
apply kron_is_0; contradict Hj; apply ord_inj; easy.
Qed.
Lemma kron_skipF_diag_r :
- forall {n} (j : 'I_n.+1), skipF (fun i : 'I_n.+1 => kron K i j) j = 0.
+ forall {n} (j : 'I_n.+1), skipF j (fun i : 'I_n.+1 => kron K i j) = 0.
Proof.
intros n j; apply skipF_zero_compat; intros i Hi.
apply kron_is_0; contradict Hi; apply ord_inj; easy.
diff --git a/Algebra/Ring/Ring_morphism.v b/Algebra/Ring/Ring_morphism.v
index c8298ed8..c97b291f 100644
--- a/Algebra/Ring/Ring_morphism.v
+++ b/Algebra/Ring/Ring_morphism.v
@@ -124,7 +124,7 @@ Proof. easy. Qed.
Lemma constF_mr : forall n, morphism_r (@constF K n).
Proof. easy. Qed.
-Lemma skipF_mr : forall {n} i0, morphism_r (skipF^~ i0 : 'K^n.+1 -> 'K^n).
+Lemma skipF_mr : forall {n} i0, morphism_r (skipF i0 : 'K^n.+1 -> 'K^n).
Proof. easy. Qed.
Lemma f_mult_compat_mapF :
diff --git a/FEM/geom_transf_affine.v b/FEM/geom_transf_affine.v
index 5ac6f193..9f3c6384 100644
--- a/FEM/geom_transf_affine.v
+++ b/FEM/geom_transf_affine.v
@@ -326,8 +326,8 @@ Qed.
Lemma T_geom_permutF_skipF :
forall i j,
- T_geom_permutF vtx pi_d (skipF vtx_ref i j) =
- T_geom vtx (skipF vtx_ref (pi_d i) (skip_f_ord Hpi_d i j)).
+ T_geom_permutF vtx pi_d (skipF i vtx_ref j) =
+ T_geom vtx (skipF (pi_d i) vtx_ref (skip_f_ord Hpi_d i j)).
Proof.
intros; unfold T_geom_permutF; rewrite !T_geom_vtx skip_f_ord_correct; easy.
Qed.
diff --git a/FEM/geometry.v b/FEM/geometry.v
index a5b60362..082e3d3b 100644
--- a/FEM/geometry.v
+++ b/FEM/geometry.v
@@ -68,17 +68,17 @@ Section Non_deg.
Context {E : ModuleSpace R_Ring}.
Definition non_deg {n} (v : 'E^n.+1) : Prop :=
- forall i, convex_envelop v <> convex_envelop (skipF v i).
+ forall i, convex_envelop v <> convex_envelop (skipF i v).
Lemma aff_indep_non_deg_aux :
forall {n} {v : 'E^n.+1} i,
aff_indep v ->
- convex_envelop v (v i) /\ ~ convex_envelop (skipF v i) (v i).
+ convex_envelop v (v i) /\ ~ convex_envelop (skipF i v) (v i).
Proof.
intros n v i Hv; split; [apply convex_envelop_inclF |].
intros Hi; inversion Hi as [L HL1 HL2 HL3].
-assert (H0 : sum (insertF L 0 i) = 1) by now rewrite sum_insertF plus_zero_l.
-assert (H1 : insertF L 0 i = kronR i).
+assert (H0 : sum (insertF i 0 L) = 1) by now rewrite sum_insertF plus_zero_l.
+assert (H1 : insertF i 0 L = kronR i).
apply (aff_indep_decomp_uniq Hv); [easy.. | rewrite kron_sum_r; easy |].
move: HL3; rewrite baryc_l_kron_r -!baryc_ms_correct !baryc_ms_eq//.
rewrite lc_insertF_l scal_zero_l plus_zero_l; easy.
diff --git a/FEM/monomial.v b/FEM/monomial.v
index 92a3020d..8b31bffe 100644
--- a/FEM/monomial.v
+++ b/FEM/monomial.v
@@ -93,12 +93,12 @@ Proof. intros; apply map2F_concatF. Qed.
Lemma powF_skipF :
forall {d} (B : 'R^d.+1) L i0,
- powF (skipF B i0) (skipF L i0) = skipF (powF B L) i0.
+ powF (skipF i0 B) (skipF i0 L) = skipF i0 (powF B L).
Proof. intros; apply map2F_skipF. Qed.
Lemma powF_replaceF_l :
forall {d} (B : 'R^d) u L i,
- powF (replaceF B u i) L = replaceF (powF B L) (u ^ L i) i.
+ powF (replaceF i u B) L = replaceF i (u ^ L i) (powF B L).
Proof.
intros d B u L i; extF j.
unfold powF; rewrite map2F_correct; destruct (ord_eq_dec j i) as [-> | H].
@@ -108,7 +108,7 @@ Qed.
Lemma powF_replaceF_r :
forall {d} (B : 'R^d) L a i,
- powF B (replaceF L a i) = replaceF (powF B L) (B i ^ a) i.
+ powF B (replaceF i a L) = replaceF i (B i ^ a) (powF B L).
Proof.
intros d B L a i; extF j.
unfold powF; rewrite map2F_correct; destruct (ord_eq_dec j i) as [-> | H].
@@ -128,7 +128,7 @@ Qed.
Lemma powF_itemF_r :
forall {d} (B : 'R^d) (a : nat) i0,
- powF B (itemF d a i0) = replaceF ones (B i0 ^ a) i0.
+ powF B (itemF d a i0) = replaceF i0 (B i0 ^ a) ones.
Proof.
intros d B a i0; extF i; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite -> Hi, powF_correct, itemF_correct_l, replaceF_correct_l; easy.
@@ -214,7 +214,7 @@ Proof. intros; unfold powF_P; rewrite powF_concatF prod_R_concatF; easy. Qed.
Lemma powF_P_replaceF_l :
forall {d} L (B : 'R^d) x i,
- (pow (B i) (L i) * powF_P (replaceF L x i) B)%K =
+ (pow (B i) (L i) * powF_P (replaceF i x L) B)%K =
(pow (B i) x * powF_P L B)%K.
Proof.
intros d; case d; [intros L B x [i Hi]; easy |].
@@ -226,7 +226,7 @@ Qed.
Lemma powF_P_replaceF_r :
forall {d} L (B : 'R^d) x i,
- (pow (B i) (L i) * powF_P L (replaceF B x i))%K =
+ (pow (B i) (L i) * powF_P L (replaceF i x B))%K =
(pow x (L i) * powF_P L B)%K.
Proof.
intros d; case d; [intros L B x [i Hi]; easy |].
diff --git a/FEM/multi_index.v b/FEM/multi_index.v
index da841b26..a05adade 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 (Slice_fun u a i) ord0 = a i.
+ skipF ord0 (Slice_fun u a i) = a i.
Proof.
intros d n u a i.
unfold Slice_fun; rewrite mapF_correct; unfold Slice_op.
@@ -321,7 +321,7 @@ Qed.
Lemma CSdk_sortedF_aux :
forall {n} (A B : 'nat^n.+1) i,
sum A = sum B -> (B i < A i)%coq_nat ->
- (sum (skipF A i) < sum (skipF B i))%coq_nat.
+ (sum (skipF i A) < sum (skipF i B))%coq_nat.
Proof.
intros n A B i H1 H2.
apply Nat.add_lt_mono_l with (A i).
@@ -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 (Adk d k idk) (k - sum (Adk d k idk))%coq_nat ord0.
+ fun idk => insertF ord0 (k - sum (Adk d k idk))%coq_nat (Adk d k idk).
(**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
diff --git a/FEM/poly_LagP1k.v b/FEM/poly_LagP1k.v
index a15cc468..68287003 100644
--- a/FEM/poly_LagP1k.v
+++ b/FEM/poly_LagP1k.v
@@ -50,7 +50,7 @@ Variable node : 'R^{(pbinom 1 k).+1,1}.
Def 1448, p. 58.#<BR>#
LagP1k i = Prod_{j<>i} (x - node j) / Prod_{j<>i} (node i - node j). *)
Definition LagP1k_aux : '(FRd 1)^(pbinom 1 k).+1 :=
- fun i1k x => prod_R ((skipF node i1k - constF _ x)^~ ord0).
+ fun i1k x => prod_R ((skipF i1k node - constF _ x)^~ ord0).
Definition LagP1k : '(FRd 1)^(pbinom 1 k).+1 :=
fun i1k x => LagP1k_aux i1k x / LagP1k_aux i1k (node i1k).
diff --git a/FEM/poly_LagPd1.v b/FEM/poly_LagPd1.v
index 4b48201f..aa01d303 100644
--- a/FEM/poly_LagPd1.v
+++ b/FEM/poly_LagPd1.v
@@ -171,7 +171,7 @@ Context {d : nat}.
Definition Hface (vtx : 'R^{d.+1,d}) (i : 'I_d.+1) : 'R^d -> Prop :=
image (T_geom vtx) (Hface_ref i).
-Lemma Hface_aff_span : forall vtx i, Hface vtx i = aff_span_ms (skipF vtx i).
+Lemma Hface_aff_span : forall vtx i, Hface vtx i = aff_span_ms (skipF i vtx).
Proof.
intros; unfold Hface, Hface_ref; rewrite am_aff_span_ms; [| apply T_geom_am].
rewrite mapF_skipF T_geom_vtxF; easy.
@@ -206,7 +206,7 @@ Context {vtx : 'R^{d.+1,d}}.
Hypothesis Hvtx : aff_indep_ms vtx.
Lemma Hface_aff_basis :
- forall (i : 'I_d.+1), aff_basis_ms (Hface vtx i) (skipF vtx i).
+ forall (i : 'I_d.+1), aff_basis_ms (Hface vtx i) (skipF i vtx).
Proof.
intro; rewrite Hface_aff_span;
apply aff_basis_aff_span_equiv, aff_indep_skipF; easy.
diff --git a/FEM/poly_LagPd1_ref.v b/FEM/poly_LagPd1_ref.v
index 96eb8340..5e266c65 100644
--- a/FEM/poly_LagPd1_ref.v
+++ b/FEM/poly_LagPd1_ref.v
@@ -228,7 +228,7 @@ Proof. intro; rewrite LagPd1_ref_bcF; apply bc_kronF_r, vtx_ref_aff_indep. Qed.
Lemma LagPd1_ref_kron_vtx : forall i j, LagPd1_ref j (vtx_ref i) = kronR i j.
Proof. intros i j; move: j; apply extF_rev, LagPd1_ref_kron_vtxF. Qed.
-Lemma LagPd1_ref_vtx_skipF : forall i j, LagPd1_ref i (skipF vtx_ref i j) = 0.
+Lemma LagPd1_ref_vtx_skipF : forall i j, LagPd1_ref i (skipF i vtx_ref j) = 0.
Proof.
intros; unfold skipF; rewrite LagPd1_ref_kron_vtx.
apply kron_is_0, ord_neq_compat, skip_ord_correct_m.
@@ -332,7 +332,7 @@ Context {d : nat}.
Note that [Hface_ref i] is the face hyperplane opposite reference vertex
\hat{v}_i *)
Definition Hface_ref (i : 'I_d.+1) : 'R^d -> Prop :=
- aff_span_ms (skipF vtx_ref i).
+ aff_span_ms (skipF i vtx_ref).
(**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
@@ -387,7 +387,7 @@ Context {d1 : nat}.
Let d := d1.+1.
Lemma Hface_ref_aff_basis :
- forall (i : 'I_d.+1), aff_basis_ms (Hface_ref i) (skipF vtx_ref i).
+ forall (i : 'I_d.+1), aff_basis_ms (Hface_ref i) (skipF i vtx_ref).
Proof.
intro; rewrite aff_basis_ms_correct; apply aff_basis_aff_span_equiv.
apply: aff_indep_skipF; apply vtx_ref_aff_indep.
@@ -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 y_ref 0 ord_max)).
+ rewrite -(Hp2 (insertF ord_max 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 9452a7cd..9a0ab5de 100644
--- a/FEM/poly_Pdk.v
+++ b/FEM/poly_Pdk.v
@@ -323,8 +323,8 @@ 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 (Adk d.+1 k.+1 iSdSk)
- (Adk d.+1 k.+1 iSdSk ord_max).-1 ord_max)).
+ (replaceF ord_max
+ (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.
apply Pdk_monot with O; auto with arith.
@@ -349,8 +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 (Adk d.+1 k.+1 iSdSk) (Adk d.+1 k.+1 iSdSk ord_max).-1
- ord_max)); try easy.
+ sum (replaceF ord_max (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.
@@ -403,7 +402,7 @@ intros jSdk; unfold Monom_dk.
apply Pdk_ext with
(powF_P (Adk d.+1 k.+1
(Adk_inv d.+1 k.+1
- (replaceF (Adk d.+1 k jSdk) (Adk d.+1 k jSdk i).+1%coq_nat i)))).
+ (replaceF i (Adk d.+1 k jSdk i).+1%coq_nat (Adk d.+1 k jSdk))))).
2: apply Pdk_powF_P.
intros x; rewrite Adk_inv_correct_r.
case (Req_dec (x i) 0); intros Hxi.
@@ -420,7 +419,7 @@ rewrite pow_S mult_assoc; easy.
apply Nat.add_le_mono_l with (Adk d.+1 k jSdk i).
replace (_ + _)%coq_nat with
(Adk d.+1 k jSdk i +
- sum (replaceF (Adk d.+1 k jSdk) (Adk d.+1 k jSdk i).+1 i)); try easy.
+ sum (replaceF i (Adk d.+1 k jSdk i).+1 (Adk d.+1 k jSdk))); try easy.
rewrite sum_replaceF.
replace (_ + _) with ((Adk d.+1 k jSdk i).+1 + sum (Adk d.+1 k jSdk))%coq_nat; try easy.
generalize (Adk_sum d.+1 k jSdk); lia.
@@ -708,26 +707,26 @@ Qed.
Definition ex_derive_onei {n} :=
fun (i:'I_n) (f: FRd n) (x:'R^n) =>
- ex_derive (fun y => f (replaceF x y i)) (x i).
+ ex_derive (fun y => f (replaceF i y x)) (x i).
Definition is_derive_onei {n} :=
fun (i:'I_n) (f: FRd n) (x:'R^n) (l:R) =>
- is_derive (fun y => f (replaceF x y i)) (x i) l.
+ is_derive (fun y => f (replaceF i y x)) (x i) l.
Definition Derive_onei {n} :=
fun (i:'I_n) (f: FRd n) (x:'R^n) =>
- Derive (fun y => f (replaceF x y i)) (x i).
+ Derive (fun y => f (replaceF i y x)) (x i).
Definition ex_derive_multii {n} :=
fun (i:'I_n) (j:nat) (f: FRd n) (x:'R^n) =>
- ex_derive_n (fun y => f (replaceF x y i)) j (x i).
+ ex_derive_n (fun y => f (replaceF i y x)) j (x i).
Definition is_derive_multii {n} :=
fun (i:'I_n) (j:nat) (f: FRd n) (x:'R^n) (l:R) =>
- is_derive_n (fun y => f (replaceF x y i)) j (x i) l.
+ is_derive_n (fun y => f (replaceF i y x)) j (x i) l.
Definition Derive_multii {n} (i:'I_n) (j:nat) (f: FRd n) (x:'R^n):=
- Derive_n (fun y => f (replaceF x y i)) j (x i).
+ Derive_n (fun y => f (replaceF i y x)) j (x i).
Lemma ex_derive_onei_lc :
forall {n m} (j:'I_n) (f :'I_m -> FRd n) (L:'R^m),
@@ -736,10 +735,10 @@ Lemma ex_derive_onei_lc :
Proof.
intros n m j f L; unfold ex_derive_onei; intros H x.
apply ex_derive_ext with
- (lin_comb L (fun (i : 'I_m) (y : R) => f i (replaceF x y j))).
+ (lin_comb L (fun (i : 'I_m) (y : R) => f i (replaceF j y x))).
intros t; rewrite 2!fct_lc_r_eq; easy.
apply ex_derive_lc.
-intros i y; specialize (H i (replaceF x y j)).
+intros i y; specialize (H i (replaceF j y x)).
rewrite replaceF_correct_l in H; try easy.
apply ex_derive_ext with (2:=H).
intros t; f_equal; extF k.
@@ -753,15 +752,15 @@ Lemma is_derive_onei_lc :
Proof.
intros n m j f L d; unfold is_derive_onei; intros H x.
apply is_derive_ext with
- (lin_comb L (fun (i : 'I_m) (y : R) => f i (replaceF x y j))).
+ (lin_comb L (fun (i : 'I_m) (y : R) => f i (replaceF j y x))).
intros t; rewrite 2!fct_lc_r_eq; easy.
-apply is_derive_ext' with (lin_comb L (fun i y => d i (replaceF x y j)) (x j)).
+apply is_derive_ext' with (lin_comb L (fun i y => d i (replaceF j y x)) (x j)).
rewrite 2! fct_lc_r_eq.
apply lc_ext_r.
intros i; f_equal.
apply replaceF_id.
apply is_derive_lc.
-intros i y; specialize (H i (replaceF x y j)).
+intros i y; specialize (H i (replaceF j y x)).
rewrite replaceF_correct_l in H; try easy.
apply is_derive_ext with (2:=H).
intros t; f_equal; extF k.
@@ -879,13 +878,13 @@ Proof. intros; apply comp_n_ind_r. Qed.
(* f1 does not depend upon (x i) therefore is a constant when deriving *)
Lemma Derive_multii_scal_fun : forall {n} (i:'I_n) j f1 f2,
- (forall x y, f1 x = f1 (replaceF x y i)) ->
+ (forall x y, f1 x = f1 (replaceF i y x)) ->
Derive_multii i j (fun x => f1 x* f2 x)
= (fun x => f1 x*(Derive_multii i j f2 x)).
Proof.
intros n i j f1 f2 H1.
fun_ext x; unfold Derive_multii.
-rewrite ->Derive_n_ext with (g:=fun y => f1 x * f2 (replaceF x y i)).
+rewrite ->Derive_n_ext with (g:=fun y => f1 x * f2 (replaceF i y x)).
2: intros t; rewrite -H1; easy.
now rewrite Derive_n_scal_l.
Qed.
@@ -895,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 x y ord_max)) ->
+ (forall (x:'R^n.+1) y, f x = f (replaceF ord_max 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).
@@ -912,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 x y ord_max)) ->
+ (forall (x:'R^n.+1) y, f x = f (replaceF ord_max y x)) ->
(narrow_ord_max (Derive_multii i j f)) =
Derive_multii (narrow_S H) j (narrow_ord_max f).
Proof.
@@ -938,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 x y ord_max)) ->
+ (forall (x:'R^n.+1) y, g2 x = g2 (replaceF ord_max 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)).
@@ -978,7 +977,7 @@ apply ord_inj; now simpl.
unfold widenF_S; f_equal; apply ord_inj; now simpl.
intros x y; unfold Derive_multii; f_equal.
fun_ext z.
-fold (replace2F x y z ord_max (Ordinal Hi')).
+fold (replace2F ord_max (Ordinal Hi') y z x).
rewrite replace2F_equiv_def; try easy.
apply ord_neq; simpl; easy.
rewrite replaceF_correct_r; try easy.
@@ -989,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 x y ord_max)) ->
+ (forall (x:'R^n.+1) y, g2 x = g2 (replaceF ord_max 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.
@@ -1069,7 +1068,7 @@ Qed.
Lemma is_derive_powF_P : forall {n} (beta:'nat^n) i x,
is_derive_onei i (powF_P beta) x
- (INR (beta i) * powF_P (replaceF beta (beta i).-1 i) x).
+ (INR (beta i) * powF_P (replaceF i (beta i).-1 beta) x).
Proof.
intros n; induction n.
intros beta i; exfalso; apply I_0_is_empty; apply (inhabits i).
@@ -1103,7 +1102,7 @@ apply is_derive_id.
(* *)
apply is_derive_ext with
(fun t => ( (x ord0)^(beta ord0) *
- (prod_R ((powF (replaceF (liftF_S x) t (lower_S Hi)) (liftF_S beta)))))).
+ (prod_R ((powF (replaceF (lower_S Hi) t (liftF_S x)) (liftF_S beta)))))).
intros t; unfold mult, plus; simpl; f_equal.
unfold powF, map2F; rewrite replaceF_correct_r; try easy.
f_equal; extF j.
@@ -1117,7 +1116,7 @@ unfold lift_S in H; apply (lift_inj H).
now rewrite lift_lower_S.
apply is_derive_ext' with ( (x ord0)^(beta ord0) *
(INR (beta i) * prod_R (powF (liftF_S x)
- (replaceF (liftF_S beta) (beta i).-1 (lower_S Hi))))).
+ (replaceF (lower_S Hi) (beta i).-1 (liftF_S beta))))).
rewrite mult_comm_R -mult_assoc; unfold mult; simpl; f_equal; rewrite Rmult_comm.
rewrite prod_R_ind_l; unfold mult, plus; simpl; f_equal.
unfold powF, map2F; rewrite replaceF_correct_r; try easy.
@@ -1166,12 +1165,12 @@ exists k.
apply lin_span_lin_span; intros jSnk.
apply: lin_span_scal_closed.
apply lin_span_ub with
- (Adk_inv n.+1 k (replaceF (Adk n.+1 k jSnk) (Adk n.+1 k jSnk i).-1 i)).
+ (Adk_inv n.+1 k (replaceF i (Adk n.+1 k jSnk i).-1 (Adk n.+1 k jSnk))).
unfold Monom_dk.
rewrite Adk_inv_correct_r; try easy.
apply Nat.add_le_mono_l with (Adk n.+1 k jSnk i).
replace (_ +_)%coq_nat with
- (Adk n.+1 k jSnk i + sum (replaceF (Adk n.+1 k jSnk) (Adk n.+1 k jSnk i).-1 i)) by easy.
+ (Adk n.+1 k jSnk i + sum (replaceF i (Adk n.+1 k jSnk i).-1 (Adk n.+1 k jSnk))) by easy.
rewrite sum_replaceF.
generalize (Adk_sum n.+1 k jSnk).
unfold plus; simpl; auto with zarith.
@@ -1215,7 +1214,7 @@ Qed.
(Prod_{j=0}^{beta_i - 1} (alpha_i - j)) x_i ^(alpha_i - beta_i). *)
Lemma Derive_multii_powF_P : forall {n} (A:'nat^n) i m, exists C,
Derive_multii i m (powF_P A)
- = (fun x => C* powF_P (replaceF A (A i-m)%coq_nat i) x)
+ = (fun x => C* powF_P (replaceF i (A i-m)%coq_nat A) x)
/\ (C = 0 <-> (A i < m)%coq_nat).
Proof.
intros n A i; induction m.
@@ -1231,7 +1230,7 @@ unfold Derive_multii; unfold Derive_multii in H1.
fun_ext x; simpl.
generalize (fun_ext_rev H1); intros H1'.
rewrite ->Derive_ext with
- (g:=fun z => C * powF_P (replaceF A (A i - m)%coq_nat i) (replaceF x z i)).
+ (g:=fun z => C * powF_P (replaceF i (A i - m)%coq_nat A) (replaceF i z x)).
rewrite Derive_scal.
rewrite -mult_assoc; unfold mult; simpl; f_equal.
apply is_derive_unique.
@@ -1373,16 +1372,16 @@ unfold Derive_alp, Derive_multii.
fun_ext x.
rewrite Derive_n_plus; try easy.
exists (mkposreal 1 Rlt_0_1); intros y Hy k Hk.
-generalize (is_Poly_ex_derive_n g1 Hg1 i k (replaceF x y i)); unfold ex_derive_multii.
+generalize (is_Poly_ex_derive_n g1 Hg1 i k (replaceF i y x)); unfold ex_derive_multii.
rewrite replaceF_correct_l; try easy.
-intros T; apply: (ex_derive_n_ext _ (fun x0 : R => g1 (replaceF x x0 i))).
+intros T; apply: (ex_derive_n_ext _ (fun x0 : R => g1 (replaceF i x0 x))).
2: apply T.
intros t; simpl; unfold replaceF; f_equal; extF i0.
case (ord_eq_dec i0 i); try easy.
exists (mkposreal 1 Rlt_0_1); intros y Hy k Hk.
-generalize (is_Poly_ex_derive_n g2 Hg2 i k (replaceF x y i)); unfold ex_derive_multii.
+generalize (is_Poly_ex_derive_n g2 Hg2 i k (replaceF i y x)); unfold ex_derive_multii.
rewrite replaceF_correct_l; try easy.
-intros T; apply: (ex_derive_n_ext _ (fun x0 : R => g2 (replaceF x x0 i))).
+intros T; apply: (ex_derive_n_ext _ (fun x0 : R => g2 (replaceF i x0 x))).
2: apply T.
intros t; simpl; unfold replaceF; f_equal; extF i0.
case (ord_eq_dec i0 i); try easy.
--
GitLab