Propagate new API.

Add vtx_ref_sum,
    node_ref_d0, node_ref_d0_eqF, node_d0_eq, node_ref_d0_node.
Modify node_d0.
Rm useless T_geom_node.

FEM/FE_LagP.v

@@ -322,9 +322,8 @@ Lemma Sigma_LagPd0_eq_from_ref :
     Sigma_LagPd0 vtx id0 p =
       Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)).
 Proof.
-intros; unfold Sigma_LagPd0, node_d0; rewrite comp_correct T_geom_am.
-do 2 apply f_equal; extF; apply eq_sym, T_geom_vtx.
-rewrite sum_ones_R; apply invertible_equiv_R, R_compl.INR_n0, S_pos.
+intros; unfold Sigma_LagPd0, node_d0 at 1;
+    rewrite comp_correct node_ref_d0_node; easy.
 Qed.
 
 (**
@@ -337,7 +336,7 @@ Lemma Sigma_LagPSdSk_eq_from_ref :
       Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)).
 Proof.
 intros; unfold Sigma_LagPSdSk.
-rewrite comp_correct -node_ref_node T_geom_node; easy.
+rewrite comp_correct -node_ref_node; easy.
 Qed.
 
 Variable d k : nat.

FEM/LagP_node.v

@@ -42,14 +42,14 @@ Local Open Scope Group_scope.
 Local Open Scope Ring_scope.
 
 
-Section Node_Facts.
+Section Nodes_Facts1.
 
 Context {d k : nat}.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Def 1588, Eq (9.80), p. 97. *)
-Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := isobarycenter_ms vtx.
+ 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>#
@@ -57,6 +57,21 @@ Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := isobarycenter_ms vtx.
 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. *)
+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. *)
+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 1599, p. 100. *)
@@ -95,14 +110,10 @@ intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
 apply node_ref_Hface_ref_S; easy.
 Qed.
 
-Lemma T_geom_node :
-  forall (idk : 'I_(pbinom d k).+1), T_geom vtx (node_ref idk) = node vtx idk.
-Proof. easy. Qed.
-
-End Node_Facts.
+End Nodes_Facts1.
 
 
-Section Nodes_Facts3.
+Section Nodes_Facts2.
 
 (** We need a dimension which is structurally nonzero.
  We take d = d1.+1 with d1 : nat. *)
@@ -134,7 +145,7 @@ Proof.
 intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_S_node_ref//.
 Qed.
 
-End Nodes_Facts3.
+End Nodes_Facts2.
 
 
 Section Nodes_d1.
@@ -210,7 +221,7 @@ Qed.
 End Sub_vertices_Facts1.
 
 
-Section Sub_node_Def.
+Section Sub_nodes_Def.
 
 Context {d : nat}.
 Variable k : nat.
@@ -224,18 +235,16 @@ Definition sub_node : 'I_(pbinom d k.-1).+1 -> 'R^d := node (sub_vtx k vtx).
 Lemma sub_nodeF : sub_node = mapF (T_geom (sub_vtx k vtx)) node_ref.
 Proof. easy. Qed.
 
-End Sub_node_Def.
+End Sub_nodes_Def.
 
 
-Section Sub_node_ref_Facts1.
+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).
-Proof.
-unfold sub_node; f_equal; extF i; unfold sub_vtx; rewrite T_geom_ref; easy.
-Qed.
+Proof. rewrite sub_vtx_refF; easy. Qed.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
@@ -251,10 +260,10 @@ rewrite !node_ref_eqF scal_assoc div_eq mult_comm_R -mult_assoc mult_inv_r;
 rewrite mult_one_r; do 2 f_equal; apply Adk_previous_layer; easy.
 Qed.
 
-End Sub_node_ref_Facts1.
+End Sub_nodes_ref_Facts1.
 
 
-Section Sub_node_Facts1.
+Section Sub_nodes_Facts1.
 
 Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
@@ -273,13 +282,13 @@ 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 T_geom_node; easy.
+f_equal; extF; rewrite mapF_correct -node_ref_node; easy.
 Qed.
 
-End Sub_node_Facts1.
+End Sub_nodes_Facts1.
 
 
-Section Sub_node_Facts2.
+Section Sub_nodes_Facts2.
 
 Context {d : nat}.
 Context {vtx : 'R^{d.+1,d}}.
@@ -297,4 +306,4 @@ rewrite Adk_last_layer;[| easy | apply S_pos].
 rewrite Nat.nle_gt; simpl; apply /ltP; easy.
 Qed.
 
-End Sub_node_Facts2.
+End Sub_nodes_Facts2.

FEM/LagP_node_ref.v

@@ -41,20 +41,31 @@ Local Open Scope Group_scope.
 Local Open Scope Ring_scope.
 
 
-Section Node_ref_Facts1.
+Section Nodes_ref_Facts1.
 
 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). *)
+
+Lemma node_ref_d0_eqF : node_ref_d0 = isobarycenter_ms vtx_ref.
+Proof.
+rewrite isobaryc_ms_eq; [| apply invertible_plusn1_R; easy].
+unfold plusn; rewrite sum_ones_R vtx_ref_sum scal_ones//.
+Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1601, Eq (9.94), p. 101.#<BR>#
- This definition uses total function [inv].
+ This definition uses total function [inv] (via [div]).
  It will be used for k>0 only.
