Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • mayero/coq-num-analysis
  • hamelin/test-ci-coq-num-analysis
  • arias/coq-num-analysis
3 results
Show changes
......@@ -29,12 +29,12 @@ COPYING file for more details.
- [alt_ones n] is the [n]-family with values [1], [-1], [1]...;
- [alt_ones_shift n] is the [n]-family with values [-1], [1], [-1]...
Let [u : 'K^n].
- [part1F u i0] is the [n+1]-family where the value [1 - sum u] is
- [part1F i0 u] is the [n+1]-family where the value [1 - sum u] is
inserted in [u] at position [i0];
- [part1F_0 u] is [part1F u ord0].
- [part1F0] is an abbreviation for [part1F ord0].
Let [x : K].
- [plusn n x] is the [sum] of [n] items equal to [x];
- [plusn1 n] is [plusn n 1].
- [plusn1] is an abbreviation for [plusn^~ 1].
- [alt_onesT m n] is the [(m,n)]-table with values [1] at location [(i,j)]
when [i+j] is even, and [-1] otherwise.
......@@ -65,9 +65,7 @@ Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Ring_FF_Facts1a.
(** Properties with the second identity element of rings (one). *)
Section Ring_FF_Def.
Context {K : Ring}.
......@@ -77,8 +75,31 @@ Definition alt_ones {n} : 'K^n :=
Definition alt_ones_shift {n} : 'K^n :=
fun i => if Nat.Even_Odd_dec i then - (1 : K) else 1.
Definition alt_onesT {m n} : 'K^{m,n} :=
fun i j => if Nat.Even_Odd_dec (i + j) then 1 else - (1 : K).
Definition part1F {n} (i0 : 'I_n.+1) (u : 'K^n) : 'K^n.+1 :=
insertF i0 (1 - sum u) u.
Definition plusn (n : nat) (x : K) : K := sum (constF n x).
End Ring_FF_Def.
Notation part1F0 := (part1F ord0).
Notation plusn1 := (plusn^~ 1).
Section Ring_FF_Facts1.
Context {K : Ring}.
(** Properties with the second identity element of rings (one). *)
(** Properties of [alt_ones]. *)
Lemma alt_ones_correct_even :
forall {n} (i : 'I_n), Nat.Even i -> alt_ones i = 1.
forall {n} (i : 'I_n), Nat.Even i -> alt_ones i = 1 :> K.
Proof.
intros n i Hi; unfold alt_ones; destruct (Nat.Even_Odd_dec i); simpl; try easy.
exfalso; apply (Nat.Even_Odd_False i); easy.
......@@ -100,14 +121,15 @@ exfalso; apply (Nat.Even_Odd_False i); easy.
Qed.
Lemma alt_ones_shift_correct_odd :
forall {n} (i : 'I_n), Nat.Odd i -> alt_ones_shift i = 1.
forall {n} (i : 'I_n), Nat.Odd i -> alt_ones_shift i = 1 :> K.
Proof.
intros n i Hi; unfold alt_ones_shift;
destruct (Nat.Even_Odd_dec i); simpl; try easy.
exfalso; apply (Nat.Even_Odd_False i); easy.
Qed.
Lemma alt_ones_eq : forall {n}, @alt_ones n = liftF_S (@alt_ones_shift n.+1).
Lemma alt_ones_eq :
forall {n}, @alt_ones K n = liftF_S (@alt_ones_shift K n.+1).
Proof.
intros n; extF i; unfold liftF_S; destruct (Nat.Even_Odd_dec i).
(* *)
......@@ -119,7 +141,7 @@ rewrite lift_S_correct; apply Nat.Even_succ; easy.
Qed.
Lemma alt_ones_shift_eq :
forall {n}, @alt_ones_shift n = liftF_S (@alt_ones n.+1).
forall {n}, @alt_ones_shift K n = liftF_S (@alt_ones K n.+1).
Proof.
intros n; extF i; unfold liftF_S; destruct (Nat.Even_Odd_dec i).
(* *)
......@@ -131,7 +153,7 @@ rewrite lift_S_correct; apply Nat.Even_succ; easy.
Qed.
Lemma alt_ones_shift2 :
forall {n}, @alt_ones n = liftF_S (liftF_S (@alt_ones n.+2)).
forall {n}, @alt_ones K n = liftF_S (liftF_S (@alt_ones K n.+2)).
Proof. intros; rewrite alt_ones_eq alt_ones_shift_eq; easy. Qed.
Lemma ones_not_zero : forall {n}, nonzero_struct K -> (1 : 'K^n.+1) <> 0.
......@@ -145,7 +167,7 @@ apply one_not_zero; easy.
apply Even_0.
Qed.
Lemma sum_alt_ones_even : forall {n}, Nat.Even n -> sum (@alt_ones n) = 0.
Lemma sum_alt_ones_even : forall {n}, Nat.Even n -> sum (@alt_ones K n) = 0.
Proof.
intros n [m Hm]; subst; induction m as [| m Hm]. apply sum_nil.
rewrite -(sum_castF (nat_double_S _)).
......@@ -153,11 +175,11 @@ rewrite 2!sum_ind_l; unfold castF at 1, liftF_S at 1, castF at 1.
rewrite {1}alt_ones_correct_even; try apply Even_0;
rewrite alt_ones_correct_odd; try apply Odd_1.
rewrite plus_assoc plus_opp_r plus_zero_l.
rewrite -(sum_eq (@alt_ones (2 * m)%coq_nat)); try easy.
rewrite -(sum_eq (@alt_ones _ (2 * m)%coq_nat)); try easy.
apply alt_ones_shift2.
Qed.
Lemma sum_alt_ones_odd : forall {n}, Nat.Odd n -> sum (@alt_ones n) = 1.
Lemma sum_alt_ones_odd : forall {n}, Nat.Odd n -> sum (@alt_ones K n) = 1.
Proof.
intros n [m Hm]; subst; induction m as [| m Hm].
rewrite sum_1; apply alt_ones_correct_even, Even_0.
......@@ -166,12 +188,12 @@ rewrite 2!sum_ind_l; unfold castF at 1, liftF_S at 1, castF at 1.
rewrite {1}alt_ones_correct_even; try apply Even_0;
rewrite alt_ones_correct_odd; try apply Odd_1.
rewrite plus_assoc plus_opp_r plus_zero_l.
rewrite -(sum_eq (@alt_ones ((2 * m)%coq_nat.+1))).
rewrite -(sum_eq (@alt_ones _ ((2 * m)%coq_nat.+1))).
rewrite -(sum_castF (addn1_sym _)); easy.
apply alt_ones_shift2.
Qed.
Lemma alt_ones_3_eq : @alt_ones 3 = tripleF 1 (- (1)) 1.
Lemma alt_ones_3_eq : @alt_ones K 3 = tripleF 1 (- (1)) 1.
Proof.
extF i; destruct (ord3_dec i) as [[-> | ->] | ->].
rewrite -> alt_ones_correct_even, tripleF_0; try apply Even_0; easy.
......@@ -185,42 +207,29 @@ Proof. rewrite -alt_ones_3_eq; apply sum_alt_ones_odd, Odd_3. Qed.
Lemma sum_alt_ones_3_invertible : invertible (sum (tripleF 1 (- (1 : K)) 1)).
Proof. rewrite sum_alt_ones_3; apply invertible_one. Qed.
Definition part1F {n} (u : 'K^n) (i0 : 'I_n.+1) : 'K^n.+1 :=
insertF i0 (1 - sum u) u.
(** Properties of [part1F]. *)
Lemma part1F_correct_0 :
forall {n} (u : 'K^n) i0 i, i = i0 -> part1F u i0 i = 1 - sum u.
forall {n} i0 i (u : 'K^n), i = i0 -> part1F i0 u i = 1 - sum u.
Proof. move=>> ->; unfold part1F; rewrite insertF_correct_l; easy. Qed.
Lemma part1F_correct_S :
forall {n} (u : 'K^n) {i0 i} (Hi : i <> i0),
part1F u i0 i = u (insert_ord Hi).
forall {n} {i0 i} (Hi : i <> i0) (u : 'K^n),
part1F i0 u i = u (insert_ord Hi).
Proof. intros; apply insertF_correct_r. Qed.
Lemma part1F_sum : forall {n} (u : 'K^n) i0, sum (part1F u i0) = 1.
Lemma part1F_sum : forall {n} i0 (u : 'K^n), sum (part1F i0 u) = 1.
Proof. intro; apply sum_insertF_baryc. Qed.
Lemma part1F_Rg :
forall {n} (i0 : 'I_n.+1), Rg (part1F^~ i0) = fun u => sum u = 1.
forall {n} (i0 : 'I_n.+1), Rg (part1F i0) = fun u => sum u = (1 : K).
Proof.
intros n i0; apply subset_ext_equiv; split.
intros _ [v _]; apply part1F_sum.
intros u Hu; rewrite image_ex; exists (skipF i0 u); split; [easy |].
unfold part1F; rewrite -Hu (sum_skipF _ i0) minus_plus_r insertF_skipF; easy.
unfold part1F; rewrite -Hu (sum_skipF i0) minus_plus_r insertF_skipF; easy.
Qed.
End Ring_FF_Facts1a.
Notation part1F0 := (part1F^~ ord0).
Section Ring_FF_Facts1b.
(** Properties with the second identity element of rings (one). *)
Context {K : Ring}.
Lemma part1F0_1_eq : forall (a : K), part1F0 (singleF a) = coupleF (1 - a) a.
Proof.
intros; extF i; destruct (ord2_dec i) as [-> | ->].
......@@ -236,7 +245,72 @@ Lemma part1F0_sum_1_invertible :
forall (a : K), invertible (sum (coupleF (1 - a) a)).
Proof. intros; rewrite part1F0_sum_1; apply invertible_one. Qed.
End Ring_FF_Facts1b.
(** Properties of [plusn]. *)
Lemma plusn_0_l : forall x : K, plusn 0 x = 0.
Proof. intros; apply sum_nil. Qed.
Lemma plusn_0_r : forall n, plusn n (0 : K) = 0.
Proof. intros; apply sum_zero. Qed.
Lemma plusn_1_l : forall x : K, plusn 1 x = x.
Proof. intros; apply sum_1. Qed.
Lemma plusn_2_l : forall x : K, plusn 2 x = x + x.
Proof. intros; apply sum_2. Qed.
Lemma plusn_2_1 : plusn 2 (1 : K) = 2.
Proof. rewrite plusn_2_l; easy. Qed.
Lemma plusn1_2 : plusn1 2%nat = 2 :> K.
Proof. apply plusn_2_1. Qed.
Lemma plusn_3_l : forall x : K, plusn 3 x = x + x + x.
Proof. intros; apply sum_3. Qed.
Lemma plusn_ind : forall n (x : K), plusn n.+1 x = x + plusn n x.
Proof. intros; apply sum_ind_l. Qed.
Lemma plusn_plus_l :
forall n1 n2 (x : K), plusn (n1 + n2) x = plusn n1 x + plusn n2 x.
Proof. intros; unfold plusn; rewrite -concatF_constF sum_concatF; easy. Qed.
Lemma plusn_plus_r :
forall n (x y : K), plusn n (x + y) = plusn n x + plusn n y.
Proof.
intros n x y; induction n as [| n Hn].
rewrite !plusn_0_l plus_zero_l; easy.
rewrite !plusn_ind Hn -(plus_assoc _ (plusn _ _)) (plus_assoc (plusn _ _))
(plus_comm (plusn _ _) y) -(plus_assoc y) -(plus_assoc x y); easy.
Qed.
Lemma plusn_assoc_l :
forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n1 (plusn n2 x).
Proof.
intros n1 n2 x; induction n1 as [| n1 Hn1].
rewrite Nat.mul_0_l !plusn_0_l; easy.
replace (n1.+1 * n2)%coq_nat with ((n1 * n2)%coq_nat + n2)%coq_nat by lia.
rewrite plusn_plus_l Hn1 plusn_ind plus_comm; easy.
Qed.
Lemma plusn_assoc_r :
forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n2 (plusn n1 x).
Proof. intros; rewrite -plusn_assoc_l; f_equal; auto with arith. Qed.
Lemma plusn_mult : forall n (x y : K), plusn n (x * y) = plusn n x * y.
Proof. intros; unfold plusn; rewrite -mult_sum_l; easy. Qed.
Lemma plusn_eq : forall n (x : K), plusn n x = (plusn1 n) * x.
Proof. intros n x; rewrite -plusn_mult mult_one_l; easy. Qed.
Lemma plusn_zero_equiv :
forall n, plusn1 n = 0 :> K <-> forall x : K, plusn n x = 0.
Proof.
intros; split; intros Hn; try easy.
intros; rewrite plusn_eq Hn mult_zero_l; easy.
Qed.
End Ring_FF_Facts1.
Section Ring_FF_Facts2.
......@@ -313,94 +387,6 @@ Proof. easy. Qed.
End Ring_FF_Facts2.
Section Ring_FF_Facts3.
Definition plusn {K : Ring} (n : nat) (x : K) : K := sum (constF n x).
Definition plusn1 (K : Ring) (n : nat) : K := plusn n 1.
Context {K : Ring}.
Lemma plusn1_eq : forall n, plusn1 K n = plusn n 1.
Proof. easy. Qed.
Lemma plusn_0_l : forall x : K, plusn 0 x = 0.
Proof. intros; apply sum_nil. Qed.
Lemma plusn_0_r : forall n, plusn n (0 : K) = 0.
Proof. intros; apply sum_zero. Qed.
Lemma plusn_1_l : forall x : K, plusn 1 x = x.
Proof. intros; apply sum_1. Qed.
Lemma plusn_2_l : forall x : K, plusn 2 x = x + x.
Proof. intros; apply sum_2. Qed.
Lemma plusn_2_1 : plusn 2 (1 : K) = 2.
Proof. rewrite plusn_2_l; easy. Qed.
Lemma plusn1_2 : plusn1 K 2 = 2.
Proof. rewrite plusn1_eq plusn_2_1; easy. Qed.
Lemma plusn_3_l : forall x : K, plusn 3 x = x + x + x.
Proof. intros; apply sum_3. Qed.
Lemma plusn_ind : forall n (x : K), plusn n.+1 x = x + plusn n x.
Proof. intros; apply sum_ind_l. Qed.
Lemma plusn_plus_l :
forall n1 n2 (x : K), plusn (n1 + n2) x = plusn n1 x + plusn n2 x.
Proof. intros; unfold plusn; rewrite -concatF_constF sum_concatF; easy. Qed.
Lemma plusn_plus_r :
forall n (x y : K), plusn n (x + y) = plusn n x + plusn n y.
Proof.
intros n x y; induction n as [| n Hn].
rewrite !plusn_0_l plus_zero_l; easy.
rewrite !plusn_ind Hn -(plus_assoc _ (plusn _ _)) (plus_assoc (plusn _ _))
(plus_comm (plusn _ _) y) -(plus_assoc y) -(plus_assoc x y); easy.
Qed.
Lemma plusn_assoc_l :
forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n1 (plusn n2 x).
Proof.
intros n1 n2 x; induction n1 as [| n1 Hn1].
rewrite Nat.mul_0_l !plusn_0_l; easy.
replace (n1.+1 * n2)%coq_nat with ((n1 * n2)%coq_nat + n2)%coq_nat by lia.
rewrite plusn_plus_l Hn1 plusn_ind plus_comm; easy.
Qed.
Lemma plusn_assoc_r :
forall n1 n2 (x : K), plusn (n1 * n2)%coq_nat x = plusn n2 (plusn n1 x).
Proof. intros; rewrite -plusn_assoc_l; f_equal; auto with arith. Qed.
Lemma plusn_mult : forall n (x y : K), plusn n (x * y) = plusn n x * y.
Proof. intros; unfold plusn; rewrite -mult_sum_l; easy. Qed.
Lemma plusn_eq : forall n (x : K), plusn n x = (plusn1 K n) * x.
Proof. intros n x; rewrite -plusn_mult mult_one_l; easy. Qed.
Lemma plusn_zero_equiv :
forall n, plusn1 K n = 0 <-> forall x : K, plusn n x = 0.
Proof.
intros; split; intros Hn; unfold plusn1; try easy.
intros; rewrite plusn_eq Hn mult_zero_l; easy.
Qed.
End Ring_FF_Facts3.
Section Ring_FT_Facts.
(** Properties with the second identity element of rings (one). *)
Context {K : Ring}.
Definition alt_onesT {m n} : 'K^{m,n} :=
fun i j => if Nat.Even_Odd_dec (i + j) then 1 else - (1 : K).
End Ring_FT_Facts.
Section Ring_FF_R_Facts.
Lemma ones_not_zero_R : forall {n}, (1 : 'R_Ring^n.+1) <> 0.
......
......@@ -58,11 +58,11 @@ Section Ring_charac.
Lemma ring_charac_EX :
forall K : Ring,
{ n | n <> 0%nat /\ plusn1 K n = 0 /\
forall p, p <> 0%nat -> (p < n)%coq_nat -> plusn1 K p <> 0 } +
{ forall n, n <> 0%nat -> plusn1 K n <> 0 }.
{ n | n <> 0%nat /\ plusn1 n = 0 :> K /\
forall p, p <> 0%nat -> (p < n)%coq_nat -> plusn1 p <> 0 :> K } +
{ forall n, n <> 0%nat -> plusn1 n <> 0 :> K }.
Proof.
intros; pose (P n := n <> 0%nat /\ plusn1 K n = 0).
intros; pose (P n := n <> 0%nat /\ plusn1 n = 0 :> K).
destruct (LPO P (fun=> classic _)) as [[N HN] | H]; [left | right].
(* *)
apply ex_EX; destruct (dec_inh_nat_subset_has_unique_least_element P)
......@@ -87,7 +87,7 @@ Definition is_field_not_charac_2 (K : Ring) : Prop :=
Context {K : Ring}.
Lemma ring_charac_0 :
ring_charac K = 0%nat <-> forall n, n <> 0%nat -> plusn1 K n <> 0.
ring_charac K = 0%nat <-> forall n, n <> 0%nat -> plusn1 n <> 0 :> K.
Proof.
unfold ring_charac;
destruct ring_charac_EX as [[n [Hn0 [Hn1 Hn2]]] | ]; simpl; try easy.
......@@ -98,7 +98,7 @@ Qed.
Lemma ring_charac_S :
forall n, ring_charac K = n.+1 <->
plusn n.+1 (1 : K) = 0 /\
(forall p, p <> 0%nat -> (p < n.+1)%coq_nat -> plusn1 K p <> 0).
(forall p, p <> 0%nat -> (p < n.+1)%coq_nat -> plusn1 p <> 0 :> K).
Proof.
intros n; unfold ring_charac;
destruct ring_charac_EX as [[m [Hm0 [Hm1 Hm2]]] | H];
......@@ -133,13 +133,12 @@ intros [Hn1 Hn2] k; split.
(* .. *)
move=> /plusn_zero_equiv Hk0.
generalize (Nat.div_mod_eq k n.+1); intros Hk1.
rewrite Hk1 plusn1_eq plusn_plus_l plusn_assoc_r
Hn1 plusn_0_r plus_zero_l in Hk0.
rewrite Hk1 plusn_plus_l plusn_assoc_r Hn1 plusn_0_r plus_zero_l in Hk0.
apply NNPP_equiv; contradict Hk0; apply Hn2; try easy.
apply Nat.mod_upper_bound; easy.
(* .. *)
move=> /Nat.Div0.div_exact Hk; apply plusn_zero_equiv; rewrite Hk; try lia.
unfold plusn1; rewrite plusn_assoc_r Hn1 plusn_0_r; easy.
rewrite plusn_assoc_r Hn1 plusn_0_r; easy.
(* . *)
intros Hn; split.
apply plusn_zero_equiv, Hn, Nat.Div0.mod_same; easy.
......@@ -175,11 +174,11 @@ assert (Hk1 : k mod 2 = 0%nat \/ k mod 2 = 1%nat)
by now apply lt_2, Nat.mod_upper_bound.
destruct Hk1 as [Hk1 | Hk1]; try easy; contradict Hk.
generalize (Nat.div_mod_eq k 2); intros Hk2; rewrite Hk2.
rewrite plusn1_eq plusn_plus_l plusn_assoc_r HK1 plusn_0_r plus_zero_l Hk1 plusn_1_l.
rewrite plusn_plus_l plusn_assoc_r HK1 plusn_0_r plus_zero_l Hk1 plusn_1_l.
apply one_not_zero; easy.
(* . *)
apply Nat.Div0.div_exact in Hk; try easy; rewrite Hk.
rewrite plusn1_eq plusn_assoc_r HK1 plusn_0_r; easy.
rewrite plusn_assoc_r HK1 plusn_0_r; easy.
Qed.
Lemma ring_not_charac_2 :
......@@ -189,13 +188,12 @@ rewrite -iff_not_r_equiv not_or_not_r_equiv -nonzero_not_zero_struct_equiv.
apply ring_charac_2.
Qed.
Lemma invertible_plusn :
Lemma invertible_plusn_not_ring_charac :
forall n, nonzero_struct K -> n <> 0%nat ->
invertible (plusn1 K n) -> ring_charac K <> n.
invertible (plusn1 n : K) -> ring_charac K <> n.
Proof.
intros n HK0 Hn HK1; contradict Hn; destruct n; try easy; contradict HK1.
apply ring_charac_S in Hn; rewrite plusn1_eq (proj1 Hn).
apply noninvertible_zero; easy.
apply ring_charac_S in Hn; rewrite (proj1 Hn); apply noninvertible_zero; easy.
Qed.
End Ring_charac.
......@@ -206,10 +204,16 @@ Section Ring_R_Facts.
Lemma ring_charac_0_R : ring_charac R_Ring = 0%nat.
Proof.
apply ring_charac_0; intro; rewrite -contra_equiv.
rewrite plusn1_eq; unfold plusn; rewrite sum_constF_R Rmult_1_r.
unfold plusn; rewrite sum_constF_R Rmult_1_r.
intros Hn; apply INR_eq; rewrite INR_0; easy.
Qed.
Lemma invertible_plusn1_R : forall n, n <> 0 -> invertible (plusn1 n : R).
Proof.
intros; unfold plusn; rewrite sum_ones_R;
apply invertible_equiv_R, not_0_INR; easy.
Qed.
Lemma is_field_not_charac_2_R : is_field_not_charac_2 R_Ring.
Proof. split; [apply is_field_R | rewrite ring_charac_0_R; easy]. Qed.
......
......@@ -564,12 +564,12 @@ Lemma invertible_sum_equiv :
Proof. intros; rewrite sum_filter_n0F; easy. Qed.
Lemma sum_insertF_baryc :
forall {n} (u : 'K^n) i0, sum (insertF i0 (1 - sum u) u) = 1.
forall {n} i0 (u : 'K^n), sum (insertF i0 (1 - sum u) u) = 1.
Proof. intros; rewrite sum_insertF plus_minus_l; easy. Qed.
Lemma invertible_sum_squeezeF :
forall {n} (u : 'K^n.+1) {i0 i1},
i1 <> i0 -> invertible (sum u) -> invertible (sum (squeezeF i0 i1 u)).
forall {n} {i0 i1} (H : i1 <> i0) (u : 'K^n.+1),
invertible (sum u) -> invertible (sum (squeezeF i0 i1 u)).
Proof. intros; rewrite sum_squeezeF; easy. Qed.
Lemma is_integral_contra :
......
......@@ -159,7 +159,7 @@ Lemma kron_sum_l :
Proof.
intros [| n] p j.
move=> /Nat.le_0_r H; subst; destruct j; easy.
move=> /leP H; rewrite (sum_one _ (widen_ord H j));
move=> /leP H; rewrite (sum_one (widen_ord H j));
[apply kron_is_1; easy | apply kron_skipF_diag_r].
Qed.
......@@ -169,7 +169,7 @@ Lemma kron_sum_r :
Proof.
intros [| n] p i.
move=> /Nat.le_0_r H; subst; destruct i; easy.
move=> /leP H; rewrite (sum_one _ (widen_ord H i));
move=> /leP H; rewrite (sum_one (widen_ord H i));
[apply kron_is_1 | rewrite (kron_skipF_diag_l (widen_ord _ _))]; easy.
Qed.
......
......@@ -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.
......
......@@ -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.
......@@ -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>#
......
......@@ -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).
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......