Rm useless commented code.

FEM/poly_LagPd1_ref.v

@@ -71,39 +71,6 @@ fun_ext2; unfold liftF_S;
     rewrite (vtx_ref_S (lift_S_not_first _)) lower_lift_S; easy.
 Qed.
 
-(* Unused!
-Lemma vtx_ref_S_is_0 :
-  forall {i} (Hi : i <> ord0) {j : 'I_d}, j <> lower_S Hi -> vtx_ref i j = 0.
-Proof.
-move=>> Hj; rewrite vtx_ref_S; apply kron_is_0, ord_neq_compat; easy.
-Qed.*)
-
-(* Unused!
-Lemma vtx_ref_S_is_1 :
-  forall {i} (Hi : i <> ord0) {j : 'I_d}, j = lower_S Hi -> vtx_ref i j = 1.
-Proof. intros; subst; rewrite vtx_ref_S; apply kron_is_1; easy. Qed.*)
-
-(* Unused!
-Lemma vtx_ref_is_0_or_1 : forall i j, vtx_ref i j = 0 \/ vtx_ref i j = 1.
-Proof.
-intros; destruct (ord_eq_dec i ord0) as [-> | Hi].
-left; rewrite vtx_ref_0; easy.
-destruct (ord_eq_dec j (lower_S Hi)) as [-> | Hj].
-right; rewrite vtx_ref_S_is_1; easy.
-left; rewrite vtx_ref_S_is_0; easy.
-Qed.*)
-
-(* Unused!
-Lemma vtx_ref_ge_0 : forall i j, 0 <= vtx_ref i j.
-Proof.
-intros i j; case (vtx_ref_is_0_or_1 i j) => ->; [easy | apply Rle_0_1].
-Qed.
-
-Lemma vtx_ref_le_1 : forall i j, vtx_ref i j <= 1.
-Proof.
-intros i j; case (vtx_ref_is_0_or_1 i j) => ->; [apply Rle_0_1 | easy].
-Qed.*)
-
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1436, p. 55. *)
@@ -141,20 +108,6 @@ Qed.
 
 End Unit_Vertices.
 
-(* Useless!
-Section Unit_Vertices_1.
-
-Lemma vtx_ref_1_aff_indep :
-  let H := eq_sym (pbinomS_1_r 1) in
-  invertible (castF H vtx_ref ord_max ord0 - castF H vtx_ref ord0 ord0).
-Proof.
-intros; rewrite castF_id; clear; apply invertible_equiv_R.
-rewrite minus_zero_equiv (vtx_ref_0 ord0)// vtx_ref_S_is_1//;
-    [apply one_not_zero_R | intro; rewrite ord_one; easy].
-Qed.
-
-End Unit_Vertices_1.*)
-
 
 Section LagPd1_ref_Facts.
 
@@ -201,10 +154,6 @@ intro; extF; unfold liftF_S.
 rewrite (LagPd1_ref_S (lift_S_not_first _)) lower_lift_S; easy.
 Qed.
 
-(* Unused!
-Lemma LagPd1_ref_SF_f : liftF_S LagPd1_ref = fun i : 'I_d => @^~ i.
-Proof. extF i; fun_ext; move: i; apply extF_rev, LagPd1_ref_SF. Qed.*)
-
 Lemma LagPd1_ref_0F :
   forall {i} x_ref, i = ord0 ->
     LagPd1_ref i x_ref = 1 - sum (liftF_S (LagPd1_ref^~ x_ref)).
@@ -251,14 +200,6 @@ Proof.
 intro; apply bc_vtx_ref_uniq; [apply LagPd1_ref_sum | apply LagPd1_ref_barycF].
 Qed.
 
-(* Useless!
-Lemma LagPd1_ref_bc :
-  forall i x_ref, LagPd1_ref i x_ref = baryc_coord_ms vtx_ref x_ref i.
-Proof. intros; rewrite -LagPd1_ref_bcF; easy. Qed.
-
-Lemma LagPd1_ref_bc_f : forall i, LagPd1_ref i = baryc_coord_ms vtx_ref ^~ i.
-Proof. intro; fun_ext; apply LagPd1_ref_bc. Qed.*)
-
 Lemma LagPd1_ref_bc_scatter : LagPd1_ref = scatter (baryc_coord_ms vtx_ref).
 Proof. extF i; fun_ext; move: i; apply extF_rev; apply LagPd1_ref_bcF. Qed.
 
@@ -281,18 +222,9 @@ Qed.
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1543, Eq (9.32), p. 81. *)
-(* Unused!
-Lemma LagPd1_ref_kron_vtx : forall i j, LagPd1_ref j (vtx_ref i) = kronR i j.
-Proof. intros; rewrite LagPd1_ref_bc; apply bc_kron, vtx_ref_aff_indep. Qed.*)
-
 Lemma LagPd1_ref_kron_vtx : forall i, LagPd1_ref^~ (vtx_ref i) = kronR i.
 Proof. intro; rewrite LagPd1_ref_bcF; apply bc_kronF_r, vtx_ref_aff_indep. Qed.
 
