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. ...@@ -29,12 +29,12 @@ COPYING file for more details.
- [alt_ones n] is the [n]-family with values [1], [-1], [1]...; - [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]... - [alt_ones_shift n] is the [n]-family with values [-1], [1], [-1]...
Let [u : 'K^n]. 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]; inserted in [u] at position [i0];
- [part1F_0 u] is [part1F u ord0]. - [part1F0] is an abbreviation for [part1F ord0].
Let [x : K]. Let [x : K].
- [plusn n x] is the [sum] of [n] items equal to [x]; - [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)] - [alt_onesT m n] is the [(m,n)]-table with values [1] at location [(i,j)]
when [i+j] is even, and [-1] otherwise. when [i+j] is even, and [-1] otherwise.
...@@ -65,9 +65,7 @@ Local Open Scope Group_scope. ...@@ -65,9 +65,7 @@ Local Open Scope Group_scope.
Local Open Scope Ring_scope. Local Open Scope Ring_scope.
Section Ring_FF_Facts1a. Section Ring_FF_Def.
(** Properties with the second identity element of rings (one). *)
Context {K : Ring}. Context {K : Ring}.
...@@ -77,8 +75,31 @@ Definition alt_ones {n} : 'K^n := ...@@ -77,8 +75,31 @@ Definition alt_ones {n} : 'K^n :=
Definition alt_ones_shift {n} : 'K^n := Definition alt_ones_shift {n} : 'K^n :=
fun i => if Nat.Even_Odd_dec i then - (1 : K) else 1. 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 : 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. Proof.
intros n i Hi; unfold alt_ones; destruct (Nat.Even_Odd_dec i); simpl; try easy. intros n i Hi; unfold alt_ones; destruct (Nat.Even_Odd_dec i); simpl; try easy.
exfalso; apply (Nat.Even_Odd_False i); easy. exfalso; apply (Nat.Even_Odd_False i); easy.
...@@ -100,14 +121,15 @@ exfalso; apply (Nat.Even_Odd_False i); easy. ...@@ -100,14 +121,15 @@ exfalso; apply (Nat.Even_Odd_False i); easy.
Qed. Qed.
Lemma alt_ones_shift_correct_odd : 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. Proof.
intros n i Hi; unfold alt_ones_shift; intros n i Hi; unfold alt_ones_shift;
destruct (Nat.Even_Odd_dec i); simpl; try easy. destruct (Nat.Even_Odd_dec i); simpl; try easy.
exfalso; apply (Nat.Even_Odd_False i); easy. exfalso; apply (Nat.Even_Odd_False i); easy.
Qed. 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. Proof.
intros n; extF i; unfold liftF_S; destruct (Nat.Even_Odd_dec i). 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. ...@@ -119,7 +141,7 @@ rewrite lift_S_correct; apply Nat.Even_succ; easy.
Qed. Qed.
Lemma alt_ones_shift_eq : 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. Proof.
intros n; extF i; unfold liftF_S; destruct (Nat.Even_Odd_dec i). 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. ...@@ -131,7 +153,7 @@ rewrite lift_S_correct; apply Nat.Even_succ; easy.
Qed. Qed.
Lemma alt_ones_shift2 : 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. 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. Lemma ones_not_zero : forall {n}, nonzero_struct K -> (1 : 'K^n.+1) <> 0.
...@@ -145,7 +167,7 @@ apply one_not_zero; easy. ...@@ -145,7 +167,7 @@ apply one_not_zero; easy.
apply Even_0. apply Even_0.
Qed. 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. Proof.
intros n [m Hm]; subst; induction m as [| m Hm]. apply sum_nil. intros n [m Hm]; subst; induction m as [| m Hm]. apply sum_nil.
rewrite -(sum_castF (nat_double_S _)). 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. ...@@ -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 {1}alt_ones_correct_even; try apply Even_0;
rewrite alt_ones_correct_odd; try apply Odd_1. rewrite alt_ones_correct_odd; try apply Odd_1.
rewrite plus_assoc plus_opp_r plus_zero_l. 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. apply alt_ones_shift2.
Qed. 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. Proof.
intros n [m Hm]; subst; induction m as [| m Hm]. intros n [m Hm]; subst; induction m as [| m Hm].
rewrite sum_1; apply alt_ones_correct_even, Even_0. 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. ...@@ -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 {1}alt_ones_correct_even; try apply Even_0;
rewrite alt_ones_correct_odd; try apply Odd_1. rewrite alt_ones_correct_odd; try apply Odd_1.
rewrite plus_assoc plus_opp_r plus_zero_l. 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. rewrite -(sum_castF (addn1_sym _)); easy.
apply alt_ones_shift2. apply alt_ones_shift2.
Qed. 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. Proof.
extF i; destruct (ord3_dec i) as [[-> | ->] | ->]. extF i; destruct (ord3_dec i) as [[-> | ->] | ->].
rewrite -> alt_ones_correct_even, tripleF_0; try apply Even_0; easy. 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. ...@@ -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)). Lemma sum_alt_ones_3_invertible : invertible (sum (tripleF 1 (- (1 : K)) 1)).
Proof. rewrite sum_alt_ones_3; apply invertible_one. Qed. Proof. rewrite sum_alt_ones_3; apply invertible_one. Qed.
Definition part1F {n} (u : 'K^n) (i0 : 'I_n.+1) : 'K^n.+1 := (** Properties of [part1F]. *)
insertF i0 (1 - sum u) u.
Lemma part1F_correct_0 : 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. Proof. move=>> ->; unfold part1F; rewrite insertF_correct_l; easy. Qed.
Lemma part1F_correct_S : Lemma part1F_correct_S :
forall {n} (u : 'K^n) {i0 i} (Hi : i <> i0), forall {n} {i0 i} (Hi : i <> i0) (u : 'K^n),
part1F u i0 i = u (insert_ord Hi). part1F i0 u i = u (insert_ord Hi).
Proof. intros; apply insertF_correct_r. Qed. 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. Proof. intro; apply sum_insertF_baryc. Qed.
Lemma part1F_Rg : 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. Proof.
intros n i0; apply subset_ext_equiv; split. intros n i0; apply subset_ext_equiv; split.
intros _ [v _]; apply part1F_sum. intros _ [v _]; apply part1F_sum.
intros u Hu; rewrite image_ex; exists (skipF i0 u); split; [easy |]. 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. 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. Lemma part1F0_1_eq : forall (a : K), part1F0 (singleF a) = coupleF (1 - a) a.
Proof. Proof.
intros; extF i; destruct (ord2_dec i) as [-> | ->]. intros; extF i; destruct (ord2_dec i) as [-> | ->].
...@@ -236,7 +245,72 @@ Lemma part1F0_sum_1_invertible : ...@@ -236,7 +245,72 @@ Lemma part1F0_sum_1_invertible :
forall (a : K), invertible (sum (coupleF (1 - a) a)). forall (a : K), invertible (sum (coupleF (1 - a) a)).
Proof. intros; rewrite part1F0_sum_1; apply invertible_one. Qed. 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. Section Ring_FF_Facts2.
...@@ -313,94 +387,6 @@ Proof. easy. Qed. ...@@ -313,94 +387,6 @@ Proof. easy. Qed.
End Ring_FF_Facts2. 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. Section Ring_FF_R_Facts.
Lemma ones_not_zero_R : forall {n}, (1 : 'R_Ring^n.+1) <> 0. Lemma ones_not_zero_R : forall {n}, (1 : 'R_Ring^n.+1) <> 0.
......
...@@ -58,11 +58,11 @@ Section Ring_charac. ...@@ -58,11 +58,11 @@ Section Ring_charac.
Lemma ring_charac_EX : Lemma ring_charac_EX :
forall K : Ring, forall K : Ring,
{ 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 K p <> 0 } + forall p, p <> 0%nat -> (p < n)%coq_nat -> plusn1 p <> 0 :> K } +
{ forall n, n <> 0%nat -> plusn1 K n <> 0 }. { forall n, n <> 0%nat -> plusn1 n <> 0 :> K }.
Proof. 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]. destruct (LPO P (fun=> classic _)) as [[N HN] | H]; [left | right].
(* *) (* *)
apply ex_EX; destruct (dec_inh_nat_subset_has_unique_least_element P) 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 := ...@@ -87,7 +87,7 @@ Definition is_field_not_charac_2 (K : Ring) : Prop :=
Context {K : Ring}. Context {K : Ring}.
Lemma ring_charac_0 : 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. Proof.
unfold ring_charac; unfold ring_charac;
destruct ring_charac_EX as [[n [Hn0 [Hn1 Hn2]]] | ]; simpl; try easy. destruct ring_charac_EX as [[n [Hn0 [Hn1 Hn2]]] | ]; simpl; try easy.
...@@ -98,7 +98,7 @@ Qed. ...@@ -98,7 +98,7 @@ Qed.
Lemma ring_charac_S : Lemma ring_charac_S :
forall n, ring_charac K = n.+1 <-> forall n, ring_charac K = n.+1 <->
plusn n.+1 (1 : K) = 0 /\ 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. Proof.
intros n; unfold ring_charac; intros n; unfold ring_charac;
destruct ring_charac_EX as [[m [Hm0 [Hm1 Hm2]]] | H]; destruct ring_charac_EX as [[m [Hm0 [Hm1 Hm2]]] | H];
...@@ -133,13 +133,12 @@ intros [Hn1 Hn2] k; split. ...@@ -133,13 +133,12 @@ intros [Hn1 Hn2] k; split.
(* .. *) (* .. *)
move=> /plusn_zero_equiv Hk0. move=> /plusn_zero_equiv Hk0.
generalize (Nat.div_mod_eq k n.+1); intros Hk1. generalize (Nat.div_mod_eq k n.+1); intros Hk1.
rewrite Hk1 plusn1_eq plusn_plus_l plusn_assoc_r rewrite Hk1 plusn_plus_l plusn_assoc_r Hn1 plusn_0_r plus_zero_l in Hk0.
Hn1 plusn_0_r plus_zero_l in Hk0.
apply NNPP_equiv; contradict Hk0; apply Hn2; try easy. apply NNPP_equiv; contradict Hk0; apply Hn2; try easy.
apply Nat.mod_upper_bound; easy. apply Nat.mod_upper_bound; easy.
(* .. *) (* .. *)
move=> /Nat.Div0.div_exact Hk; apply plusn_zero_equiv; rewrite Hk; try lia. 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. intros Hn; split.
apply plusn_zero_equiv, Hn, Nat.Div0.mod_same; easy. 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) ...@@ -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. by now apply lt_2, Nat.mod_upper_bound.
destruct Hk1 as [Hk1 | Hk1]; try easy; contradict Hk. destruct Hk1 as [Hk1 | Hk1]; try easy; contradict Hk.
generalize (Nat.div_mod_eq k 2); intros Hk2; rewrite Hk2. 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 one_not_zero; easy.
(* . *) (* . *)
apply Nat.Div0.div_exact in Hk; try easy; rewrite Hk. 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. Qed.
Lemma ring_not_charac_2 : Lemma ring_not_charac_2 :
...@@ -189,13 +188,12 @@ rewrite -iff_not_r_equiv not_or_not_r_equiv -nonzero_not_zero_struct_equiv. ...@@ -189,13 +188,12 @@ rewrite -iff_not_r_equiv not_or_not_r_equiv -nonzero_not_zero_struct_equiv.
apply ring_charac_2. apply ring_charac_2.
Qed. Qed.
Lemma invertible_plusn : Lemma invertible_plusn_not_ring_charac :
forall n, nonzero_struct K -> n <> 0%nat -> 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. Proof.
intros n HK0 Hn HK1; contradict Hn; destruct n; try easy; contradict HK1. 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 ring_charac_S in Hn; rewrite (proj1 Hn); apply noninvertible_zero; easy.
apply noninvertible_zero; easy.
Qed. Qed.
End Ring_charac. End Ring_charac.
...@@ -206,10 +204,16 @@ Section Ring_R_Facts. ...@@ -206,10 +204,16 @@ Section Ring_R_Facts.
Lemma ring_charac_0_R : ring_charac R_Ring = 0%nat. Lemma ring_charac_0_R : ring_charac R_Ring = 0%nat.
Proof. Proof.
apply ring_charac_0; intro; rewrite -contra_equiv. 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. intros Hn; apply INR_eq; rewrite INR_0; easy.
Qed. 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. 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. Proof. split; [apply is_field_R | rewrite ring_charac_0_R; easy]. Qed.
......
...@@ -564,12 +564,12 @@ Lemma invertible_sum_equiv : ...@@ -564,12 +564,12 @@ Lemma invertible_sum_equiv :
Proof. intros; rewrite sum_filter_n0F; easy. Qed. Proof. intros; rewrite sum_filter_n0F; easy. Qed.
Lemma sum_insertF_baryc : 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. Proof. intros; rewrite sum_insertF plus_minus_l; easy. Qed.
Lemma invertible_sum_squeezeF : Lemma invertible_sum_squeezeF :
forall {n} (u : 'K^n.+1) {i0 i1}, forall {n} {i0 i1} (H : i1 <> i0) (u : 'K^n.+1),
i1 <> i0 -> invertible (sum u) -> invertible (sum (squeezeF i0 i1 u)). invertible (sum u) -> invertible (sum (squeezeF i0 i1 u)).
Proof. intros; rewrite sum_squeezeF; easy. Qed. Proof. intros; rewrite sum_squeezeF; easy. Qed.
Lemma is_integral_contra : Lemma is_integral_contra :
......
...@@ -159,7 +159,7 @@ Lemma kron_sum_l : ...@@ -159,7 +159,7 @@ Lemma kron_sum_l :
Proof. Proof.
intros [| n] p j. intros [| n] p j.
move=> /Nat.le_0_r H; subst; destruct j; easy. 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]. [apply kron_is_1; easy | apply kron_skipF_diag_r].
Qed. Qed.
...@@ -169,7 +169,7 @@ Lemma kron_sum_r : ...@@ -169,7 +169,7 @@ Lemma kron_sum_r :
Proof. Proof.
intros [| n] p i. intros [| n] p i.
move=> /Nat.le_0_r H; subst; destruct i; easy. 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. [apply kron_is_1 | rewrite (kron_skipF_diag_l (widen_ord _ _))]; easy.
Qed. Qed.
......
...@@ -322,9 +322,8 @@ Lemma Sigma_LagPd0_eq_from_ref : ...@@ -322,9 +322,8 @@ Lemma Sigma_LagPd0_eq_from_ref :
Sigma_LagPd0 vtx id0 p = Sigma_LagPd0 vtx id0 p =
Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)). Sigma_LagPd0 vtx_ref id0 (p \o (T_geom vtx)).
Proof. Proof.
intros; unfold Sigma_LagPd0, node_d0; rewrite comp_correct T_geom_am. intros; unfold Sigma_LagPd0, node_d0 at 1;
do 2 apply f_equal; extF; apply eq_sym, T_geom_vtx. rewrite comp_correct node_ref_d0_node; easy.
rewrite sum_ones_R; apply invertible_equiv_R, R_compl.INR_n0, S_pos.
Qed. Qed.
(** (**
...@@ -337,7 +336,7 @@ Lemma Sigma_LagPSdSk_eq_from_ref : ...@@ -337,7 +336,7 @@ Lemma Sigma_LagPSdSk_eq_from_ref :
Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)). Sigma_LagPSdSk k vtx_ref i (p \o (T_geom vtx)).
Proof. Proof.
intros; unfold Sigma_LagPSdSk. intros; unfold Sigma_LagPSdSk.
rewrite comp_correct -node_ref_node T_geom_node; easy. rewrite comp_correct -node_ref_node; easy.
Qed. Qed.
Variable d k : nat. Variable d k : nat.
......
...@@ -42,14 +42,14 @@ Local Open Scope Group_scope. ...@@ -42,14 +42,14 @@ Local Open Scope Group_scope.
Local Open Scope Ring_scope. Local Open Scope Ring_scope.
Section Node_Facts. Section Nodes_Facts1.
Context {d k : nat}. Context {d k : nat}.
(** (**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Def 1588, Eq (9.80), p. 97. *) Lem 1604, p. 101. *)
Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := isobarycenter_ms vtx. Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := T_geom vtx node_ref_d0.
(** (**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
...@@ -57,6 +57,21 @@ Definition node_d0 (vtx : 'R^{d.+1,d}) : 'R^d := isobarycenter_ms vtx. ...@@ -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 := Definition node (vtx : 'R^{d.+1,d}) (idk : 'I_(pbinom d k).+1) : 'R^d :=
T_geom vtx (node_ref idk). 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># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1599, p. 100. *) Lem 1599, p. 100. *)
...@@ -95,14 +110,10 @@ intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy]. ...@@ -95,14 +110,10 @@ intros; unfold Hface, node; rewrite Im_equiv; [| apply T_geom_inj; easy].
apply node_ref_Hface_ref_S; easy. apply node_ref_Hface_ref_S; easy.
Qed. Qed.
Lemma T_geom_node : End Nodes_Facts1.
forall (idk : 'I_(pbinom d k).+1), T_geom vtx (node_ref idk) = node vtx idk.
Proof. easy. Qed.
End Node_Facts.
Section Nodes_Facts3. Section Nodes_Facts2.
(** We need a dimension which is structurally nonzero. (** We need a dimension which is structurally nonzero.
We take d = d1.+1 with d1 : nat. *) We take d = d1.+1 with d1 : nat. *)
...@@ -134,7 +145,7 @@ Proof. ...@@ -134,7 +145,7 @@ Proof.
intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_S_node_ref//. intros; unfold T_geom_Hface; rewrite comp_correct inj_Hface_ref_S_node_ref//.
Qed. Qed.
End Nodes_Facts3. End Nodes_Facts2.
Section Nodes_d1. Section Nodes_d1.
...@@ -210,7 +221,7 @@ Qed. ...@@ -210,7 +221,7 @@ Qed.
End Sub_vertices_Facts1. End Sub_vertices_Facts1.
Section Sub_node_Def. Section Sub_nodes_Def.
Context {d : nat}. Context {d : nat}.
Variable k : nat. Variable k : nat.
...@@ -224,18 +235,16 @@ Definition sub_node : 'I_(pbinom d k.-1).+1 -> 'R^d := node (sub_vtx k vtx). ...@@ -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. Lemma sub_nodeF : sub_node = mapF (T_geom (sub_vtx k vtx)) node_ref.
Proof. easy. Qed. 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}. Context {d k : nat}.
Hypothesis Hk : (1 < k)%coq_nat. Hypothesis Hk : (1 < k)%coq_nat.
Lemma sub_node_ref : sub_node k (@vtx_ref d) = node (sub_vtx_ref k). Lemma sub_node_ref : sub_node k (@vtx_ref d) = node (sub_vtx_ref k).
Proof. Proof. rewrite sub_vtx_refF; easy. Qed.
unfold sub_node; f_equal; extF i; unfold sub_vtx; rewrite T_geom_ref; easy.
Qed.
(** (**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<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; ...@@ -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. rewrite mult_one_r; do 2 f_equal; apply Adk_previous_layer; easy.
Qed. Qed.
End Sub_node_ref_Facts1. End Sub_nodes_ref_Facts1.
Section Sub_node_Facts1. Section Sub_nodes_Facts1.
Context {d k : nat}. Context {d k : nat}.
Hypothesis Hk : (1 < k)%coq_nat. Hypothesis Hk : (1 < k)%coq_nat.
...@@ -273,13 +282,13 @@ Lemma sub_node_eq : ...@@ -273,13 +282,13 @@ Lemma sub_node_eq :
sub_node k vtx = widenF (pbinomS_monot_pred d k) (node vtx). sub_node k vtx = widenF (pbinomS_monot_pred d k) (node vtx).
Proof. Proof.
rewrite -T_geom_sub_nodeF sub_node_ref_eq// -widenF_mapF. 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. Qed.
End Sub_node_Facts1. End Sub_nodes_Facts1.
Section Sub_node_Facts2. Section Sub_nodes_Facts2.
Context {d : nat}. Context {d : nat}.
Context {vtx : 'R^{d.+1,d}}. Context {vtx : 'R^{d.+1,d}}.
...@@ -297,4 +306,4 @@ rewrite Adk_last_layer;[| easy | apply S_pos]. ...@@ -297,4 +306,4 @@ rewrite Adk_last_layer;[| easy | apply S_pos].
rewrite Nat.nle_gt; simpl; apply /ltP; easy. rewrite Nat.nle_gt; simpl; apply /ltP; easy.
Qed. Qed.
End Sub_node_Facts2. End Sub_nodes_Facts2.
...@@ -41,20 +41,31 @@ Local Open Scope Group_scope. ...@@ -41,20 +41,31 @@ Local Open Scope Group_scope.
Local Open Scope Ring_scope. Local Open Scope Ring_scope.
Section Node_ref_Facts1. Section Nodes_ref_Facts1.
Context {d k : nat}. 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># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1601, Eq (9.94), p. 101.#<BR># 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. 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 := Definition node_ref (idk : 'I_(pbinom d k).+1) : 'R^d :=
fun i => INR (Adk d k idk i) / INR k. 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 : Lemma node_ref_eqF :
forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)). forall idk, node_ref idk = scal (/ INR k) (mapF INR (Adk d k idk)).
...@@ -107,10 +118,10 @@ Lemma node_ref_Hface_ref_S : ...@@ -107,10 +118,10 @@ Lemma node_ref_Hface_ref_S :
Hface_ref i (node_ref idk) <-> Adk d k idk (lower_S Hi) = O. 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. 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 need a dimension which is structurally nonzero.
We take d = d1.+1 with d1 : nat. *) 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//. ...@@ -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]. rewrite -mapF_insert0F; [easy | apply INR_0].
Qed. Qed.
End Node_ref_Facts2. End Nodes_ref_Facts2.
Section Node_ref_d1. Section Nodes_ref_d1.
Context {d : nat}. Context {d : nat}.
...@@ -168,14 +179,13 @@ Qed. ...@@ -168,14 +179,13 @@ Qed.
Lemma node_vtx_ref_d1 : node_ref = castF (eq_sym (pbinomS_1_r d)) vtx_ref. 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. 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. Section Sub_vertices_ref_Def.
Context {d : nat}. Context {d : nat}.
Variable k : nat. Variable k : nat.
Variable vtx : 'R^{d.+1,d}.
(** (**
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
......
...@@ -304,9 +304,7 @@ Let pi_d_inv_inj := f_inv_inj pi_d_bij. ...@@ -304,9 +304,7 @@ Let pi_d_inv_inj := f_inv_inj pi_d_bij.
#<A HREF="##RR9557v1">#[[RR9557v1]]#</A># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1586, p. 96. *) Lem 1586, p. 96. *)
Lemma T_geom_permutF_bij : bijective (T_geom_permutF vtx pi_d). Lemma T_geom_permutF_bij : bijective (T_geom_permutF vtx pi_d).
Proof. Proof. apply T_geom_bij, aff_indep_permutF; easy. Qed.
apply T_geom_bij, aff_indep_permutF_equiv; [ apply injF_bij |]; easy.
Qed.
Definition T_geom_permutF_inv : 'R^d -> 'R^d := f_inv (T_geom_permutF_bij). Definition T_geom_permutF_inv : 'R^d -> 'R^d := f_inv (T_geom_permutF_bij).
......
...@@ -195,7 +195,7 @@ Lemma powF_P_one : ...@@ -195,7 +195,7 @@ Lemma powF_P_one :
powF_P L B = pow (B k) a. powF_P L B = pow (B k) a.
Proof. Proof.
intros d B L a k HL; destruct d; [destruct k; easy |]. 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. rewrite HL powF_correct; f_equal; apply itemF_correct_l; easy.
(* Warning: the multiplicative identity element of R_mul is displayed here as 0! *) (* Warning: the multiplicative identity element of R_mul is displayed here as 0! *)
rewrite -powF_skipF HL skipF_itemF_diag. rewrite -powF_skipF HL skipF_itemF_diag.
......
...@@ -78,7 +78,7 @@ now apply Nat.eq_le_incl. ...@@ -78,7 +78,7 @@ now apply Nat.eq_le_incl.
apply nat_add_sub_r. apply nat_add_sub_r.
rewrite <- H. rewrite <- H.
rewrite -skipF_first. rewrite -skipF_first.
apply (sum_skipF alpha ord0). apply (sum_skipF ord0 alpha).
(* *) (* *)
unfold Slice_op; extF i; unfold castF; simpl. unfold Slice_op; extF i; unfold castF; simpl.
case (Nat.eq_0_gt_0_cases i); intros Hi. case (Nat.eq_0_gt_0_cases i); intros Hi.
...@@ -325,8 +325,8 @@ Proof. ...@@ -325,8 +325,8 @@ Proof.
intros n A B i H1 H2. intros n A B i H1 H2.
apply Nat.add_lt_mono_l with (A i). apply Nat.add_lt_mono_l with (A i).
apply Nat.le_lt_trans with (sum A). apply Nat.le_lt_trans with (sum A).
rewrite (sum_skipF A i); unfold plus; simpl; auto with arith. rewrite (sum_skipF i A); unfold plus; simpl; auto with arith.
rewrite H1; rewrite (sum_skipF B i). rewrite H1; rewrite (sum_skipF i B).
unfold plus; simpl. unfold plus; simpl.
apply Nat.add_lt_mono_r; auto with arith. apply Nat.add_lt_mono_r; auto with arith.
Qed. Qed.
......
...@@ -71,6 +71,12 @@ fun_ext2; unfold liftF_S; ...@@ -71,6 +71,12 @@ fun_ext2; unfold liftF_S;
rewrite (vtx_ref_S (lift_S_not_first _)) lower_lift_S; easy. rewrite (vtx_ref_S (lift_S_not_first _)) lower_lift_S; easy.
Qed. 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># #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
Lem 1436, p. 55. *) Lem 1436, p. 55. *)
...@@ -347,7 +353,7 @@ intros j; rewrite Ker_equiv; apply LagPd1_ref_vtx_skipF. ...@@ -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 ->]]. intros x_ref; move: (vtx_ref_aff_span x_ref) => /aff_span_EX [L [HL ->]].
rewrite Ker_equiv. rewrite Ker_equiv.
move: (LagPd1_ref_barycF_rev HL) => /extF_rev HL1; rewrite (HL1 i) => HLi. 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. rewrite -(plus_zero_l (sum _)) -HLi -sum_skipF.
1,2: apply invertible_eq_one; easy. 1,2: apply invertible_eq_one; easy.
Qed. Qed.
......