Library Algebra.AffineSpace.AffineSpace_FF

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 finite families on affine spaces.

Description

Let K : Ring, V : ModuleSpace K and E : AffineSpace V.

Operator

Let O : E, A : 'E^n, B : 'E^n.+1 and u : 'V^n.

Used logic axioms

Usage

This module may be used through the import of Algebra.AffineSpace.AffineSpace, 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 ModuleSpace.
From Algebra Require Import AffineSpace_def.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Local Open Scope AffineSpace_scope.

Section FF_AffineSpace_Def.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Definition vectF {n} O (A : 'E^n) : 'V^n := mapF (vect O) A.
Definition translF {n} O (u : 'V^n) : 'E^n := mapF (transl O) u.

Definition frameF {n} (A : 'E^n.+1) i0 : 'V^n := vectF (A i0) (skipF A i0).
Definition inv_frameF {n} O (u : 'V^n) i0 : 'E^n.+1 :=
  translF O (insertF u 0 i0).

Correctness lemmas.

Lemma vectF_correct : {n} O (A : 'E^n) i, vectF O A i = O --> A i.
Proof. easy. Qed.

Lemma translF_correct : {n} O (u : 'V^n) i, translF O u i = O +++ u i.
Proof. easy. Qed.

Lemma frameF_correct :
   {n} (A : 'E^n.+1) i0 i (H : i i0),
    frameF A i0 (insert_ord H) = A i0 --> A i.
Proof. intros; unfold frameF; rewrite vectF_correct skipF_correct; easy. Qed.

Lemma inv_frameF_correct :
   {n} (O : E) (u : 'V^n) i0 j,
    inv_frameF O u i0 (skip_ord i0 j) = O +++ u j.
Proof.
intros; unfold inv_frameF; rewrite translF_correct insertF_correct; easy.
Qed.

End FF_AffineSpace_Def.

Section FF_AffineSpace_Facts.

Context {K : Ring}.
Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.

Lemma vectF_change_orig :
   {n} O1 O2 (A : 'E^n), vectF O2 A = constF n (O2 --> O1) + vectF O1 A.
Proof.
intros; apply extF; intro; rewrite fct_plus_eq !vectF_correct constF_correct.
apply eq_sym, vect_chasles.
Qed.

Lemma vectF_chasles :
   {n} O (A B : 'E^n), vectF O A + (A --> B) = vectF O B.
Proof.
intros; apply extF; intro; rewrite fct_plus_eq !vectF_correct fct_vect_eq.
apply vect_chasles.
Qed.

Lemma vectF_l_bij_ex : {n} O u, ! (A : 'E^n), vectF O A = u.
Proof.
intros n O u; destruct (unique_choice _ (vect_l_bij_ex O)) as [A HA].
(mapF A u); split.
apply extF; intro; rewrite vectF_correct mapF_correct; easy.
moveB /extF_rev HB; apply extF; intro.
apply (vect_l_inj O); rewrite mapF_correct -vectF_correct HB; easy.
Qed.

Lemma vectF_l_bij : {n} (O : E), bijective (@vectF _ _ _ n O).
Proof. intros; apply bij_ex_uniq_rev, vectF_l_bij_ex. Qed.

Lemma vectF_zero : {n} (O : E), vectF O (constF n O) = 0.
Proof. intros; apply extF; intro; apply vect_zero. Qed.

Lemma vectF_zero_equiv :
   {n} O (A : 'E^n), vectF O A = 0 A = constF n O.
Proof.
intros; split.
move⇒ /extF_rev H; apply extF; intro; apply vect_zero_equiv; apply H.
intros; subst; apply vectF_zero.
Qed.

Lemma vectF_zero_alt : {n} (A : 'E^n) i, vectF (A i) A i = 0.
Proof. intros; apply vect_zero. Qed.

Lemma vectF_l_eq :
   {n} O (A1 A2 : 'E^n), A1 = A2 vectF O A1 = vectF O A2.
Proof. intros; subst; easy. Qed.

Lemma vectF_r_eq :
   {n} (A : 'E^n) O1 O2, O1 = O2 vectF O1 A = vectF O2 A.
Proof. intros; subst; easy. Qed.

Lemma vectF_l_inj :
   {n} O (A1 A2 : 'E^n), vectF O A1 = vectF O A2 A1 = A2.
Proof. move=>>; eapply (bij_inj (vectF_l_bij _)). Qed.

Lemma vectF_r_inj :
   {n} (A : 'E^n.+1) O1 O2, vectF O1 A = vectF O2 A O1 = O2.
Proof.
moven A O1 O2 /extF_rev H; specialize (H ord0).
apply (vect_r_inj (A ord0)); easy.
Qed.

Lemma vectF_l_inj_equiv :
   {n} O (A1 A2 : 'E^n), vectF O A1 = vectF O A2 A1 = A2.
Proof. intros; split. apply vectF_l_inj. apply vectF_l_eq. Qed.

Lemma vectF_r_inj_equiv :
   {n} (A : 'E^n.+1) O1 O2, vectF O1 A = vectF O2 A O1 = O2.
Proof. intros; split. apply vectF_r_inj. apply vectF_r_eq. Qed.

Lemma vectF_inj_equiv :
   {n} O (A : 'E^n), injective (vectF O A) injective A.
Proof.
intros n O A; split; intros HA i1 i2 H; apply HA;
    [rewrite vectF_correct H | apply (vect_l_inj O)]; easy.
Qed.

Lemma vectF_constF :
   {n} (O A : E), vectF O (constF n A) = constF n (O --> A).
Proof.
intros; apply extF; intro; rewrite vectF_correct !constF_correct; easy.
Qed.

Lemma vectF_w_zero_struct_r :
   {n} O (A : 'E^n), zero_struct K vectF O A = 0.
Proof.
move=>> HK; move: (@ms_w_zero_struct_r _ V HK) ⇒ HV.
apply extF; intro; rewrite vectF_correct; apply HV.
Qed.

Lemma vectF_singleF :
   (O A0 : E), vectF O (singleF A0) = singleF (O --> A0).
Proof.
intros; apply extF; intro; rewrite I_1_is_unit vectF_correct !singleF_0; easy.
Qed.

Lemma vectF_coupleF :
   (O A0 A1 : E), vectF O (coupleF A0 A1) = coupleF (O --> A0) (O --> A1).
Proof.
intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
rewrite vectF_correct !coupleF_0; easy.
rewrite vectF_correct !coupleF_1; easy.
Qed.

Lemma vectF_tripleF :
   (O A0 A1 A2 : E),
    vectF O (tripleF A0 A1 A2) = tripleF (O --> A0) (O --> A1) (O --> A2).
Proof.
intros; apply extF; intros i;
    destruct (ord3_dec i) as [[Hi | Hi] | Hi]; rewrite Hi vectF_correct.
rewrite !tripleF_0; easy.
rewrite !tripleF_1; easy.
rewrite !tripleF_2; easy.
Qed.

Lemma vectF_invalF :
   {n1 n2} O (A1 : 'E^n1) (A2 : 'E^n2),
    invalF (vectF O A1) (vectF O A2) invalF A1 A2.
Proof.
intros; split; intros HA i1; destruct (HA i1) as [i2 Hi2]; i2.
apply (vect_l_inj O); easy.
rewrite !vectF_correct Hi2; easy.
Qed.

Lemma vectF_insertF :
   {n} O (A : 'E^n) Ai0 i0,
    vectF O (insertF A Ai0 i0) = insertF (vectF O A) (O --> Ai0) i0.
Proof.
intros n O A Ai0 i0; apply extF; intros i;
    destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite vectF_correct !insertF_correct_l; easy.
rewrite vectF_correct !insertF_correct_r; easy.
Qed.

Lemma vectF_skipF :
   {n} O (A : 'E^n.+1) i0,
    vectF O (skipF A i0) = skipF (vectF O A) i0.
Proof.
intros n O A i0; apply extF; intros j; destruct (lt_dec j i0) as [Hj | Hj].
rewrite vectF_correct !skipF_correct_l; easy.
rewrite vectF_correct !skipF_correct_r; easy.
Qed.

Lemma vectF_permutF :
   {n} p O (A : 'E^n), vectF O (permutF p A) = permutF p (vectF O A).
Proof. easy. Qed.

Lemma vectF_revF :
   {n} O (A : 'E^n), vectF O (revF A) = revF (vectF O A).
Proof. easy. Qed.

Lemma vectF_moveF :
   {n} O (A : 'E^n.+1) i0 i1,
    vectF O (moveF A i0 i1) = moveF (vectF O A) i0 i1.
Proof. easy. Qed.

Lemma vectF_transpF :
   {n} O (A : 'E^n) i0 i1,
    vectF O (transpF A i0 i1) = transpF (vectF O A) i0 i1.
Proof. easy. Qed.

Lemma vectF_filterPF :
   {n} P O (A : 'E^n), vectF O (filterPF P A) = filterPF P (vectF O A).
Proof. easy. Qed.

Lemma vectF_concatnF :
   {n} {b : 'nat^n} (O : E) (A : i, 'E^(b i)),
    vectF O (concatnF A) = concatnF (fun ivectF O (A i)).
Proof.
intros; apply extF; intros k; rewrite (splitn_ord k).
rewrite vectF_correct !concatn_ord_correct; easy.
Qed.

Lemma translF_vectF :
   {n} (O : E), cancel (@vectF _ _ _ n O) (translF O).
Proof.
move=>>; apply extF; intro; rewrite translF_correct vectF_correct.
apply transl_correct_l.
Qed.

Lemma vectF_translF :
   {n} (O : E), cancel (@translF _ _ _ n O) (vectF O).
Proof.
move=>>; apply extF; intro; rewrite vectF_correct translF_correct.
apply transl_correct_r.
Qed.

Lemma translF_assoc :
   {n} (O : E) (u v : 'V^n), (translF O u) +++ v = translF O (u + v).
Proof.
intros n O u v; rewrite -(translF_vectF O (_ +++ _)).
rewrite -(vectF_chasles _ (translF O u)) vectF_translF transl_correct_r; easy.
Qed.

Lemma translF_zero : {n} (O : E), translF O 0 = constF n O.
Proof. intros; apply extF; intro; rewrite translF_correct transl_zero //. Qed.

Lemma translF_zero_equiv :
   {n} (O : E) u, translF O u = constF n O u = 0.
Proof. intros; rewrite -vectF_zero_equiv vectF_translF; easy. Qed.

Lemma translF_l_eq :
   {n} (O : E) (u1 u2 : 'V^n), u1 = u2 translF O u1 = translF O u2.
Proof. intros; subst; easy. Qed.

Lemma translF_r_eq :
   {n} (u : 'V^n) (O1 O2 : E), O1 = O2 translF O1 u = translF O2 u.
Proof. intros; subst; easy. Qed.

Lemma translF_l_inj :
   {n} (O : E) (u1 u2 : 'V^n), translF O u1 = translF O u2 u1 = u2.
Proof.
intros n O u1 u2 H; rewrite -(vectF_translF O u1) -(vectF_translF O u2).
apply vectF_l_eq; easy.
Qed.

Lemma translF_r_inj :
   {n} (u : 'V^n.+1) (O1 O2 : E), translF O1 u = translF O2 u O1 = O2.
Proof.
intros n u O1 O2 H; apply constF_inj with n.
rewrite -(translF_zero O1) -(translF_zero O2) -(plus_opp_r u) -!translF_assoc.
rewrite H; easy.
Qed.

Lemma translF_l_inj_equiv :
   {n} (O : E) (u1 u2 : 'V^n), translF O u1 = translF O u2 u1 = u2.
Proof. intros; split. apply translF_l_inj. apply translF_l_eq. Qed.

Lemma translF_r_inj_equiv :
   {n} (u : 'V^n.+1) (O1 O2 : E),
    translF O1 u = translF O2 u O1 = O2.
Proof. intros; split. apply translF_r_inj. apply translF_r_eq. Qed.

Lemma translF_vectF_equiv :
   {n} O (A : 'E^n) u, A = translF O u u = vectF O A.
Proof. intros; erewrite <- vectF_l_inj_equiv, vectF_translF; easy. Qed.

Lemma translF_l_bij : {n} (O : E), bijective (@translF _ _ _ n O).
Proof.
intros n O; apply (bij_can_bij (vectF_l_bij O)); apply translF_vectF.
Qed.

Lemma translF_l_bij_ex : {n} O (A : 'E^n), ! u, translF O u = A.
Proof. intros; apply bij_ex_uniq, translF_l_bij. Qed.

Lemma translF_inj_equiv :
   {n} (O : E) (u : 'V^n), injective (translF O u) injective u.
Proof.
intros n O u; split; intros Hu i1 i2 H; apply Hu;
    [rewrite translF_correct H | apply (transl_l_inj O)]; easy.
Qed.

Lemma translF_constF :
   {n} (O : E) u, translF O (constF n u) = constF n (O +++ u).
Proof.
intros; apply extF; intro; rewrite translF_correct !constF_correct; easy.
Qed.

Lemma translF_w_zero_struct_r :
   {n} (O O' : E) (u : 'V^n), zero_struct K translF O u = constF n O'.
Proof.
intros n O O' u HK; move: (@ms_w_zero_struct_r _ V HK) ⇒ HV.
apply eq_sym, translF_vectF_equiv, extF; intros i.
rewrite vectF_w_zero_struct_r; easy.
Qed.

Lemma translF_singleF :
   (O : E) u0, translF O (singleF u0) = singleF (O +++ u0).
Proof.
intros; apply extF; intro; rewrite I_1_is_unit translF_correct !singleF_0; easy.
Qed.

Lemma translF_coupleF :
   (O : E) u0 u1, translF O (coupleF u0 u1) = coupleF (O +++ u0) (O +++ u1).
Proof.
intros; apply extF; intros i; destruct (ord2_dec i) as [Hi | Hi]; rewrite Hi.
rewrite translF_correct !coupleF_0; easy.
rewrite translF_correct !coupleF_1; easy.
Qed.

Lemma translF_tripleF :
   (O : E) u0 u1 u2,
    translF O (tripleF u0 u1 u2) = tripleF (O +++ u0) (O +++ u1) (O +++ u2).
Proof.
intros; apply extF; intros i;
    destruct (ord3_dec i) as [[Hi | Hi] | Hi]; rewrite Hi translF_correct.
rewrite !tripleF_0; easy.
rewrite !tripleF_1; easy.
rewrite !tripleF_2; easy.
Qed.

Lemma translF_invalF :
   {n1 n2} (O : E) (u1 : 'V^n1) (u2 : 'V^n2),
    invalF (translF O u1) (translF O u2) invalF u1 u2.
Proof.
intros; split; intros Hu i1; destruct (Hu i1) as [i2 Hi2]; i2.
apply (transl_l_inj O); easy.
rewrite !translF_correct Hi2; easy.
Qed.

Lemma translF_insertF :
   {n} (O : E) (u : 'V^n) u0 i0,
    translF O (insertF u u0 i0) = insertF (translF O u) (O +++ u0) i0.
Proof.
intros n O u u0 i0; apply extF; intros i; destruct (ord_eq_dec i i0) as [Hi | Hi].
rewrite translF_correct !insertF_correct_l; easy.
rewrite translF_correct !insertF_correct_r; easy.
Qed.

Lemma translF_skipF :
   {n} (O : E) (u : 'V^n.+1) i0,
    translF O (skipF u i0) = skipF (translF O u) i0.
Proof.
intros n O A i0; apply extF; intros j; destruct (lt_dec j i0) as [Hj | Hj].
rewrite translF_correct !skipF_correct_l; easy.
rewrite translF_correct !skipF_correct_r; easy.
Qed.

Lemma translF_permutF :
   {n} p (O : E) (u : 'V^n),
    translF O (permutF p u) = permutF p (translF O u).
Proof. easy. Qed.

Lemma translF_revF :
   {n} (O : E) (u : 'V^n), translF O (revF u) = revF (translF O u).
Proof. easy. Qed.

Lemma translF_moveF :
   {n} (O : E) (u : 'V^n.+1) i0 i1,
    translF O (moveF u i0 i1) = moveF (translF O u) i0 i1.
Proof. easy. Qed.

Lemma translF_transpF :
   {n} (O : E) (u : 'V^n) i0 i1,
    translF O (transpF u i0 i1) = transpF (translF O u) i0 i1.
Proof. easy. Qed.

Lemma translF_filterPF :
   {n} P (O : E) (u : 'V^n),
    translF O (filterPF P u) = filterPF P (translF O u).
Proof. easy. Qed.

Lemma translF_concatnF :
   {n} {b : 'nat^n} (O : E) (u : i, 'V^(b i)),
    translF O (concatnF u) = concatnF (fun itranslF O (u i)).
Proof.
intros; apply extF; intros k; rewrite (splitn_ord k).
rewrite translF_correct !concatn_ord_correct; easy.
Qed.

Lemma frameF_inv_frameF :
   {n} (O : E) (u : 'V^n) i0, frameF (inv_frameF O u i0) i0 = u.
Proof.
intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
rewrite translF_correct (insertF_correct_l _ _ (erefl _)).
rewrite -{1}(transl_zero O) translF_insertF skipF_insertF; easy.
Qed.

Lemma inv_frameF_frameF :
   {n} (A : 'E^n.+1) i0, inv_frameF (A i0) (frameF A i0) i0 = A.
Proof.
intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
rewrite -(vect_zero (A i0)) -vectF_insertF insertF_skipF; easy.
Qed.

Lemma frameF_inj_equiv :
   {n} (A : 'E^n.+1) i0,
    injective (frameF A i0) injective (skipF A i0).
Proof. move=>>; apply vectF_inj_equiv. Qed.

Lemma inv_frameF_inj_equiv :
   {n} (O : E) (u : 'V^n) i0,
    injective (skipF (inv_frameF O u i0) i0) injective u.
Proof. move=>>; rewrite -frameF_inj_equiv frameF_inv_frameF; easy. Qed.

Lemma frameF_inclF :
   {PE : E Prop} {n} {A : 'E^n.+1} i0,
    inclF A PE inclF (frameF A i0) (preimage (transl (A i0)) PE).
Proof.
move=>> HA i; unfold preimage, frameF.
rewrite vectF_correct transl_correct_l.
apply: (inclF_monot_l _ _ _ _ HA); try easy.
apply skipF_monot_l, invalF_refl.
Qed.

Lemma frameF_invalF :
   {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
    A1 i1 = A2 i2
    invalF (skipF A1 i1) (skipF A2 i2) invalF (frameF A1 i1) (frameF A2 i2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.

Lemma frameF_invalF_rev :
   {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
    A1 i1 = A2 i2
    invalF (frameF A1 i1) (frameF A2 i2) invalF (skipF A1 i1) (skipF A2 i2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.

Lemma frameF_invalF_equiv :
   {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2,
    A1 i1 = A2 i2
    invalF (frameF A1 i1) (frameF A2 i2)
    invalF (skipF A1 i1) (skipF A2 i2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.

Lemma frameF_skipF :
   {n} (A : 'E^n.+2) {i0 i1} (H10 : i1 i0) (H01 : i0 i1),
    frameF (skipF A i0) (insert_ord H10) =
      skipF (frameF A i1) (insert_ord H01).
Proof.
intros n A i0 i1 H10 H01; unfold frameF.
rewrite -vectF_skipF (skipF_correct_alt H10); [| apply skip_insert_ord].
rewrite -skip2F_correct skip2F_equiv_def; easy.
Qed.

Lemma frameF_skipF_alt :
   {n} (A : 'E^n.+2) {i0 i1} {H10 : i1 i0},
    frameF (skipF A i0) (insert_ord H10) =
      skipF (frameF A i1) (insert_ord (not_eq_sym H10)).
Proof. intros; apply frameF_skipF. Qed.

Lemma frameF_permutF :
   {n} {A : 'E^n.+1} {i0} {p} (Hp : injective p),
    frameF (permutF p A) i0 = permutF (skip_f_ord Hp i0) (frameF A (p i0)).
Proof. intros; unfold frameF; rewrite skipF_permutF; easy. Qed.

Context {V1 V2 : ModuleSpace K}.
Context {E1 : AffineSpace V1}.
Context {E2 : AffineSpace V2}.

Lemma vectF_mapF :
   {n} O1 (A1 : 'E1^n) (f : E1 E2),
    vectF O1 (mapF f A1) = mapF (fun A1iO1 --> f A1i) A1.
Proof. easy. Qed.

Lemma translF_mapF :
   {n} (O2 : E2) (u1 : 'V1^n) (f : V1 V2),
    translF O2 (mapF f u1) = mapF (fun u1iO2 +++ f u1i) u1.
Proof. easy. Qed.

Lemma fct_vectF_eq :
   {T : Type} {n} (fO : T E) (fA : '(T E)^n) t,
    (vectF fO fA)^~ t = vectF (fO t) (fA^~ t).
Proof. easy. Qed.

Lemma fct_translF_eq :
   {T : Type} {n} (fO : T E) (fu : '(T V)^n) t,
    (translF fO fu)^~ t = translF (fO t) (fu^~ t).
Proof.
intros; apply extF; intro; rewrite !translF_correct; apply fct_transl_eq.
Qed.

End FF_AffineSpace_Facts.