Skip to content
Snippets Groups Projects
Commit e7aebdb7 authored by Houda Mouhcine's avatar Houda Mouhcine
Browse files

Change in indices.

parent c78ee4be
No related branches found
No related tags found
No related merge requests found
Pipeline #8616 waiting for manual action
......@@ -247,18 +247,18 @@ Qed.
Lemma vtx_cur_invalF : forall vtx_cur, (0 < k)%coq_nat ->
invalF vtx_cur (node_cur vtx_cur).
Proof.
intros vtx_cur Hk i.
destruct (ord_eq_dec i ord0) as [Hi | Hi].
(* i = ord0 *)
rewrite Hi.
intros vtx_cur Hk ipk. unfold inF.
destruct (ord_eq_dec ipk ord0) as [Hipk | Hipk].
(* ipk = ord0 *)
rewrite Hipk.
exists ord0.
unfold node_cur.
rewrite (Adk_0 d k) !scal_zero_r !lc_zero_l
minus_zero_r scal_one plus_zero_r; easy.
(* i <> ord0 *)
exists (Adk_inv d k (itemF d k (lower_S Hi))).
(* ipk <> ord0 *)
exists (Adk_inv d k (itemF d k (lower_S Hipk))).
unfold node_cur.
rewrite Adk_kron !(lc_eq_l _ (kronecker (lower_S Hi))).
rewrite Adk_kron !(lc_eq_l _ (kronecker (lower_S Hipk))).
rewrite lc_ones_r sum_kronecker_r minus_eq_zero
scal_zero_l plus_zero_l lc_kronecker_l_in_r
liftF_lower_S; easy.
......@@ -319,27 +319,27 @@ Variable d : nat.
Lemma vtx_node_Pd1_cur : forall (vtx_cur : 'R^{d.+1,d}) (ipk :'I_d.+1),
vtx_cur ipk = node_cur d 1 vtx_cur (cast_ord (eq_sym (pbinomS_1_r d)) ipk).
Proof.
intros vtx_cur i; unfold node_cur.
intros vtx_cur ipk; unfold node_cur.
rewrite Rinv_1 scal_one.
destruct (ord_eq_dec i ord0) as [Hi | Hi].
(* i = ord0 *)
destruct (ord_eq_dec ipk ord0) as [Hi | Hi].
(* ipk = ord0 *)
rewrite Hi.
replace (mapF INR (Adk d 1 (cast_ord (eq_sym (pbinomS_1_r d)) ord0))) with
(mapF INR (Adk d 1 ord0)).
rewrite (Adk_0 d 1) !lc_zero_l minus_zero_r
scal_one plus_zero_r; auto.
f_equal; f_equal; apply ord_inj; easy.
(* i <> ord0 *)
(* ipk <> ord0 *)
rewrite Ad1_eq.
unfold castF.
rewrite concatF_correct_r; simpl.
apply ord_n0_nlt_equiv; easy.
intros H.
rewrite mapF_itemF_0// itemF_kronecker_eq; auto; simpl.
replace (fun j : 'I_d => 1 * kronecker (i - 1) j) with
(fun j : 'I_d => kronecker (i - 1) j).
replace (fun j : 'I_d => 1 * kronecker (ipk - 1) j) with
(fun j : 'I_d => kronecker (ipk - 1) j).
rewrite lc_ones_r.
replace (sum (fun j : 'I_d => kronecker (i - 1) j)) with 1.
replace (sum (fun j : 'I_d => kronecker (ipk - 1) j)) with 1.
rewrite minus_eq_zero scal_zero_l plus_zero_l.
apply eq_sym.
rewrite (lc_kronecker_l_in_r (lower_S Hi))
......
......@@ -319,8 +319,10 @@ Variable d : nat.
Lemma Pd1_lin_span_LagPd1_ref : Pdk d 1 = lin_span (LagPd1_ref d).
Proof.
apply lin_span_ext; intro ipk.
unfold Pdk.
apply lin_span_ext.
(* <= *)
intro ipk.
destruct (ord_eq_dec ipk ord0) as [Hipk | Hipk].
(* ipk = ord0 *)
apply lin_span_ex.
......@@ -359,7 +361,8 @@ apply cast_ordS_n0; easy.
intros H1; apply fun_ext; intros x.
f_equal; f_equal; easy.
(* => *)
destruct (ord_eq_dec ipk ord0) as [Hipk | Hipk].
intros j.
destruct (ord_eq_dec j ord0) as [Hj | Hj].
apply lin_span_ex.
(* ipk = ord0 *)
pose (L := concatF (singleF 1) (opp (@ones _ d))).
......@@ -398,8 +401,8 @@ apply ord_inj; simpl.
rewrite bump_r; auto with arith.
f_equal; apply ord_inj; easy.
(* ipk <> ord0 *)
replace (LagPd1_ref d ipk) with
(BasisPdk d 1 (cast_ord (eq_sym (pbinomS_1_r d)) ipk)).
replace (LagPd1_ref d j) with
(BasisPdk d 1 (cast_ord (eq_sym (pbinomS_1_r d)) j)).
apply lin_span_inclF_diag.
rewrite BasisPd1_neq0; simpl.
apply cast_ordS_n0; easy.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment