FEM/FE_LagP.v

@@ -154,28 +154,28 @@ Qed.
 (** Induction step: unisolvence result for d,k>1. *)
 
 Lemma unisolvence_inj_Hface :
-  forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat -> PI d k.+1 ->
-    forall i {vtx p}, aff_indep_ms vtx -> Pdk d.+1 k.+1 p ->
-      (forall (idk : [0..(pbinom d.+1 k.+1).+1)),
+  forall {d k}, (0 < d)%coq_nat -> (0 < k)%coq_nat -> PI d k ->
+    forall i {vtx p}, aff_indep_ms vtx -> Pdk d.+1 k p ->
+      (forall (idk : [0..(pbinom d.+1 k).+1)),
         Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) ->
       forall x, Hface vtx i x -> p x = 0.
 Proof.
-intros d k Hd Hk H i vtx p Hvtx Hp1 Hp2 x Hx.
+intros d k Hd Hk.
 assert (HSd : (0 < d.+1)%coq_nat) by apply S_pos.
-assert (HSk : (0 < k.+1)%coq_nat) by apply S_pos.
+destruct k as [| k1]; [easy |].
+intros H i vtx p Hvtx Hp1 Hp2 x Hx.
 rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
 fold (T_geom_Hface_invS Hvtx i x).
 pose (pi := fun y => p (T_geom_Hface vtx i y));
   fold (pi (T_geom_Hface_invS Hvtx i x)).
-rewrite (H _ vtx_ref_aff_indep pi)//.
-apply T_geom_Hface_comp; easy.
+rewrite (H _ vtx_ref_aff_indep pi)//; [apply T_geom_Hface_comp; easy |].
 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.. |].
 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 T_geom_Hface_S_node//; apply Hp2, (node_Hface_S Hvtx _ Hi HSd Hk).
 rewrite Adk_inv_correct_r;
     [apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
 Qed.
@@ -190,17 +190,8 @@ assert (HSk0 : (0 < k.+1)%coq_nat) by apply S_pos.
 assert (HSk1 : (1 < k.+1)%coq_nat) by now rewrite -Nat.succ_lt_mono.
 apply KerS0_gather_equiv; intros p Hp1 Hp2.
 (* Step 1: factorization. *)
-pose (p' := p \o T_geom_Hface vtx ord0).
-assert (Hp' : Pdk d k.+1 p') by now apply T_geom_Hface_comp.
-specialize (IH1 _ vtx_ref_aff_indep); rewrite KerS0_gather_equiv in IH1.
-specialize (IH1 _ Hp'); rewrite -node_ref_node in IH1.
-assert (Hp3 : forall y, Hface vtx ord0 y ->
-    p y = p' (T_geom_Hface_invS Hvtx ord0 y))
-  by now intros; unfold p'; rewrite comp_correct f_invS_canS_r.
-assert (Hp4 : forall x, Hface vtx ord0 x -> p x = 0).
-  intros; rewrite Hp3// IH1//.
-  intros; unfold p'; rewrite comp_correct T_geom_Hface_0_node//.
-destruct (factor_zero_on_Hface HSd0 Hvtx _ Hp1 Hp4) as [q [Hq1 Hq2]].
+destruct (factor_zero_on_Hface HSd0 Hvtx ord0 Hp1) as [q [Hq1 Hq2]].
+apply (unisolvence_inj_Hface Hd0 HSk0); easy.
 (* Step 2: cancellation. *)
 specialize (IH2 _ (sub_vtx_aff_indep HSk1 Hvtx));
     rewrite KerS0_gather_equiv in IH2.
@@ -414,25 +405,10 @@ Lemma Hface_unisolvence :
       Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) <->
     (forall x, Hface vtx i x -> p x = 0).
 Proof.
-assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
 intros i p Hp; split; [| move=> H idk Hidk; apply H; easy].
-intros H x Hx; destruct d as [| d1]; [easy |].
-assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
-rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
-fold (T_geom_Hface_invS Hvtx i x).
-pose (pi := fun y => p (T_geom_Hface vtx i y));
-  fold (pi (T_geom_Hface_invS Hvtx i x)).
-rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep pi)//.
-apply T_geom_Hface_comp; easy.
-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.. |].
-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;
-    [apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
+destruct d as [| d1]; [easy |].
+assert (Hd0 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
+apply: (unisolvence_inj_Hface _ _ (unisolvence_inj_LagPSdSk _ _)); easy.
 Qed.
 
 End Face_unisolvence.