From 44e55dfb97332d40c75634510d9d9fea803a2354 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 12 Mar 2025 19:35:19 +0100
Subject: [PATCH] Modif node_ref, sub_vtx, sub_node. Rm useless node_ref_eqF,
 node_ref_CSdk, node_ref_ASdki,            node_d0_eq, sub_vtxF, sub_vtx_refF,
 sub_nodeF.

---
 FEM/FE_LagP.v       |  2 +-
 FEM/LagP_node.v     | 56 ++++++++++++---------------------------------
 FEM/LagP_node_ref.v | 50 ++++++++++++++--------------------------
 3 files changed, 32 insertions(+), 76 deletions(-)

diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index 837f247d..e1322513 100644
--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -199,7 +199,7 @@ rewrite Hq2 (IH2 q)//; [apply: mult_zero_r |]; intros iSdk.
 apply mult_reg_l with (LagPd1 Hvtx ord0 (sub_node k.+1 vtx iSdk)).
 apply invertible_equiv_R; rewrite -Hface_equiv;
     apply sub_node_out_Hface_0; easy.
-rewrite -(sub_node_node k.+1) -fct_mult_eq -Hq2 sub_node_eq// Hp2 mult_zero_r//.
+rewrite -(sub_node_node HSk1) -fct_mult_eq -Hq2 sub_node_eq// Hp2 mult_zero_r//.
 Qed.
 
 (** Unisolvence result for d,k>0. *)
diff --git a/FEM/LagP_node.v b/FEM/LagP_node.v
index 6e472b0a..698ec107 100644
--- a/FEM/LagP_node.v
+++ b/FEM/LagP_node.v
@@ -51,15 +51,6 @@ Context {d k : nat}.
  Lem 1604, p. 101. *)
 Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := T_geom vtx node_ref_d0.
 
-(**
- #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Def 1588, Eq (9.80), p. 97. *)
-Lemma node_d0_eq : forall vtx, node_d0 vtx = isobarycenter_ms vtx.
-Proof.
-intro; unfold node_d0; rewrite node_ref_d0_eqF T_geom_am;
-    [rewrite T_geom_vtxF | apply invertible_plusn1_R]; easy.
-Qed.
-
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1599, p. 100. *)
@@ -151,7 +142,7 @@ Qed.
 End Nodes_Facts2.
 
 
-Section Nodes_d1.
+Section Nodes_d1_Facts.
 
 Context {d : nat}.
 
@@ -172,7 +163,7 @@ Proof.
 intro; rewrite node_vtx_d1 mapF_castF lc_castF; apply LagPd1_decomp_vtx.
 Qed.
 
-End Nodes_d1.
+End Nodes_d1_Facts.
 
 
 Section Sub_vertices_Def.
@@ -186,26 +177,12 @@ Variable vtx : 'R^{d.+1,d}.
  Def 1594, Eq (9.88), p. 98.
  sub_vtx 0 = \underline{v}_0 = v_0,
  sub_vtx i = \underline{v}_i = a_{(k-1)e^i}, for i <> 0. *)
-Definition sub_vtx (i : 'I_d.+1) : 'R^d := T_geom vtx (sub_vtx_ref k i).
-(* Could be: sub_vtx i := T_geom (sub_vtx_ref k) vtx. *)
-
-Lemma sub_vtxF : sub_vtx = mapF (T_geom vtx) (sub_vtx_ref k).
-Proof. easy. Qed.
+Definition sub_vtx : [0..d.+1) -> 'R^d := mapF (T_geom vtx) (sub_vtx_ref k).
 
 End Sub_vertices_Def.
 
 
-Section Sub_vertices_Facts0.
-
-Context {d k : nat}.
-
-Lemma sub_vtx_refF : @sub_vtx_ref d k = sub_vtx k vtx_ref.
-Proof. rewrite sub_vtxF T_geom_ref; easy. Qed.
-
-End Sub_vertices_Facts0.
-
-
-Section Sub_vertices_Facts1.
+Section Sub_vertices_Facts.
 
 Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
@@ -221,7 +198,7 @@ apply (am_aff_indep (T_geom_am _));
     [apply T_geom_inj | apply sub_vtx_ref_aff_indep]; easy.
 Qed.
 
-End Sub_vertices_Facts1.
+End Sub_vertices_Facts.
 
 
 Section Sub_nodes_Def.
@@ -233,19 +210,8 @@ Variable vtx : 'R^{d.+1,d}.
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1604, p. 101. *)
-Definition sub_node (idk : [0..(pbinom d k.-1).+1)) : 'R^d :=
-  T_geom vtx (sub_node_ref idk).
-
-Lemma sub_nodeF : sub_node = mapF (T_geom vtx) sub_node_ref.
-Proof. easy. Qed.
-
-Lemma sub_node_node : sub_node = node (sub_vtx k vtx).
-Proof.
-rewrite sub_nodeF nodeF sub_vtxF -T_geom_comp mapF_comp.
-f_equal.
-
-
-Admitted.
+Definition sub_node : [0..(pbinom d k.-1).+1) -> 'R^d :=
+  mapF (T_geom vtx) sub_node_ref.
 
 End Sub_nodes_Def.
 
