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.

Brief description

Support for finite families/tables on rings.

Description

Let K : Ring.

Constructors

Let u : 'K^n. Let x : K.

Used logic axioms

Usage

This module may be used through the import of Algebra.Ring.Ring, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

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 iif Nat.Even_Odd_dec i then 1 else - (1 : K).

Definition alt_ones_shift {n} : 'K^n :=
  fun iif 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).
rewritealt_ones_shift_correct_odd, alt_ones_correct_even; try easy.
rewrite lift_S_correct; apply Nat.Odd_succ; easy.
rewritealt_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).
rewritealt_ones_shift_correct_even, alt_ones_correct_odd; try easy.
rewrite lift_S_correct; apply Nat.Odd_succ; easy.
rewritealt_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.
rewritealt_ones_correct_even, tripleF_0; try apply Even_0; easy.
rewritealt_ones_correct_odd, tripleF_1; try apply Odd_1; easy.
rewritealt_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.
rewriteunit_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 jif 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.