-(* Unused
-Lemma LagPd1_ref_kron_vtx_l :
-   forall j, mapF (LagPd1_ref j) vtx_ref = kronR^~ j.
-Proof. intro; extF; rewrite mapF_correct; apply LagPd1_ref_kron_vtx. Qed.*)
-
 Lemma LagPd1_ref_S_Monom :
   liftF_S LagPd1_ref = castF (pbinom_1_r d) (liftF_S (Monom_dk d 1)).
 Proof.
@@ -301,11 +233,6 @@ extF i; fun_ext; move: i; apply extF_rev;
 rewrite castF_comp castF_id; easy.
 Qed.
 
-(* Unused!
-Lemma LagPd1_ref_S_Monom_rev :
-  liftF_S (Monom_dk d 1) = castF (eq_sym (pbinom_1_r d)) (liftF_S LagPd1_ref).
-Proof. rewrite LagPd1_ref_S_Monom castF_comp castF_refl//. Qed.*)
-
 Lemma LagPd1_ref_S_is_Pd1 : inclF (liftF_S LagPd1_ref) (Pdk d 1).
 Proof.
 intro; rewrite LagPd1_ref_S_Monom;
@@ -345,18 +272,6 @@ Qed.
 Lemma Pd1_has_dim : has_dim (Pdk d 1) d.+1.
 Proof. apply (Dim _ _ _ LagPd1_ref_basis). Qed.
 
-(* Useless!
-(**
- #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1555 (for [vtx_ref]), p. 85. *)
-Lemma LagPd1_ref_decomp_vtx :
-  forall {p}, Pdk d 1 p -> p = lin_comb (mapF p vtx_ref) LagPd1_ref.
-Proof.
-intros p Hp; destruct (basis_decomp_ex LagPd1_ref_basis p Hp) as [L ->].
-apply lc_ext_l; intro; rewrite mapF_correct fct_lc_r_eq LagPd1_ref_kron_vtx_r.
-apply eq_sym, lc_r_kron_r.
-Qed.*)
-
 Lemma LagPd1_ref_baryc_lc :
   forall L i, sum L = 1 -> LagPd1_ref i (lin_comb L vtx_ref) = L i.
 Proof. intros; rewrite -baryc_ms_eq// -{2}(LagPd1_ref_barycF_rev L); easy. Qed.
@@ -559,26 +474,4 @@ rewrite Hp3 widenF_S_insertF_max insertF_correct_l// mult_zero_l plus_zero_r//.
 rewrite Hface_ref_equiv (LagPd1_ref_S ord_max_not_0) insertF_correct_l; easy.
 Qed.
 
-(* Unused!
-(**
- #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1621, reverse way, pp. 104-105. *)
-Lemma factor_zero_on_last_Hface_ref_rev :
-  forall {p}, Pdk d k.+1 p ->
-    (exists q, Pdk d k q /\ p = LagPd1_ref ord_max * q) ->
-    forall x_ref, Hface_ref ord_max x_ref -> p x_ref = 0.
-Proof.
-move=> p Hp [q [Hq1 Hq2]] x_ref; rewrite Hface_ref_is_Ker => Hx_ref;
-    rewrite Hq2 fct_mult_eq Hx_ref mult_zero_l; easy.
-Qed.
-
-Lemma factor_zero_on_last_Hface_ref_equiv :
-  forall {p}, Pdk d k.+1 p ->
-    (forall x_ref, Hface_ref ord_max x_ref -> p x_ref = 0) <->
-    (exists q, Pdk d k q /\ p = LagPd1_ref ord_max * q).
-Proof.
-intros; split; [apply factor_zero_on_last_Hface_ref |
-    apply factor_zero_on_last_Hface_ref_rev]; easy.
-Qed.*)
-
 End Pdk_Facts.