Library Algebra.Ring.Ring_FF_FT
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for finite families/tables on rings.
Let K : Ring.
This module may be used through the import of Algebra.Ring.Ring,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Constructors
- ones n is the n-family made of ones;
- 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...
- plusn n x is the sum of n items equal to x;
- plusn1 n is plusn n 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.
Used logic axioms
- classic, the weak form of excluded middle;
- classic_dec, an alias for excluded_middle_informative, the strong form of excluded middle;
- ex_EX, an alias for constructive_indefinite_description.
Usage
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring_compl.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Ring_FF_Facts1.
Properties with the second identity element of rings (one).
Context {K : Ring}.
Definition ones {n} : 'K^n := constF n 1.
Definition alt_ones {n} : 'K^n :=
fun i ⇒ if Nat.Even_Odd_dec i then 1 else - (1 : K).
Definition alt_ones_shift {n} : 'K^n :=
fun i ⇒ if Nat.Even_Odd_dec i then - (1 : K) else 1.
Lemma ones_correct : ∀ {n} (i : 'I_n), ones i = 1.
Proof. easy. Qed.
Lemma alt_ones_correct_even :
∀ {n} (i : 'I_n), Nat.Even i → alt_ones i = 1.
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.
Qed.
Lemma alt_ones_correct_odd :
∀ {n} (i : 'I_n), Nat.Odd 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.
Qed.
Lemma alt_ones_shift_correct_even :
∀ {n} (i : 'I_n), Nat.Even 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_shift_correct_odd :
∀ {n} (i : 'I_n), Nat.Odd i → alt_ones_shift i = 1.
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 : ∀ {n}, @alt_ones n = liftF_S (@alt_ones_shift n.+1).
Proof.
intros n; apply extF; intros i; unfold liftF_S; destruct (Nat.Even_Odd_dec i).
rewrite → alt_ones_shift_correct_odd, alt_ones_correct_even; try easy.
rewrite lift_S_correct; apply Nat.Odd_succ; easy.
rewrite → alt_ones_shift_correct_even, alt_ones_correct_odd; try easy.
rewrite lift_S_correct; apply Nat.Even_succ; easy.
Qed.
Lemma alt_ones_shift_eq :
∀ {n}, @alt_ones_shift n = liftF_S (@alt_ones n.+1).
Proof.
intros n; apply extF; intros i; unfold liftF_S; destruct (Nat.Even_Odd_dec i).
rewrite → alt_ones_shift_correct_even, alt_ones_correct_odd; try easy.
rewrite lift_S_correct; apply Nat.Odd_succ; easy.
rewrite → alt_ones_shift_correct_odd, alt_ones_correct_even; try easy.
rewrite lift_S_correct; apply Nat.Even_succ; easy.
Qed.
Lemma alt_ones_shift2 :
∀ {n}, @alt_ones n = liftF_S (liftF_S (@alt_ones n.+2)).
Proof. intros; rewrite alt_ones_eq alt_ones_shift_eq; easy. Qed.
Lemma ones_not_zero : ∀ {n}, nonzero_struct K → (ones : 'K^n.+1) ≠ 0.
Proof. intros; apply nextF; ∃ ord0; apply one_not_zero; easy. Qed.
Lemma alt_ones_not_zero :
∀ {n}, nonzero_struct K → (alt_ones : 'K^n.+1) ≠ 0.
Proof.
intros; apply nextF; ∃ ord0; rewrite alt_ones_correct_even.
apply one_not_zero; easy.
apply Even_0.
Qed.
Lemma sum_alt_ones_even : ∀ {n}, Nat.Even n → sum (@alt_ones n) = 0.
Proof.
intros n [m Hm]; subst; induction m as [| m Hm]. apply sum_nil.
rewrite -(sum_castF (nat_double_S _)).
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.
apply alt_ones_shift2.
Qed.
Lemma sum_alt_ones_odd : ∀ {n}, Nat.Odd n → sum (@alt_ones n) = 1.
Proof.
intros n [m Hm]; subst; induction m as [| m Hm].
rewrite sum_1; apply alt_ones_correct_even, Even_0.
rewrite -(sum_castF (nat_S_double_S _)).
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_castF (addn1_sym _)); easy.
apply alt_ones_shift2.
Qed.
Lemma alt_ones_3_eq : @alt_ones 3 = tripleF 1 (- (1)) 1.
Proof.
apply extF; intros i; destruct (ord3_dec i) as [[Hi | Hi] | Hi]; rewrite Hi.
rewrite → alt_ones_correct_even, tripleF_0; try apply Even_0; easy.
rewrite → alt_ones_correct_odd, tripleF_1; try apply Odd_1; easy.
rewrite → alt_ones_correct_even, tripleF_2; try apply Even_2; easy.
Qed.
Lemma sum_alt_ones_3 : sum (tripleF 1 (- (1 : K)) 1) = 1.
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 unit_partition {n} (u : 'K^n) : 'K^n.+1 :=
insertF u (1 - sum u) ord0.
Lemma unit_partition_correct_0 :
∀ {n} (u : 'K^n) i, i = ord0 → unit_partition u i = 1 - sum u.
Proof. move=>> ->; unfold unit_partition; rewrite insertF_correct_l; easy. Qed.
Lemma unit_partition_correct_S :
∀ {n} (u : 'K^n) {i} (Hi : i ≠ ord0),
unit_partition u i = u (lower_S Hi).
Proof.
intros n u i Hi; unfold unit_partition; rewrite insertF_correct_rr.
apply ord_n0_nlt_equiv in Hi; destruct i; simpl in *; auto with zarith.
intros Hi'; f_equal; apply ord_inj; easy.
Qed.
Lemma sum_unit_partition : ∀ {n} (u : 'K^n), sum (unit_partition u) = 1.
Proof.
intros; unfold unit_partition; rewrite sum_insertF plus_minus_l; easy.
Qed.
Lemma unit_partition_1_eq :
∀ a, unit_partition (singleF a) = coupleF (1 - a) a.
Proof.
intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
rewrite → unit_partition_correct_0, sum_singleF, coupleF_0; easy.
rewrite unit_partition_correct_S; try easy.
intros Hi'; rewrite singleF_0 coupleF_1; easy.
Qed.
Lemma sum_unit_partition_1 :
∀ (a : K), sum (coupleF (1 - a) a) = 1.
Proof. intros; rewrite -unit_partition_1_eq; apply sum_unit_partition. Qed.
Lemma sum_unit_partition_1_invertible :
∀ (a : K), invertible (sum (coupleF (1 - a) a)).
Proof. intros; rewrite sum_unit_partition_1; apply invertible_one. Qed.
End Ring_FF_Facts1.
Section Ring_FF_Facts2.
Properties with the second law of rings (mult).
Context {K : Ring}.
Lemma constF_mult :
∀ n (x y : K), constF n (x × y) = constF n x × constF n y.
Proof. easy. Qed.
Lemma castF_mult :
∀ {n1 n2} (H : n1 = n2) (A1 B1 : 'K^n1),
castF H (A1 × B1) = castF H A1 × castF H B1.
Proof. easy. Qed.
Lemma widenF_S_mult :
∀ {n} (A B : 'K^n.+1), widenF_S (A × B) = widenF_S A × widenF_S B.
Proof. easy. Qed.
Lemma liftF_S_mult :
∀ {n} (A B : 'K^n.+1), liftF_S (A × B) = liftF_S A × liftF_S B.
Proof. easy. Qed.
Lemma widenF_mult :
∀ {n1 n2} (H : n1 ≤ n2) (A2 B2 : 'K^n2),
widenF H (A2 × B2) = widenF H A2 × widenF H B2.
Proof. easy. Qed.
Lemma firstF_mult :
∀ {n1 n2} (A B : 'K^(n1 + n2)), firstF (A × B) = firstF A × firstF B.
Proof. easy. Qed.
Lemma lastF_mult :
∀ {n1 n2} (A B : 'K^(n1 + n2)), lastF (A × B) = lastF A × lastF B.
Proof. easy. Qed.
Lemma concatF_mult :
∀ {n1 n2} (A1 B1 : 'K^n1) (A2 B2 : 'K^n2),
concatF (A1 × B1) (A2 × B2) = concatF A1 A2 × concatF B1 B2.
Proof.
intros n1 n2 A1 B1 A2 B2; apply extF; intros i; rewrite fct_mult_eq;
destruct (lt_dec i n1) as [Hi | Hi];
[rewrite !concatF_correct_l | rewrite !concatF_correct_r]; easy.
Qed.
Lemma insertF_mult :
∀ {n} (A B : 'K^n) a0 b0 i0,
insertF (A × B) (a0 × b0) i0 = insertF A a0 i0 × insertF B b0 i0.
Proof.
intros n A B a0 b0 i0; apply extF; intros i; rewrite fct_mult_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed.
Lemma skipF_mult :
∀ {n} (A B : 'K^n.+1) i0, skipF (A × B) i0 = skipF A i0 × skipF B i0.
Proof. easy. Qed.
Lemma replaceF_mult :
∀ {n} (A B : 'K^n.+1) a0 b0 i0,
replaceF (A × B) (a0 × b0) i0 = replaceF A a0 i0 × replaceF B b0 i0.
Proof.
intros n A B a b i0; apply extF; intros i; rewrite fct_mult_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
Qed.
Lemma permutF_mult :
∀ {n} (p : 'I_[n]) (A B : 'K^n),
permutF p (A × B) = permutF p A × permutF p B.
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 : ∀ n, plusn1 K n = plusn n 1.
Proof. easy. Qed.
Lemma plusn_0_l : ∀ x : K, plusn 0 x = 0.
Proof. intros; apply sum_nil. Qed.
Lemma plusn_0_r : ∀ n, plusn n (0 : K) = 0.
Proof. intros; apply sum_zero. Qed.
Lemma plusn_1_l : ∀ x : K, plusn 1 x = x.
Proof. intros; apply sum_1. Qed.
Lemma plusn_2_l : ∀ 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 : ∀ x : K, plusn 3 x = x + x + x.
Proof. intros; apply sum_3. Qed.
Lemma plusn_ind : ∀ n (x : K), plusn n.+1 x = x + plusn n x.
Proof. intros; apply sum_ind_l. Qed.
Lemma plusn_distr_l :
∀ 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_distr_r :
∀ 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 :
∀ 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_distr_l Hn1 plusn_ind plus_comm; easy.
Qed.
Lemma plusn_assoc_r :
∀ 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 : ∀ n (x y : K), plusn n (x × y) = plusn n x × y.
Proof. intros; unfold plusn; rewrite -mult_sum_distr_r; easy. Qed.
Lemma plusn_eq : ∀ 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 :
∀ n, plusn1 K n = 0 ↔ ∀ 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}.
Lemma onesT : ∀ {m n} (i : 'I_m), (ones : 'K^{m,n}) i = ones.
Proof. easy. Qed.
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 : ∀ {n}, (ones : 'R_Ring^n.+1) ≠ 0.
Proof. intros n; apply (@ones_not_zero _ n), nonzero_struct_R. Qed.
Lemma sum_ones_R : ∀ {n}, sum (ones : 'R_Ring^n) = INR n.
Proof.
intros n; induction n as [| n Hn].
rewrite sum_nil; easy.
rewrite sum_ind_l plus_comm Hn S_INR; easy.
Qed.
End Ring_FF_R_Facts.