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.

Brief description

Support for finite families/tables on module spaces.

Description

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.

Operator

Let a : 'K^n and u : 'E^n. Let T : Type and f : '(T E)^n.

Usage

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

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 i1scalF 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 i1sum (u12 i1)) = sum (fun i2scalF 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 i1scalF (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 i1sum (a12 i1)) u1 = sum (fun i2scalF (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 iscalF (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.