From bed43959d861ef4899d2cf1f3a8c20e132c8a798 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 00:09:33 +0100
Subject: [PATCH] WIP: get properties on sub_node from sub_node_ref. Add
 sub_node_ref, sub_node_ref_eq, sub_node_ref_out_Hface_ref_0, nodeF. Rename
 sub_nodeF -> sub_nodeF_alt,        sub_node_ref -> sub_node_ref_sub_node.
 Modify sub_node. WIP: sub_nodeF, sub_node_out_Hface_0 (should use
 sub_node_ref_out_Hface_ref_0). Hide presumably useless   sub_nodeF_alt,
 sub_node_ref_sub_node, sub_node_ref_eq, T_geom_sub_nodeF.

---
 FEM/FE_LagP.v       |  2 +-
 FEM/LagP_node.v     | 67 +++++++++++++++++++++++++++++----------------
 FEM/LagP_node_ref.v | 50 +++++++++++++++++++++++++++++++++
 3 files changed, 95 insertions(+), 24 deletions(-)

diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index 8ac3c48c..37b835ed 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 -fct_mult_eq -Hq2 sub_node_eq// Hp2 mult_zero_r; easy.
+rewrite -(sub_nodeF k.+1) -fct_mult_eq -Hq2 sub_node_eq// Hp2 mult_zero_r; easy.
 Qed.
 
 (** Unisolvence result for d,k>0. *)
diff --git a/FEM/LagP_node.v b/FEM/LagP_node.v
index 13bd282e..249705e5 100644
--- a/FEM/LagP_node.v
+++ b/FEM/LagP_node.v
@@ -51,12 +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>#
- 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).
-
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Def 1588, Eq (9.80), p. 97. *)
@@ -72,6 +66,15 @@ Qed.
 Lemma node_ref_d0_node : node_ref_d0 = node_d0 vtx_ref.
 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).
+
+Lemma nodeF : forall vtx, node vtx = mapF (T_geom vtx) node_ref.
+Proof. easy. Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1599, p. 100. *)
@@ -229,21 +232,38 @@ Variable vtx : 'R^{d.+1,d}.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1598, p. 100. *)
-Definition sub_node : 'I_(pbinom d k.-1).+1 -> 'R^d := node (sub_vtx k vtx).
+ 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 (sub_vtx k vtx)) node_ref.
+Lemma sub_nodeF_alt : sub_node = mapF (T_geom vtx) sub_node_ref.
 Proof. easy. Qed.
 
-End Sub_nodes_Def.
+Lemma sub_nodeF : sub_node = node (sub_vtx k vtx).
+Proof.
+rewrite sub_nodeF_alt nodeF sub_vtxF -T_geom_comp mapF_comp.
+f_equal.
 
 
+Admitted.
+
+(*
+Lemma sub_nodeF_alt : sub_node = mapF (T_geom (sub_vtx k vtx)) node_ref.
+Proof.
+rewrite sub_nodeF; extF; rewrite !mapF_correct.
+
+
+ easy. Qed.
+*)
+End Sub_nodes_Def.
+
+(*
 Section Sub_nodes_ref_Facts1.
 
 Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
 
-Lemma sub_node_ref : sub_node k (@vtx_ref d) = node (sub_vtx_ref k).
+Lemma sub_node_ref_sub_node : sub_node k (@vtx_ref d) = node (sub_vtx_ref k).
 Proof. rewrite sub_vtx_refF; easy. Qed.
 
 (**
@@ -261,7 +281,7 @@ rewrite mult_one_r; do 2 f_equal; apply Adk_previous_layer; easy.
 Qed.
 
 End Sub_nodes_ref_Facts1.
-
+*)
 
 Section Sub_nodes_Facts1.
 
@@ -269,40 +289,41 @@ Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
 Variable vtx : 'R^{d.+1,d}.
 
+(*
 Lemma T_geom_sub_nodeF :
   mapF (T_geom vtx) (sub_node k vtx_ref) = sub_node k vtx.
 Proof.
 rewrite !sub_nodeF -mapF_comp T_geom_comp -sub_vtx_refF sub_vtxF; easy.
 Qed.
+*)
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1598, p. 100. *)
 Lemma sub_node_eq :
   sub_node k vtx = widenF (pbinomS_monot_pred d k) (node vtx).