@@ -256,6 +222,12 @@ Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
 Variable vtx : 'R^{d.+1,d}.
 
+Lemma sub_node_node : sub_node k vtx = node (sub_vtx k vtx).
+Proof.
+rewrite nodeF -T_geom_comp mapF_comp T_geom_scal_ref//.
+apply INR_ratio_invertible; easy.
+Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1598, p. 100. *)
@@ -279,7 +251,7 @@ Lemma sub_node_out_Hface_0 :
   forall (idk : [0..(pbinom d k.-1).+1)),
     ~ Hface vtx ord0 (sub_node k vtx idk).
 Proof.
-intro; rewrite -T_geom_Hface_eq// sub_nodeF mapF_correct Im_equiv;
+intro; rewrite -T_geom_Hface_eq// Im_equiv;
     [apply sub_node_ref_out_Hface_ref_0 | apply T_geom_inj]; easy.
 Qed.
 
diff --git a/FEM/LagP_node_ref.v b/FEM/LagP_node_ref.v
index b13c93bf..cd2bdc0e 100644
--- a/FEM/LagP_node_ref.v
+++ b/FEM/LagP_node_ref.v
@@ -63,39 +63,16 @@ Qed.
  This definition uses total function [inv] (via [div]).
  It will be used for k>0 only.
  The specific definition for k=0 is [node_ref_d0]. *)
-Definition node_ref (idk : 'I_(pbinom d k).+1) : 'R^d :=
-  fun i => INR (Adk d k idk i) / INR k.
+Definition node_ref : [0..(pbinom d k).+1) -> 'R^d :=
+  fun idk => scal (/ INR k) (mapF INR (Adk d k idk)).
 (* = mapF (scal (/ INR k) (mapF INR)) (Adk d k).*)
 
-Lemma node_ref_eqF :
-  forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)).
-Proof. intros; unfold node_ref; extF; rewrite div_eq mult_comm_R; easy. Qed.
-
 Lemma node_ref_inj : injective node_ref.
 Proof.
 case (Nat.eq_dec k 0); intros Hk.
-(* *)
 intros [i Hi] [j Hj] _; subst; apply ord_inj; simpl.
 rewrite pbinom_0_r in Hi, Hj; move: Hi => /ltP Hi; move: Hj => /ltP Hj; lia.
