From 24f93fc74c5445397098b5d7ebb85169e916ee2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 14 Mar 2025 01:47:43 +0100
Subject: [PATCH] Go for higher level (constF, mapF). Factor hypotheses.

---
 FEM/LagP_node.v     | 15 ++++++++-------
 FEM/LagP_node_ref.v | 17 ++++++++++-------
 2 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/FEM/LagP_node.v b/FEM/LagP_node.v
index 698ec107..d2ba4916 100644
--- a/FEM/LagP_node.v
+++ b/FEM/LagP_node.v
@@ -60,8 +60,8 @@ Proof. unfold node_d0; extF; rewrite T_geom_ref; easy. Qed.
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1604, p. 101. *)
-Definition node (vtx : 'R^{d.+1,d}) (idk : 'I_(pbinom d k).+1) : 'R^d :=
-  T_geom vtx (node_ref idk).
+Definition node (vtx : 'R^{d.+1,d}) : [0..(pbinom d k).+1) -> 'R^d :=
+  mapF (T_geom vtx) node_ref.
 
 Lemma nodeF : forall vtx, node vtx = mapF (T_geom vtx) node_ref.
 Proof. easy. Qed.
@@ -90,6 +90,7 @@ intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
 apply node_ref_Hface_ref_0; easy.
 Qed.
 
+(* TODO FC (13/03/2025): or rather use liftF_S. *)
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1605, Eq (9.96), p. 101. #<BR>#
@@ -113,6 +114,7 @@ Section Nodes_Facts2.
  We take d = d1.+1 with d1 : nat. *)
 Context {d1 k : nat}.
 Let d := d1.+1.
+Hypothesis Hk : (0 < k)%coq_nat.
 Variable vtx : 'R^{d.+1,d}.
 
 (**
@@ -120,11 +122,11 @@ Variable vtx : 'R^{d.+1,d}.
  Lem 1607, p. 102, case i=0.#<BR># 
  See also Rem 1606. *)
 Lemma T_geom_Hface_0_node :
-  forall (idk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat ->
+  forall (idk : 'I_(pbinom d1 k).+1),
     T_geom_Hface vtx ord0 (node_ref idk) =
       node vtx (Adk_inv d k (inj_CSdk idk)).
 Proof.
-intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_0_node_ref//.
+intro; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_0_node_ref//.
 Qed.
 
 (**
@@ -132,7 +134,7 @@ Qed.
  Lem 1607, p. 102, case i>0.#<BR>#
  See also Rem 1606. *)
 Lemma T_geom_Hface_S_node :
-  forall {i} (Hi : i <> ord0) (idk : 'I_(pbinom d1 k).+1), (0 < k)%coq_nat ->
+  forall {i} (Hi : i <> ord0) (idk : 'I_(pbinom d1 k).+1),
     T_geom_Hface vtx i (node_ref idk) =
       node vtx (Adk_inv d k (inj_ASdki (lower_S Hi) idk)).
 Proof.
@@ -148,8 +150,7 @@ Context {d : nat}.
 
 Lemma node_vtx_d1 : forall vtx, node vtx = castF (eq_sym (pbinomS_1_r d)) vtx.
 Proof.
-intro; extF; unfold node; rewrite node_vtx_ref_d1;
-    unfold castF; rewrite T_geom_vtx; easy.
+intro; unfold node; rewrite node_vtx_ref_d1 mapF_castF T_geom_vtxF; easy.
 Qed.
 
 Context {vtx : 'R^{d.+1,d}}.
diff --git a/FEM/LagP_node_ref.v b/FEM/LagP_node_ref.v
index cd2bdc0e..0f1cbaa1 100644
--- a/FEM/LagP_node_ref.v
+++ b/FEM/LagP_node_ref.v
@@ -48,8 +48,7 @@ Context {d k : nat}.
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1601, Eq (9.93), p. 101. *)
-Definition node_ref_d0 : 'R^d := fun=> / INR d.+1.
-(* = constF d (/ INR d.+1). *)
+Definition node_ref_d0 : 'R^d := constF d (/ INR d.+1).
 
 Lemma node_ref_d0_eqF : node_ref_d0 = isobarycenter_ms vtx_ref.
 Proof.
@@ -75,18 +74,23 @@ rewrite pbinom_0_r in Hi, Hj; move: Hi => /ltP Hi; move: Hj => /ltP Hj; lia.
 move=>> /(scal_reg_r_R _ (INR_inv_n0 Hk)) /(mapF_inj INR_eq) /Adk_inj; easy.
 Qed.
 
+Hypothesis Hd : (0 < d)%coq_nat.
+Hypothesis Hk : (0 < k)%coq_nat.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1605 (for [vtx_ref]), Eq (9.95), p. 101. #<BR>#
  \hat{a}_alpha \in \hat{Hface}_0 <-> alpha \in CSdk, ie \sum alpha = k. *)
 Lemma node_ref_Hface_ref_0 :
-  forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
+  forall (idk : 'I_((pbinom d k).+1)),
     Hface_ref ord0 (node_ref idk) <-> sum (Adk d k idk) = k.
 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.
+apply INR_n0, invertible_equiv_R in Hk; intro; rewrite Hface_ref_0_eq//.
+rewrite -scal_sum_r sum_INR scal_eq_K mult_comm_R.
+rewrite div_one_equiv// INR_eq_equiv; easy.
 Qed.
 
+(* TODO FC (13/03/2025): or rather use liftF_S. *)
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1605 (for [vtx_ref]), Eq (9.96), p. 101. #<BR>#
@@ -94,10 +98,9 @@ Qed.
  a_alpha \in Hface_{i+1} iff alpha \in ASdki, ie alpha_i = 0. *)
 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.
-move=>> Hd /INR_n0 /invertible_equiv_R Hk; rewrite Hface_ref_S_eq.
+apply INR_n0, invertible_equiv_R in Hk; intros; 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.
-- 
GitLab