FEM/FE_LagP.v

@@ -173,7 +173,7 @@ extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi; rewrite -node_ref_node.
 destruct (ord_eq_dec i ord0) as [-> | Hi].
 (* i = ord0 *)
 rewrite T_geom_Hface_0_node//; apply Hp2, node_Hface_0; [easy.. |].
-apply Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
+rewrite Adk_inv_correct_r inj_CSdk_sum//.
 (* i <> ord0 *)
 rewrite T_geom_Hface_S_node//; apply Hp2, (node_Hface_S Hvtx _ Hi HSd HSk).
 rewrite Adk_inv_correct_r;
@@ -428,7 +428,7 @@ extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi; rewrite -node_ref_node.
 destruct (ord_eq_dec i ord0) as [-> | Hi].
 (* i = ord0 *)
 rewrite T_geom_Hface_0_node//; apply H, node_Hface_0; [easy.. |].
-apply Adk_last_layer; [easy.. |]; rewrite Adk_inv_correct_r inj_CSdk_sum//.
+rewrite Adk_inv_correct_r inj_CSdk_sum//.
 (* i <> ord0 *)
 rewrite T_geom_Hface_S_node//; apply H, (node_Hface_S Hvtx _ Hi Hd0 Hk).
 rewrite Adk_inv_correct_r;

FEM/LagP_node.v

@@ -75,7 +75,7 @@ Proof. move=>> /(T_geom_inj Hvtx) /node_ref_inj; easy. Qed.
  a_alpha \in Hface_0 <-> alpha \in CSdk. *)
 Lemma node_Hface_0 :
   forall (idk : 'I_((pbinom d k).+1)), (0 < d)%coq_nat -> (0 < k)%coq_nat ->
-    Hface vtx ord0 (node vtx idk) <-> ((pbinom d k.-1).+1 <= idk)%coq_nat.
+    Hface vtx ord0 (node vtx idk) <-> sum (Adk d k idk) = k.
 Proof.
 intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
 apply node_ref_Hface_ref_0; easy.
@@ -293,6 +293,7 @@ Lemma sub_node_out_Hface_0 :
 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].
 rewrite Nat.nle_gt; simpl; apply /ltP; easy.
 Qed.
 

FEM/LagP_node_ref.v

@@ -73,9 +73,9 @@ 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 <-> ((pbinom d k.-1).+1 <= idk)%coq_nat.
+    sum (node_ref idk) = 1 <-> sum (Adk d k idk) = k.
 Proof.
-move=>> Hd Hk; rewrite -Adk_last_layer// node_ref_eqF -scal_sum_r sum_INR.
+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.
@@ -93,7 +93,7 @@ Qed.
  \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 ->