-(* *)
-intros idk jdk; rewrite !node_ref_eqF;
-    move=> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
-Qed.
-
-Lemma node_ref_CSdk :
-  forall (idk : 'I_(pbinom d k).+1), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
-    sum (node_ref idk) = 1 <-> sum (Adk d k idk) = k.
-Proof.
-move=>> Hd Hk; rewrite node_ref_eqF -scal_sum_r sum_INR.
-apply INR_n0, invertible_equiv_R in Hk.
-rewrite scal_eq_K mult_comm_R div_one_equiv// INR_eq_equiv; easy.
-Qed.
-
-Lemma node_ref_ASdki :
-  forall idk i, (0 < k)%coq_nat -> node_ref idk i = 0 <-> Adk d k idk i = 0.
-Proof.
-move=>> /INR_n0 /invertible_equiv_R Hk.
-unfold node_ref; rewrite div_zero_equiv// INR_0_equiv; easy.
+move=>> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
 Qed.
 
 (**
@@ -105,7 +82,10 @@ Qed.
 Lemma node_ref_Hface_ref_0 :
   forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
     Hface_ref ord0 (node_ref idk) <-> sum (Adk d k idk) = k.
-Proof. intros; rewrite Hface_ref_0_eq// node_ref_CSdk; easy. Qed.
+Proof.
+move=>> Hd /INR_n0 /invertible_equiv_R Hk; rewrite Hface_ref_0_eq//
+    -scal_sum_r sum_INR scal_eq_K mult_comm_R div_one_equiv// INR_eq_equiv; easy.
+Qed.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
@@ -116,7 +96,11 @@ Lemma node_ref_Hface_ref_S :
   forall (idk : 'I_((pbinom d k).+1)) {i : 'I_d.+1} (Hi : i <> ord0),
     (0 < d)%coq_nat -> (0 < k)%coq_nat ->
     Hface_ref i (node_ref idk) <-> Adk d k idk (lower_S Hi) = O.
-Proof. intros; rewrite Hface_ref_S_eq node_ref_ASdki; easy. Qed.
+Proof.
+move=>> Hd /INR_n0 /invertible_equiv_R Hk; rewrite Hface_ref_S_eq.
+unfold node_ref; rewrite fct_scal_eq mapF_correct scal_eq_K mult_comm_R.
+rewrite div_zero_equiv// INR_0_equiv; easy.
+Qed.
 
 End Nodes_ref_Facts1.
 
@@ -134,7 +118,7 @@ Lemma inj_Hface_ref_0_node_ref :
     inj_Hface_ref ord0 (node_ref idk) = node_ref (Adk_inv d k (inj_CSdk idk)).
 Proof.
 intros idk Hk; assert (Hk1 : invertible (INR k)) by now apply INR_invertible.
-rewrite inj_Hface_ref_0// !node_ref_eqF; unfold part1F.
+rewrite inj_Hface_ref_0//; unfold part1F, node_ref.
 rewrite Adk_inv_correct_r; [| rewrite inj_CSdk_sum; easy].
 apply (scal_reg_r _ Hk1); rewrite -3!fct_scal_eq -insertF_scal.
 rewrite scal_minus_r scal_one_r// scal_sum_r.
@@ -148,9 +132,9 @@ Lemma inj_Hface_ref_S_node_ref :
     inj_Hface_ref i (node_ref idk) =
       node_ref (Adk_inv d k (inj_ASdki (lower_S Hi) idk)).
 Proof.
-intros i Hi idk Hk.
+intros i Hi idk Hk; unfold node_ref.
 assert (Hk1 : invertible (INR k)) by now apply INR_invertible.
-rewrite inj_Hface_ref_S !node_ref_eqF insert0F_scal Adk_inv_correct_r;
+rewrite inj_Hface_ref_S insert0F_scal Adk_inv_correct_r;
     [| rewrite inj_ASdki_sum; apply Adk_sum].
 apply (scal_reg_r _ Hk1); rewrite !scal_assoc mult_inv_r// !scal_one_l//.
 rewrite -mapF_insert0F; [easy | apply INR_0].
@@ -165,7 +149,7 @@ Context {d : nat}.
 
 Lemma vtx_node_ref_d1 : vtx_ref = castF (pbinomS_1_r d) node_ref.
 Proof.
-extF i; unfold castF; rewrite node_ref_eqF.
+extF i; unfold castF, node_ref.
 rewrite INR_1 inv_one scal_one; destruct (ord_eq_dec i ord0) as [-> | Hi].
 (* i = ord0 *)
 rewrite vtx_ref_0// cast_ordS_0// Adk_0; easy.
@@ -239,7 +223,7 @@ Hypothesis Hk : (1 < k)%coq_nat.
 Lemma sub_node_ref_eq :
   sub_node_ref = widenF (pbinomS_monot_pred d k) node_ref.
 Proof.
-extF idk; unfold sub_node_ref, widenF; rewrite mapF_correct !node_ref_eqF
+extF idk; unfold sub_node_ref, node_ref, widenF; rewrite mapF_correct
     scal_assoc div_eq (mult_comm_R (INR _)) -mult_assoc mult_inv_r;
     [| apply INR_pred_invertible; easy].
 rewrite mult_one_r; do 2 f_equal; apply Adk_previous_layer; easy.
-- 
GitLab