From e7aebdb721f8fe8a8f7150114045f4e1f75d510d Mon Sep 17 00:00:00 2001
From: Houda Mouhcine <houda.mouhcine@inria.fr>
Date: Wed, 25 Sep 2024 01:54:19 +0200
Subject: [PATCH] Change in indices.
---
FEM/geom_simplex.v | 28 ++++++++++++++--------------
FEM/poly_LagPd1_ref.v | 11 +++++++----
2 files changed, 21 insertions(+), 18 deletions(-)
diff --git a/FEM/geom_simplex.v b/FEM/geom_simplex.v
index 9794f769..9da0a06b 100644
--- a/FEM/geom_simplex.v
+++ b/FEM/geom_simplex.v
@@ -247,18 +247,18 @@ Qed.
Lemma vtx_cur_invalF : forall vtx_cur, (0 < k)%coq_nat ->
invalF vtx_cur (node_cur vtx_cur).
Proof.
-intros vtx_cur Hk i.
-destruct (ord_eq_dec i ord0) as [Hi | Hi].
-(* i = ord0 *)
-rewrite Hi.
+intros vtx_cur Hk ipk. unfold inF.
+destruct (ord_eq_dec ipk ord0) as [Hipk | Hipk].
+(* ipk = ord0 *)
+rewrite Hipk.
exists ord0.
unfold node_cur.
rewrite (Adk_0 d k) !scal_zero_r !lc_zero_l
minus_zero_r scal_one plus_zero_r; easy.
-(* i <> ord0 *)
-exists (Adk_inv d k (itemF d k (lower_S Hi))).
+(* ipk <> ord0 *)
+exists (Adk_inv d k (itemF d k (lower_S Hipk))).
unfold node_cur.
-rewrite Adk_kron !(lc_eq_l _ (kronecker (lower_S Hi))).
+rewrite Adk_kron !(lc_eq_l _ (kronecker (lower_S Hipk))).
rewrite lc_ones_r sum_kronecker_r minus_eq_zero
scal_zero_l plus_zero_l lc_kronecker_l_in_r
liftF_lower_S; easy.
@@ -319,27 +319,27 @@ Variable d : nat.
Lemma vtx_node_Pd1_cur : forall (vtx_cur : 'R^{d.+1,d}) (ipk :'I_d.+1),
vtx_cur ipk = node_cur d 1 vtx_cur (cast_ord (eq_sym (pbinomS_1_r d)) ipk).
Proof.
-intros vtx_cur i; unfold node_cur.
+intros vtx_cur ipk; unfold node_cur.
rewrite Rinv_1 scal_one.
-destruct (ord_eq_dec i ord0) as [Hi | Hi].
-(* i = ord0 *)
+destruct (ord_eq_dec ipk ord0) as [Hi | Hi].
+(* ipk = ord0 *)
rewrite Hi.
replace (mapF INR (Adk d 1 (cast_ord (eq_sym (pbinomS_1_r d)) ord0))) with
(mapF INR (Adk d 1 ord0)).
rewrite (Adk_0 d 1) !lc_zero_l minus_zero_r
scal_one plus_zero_r; auto.
f_equal; f_equal; apply ord_inj; easy.
-(* i <> ord0 *)
+(* ipk <> ord0 *)
rewrite Ad1_eq.
unfold castF.
rewrite concatF_correct_r; simpl.
apply ord_n0_nlt_equiv; easy.
intros H.
rewrite mapF_itemF_0// itemF_kronecker_eq; auto; simpl.
-replace (fun j : 'I_d => 1 * kronecker (i - 1) j) with
- (fun j : 'I_d => kronecker (i - 1) j).
+replace (fun j : 'I_d => 1 * kronecker (ipk - 1) j) with
+ (fun j : 'I_d => kronecker (ipk - 1) j).
rewrite lc_ones_r.
-replace (sum (fun j : 'I_d => kronecker (i - 1) j)) with 1.
+replace (sum (fun j : 'I_d => kronecker (ipk - 1) j)) with 1.
rewrite minus_eq_zero scal_zero_l plus_zero_l.
apply eq_sym.
rewrite (lc_kronecker_l_in_r (lower_S Hi))
diff --git a/FEM/poly_LagPd1_ref.v b/FEM/poly_LagPd1_ref.v
index 55591c2d..124abead 100644
--- a/FEM/poly_LagPd1_ref.v
+++ b/FEM/poly_LagPd1_ref.v
@@ -319,8 +319,10 @@ Variable d : nat.
Lemma Pd1_lin_span_LagPd1_ref : Pdk d 1 = lin_span (LagPd1_ref d).
Proof.
-apply lin_span_ext; intro ipk.
+unfold Pdk.
+apply lin_span_ext.
(* <= *)
+intro ipk.
destruct (ord_eq_dec ipk ord0) as [Hipk | Hipk].
(* ipk = ord0 *)
apply lin_span_ex.
@@ -359,7 +361,8 @@ apply cast_ordS_n0; easy.
intros H1; apply fun_ext; intros x.
f_equal; f_equal; easy.
(* => *)
-destruct (ord_eq_dec ipk ord0) as [Hipk | Hipk].
+intros j.
+destruct (ord_eq_dec j ord0) as [Hj | Hj].
apply lin_span_ex.
(* ipk = ord0 *)
pose (L := concatF (singleF 1) (opp (@ones _ d))).
@@ -398,8 +401,8 @@ apply ord_inj; simpl.
rewrite bump_r; auto with arith.
f_equal; apply ord_inj; easy.
(* ipk <> ord0 *)
-replace (LagPd1_ref d ipk) with
- (BasisPdk d 1 (cast_ord (eq_sym (pbinomS_1_r d)) ipk)).
+replace (LagPd1_ref d j) with
+ (BasisPdk d 1 (cast_ord (eq_sym (pbinomS_1_r d)) j)).
apply lin_span_inclF_diag.
rewrite BasisPd1_neq0; simpl.
apply cast_ordS_n0; easy.
--
GitLab