- The specific definition for k=0 is [node_d0], for any [vtx]. *)
+ 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.
-(*  scal (/ INR k) (mapF INR (Adk d k idk)).*)
-(*  mapF (scal (/ INR k) (mapF INR)) (Adk d k).*)
+(* = 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)).
@@ -107,10 +118,10 @@ Lemma node_ref_Hface_ref_S :
     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.
 
-End Node_ref_Facts1.
+End Nodes_ref_Facts1.
 
 
-Section Node_ref_Facts2.
+Section Nodes_ref_Facts2.
 
 (** We need a dimension which is structurally nonzero.
  We take d = d1.+1 with d1 : nat. *)
@@ -145,10 +156,10 @@ apply (scal_reg_r _ Hk1); rewrite !scal_assoc mult_inv_r// !scal_one_l//.
 rewrite -mapF_insert0F; [easy | apply INR_0].
 Qed.
 
-End Node_ref_Facts2.
+End Nodes_ref_Facts2.
 
 
-Section Node_ref_d1.
+Section Nodes_ref_d1.
 
 Context {d : nat}.
 
@@ -168,14 +179,13 @@ Qed.
 Lemma node_vtx_ref_d1 : node_ref = castF (eq_sym (pbinomS_1_r d)) vtx_ref.
 Proof. intros; rewrite eq_sym_equiv -castF_sym_equiv -vtx_node_ref_d1//. Qed.
 
-End Node_ref_d1.
+End Nodes_ref_d1.
 
 
 Section Sub_vertices_ref_Def.
 
 Context {d : nat}.
 Variable k : nat.
-Variable vtx : 'R^{d.+1,d}.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#

FEM/geom_transf_affine.v

@@ -304,9 +304,7 @@ Let pi_d_inv_inj := f_inv_inj pi_d_bij.
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1586, p. 96. *)
 Lemma T_geom_permutF_bij : bijective (T_geom_permutF vtx pi_d).
-Proof.
-apply T_geom_bij, aff_indep_permutF_equiv; [ apply injF_bij |]; easy.
-Qed.
+Proof. apply T_geom_bij, aff_indep_permutF; easy. Qed.
 
 Definition T_geom_permutF_inv : 'R^d -> 'R^d := f_inv (T_geom_permutF_bij).
 

FEM/monomial.v

@@ -195,7 +195,7 @@ Lemma powF_P_one :
     powF_P L B = pow (B k) a.
 Proof.
 intros d B L a k HL; destruct d; [destruct k; easy |].
-unfold powF_P; rewrite (prod_R_singl _ k).
+unfold powF_P; rewrite (prod_R_singl k).
 rewrite HL powF_correct; f_equal; apply itemF_correct_l; easy.
 (* Warning: the multiplicative identity element of R_mul is displayed here as 0! *)
 rewrite -powF_skipF HL skipF_itemF_diag.

FEM/multi_index.v

@@ -78,7 +78,7 @@ now apply Nat.eq_le_incl.
 apply nat_add_sub_r.
 rewrite <- H.
 rewrite -skipF_first.
-apply (sum_skipF alpha ord0).
+apply (sum_skipF ord0 alpha).
 (* *)
 unfold Slice_op; extF i; unfold castF; simpl.
 case (Nat.eq_0_gt_0_cases i); intros Hi.
@@ -325,8 +325,8 @@ Proof.
 intros n A B i H1 H2.
 apply Nat.add_lt_mono_l with (A i).
 apply Nat.le_lt_trans with (sum A).
-rewrite (sum_skipF A i); unfold plus; simpl; auto with arith.
-rewrite H1; rewrite (sum_skipF B i).
+rewrite (sum_skipF i A); unfold plus; simpl; auto with arith.
+rewrite H1; rewrite (sum_skipF i B).
 unfold plus; simpl.
 apply Nat.add_lt_mono_r; auto with arith.
 Qed.

FEM/poly_LagPd1_ref.v

@@ -71,6 +71,12 @@ fun_ext2; unfold liftF_S;
     rewrite (vtx_ref_S (lift_S_not_first _)) lower_lift_S; easy.
 Qed.
 
+Lemma vtx_ref_sum : sum vtx_ref = 1.
+Proof.
+rewrite sum_ind_l vtx_ref_0// plus_zero_l vtx_ref_SF.
+extF; rewrite fct_sum_eq kron_sum_l; easy.
+Qed.
+
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1436, p. 55. *)
@@ -347,7 +353,7 @@ intros j; rewrite Ker_equiv; apply LagPd1_ref_vtx_skipF.
 intros x_ref; move: (vtx_ref_aff_span x_ref) => /aff_span_EX [L [HL ->]].
 rewrite Ker_equiv.
 move: (LagPd1_ref_barycF_rev HL) => /extF_rev HL1; rewrite (HL1 i) => HLi.
-rewrite (baryc_skip_zero _ _ i)//; [apply Aff_span |].
+rewrite (baryc_skip_zero i)//; [apply Aff_span |].
 rewrite -(plus_zero_l (sum _)) -HLi -sum_skipF.
 1,2: apply invertible_eq_one; easy.
 Qed.