Library Algebra.ModuleSpace.ModuleSpace_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 module spaces.
For results that are only valid when the ring of scalars is commutative, or
being ordered, see Algebra.ModuleSpace.ModuleSpace_R_compl where they are
only stated in the case of the ring of real numbers R_Ring.
Let K : Ring and E : ModuleSpace K.
Let a : 'K^n and u : 'E^n.
Let T : Type and f : '(T → E)^n.
This module may be used through the import of Algebra.ModuleSpace.ModuleSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Operator
Usage
From Requisite Require Import stdlib 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.
From Algebra Require Import ModuleSpace_compl.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section ModuleSpace_FF_Def1.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Definition scalF {n} a (u : 'E^n) : 'E^n := map2F scal a u.
Correctness lemma.
Lemma scalF_correct :
∀ {n} a (u : 'E^n) i, scalF a u i = scal (a i) (u i).
Proof. easy. Qed.
End ModuleSpace_FF_Def1.
Section ModuleSpace_FF_Def2.
Context {T : Type}.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Definition fct_scalF_l {n} (f : '(T → K)^n) (u : 'E^n) : '(T → E)^n :=
map2F fct_scal_l f u.
Correctness lemmas.
Lemma fct_scalF_l_eq :
∀ {n} (f : '(T → K)^n) (u : 'E^n) i t,
fct_scalF_l f u i t = scalF (f^~ t) u i.
Proof. easy. Qed.
Lemma fct_scalF_r_eq :
∀ {n} a (f : '(T → E)^n) i t, scalF a f i t = scalF a (f^~ t) i.
Proof. easy. Qed.
End ModuleSpace_FF_Def2.
Section ModuleSpace_FF_Facts1.
Context {K : Ring}.
Context {E F : ModuleSpace K}.
Properties of the operator scalF.
Lemma scalF_compat :
∀ {n} a b (u v : 'E^n), a = b → u = v → scalF a u = scalF b v.
Proof. intros; f_equal; easy. Qed.
Lemma scalF_assoc :
∀ {n} a b (u : 'E^n), scalF a (scalF b u) = scalF (scalF a b) u.
Proof. intros; apply extF; intro; apply scal_assoc. Qed.
Lemma scalF_opp_l : ∀ {n} a (u : 'E^n), scalF (- a) u = - scalF a u.
Proof. intros; apply extF; intro; apply scal_opp_l. Qed.
Lemma scalF_opp_r : ∀ {n} a (u : 'E^n), scalF a (- u) = - scalF a u.
Proof. intros; apply extF; intro; apply scal_opp_r. Qed.
Lemma scalF_minus_l :
∀ {n} a1 a2 (u : 'E^n), scalF (a1 - a2) u = scalF a1 u - scalF a2 u.
Proof. intros; apply extF; intro; apply scal_minus_l. Qed.
Lemma scalF_minus_r :
∀ {n} a (u1 u2 : 'E^n), scalF a (u1 - u2) = scalF a u1 - scalF a u2.
Proof. intros; apply extF; intro; apply scal_minus_r. Qed.
Lemma scalF_scal_l :
∀ {n} a x (u : 'E^n), scalF (scal x a) u = scal x (scalF a u).
Proof. intros; apply extF; intro; rewrite scalF_correct -scal_assoc; easy. Qed.
Lemma scalF_scal_r :
∀ {n} a x (u : 'E^n),
scalF a (scal x u) = scalF (scalF a (constF n x)) u.
Proof. intros; apply extF; intro; apply scal_assoc. Qed.
Lemma scalF_distr_l :
∀ {n} a (u v : 'E^n), scalF a (u + v) = scalF a u + scalF a v.
Proof. intros; apply extF; intro; apply scal_distr_l. Qed.
Lemma scalF_distr_r :
∀ {n} a b (u : 'E^n), scalF (a + b) u = scalF a u + scalF b u.
Proof. intros; apply extF; intro; apply scal_distr_r. Qed.
Lemma scalF_sum_ll :
∀ {n1 n2} a2 (u12 : 'E^{n1,n2}),
scalF a2 (sum u12) = sum (fun i1 ⇒ scalF a2 (u12 i1)).
Proof.
intros; apply extF; intro.
rewrite scalF_correct !fct_sum_eq scal_sum_distr_l; easy.
Qed.
Lemma scalF_sum_lr :
∀ {n1 n2} a1 (u12 : 'E^{n1,n2}),
scalF a1 (fun i1 ⇒ sum (u12 i1)) = sum (fun i2 ⇒ scalF a1 (u12^~ i2)).
Proof.
intros; apply extF; intro.
rewrite scalF_correct !fct_sum_eq scal_sum_distr_l; easy.
Qed.
Lemma scalF_sum_rl :
∀ {n1 n2} (a12 : 'K^{n1,n2}) (u2 : 'E^n2),
scalF (sum a12) u2 = sum (fun i1 ⇒ scalF (a12 i1) u2).
Proof.
intros; apply extF; intro.
rewrite scalF_correct !fct_sum_eq scal_sum_distr_r; easy.
Qed.
Lemma scalF_sum_rr :
∀ {n1 n2} (a12 : 'K^{n1,n2}) (u1 : 'E^n1),
scalF (fun i1 ⇒ sum (a12 i1)) u1 = sum (fun i2 ⇒ scalF (a12^~ i2) u1).
Proof.
intros; apply extF; intro.
rewrite scalF_correct !fct_sum_eq scal_sum_distr_r; easy.
Qed.
Lemma scalF_ones_l : ∀ {n} (u : 'E^n), scalF ones u = u.
Proof. intros; apply extF; intro; apply scal_one_l; easy. Qed.
Lemma scalF_ones_r : ∀ {n} (a : 'K^n), scalF a ones = a.
Proof. intros; apply extF; intro; apply scal_one_r; easy. Qed.
Lemma scalF_zero_l : ∀ {n} (u : 'E^n), scalF 0 u = 0.
Proof. intros; apply extF; intro; apply scal_zero_l. Qed.
Lemma scalF_zero_r : ∀ {n} a, scalF a (0 : 'E^n) = 0.
Proof. intros; apply extF; intro; apply scal_zero_r. Qed.
Lemma scalF_zero_compat_l :
∀ {n} a (u : 'E^n), a = 0 → scalF a u = 0.
Proof. move=>> H; rewrite H; apply scalF_zero_l. Qed.
Lemma scalF_zero_compat_r :
∀ {n} a (u : 'E^n), u = 0 → scalF a u = 0.
Proof. move=>> H; rewrite H; apply scalF_zero_r. Qed.
Lemma scalF_singleF :
∀ a0 (u0 : E), scalF (singleF a0) (singleF u0) = singleF (scal a0 u0).
Proof. easy. Qed.
Lemma scalF_coupleF :
∀ a0 a1 (u0 u1 : E),
scalF (coupleF a0 a1) (coupleF u0 u1) =
coupleF (scal a0 u0) (scal a1 u1).
Proof.
intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
rewrite scalF_correct !coupleF_0; easy.
rewrite scalF_correct !coupleF_1; easy.
Qed.
Lemma scalF_tripleF :
∀ a0 a1 a2 (u0 u1 u2 : E),
scalF (tripleF a0 a1 a2) (tripleF u0 u1 u2) =
tripleF (scal a0 u0) (scal a1 u1) (scal a2 u2).
Proof.
intros; apply extF; intros i;
destruct (ord3_dec i) as [[Hi | Hi] | Hi]; rewrite Hi.
rewrite scalF_correct !tripleF_0; easy.
rewrite scalF_correct !tripleF_1; easy.
rewrite scalF_correct !tripleF_2; easy.
Qed.
Lemma scalF_castF_compat :
∀ {n1 n2} (H : n1 = n2) a1 a2 (u1 : 'E^n1) u2,
castF H a1 = a2 → castF H u1 = u2 → castF H (scalF a1 u1) = scalF a2 u2.
Proof. intros; subst; easy. Qed.
Lemma scalF_castF :
∀ {n1 n2} (H : n1 = n2) a1 (u1 : 'E^n1),
scalF (castF H a1) (castF H u1) = castF H (scalF a1 u1).
Proof. intros; apply eq_sym, scalF_castF_compat; easy. Qed.
Lemma scalF_firstF :
∀ {n1 n2} a (u : 'E^(n1 + n2)),
scalF (firstF a) (firstF u) = firstF (scalF a u).
Proof. easy. Qed.
Lemma scalF_lastF :
∀ {n1 n2} a (u : 'E^(n1 + n2)),
scalF (lastF a) (lastF u) = lastF (scalF a u).
Proof. easy. Qed.
Lemma scalF_concatF :
∀ {n1 n2} a1 a2 (u1 : 'E^n1) (u2 : 'E^n2),
scalF (concatF a1 a2) (concatF u1 u2) = concatF (scalF a1 u1) (scalF a2 u2).
Proof.
intros; apply extF; intros i; destruct (lt_dec i n1).
rewrite scalF_correct !concatF_correct_l; easy.
rewrite scalF_correct !concatF_correct_r; easy.
Qed.
Lemma scalF_splitF_l :
∀ {n1 n2} a (u1 : 'E^n1) (u2 : 'E^n2),
scalF a (concatF u1 u2) = concatF (scalF (firstF a) u1) (scalF (lastF a) u2).
Proof. intros; rewrite -scalF_concatF -concatF_splitF; easy. Qed.
Lemma scalF_splitF_r :
∀ {n1 n2} a1 a2 (u : 'E^(n1 + n2)),
scalF (concatF a1 a2) u = concatF (scalF a1 (firstF u)) (scalF a2 (lastF u)).
Proof. intros; rewrite -scalF_concatF -concatF_splitF; easy. Qed.
Lemma scalF_splitF :
∀ {n1 n2} a (u : 'E^(n1 + n2)),
scalF a u =
concatF (scalF (firstF a) (firstF u)) (scalF (lastF a) (lastF u)).
Proof. intros; rewrite -scalF_concatF -!concatF_splitF; easy. Qed.
Lemma scalF_widenF_S :
∀ {n} a (u : 'E^n.+1),
scalF (widenF_S a) (widenF_S u) = widenF_S (scalF a u).
Proof. easy. Qed.
Lemma scalF_liftF_S :
∀ {n} a (u : 'E^n.+1),
scalF (liftF_S a) (liftF_S u) = liftF_S (scalF a u).
Proof. easy. Qed.
Lemma scalF_insertF :
∀ {n} a a0 (u : 'E^n) x0 i0,
scalF (insertF a a0 i0) (insertF u x0 i0) =
insertF (scalF a u) (scal a0 x0) i0.
Proof.
intros; apply extF; intro; rewrite scalF_correct; unfold insertF;
destruct (ord_eq_dec _ _); easy.
Qed.
Lemma scalF_insert2F :
∀ {n} a a0 a1 (u : 'E^n) x0 x1 {i0 i1} (H : i1 ≠ i0),
scalF (insert2F a a0 a1 H) (insert2F u x0 x1 H) =
insert2F (scalF a u) (scal a0 x0) (scal a1 x1) H.
Proof. intros; rewrite 3!insert2F_correct 2!scalF_insertF; easy. Qed.
Lemma scalF_skipF :
∀ {n} a (u : 'E^n.+1) i0,
scalF (skipF a i0) (skipF u i0) = skipF (scalF a u) i0.
Proof. easy. Qed.
Lemma scalF_skip2F :
∀ {n} a (u : 'E^n.+2) {i0 i1} (H : i1 ≠ i0),
scalF (skip2F a H) (skip2F u H) = skip2F (scalF a u) H.
Proof. easy. Qed.
Lemma scalF_replaceF :
∀ {n} a a0 (u : 'E^n) x0 i0,
scalF (replaceF a a0 i0) (replaceF u x0 i0) =
replaceF (scalF a u) (scal a0 x0) i0.
Proof.
intros; rewrite 3!replaceF_equiv_def_skipF scalF_skipF scalF_insertF; easy.
Qed.
Lemma scalF_replace2F :
∀ {n} a a0 a1 (u : 'E^n) x0 x1 i0 i1,
scalF (replace2F a a0 a1 i0 i1) (replace2F u x0 x1 i0 i1) =
replace2F (scalF a u) (scal a0 x0) (scal a1 x1) i0 i1.
Proof. intros; rewrite 2!scalF_replaceF; easy. Qed.
Lemma scalF_permutF :
∀ {n} p a (u : 'E^n),
scalF (permutF p a) (permutF p u) = permutF p (scalF a u).
Proof. easy. Qed.
Lemma scalF_revF :
∀ {n} a (u : 'E^n), scalF (revF a) (revF u) = revF (scalF a u).
Proof. easy. Qed.
Lemma scalF_moveF :
∀ {n} a (u : 'E^n.+1) i0 i1,
scalF (moveF a i0 i1) (moveF u i0 i1) = moveF (scalF a u) i0 i1.
Proof. easy. Qed.
Lemma scalF_transpF :
∀ {n} a (u : 'E^n) i0 i1,
scalF (transpF a i0 i1) (transpF u i0 i1) = transpF (scalF a u) i0 i1.
Proof. easy. Qed.
Lemma scalF_filterPF :
∀ {n} P a (u : 'E^n),
scalF (filterPF P a) (filterPF P u) = filterPF P (scalF a u).
Proof. easy. Qed.
Lemma scalF_splitPF :
∀ {n} P a (u : 'E^n),
scalF (splitPF P a) (splitPF P u) = splitPF P (scalF a u).
Proof.
intros; unfold splitPF; rewrite scalF_concatF !scalF_filterPF; easy.
Qed.
Lemma scalF_itemF_l :
∀ n a0 (u : 'E^n) i0,
scalF (itemF n a0 i0) u = itemF n (scal a0 (u i0)) i0.
Proof.
intros n a0 u i0; apply extF; intros i; rewrite scalF_correct.
destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite Hi !itemF_correct_l; easy.
rewrite → !itemF_correct_r, scal_zero_l; easy.
Qed.
Lemma scalF_itemF_r :
∀ n a (x0 : E) i0,
scalF a (itemF n x0 i0) = itemF n (scal (a i0) x0) i0.
Proof.
intros n a0 u i0; apply extF; intros i; rewrite scalF_correct.
destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite Hi !itemF_correct_l; easy.
rewrite → !itemF_correct_r, scal_zero_r; easy.
Qed.
Lemma scalF_unfun0F :
∀ {n1 n2} (f : '('I_n2)^n1) a1 (u1 : 'E^n1),
scalF (unfun0F f a1) (unfun0F f u1) = unfun0F f (scalF a1 u1).
Proof.
intros; apply extF; intro; rewrite scalF_correct; unfold unfun0F, unfunF.
destruct (im_dec _ _) as [[i1 Hi1] | Hi2]; [easy | apply scal_zero_l].
Qed.
Lemma scalF_squeezeF :
∀ {n} a (u : 'E^n.+1) {i0 i1},
i1 ≠ i0 → u i1 = u i0 →
scalF (squeezeF a i0 i1) (skipF u i1) = squeezeF (scalF a u) i0 i1.
Proof.
intros n a u i0 i1 Hi Hu; apply extF; intros j.
rewrite scalF_correct; destruct (ord_eq_dec (skip_ord i1 j) i0) as [Hj | Hj].
rewrite !squeezeF_correct_l_alt// (skipF_correct_alt (not_eq_sym Hi) Hj).
rewrite !scalF_correct Hu; apply scal_distr_r.
rewrite !squeezeF_correct_r; easy.
Qed.
Lemma scalF_concatnF :
∀ {n} {b : 'nat^n} L (B : ∀ i, 'E^(b i)),
scalF (concatnF L) (concatnF B) = concatnF (fun i ⇒ scalF (L i) (B i)).
Proof.
intros; apply extF; intros k; rewrite (splitn_ord k).
rewrite scalF_correct !concatn_ord_correct; easy.
Qed.
End ModuleSpace_FF_Facts1.
Section ModuleSpace_FF_Facts2.
More properties of the operator scalF.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Context {T1 T2 : Type}.
Lemma scalF_compF_rl :
∀ {n} (L : 'K^n) (B : '(T2 → E)^n) (f : T1 → T2),
scalF L (compF_l B f) = compF_l (scalF L B) f.
Proof. easy. Qed.
Lemma scalF_compF_r :
∀ {n} (L : 'K^n) (B : '(T2 → E)^n) (f : '(T1 → T2)^n),
scalF L (compF B f) = compF (scalF L B) f.
Proof. easy. Qed.
End ModuleSpace_FF_Facts2.
Section ModuleSpace_FF_Facts3.
Properties with the external law of module spaces (scal).
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma constF_scal :
∀ n l (x : E), constF n (scal l x) = scal l (constF n x).
Proof. easy. Qed.
Lemma castF_scal :
∀ {n1 n2} (H : n1 = n2) l (A1 : 'E^n1),
castF H (scal l A1) = scal l castF H A1.
Proof. easy. Qed.
Lemma widenF_S_scal :
∀ {n} l (A : 'E^n.+1), widenF_S (scal l A) = scal l widenF_S A.
Proof. easy. Qed.
Lemma liftF_S_scal :
∀ {n} l (A : 'E^n.+1), liftF_S (scal l A) = scal l liftF_S A.
Proof. easy. Qed.
Lemma widenF_scal :
∀ {n1 n2} (H : n1 ≤ n2) l (A2 : 'E^n2),
widenF H (scal l A2) = scal l widenF H A2.
Proof. easy. Qed.
Lemma firstF_scal :
∀ {n1 n2} l (A : 'E^(n1 + n2)), firstF (scal l A) = scal l firstF A.
Proof. easy. Qed.
Lemma lastF_scal :
∀ {n1 n2} l (A : 'E^(n1 + n2)), lastF (scal l A) = scal l lastF A.
Proof. easy. Qed.
Lemma concatF_scal :
∀ {n1 n2} l (A1 : 'E^n1) (A2 : 'E^n2),
concatF (scal l A1) (scal l A2) = scal l concatF A1 A2.
Proof.
intros n1 n2 l A1 A2; apply extF; intros i; rewrite !fct_scal_eq;
destruct (lt_dec i n1) as [Hi | Hi];
[rewrite !concatF_correct_l | rewrite !concatF_correct_r]; easy.
Qed.
Lemma insertF_scal :
∀ {n} l (A : 'E^n) a0 i0,
insertF (scal l A) (scal l a0) i0 = scal l insertF A a0 i0.
Proof.
intros n l A a0 i0; apply extF; intros i; rewrite !fct_scal_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed.
Lemma skipF_scal :
∀ {n} l (A : 'E^n.+1) i0, skipF (scal l A) i0 = scal l skipF A i0.
Proof. easy. Qed.
Lemma replaceF_scal :
∀ {n} l (A : 'E^n.+1) a0 i0,
replaceF (scal l A) (scal l a0) i0 = scal l replaceF A a0 i0.
Proof.
intros n l A a0 i0; apply extF; intros i; rewrite !fct_scal_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
Qed.
Lemma permutF_scal :
∀ {n} (p : 'I_[n]) l (A : 'E^n),
permutF p (scal l A) = scal l permutF p A.
Proof. easy. Qed.
End ModuleSpace_FF_Facts3.
Section ModuleSpace_FT_Facts.
Context {K : Ring}.
Context {E : ModuleSpace K}.
Lemma scalF_skipTc_r :
∀ {n1 n2} L1 (B12 : 'E^{n1,n2.+1}) i20,
scalF L1 (skipTc B12 i20) = skipTc (scalF L1 B12) i20.
Proof. easy. Qed.
End ModuleSpace_FT_Facts.