From b81d0a40ae27c6a60043c8432e66e9d46bbfc7c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 20 Feb 2024 23:11:04 +0100
Subject: [PATCH] Generalize FE_simplex.bijS_equiv_nodal   and move it to
 Finite_dim.lmS_bijS_sub_gather_equiv.

FE:
Add def nvtx_of_shape.

FE_LagP:
Propagate new API (from Finite_dim).
---
 FEM/Algebra/Finite_dim.v | 36 ++++++++++++++++++++++++++++++++++++
 FEM/FE.v                 | 17 ++++++++++-------
 FEM/FE_LagP.v            | 20 ++++++++++++++------
 FEM/FE_simplex.v         | 29 -----------------------------
 4 files changed, 60 insertions(+), 42 deletions(-)

diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index bd03d4bd..e3629642 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -2858,6 +2858,42 @@ Proof. apply lmS_bijS_sub_dim_equiv; easy. Qed.
 End Linear_mapping_R_Facts3.
 
 
+Section Linear_mapping_R_Facts4.
+
+Context {E : ModuleSpace R_Ring}.
+
+Context {PE' : (E -> R) -> Prop}.
+Context {nPE' : nat}.
+Hypothesis HPE' : has_dim PE' nPE'.
+Let HPE'' :=  has_dim_compatible_ms HPE'.
+
+(*
+Variable nF : nat.
+Hypothesis HF : has_dim (@fullset F) nF.
+*)
+
+Context {n : nat}.
+Variable A : 'E^n.
+
+Let f : '((E -> R) -> R)^n := fun i u => u (A i).
+Let Hf : forall i, is_linear_mapping (f i) :=
+    fun i => is_linear_mapping_pt_value (A i).
+
+Lemma lmS_bijS_sub_gather_equiv :
+  n = nPE' ->
+  bijS PE' fullset (gather f) <->
+  forall (u : sub_ms HPE''), (forall i, val u (A i) = 0) -> u = 0.
+Proof.
+intros Hn; rewrite (lmS_bijS_sub_full_equiv _ HPE' _ has_dim_Rn _ Hn);
+    [| apply gather_is_linear_mapping_compat, Hf].
+split; intros Hf1 [u Hu] Hu1; apply Hf1.
+apply extF; intros i; apply Hu1.
+intros i; apply (extF_rev _ _ Hu1).
+Qed.
+
+End Linear_mapping_R_Facts4.
+
+
 Section Swap_fun_R.
 
 Context {E F : ModuleSpace R_Ring}.
diff --git a/FEM/FE.v b/FEM/FE.v
index da3e45de..a4484547 100644
--- a/FEM/FE.v
+++ b/FEM/FE.v
@@ -44,6 +44,12 @@ Section FE_Local_simplex.
 
 Inductive shape_type :=  Simplex  | Quad.
 
+Definition nvtx_of_shape (d : nat) (shape : shape_type) : nat :=
+  match shape with
+    | Simplex => d.+1
+    | Quad => 2^d
+  end.
+
 (* TODO: add an admissibility property for the geometrical element?
   Il manque peut-être des hypothèses géométriques 
     du type triangle pas plat ou dim (span_as vertex) = d. 
@@ -57,14 +63,11 @@ Record FE : Type := mk_FE {
   d_pos :    (0 < d)%coq_nat ;
   ndof_pos : (0 < ndof)%coq_nat ;
   shape : shape_type ;
-  nvtx : nat := match shape with (* number of vertices *)
-       | Simplex => (S d)
-       | Quad => 2^d
-    end;
+  nvtx : nat := nvtx_of_shape d shape ; (* number of vertices *)
   vtx : '('R^d)^nvtx ; (* vertices of geometrical element *)
   K_geom : 'R^d -> Prop := convex_envelop vtx ; (* geometrical element *)
-  P_approx : FRd d -> Prop ; (* Subspace of F *)
-  P_approx_has_dim : has_dim P_approx ndof ;
+  P_approx : FRd d -> Prop ; (* Subset of FRd *)
+  P_approx_has_dim : has_dim P_approx ndof ; (* Subspace of dimension ndof  *)
   Sigma : '(FRd d -> R)^ndof ;
   Sigma_lin_map : forall i, is_linear_mapping (Sigma i) ;
   unisolvence : bijS P_approx fullset (gather Sigma) ;
@@ -74,7 +77,7 @@ Variable fe: FE.
 
 Lemma nvtx_pos : (0 < nvtx fe)%coq_nat.
 Proof.
-unfold nvtx; case shape.
+unfold nvtx, nvtx_of_shape; case shape.
 auto with arith.
 apply nat_compl.S_pow_pos; auto.
 Qed.
diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index e432f3a4..d35ceb39 100644
--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -127,9 +127,10 @@ Lemma unisolvence_LagP1_d_cur : forall dL vtx_cur,
   bijS (P_approx_k_d dL 1) fullset (gather (Sigma_LagPk_d_cur dL 1 vtx_cur)).
 Proof.
 intros dL vtx_cur dL_pos Hvtx.
-destruct dL; try easy. 
+destruct dL; try easy.
 (* case dL + 1 *)
-apply (bijS_equiv_nodal _ _ _ _ (P_approx_k_d_compat_fin dL.+1 1)).
+apply (lmS_bijS_sub_gather_equiv (P_approx_k_d_compat_fin _ _)).
+rewrite ndof_is_dim_Pk; easy.
 intros [p Hp1] Hp2.
 apply val_inj; simpl.
 simpl in Hp2.
@@ -157,7 +158,9 @@ Proof.
 intros kL vtx_cur HkL Hvtx.
 destruct kL; try easy.
 (* case kL + 1 *)
-apply (bijS_equiv_nodal _ _ _ _ (P_approx_k_d_compat_fin 1 kL.+1)); intros [p Hp1] Hp2.
+apply (lmS_bijS_sub_gather_equiv (P_approx_k_d_compat_fin _ _)).
+rewrite ndof_is_dim_Pk; easy.
+intros [p Hp1] Hp2.
 apply val_inj; simpl.
 destruct (is_basis_ex_decomp (LagPk_1_cur_is_basis kL.+1 HkL vtx_cur Hvtx) p Hp1) as [L HL].
 simpl in Hp2.
@@ -498,12 +501,15 @@ intros dL HdL vtx_cur Hvtx.
 apply unisolvence_LagP1_d_cur; easy.
 clear HdL HkL kL dL.
 intros kL dL HkL HdL IH1 IH2 vtx_cur Hvtx.
-apply (bijS_equiv_nodal _ _ _ _ (P_approx_k_d_compat_fin dL.+1 kL.+1)); intros [p Hp1] Hp2.
+apply (lmS_bijS_sub_gather_equiv (P_approx_k_d_compat_fin _ _)).
+rewrite ndof_is_dim_Pk; easy.
+intros [p Hp1] Hp2.
 simpl in Hp2.
 apply val_inj; simpl.
 (* Step 1 *)
 specialize (IH1 (vtx_simplex_ref dL) (vtx_simplex_ref_affine_ind dL (kL.+1) (Nat.lt_0_succ kL))).
-rewrite bijS_equiv_nodal in IH1.
+rewrite lmS_bijS_sub_gather_equiv in IH1.
+2: rewrite ndof_is_dim_Pk; easy.
 pose (p0' := compose p (Phi dL vtx_cur )).
 assert (Hp0' : P_approx_k_d dL kL.+1 p0') by now apply Phi_compose.
 pose (p0 := mk_sub_ms_ (has_dim_compatible_ms
@@ -534,7 +540,9 @@ rewrite Hq2.
 (* Step 2 *)
 assert (H1 : (1 < kL.+1)%coq_nat); auto with zarith. 
 specialize (IH2 (sub_vertex (dL.+1) (kL.+1) vtx_cur) (sub_vertex_affine_ind (dL.+1) (kL.+1) (Nat.lt_0_succ dL) H1 vtx_cur Hvtx)).
-destruct (bijS_equiv_nodal _ _ (sub_node (dL.+1) (kL.+1) vtx_cur) _ (P_compat_fin_LagPk_d (dL.+1) kL)) as [H3 _].
+destruct (lmS_bijS_sub_gather_equiv
+    (P_compat_fin_LagPk_d (dL.+1) kL) (sub_node (dL.+1) (kL.+1) vtx_cur)) as [H3 _].
+rewrite ndof_is_dim_Pk; easy.
 unfold Sigma_LagPk_d_cur, nnode_LagP in IH2.
 unfold ndof_nodal, sub_node in H3.
 simpl in H3.
diff --git a/FEM/FE_simplex.v b/FEM/FE_simplex.v
index 69f396ed..13096e10 100644
--- a/FEM/FE_simplex.v
+++ b/FEM/FE_simplex.v
@@ -472,33 +472,4 @@ Proof.
 intros; apply is_linear_mapping_pt_value.
 Qed.
 
-Variable P : FRd dn -> Prop.
-
-Hypothesis P_has_dim : has_dim P ndof_nodal.
-Let PC := has_dim_compatible_ms P_has_dim.
-
-Local Notation Pol := (sub_ms PC).
-Let Pval : Pol -> ('R^dn -> R) := fun (p : Pol) => val p.
-Local Coercion Pval : Pol >-> Funclass.
-
-(* From FE v3 Alexandre Ern : Proposition 7.12 p. 64 *)
-(** "Livre Vincent Lemma 1539 - p17." *)
-Lemma bijS_equiv_nodal :
-  bijS P fullset (gather Sigma_nodal) <->
-    (forall (p : sub_ms PC), (forall i, p (nodes i) = zero) -> p = 0%M).
-Proof.
-rewrite (lmS_bijS_sub_full_equiv _ P_has_dim _ has_dim_Rn _ eq_refl).
-(* *)
-split; intros H1.
-(* . *)
-intros [p Hp] H2; apply H1.
-apply extF; intro; apply H2.
-(* . *)
-intros [p Hp] H2; apply H1; intros i.
-apply (extF_rev _ _ H2 i).
-(* *)
-apply gather_is_linear_mapping_compat.
-intros; apply Sigma_nodal_lin_map.
-Qed.
-
 End FE_Nodal.
-- 
GitLab