-Proof.
-rewrite -T_geom_sub_nodeF sub_node_ref_eq// -widenF_mapF.
-f_equal; extF; rewrite mapF_correct -node_ref_node; easy.
-Qed.
+Proof. extF; unfold sub_node; rewrite sub_node_ref_eq//. Qed.
 
 End Sub_nodes_Facts1.
 
 
 Section Sub_nodes_Facts2.
 
-Context {d : nat}.
+Context {d k : nat}.
+Hypothesis Hd : (0 < d)%coq_nat.
+Hypothesis Hk : (1 < k)%coq_nat.
 Context {vtx : 'R^{d.+1,d}}.
 Hypothesis Hvtx : aff_indep_ms vtx.
 
 (** sub_node \notin Hface_0 *)
 Lemma sub_node_out_Hface_0 :
-  forall {k} (idk : 'I_((pbinom d k).+1)),
-    (0 < d)%coq_nat -> (0 < k)%coq_nat ->
-    ~ Hface vtx ord0 (sub_node k.+1 vtx idk).
+  forall (idk : [0..(pbinom d k.-1).+1)),
+    ~ Hface vtx ord0 (sub_node k vtx idk).
 Proof.
-intros; rewrite sub_node_eq; [| rewrite -Nat.succ_lt_mono; easy].
-rewrite node_Hface_0//; [| apply S_pos].
-rewrite Adk_last_layer;[| easy | apply S_pos].
+(*intros idk H. apply (sub_node_ref_out_Hface_ref_0 ).*)
+
+assert (Hk0 : (0 < k)%coq_nat) by now apply Nat.lt_succ_l.
+intros; rewrite sub_node_eq// node_Hface_0// Adk_last_layer//.
 rewrite Nat.nle_gt; simpl; apply /ltP; easy.
 Qed.
 
diff --git a/FEM/LagP_node_ref.v b/FEM/LagP_node_ref.v
index b15f6abb..b13c93bf 100644
--- a/FEM/LagP_node_ref.v
+++ b/FEM/LagP_node_ref.v
@@ -214,3 +214,53 @@ apply bij_inj, scal_bij, INR_ratio_invertible; easy.
 Qed.
 
 End Sub_vertices_ref_Facts.
+
+
+Section Sub_nodes_ref_Def.
+
+Context {d k : nat}.
+
+(** This definition uses total function [inv].
+ It is meaningful for k>0 only, and useful for k>1. *)
+Definition sub_node_ref : [0..(pbinom d k.-1).+1) -> 'R^d :=
+  mapF (scal (INR k.-1 / INR k)) node_ref.
+
+End Sub_nodes_ref_Def.
+
+
+Section Sub_nodes_ref_Facts1.
+
+Context {d k : nat}.
+Hypothesis Hk : (1 < k)%coq_nat.
+
+(**
+ #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
+ Lem 1598 (for [vtx_ref]), p. 100. *)
+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
+    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.
+Qed.
+
+End Sub_nodes_ref_Facts1.
+
+
+Section Sub_nodes_ref_Facts2.
+
+Context {d k : nat}.
+Hypothesis Hd : (0 < d)%coq_nat.
+Hypothesis Hk : (1 < k)%coq_nat.
+
+(** sub_node_ref \notin Hface_ref_0 *)
+Lemma sub_node_ref_out_Hface_ref_0 :
+  forall (idk : [0..(pbinom d k.-1).+1)), ~ Hface_ref ord0 (sub_node_ref idk).
+Proof.
+assert (Hk0 : (0 < k)%coq_nat) by now apply Nat.lt_succ_l.
+intros; rewrite sub_node_ref_eq// node_ref_Hface_ref_0// Adk_last_layer//.
+rewrite Nat.nle_gt; simpl; apply /ltP; easy.
+Qed.
+
+End Sub_nodes_ref_Facts2.
-- 
GitLab