-    Hface_ref ord0 (node_ref idk) <-> ((pbinom d k.-1).+1 <= idk)%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.
 
 (**

FEM/multi_index.v

@@ -93,14 +93,14 @@ intros V; unfold liftF_S; simpl; f_equal.
 apply ord_inj; simpl; unfold bump; simpl; auto with arith.
 Qed.
 
-Definition Slice_fun {d n:nat} (u:nat) (a:'I_n -> 'nat^d) : 'I_n -> 'nat^d.+1
+Definition Slice_opF {d n:nat} (u:nat) (a:'I_n -> 'nat^d) : 'I_n -> 'nat^d.+1
    := mapF (Slice_op u) a.
 
-Lemma Slice_fun_skipF0: forall {d n} u (a:'I_n -> 'nat^d.+1) i,
-   skipF0 (Slice_fun u a i) = a i.
+Lemma Slice_opF_skipF0: forall {d n} u (a:'I_n -> 'nat^d.+1) i,
+   skipF0 (Slice_opF u a i) = a i.
 Proof.
 intros d n u a i.
-unfold Slice_fun; rewrite mapF_correct; unfold Slice_op.
+unfold Slice_opF; rewrite mapF_correct; unfold Slice_op.
 extF j.
 unfold skipF, castF, concatF.
 case (lt_dec _ _).
@@ -110,10 +110,10 @@ intros V; f_equal.
 apply ord_inj; simpl; unfold bump; simpl; auto with arith.
 Qed.
 
-Lemma Slice_fun_monot : forall {d n} u (alpha:'I_n -> 'nat^d)
+Lemma Slice_opF_monot : forall {d n} u (alpha:'I_n -> 'nat^d)
      (i j:'I_n), (i < j)%coq_nat ->
      grsymlex_lt (alpha i) (alpha j) ->
-     grsymlex_lt (Slice_fun u alpha i) (Slice_fun u alpha j).
+     grsymlex_lt (Slice_opF u alpha i) (Slice_opF u alpha j).
 Proof.
 intros d; induction d.
 intros n u alpha i j H1 H.
@@ -133,13 +133,13 @@ rewrite (Slice_op_sum _ (sum (alpha i)+u) u); auto with arith.
 rewrite (Slice_op_sum _ (sum (alpha j)+u) u); auto with arith.
 now rewrite Nat.add_sub.
 now rewrite Nat.add_sub.
-rewrite 2!Slice_fun_skipF0; easy.
+rewrite 2!Slice_opF_skipF0; easy.
 Qed.
 
-Lemma Slice_fun_sortedF : forall {d n} u (alpha:'I_n -> 'nat^d),
-   sortedF grsymlex_lt alpha -> sortedF grsymlex_lt (Slice_fun u alpha).
+Lemma Slice_opF_sortedF : forall {d n} u (alpha:'I_n -> 'nat^d),
+   sortedF grsymlex_lt alpha -> sortedF grsymlex_lt (Slice_opF u alpha).
 Proof.
-move=>> H =>> H1; apply Slice_fun_monot; [| apply H]; easy.
+move=>> H =>> H1; apply Slice_opF_monot; [| apply H]; easy.
 Qed.
 
 Lemma CSdk_aux : forall (d k:nat),
@@ -152,7 +152,7 @@ Fixpoint CSdk (d k : nat) : 'nat^{(pbinom d k).+1,d.+1} :=
   match d with
   | O => fun _ _ => k
   | S d1 => castF (pbinomS_rising_sum_l d1 k)
-                  (concatnF (fun i => Slice_fun (k - i) (CSdk d1 i)))
+                  (concatnF (fun i => Slice_opF (k - i) (CSdk d1 i)))
   end.
 
 Lemma CS0k_eq : forall k, CSdk 0 k = fun _ _ => k.
@@ -161,7 +161,7 @@ Proof. easy. Qed.
 Lemma CSdk_eq :
   forall d k, CSdk d.+1 k =
     castF (pbinomS_rising_sum_l d k)
-          (concatnF (fun i => Slice_fun (k - i)%coq_nat (CSdk d i))).
+          (concatnF (fun i => Slice_opF (k - i)%coq_nat (CSdk d i))).
 Proof. intros; extF; simpl; unfold castF; f_equal. Qed.
 
 Lemma CSdk_ext :
@@ -180,7 +180,7 @@ rewrite CSdk_eq.
 unfold castF.
 rewrite (splitn_ord (cast_ord (eq_sym (pbinomS_rising_sum_l d k)) iSdk)).
 rewrite concatn_ord_correct.
-unfold Slice_fun; rewrite mapF_correct.
+unfold Slice_opF; rewrite mapF_correct.
 apply Slice_op_sum.
 auto with arith zarith.
 rewrite IHd.
@@ -230,7 +230,7 @@ rewrite castF_comp.
 apply: concatF_castF_eq.
 apply pbinomS_0_r.
 apply pbinomS_1_r.
-intros K1; extF i; unfold castF, Slice_fun; simpl.
+intros K1; extF i; unfold castF, Slice_opF; simpl.
 rewrite mapF_correct; unfold Slice_op.
 unfold singleF; rewrite constF_correct.
 unfold itemF.
@@ -246,7 +246,7 @@ intros T; apply Hj; apply ord_inj; easy.
 apply Nat.le_ngt, Nat.neq_0_le_1; easy.
 intros K1; rewrite mapF_correct.
 extF i.
-unfold castF, Slice_fun; simpl.
+unfold castF, Slice_opF; simpl.
 rewrite mapF_correct; unfold Slice_op.
 extF j; unfold castF.
 f_equal.
@@ -265,7 +265,7 @@ rewrite ord_one; case (ord_eq_dec _ _); easy.
 intros k; rewrite CSdk_eq.
 unfold castF; extF i.
 rewrite concatnF_splitn_ord.
-unfold Slice_fun; rewrite mapF_correct; unfold Slice_op, castF.
+unfold Slice_opF; rewrite mapF_correct; unfold Slice_op, castF.
 rewrite splitn_ord2_0; try easy; auto with arith.
 rewrite IHd.
 rewrite splitn_ord1_0; try easy; auto with arith.
@@ -293,7 +293,7 @@ generalize (CSdk_aux d k); intros H1.
 unfold castF.
 rewrite concatnF_splitn_ord.
 rewrite splitn_ord2_max; try easy.
-unfold Slice_fun, Slice_op; rewrite mapF_correct.
+unfold Slice_opF, Slice_op; rewrite mapF_correct.
 rewrite IHd.
 replace (k - _)%coq_nat with 0%nat.
 unfold castF; extF i.
@@ -343,7 +343,7 @@ intros k; rewrite CSdk_eq.
 apply sortedF_castF.
 apply concatnF_order.
 apply grsymlex_lt_strict_total_order.
-intros i; apply Slice_fun_sortedF.
+intros i; apply Slice_opF_sortedF.
 apply IHd.
 intros i Him.
 apply grsymlex_lt_S; right.
@@ -369,7 +369,7 @@ rewrite (Slice_op_sum _ k); try auto with zarith.
 rewrite CSdk_0 sum_itemF.
 simpl; rewrite bump_r; auto with zarith arith.
 rewrite CSdk_max sum_itemF; simpl; auto with arith zarith.
-unfold Slice_fun, Slice_op; rewrite 2!mapF_correct; simpl.
+unfold Slice_opF, Slice_op; rewrite 2!mapF_correct; simpl.
 unfold castF; rewrite 2!concatF_correct_l; simpl.
 rewrite 2!singleF_0.
 rewrite bump_r; auto with zarith arith.
@@ -404,7 +404,7 @@ extF z; unfold castF.
 rewrite (concatn_ord_correct' _ _ (Ordinal Vu) i1).
 2: now simpl.
 rewrite -Hu3 Hi1.
-unfold Slice_fun; rewrite mapF_correct; unfold Slice_op.
+unfold Slice_opF; rewrite mapF_correct; unfold Slice_op.
 unfold castF; f_equal; f_equal; simpl.
 apply eq_sym, Nat.add_sub_eq_l; auto with arith zarith.
 apply Nat.sub_add; easy.