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.
Support finite families on affine spaces.
Let K : Ring, V : ModuleSpace K and E : AffineSpace V.
Let O : E, A : 'E^n, B : 'E^n.+1 and u : 'V^n.
This module may be used through the import of Algebra.AffineSpace.AffineSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Operator
- vectF O A is the n-family of V with i-th item vect O (A i);
- translF O u is the n-family of E with i-th item transl O (u i);
- frameF B i0 is the n-family vectF (B i0) (skipF B i0);
- inv_frameF O u i0 is the n-family translF O (insertF u 0 i0).
Used logic axioms
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 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.
move⇒ B /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.
move⇒ n 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 i ⇒ vectF 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 i ⇒ translF 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 A1i ⇒ O1 --> 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 u1i ⇒ O2 +++ 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.