Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • mayero/coq-num-analysis
  • hamelin/test-ci-coq-num-analysis
  • arias/coq-num-analysis
3 results
Show changes
Commits on Source (3)
Hide whitespace changes
Inline Side-by-side
Showing
with 317 additions and 313 deletions
Algebra/AffineSpace/AffineSpace_FF.v
View file @ 5ba16a8b
...@@ -30,7 +30,7 @@ COPYING file for more details. ...@@ -30,7 +30,7 @@ COPYING file for more details.
- [vectF O A] is the [n]-family of [V] with [i]-th item [vect O (A i)]; - [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)]; - [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)]; - [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 i0 0 u)]. - [inv_frameF O i0 u] is the [n]-family [translF O (insert0F i0 u)].
* Used logic axioms * Used logic axioms
...@@ -67,9 +67,9 @@ Context {E : AffineSpace V}. ...@@ -67,9 +67,9 @@ Context {E : AffineSpace V}.
Definition vectF {n} O (A : 'E^n) : 'V^n := mapF (vect O) A. 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 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 i0 A). Definition frameF {n} i0 (A : 'E^n.+1) : 'V^n := vectF (A i0) (skipF i0 A).
Definition inv_frameF {n} O (u : 'V^n) i0 : 'E^n.+1 := Definition inv_frameF {n} i0 O (u : 'V^n) : 'E^n.+1 :=
translF O (insertF i0 0 u). translF O (insert0F i0 u).
(** Correctness lemmas. *) (** Correctness lemmas. *)
...@@ -80,13 +80,13 @@ Lemma translF_correct : forall {n} O (u : 'V^n) i, translF O u i = O +++ u i. ...@@ -80,13 +80,13 @@ Lemma translF_correct : forall {n} O (u : 'V^n) i, translF O u i = O +++ u i.
Proof. easy. Qed. Proof. easy. Qed.
Lemma frameF_correct : Lemma frameF_correct :
forall {n} (A : 'E^n.+1) i0 i (H : i <> i0), forall {n i0 i} (H : i <> i0) (A : 'E^n.+1),
frameF A i0 (insert_ord H) = A i0 --> A i. frameF i0 A (insert_ord H) = A i0 --> A i.
Proof. intros; unfold frameF; rewrite vectF_correct skipF_correct; easy. Qed. Proof. intros; unfold frameF; rewrite vectF_correct skipF_correct; easy. Qed.
Lemma inv_frameF_correct : Lemma inv_frameF_correct :
forall {n} (O : E) (u : 'V^n) i0 j, forall {n} i0 j (O : E) (u : 'V^n),
inv_frameF O u i0 (skip_ord i0 j) = O +++ u j. inv_frameF i0 O u (skip_ord i0 j) = O +++ u j.
Proof. Proof.
intros; unfold inv_frameF; rewrite translF_correct insertF_correct; easy. intros; unfold inv_frameF; rewrite translF_correct insertF_correct; easy.
Qed. Qed.
...@@ -221,19 +221,19 @@ rewrite !vectF_correct Hi2; easy. ...@@ -221,19 +221,19 @@ rewrite !vectF_correct Hi2; easy.
Qed. Qed.
Lemma vectF_insertF : Lemma vectF_insertF :
forall {n} O (A : 'E^n) Ai0 i0, forall {n} O i0 Ai0 (A : 'E^n),
vectF O (insertF i0 Ai0 A) = insertF i0 (O --> Ai0) (vectF O A). vectF O (insertF i0 Ai0 A) = insertF i0 (O --> Ai0) (vectF O A).
Proof. Proof.
intros n O A Ai0 i0; extF i; destruct (ord_eq_dec i i0). intros n O i0 Ai0 A; extF i; destruct (ord_eq_dec i i0).
rewrite vectF_correct !insertF_correct_l; easy. rewrite vectF_correct !insertF_correct_l; easy.
rewrite vectF_correct !insertF_correct_r; easy. rewrite vectF_correct !insertF_correct_r; easy.
Qed. Qed.
Lemma vectF_skipF : Lemma vectF_skipF :
forall {n} O (A : 'E^n.+1) i0, forall {n} O i0 (A : 'E^n.+1),
vectF O (skipF i0 A) = skipF i0 (vectF O A). vectF O (skipF i0 A) = skipF i0 (vectF O A).
Proof. Proof.
intros n O A i0; extF j; destruct (lt_dec j i0). intros n O i0 A; extF j; destruct (lt_dec j i0).
rewrite vectF_correct !skipF_correct_l; easy. rewrite vectF_correct !skipF_correct_l; easy.
rewrite vectF_correct !skipF_correct_r; easy. rewrite vectF_correct !skipF_correct_r; easy.
Qed. Qed.
...@@ -400,19 +400,19 @@ rewrite !translF_correct Hi2; easy. ...@@ -400,19 +400,19 @@ rewrite !translF_correct Hi2; easy.
Qed. Qed.
Lemma translF_insertF : Lemma translF_insertF :
forall {n} (O : E) (u : 'V^n) u0 i0, forall {n} (O : E) i0 u0 (u : 'V^n),
translF O (insertF i0 u0 u) = insertF i0 (O +++ u0) (translF O u). translF O (insertF i0 u0 u) = insertF i0 (O +++ u0) (translF O u).
Proof. Proof.
intros n O u u0 i0; extF i; destruct (ord_eq_dec i i0). intros n O i0 u0 u; extF i; destruct (ord_eq_dec i i0).
rewrite translF_correct !insertF_correct_l; easy. rewrite translF_correct !insertF_correct_l; easy.
rewrite translF_correct !insertF_correct_r; easy. rewrite translF_correct !insertF_correct_r; easy.
Qed. Qed.
Lemma translF_skipF : Lemma translF_skipF :
forall {n} (O : E) (u : 'V^n.+1) i0, forall {n} (O : E) i0 (u : 'V^n.+1),
translF O (skipF i0 u) = skipF i0 (translF O u). translF O (skipF i0 u) = skipF i0 (translF O u).
Proof. Proof.
intros n O A i0; extF j; destruct (lt_dec j i0). intros n O i0 u; extF j; destruct (lt_dec j i0).
rewrite translF_correct !skipF_correct_l; easy. rewrite translF_correct !skipF_correct_l; easy.
rewrite translF_correct !skipF_correct_r; easy. rewrite translF_correct !skipF_correct_r; easy.
Qed. Qed.
...@@ -450,7 +450,7 @@ rewrite translF_correct !concatn_ord_correct; easy. ...@@ -450,7 +450,7 @@ rewrite translF_correct !concatn_ord_correct; easy.
Qed. Qed.
Lemma frameF_inv_frameF : Lemma frameF_inv_frameF :
forall {n} (O : E) (u : 'V^n) i0, frameF (inv_frameF O u i0) i0 = u. forall {n} i0 (O : E) (u : 'V^n), frameF i0 (inv_frameF i0 O u) = u.
Proof. Proof.
intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv. intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
rewrite translF_correct (insertF_correct_l _ _ (erefl _)). rewrite translF_correct (insertF_correct_l _ _ (erefl _)).
...@@ -458,26 +458,26 @@ rewrite -{1}(transl_zero O) translF_insertF skipF_insertF; easy. ...@@ -458,26 +458,26 @@ rewrite -{1}(transl_zero O) translF_insertF skipF_insertF; easy.
Qed. Qed.
Lemma inv_frameF_frameF : Lemma inv_frameF_frameF :
forall {n} (A : 'E^n.+1) i0, inv_frameF (A i0) (frameF A i0) i0 = A. forall {n} i0 (A : 'E^n.+1), inv_frameF i0 (A i0) (frameF i0 A) = A.
Proof. Proof.
intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv. intros; unfold frameF, inv_frameF; apply eq_sym, translF_vectF_equiv.
rewrite -(vect_zero (A i0)) -vectF_insertF insertF_skipF; easy. rewrite -(vect_zero (A i0)) -vectF_insertF insertF_skipF; easy.
Qed. Qed.
Lemma frameF_inj_equiv : Lemma frameF_inj_equiv :
forall {n} (A : 'E^n.+1) i0, forall {n} i0 (A : 'E^n.+1),
injective (frameF A i0) <-> injective (skipF i0 A). injective (frameF i0 A) <-> injective (skipF i0 A).
Proof. move=>>; apply vectF_inj_equiv. Qed. Proof. move=>>; apply vectF_inj_equiv. Qed.
Lemma inv_frameF_inj_equiv : Lemma inv_frameF_inj_equiv :
forall {n} (O : E) (u : 'V^n) i0, forall {n} i0 (O : E) (u : 'V^n),
injective (skipF i0 (inv_frameF O u i0)) <-> injective u. injective (skipF i0 (inv_frameF i0 O u)) <-> injective u.
Proof. move=>>; rewrite -frameF_inj_equiv frameF_inv_frameF; easy. Qed. Proof. move=>>; rewrite -frameF_inj_equiv frameF_inv_frameF; easy. Qed.
(* (preimage (transl (A i0)) PE) will be (vectP PE (A i0)) below *) (* (preimage (transl (A i0)) PE) will be (vectP PE (A i0)) below *)
Lemma frameF_inclF : Lemma frameF_inclF :
forall {PE : E -> Prop} {n} {A : 'E^n.+1} i0, forall {PE : E -> Prop} {n} i0 {A : 'E^n.+1},
inclF A PE -> inclF (frameF A i0) (preimage (transl (A i0)) PE). inclF A PE -> inclF (frameF i0 A) (preimage (transl (A i0)) PE).
Proof. Proof.
move=>> HA i; unfold preimage, frameF. move=>> HA i; unfold preimage, frameF.
rewrite vectF_correct transl_correct_l. rewrite vectF_correct transl_correct_l.
...@@ -486,70 +486,67 @@ apply skipF_monot_l, invalF_refl. ...@@ -486,70 +486,67 @@ apply skipF_monot_l, invalF_refl.
Qed. Qed.
Lemma frameF_invalF : Lemma frameF_invalF :
forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2, forall {n1 n2} i1 i2 (A1 : 'E^n1.+1) (A2 : 'E^n2.+1),
A1 i1 = A2 i2 -> A1 i1 = A2 i2 ->
invalF (skipF i1 A1) (skipF i2 A2) -> invalF (frameF A1 i1) (frameF A2 i2). invalF (skipF i1 A1) (skipF i2 A2) -> invalF (frameF i1 A1) (frameF i2 A2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed. Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.
Lemma frameF_invalF_rev : Lemma frameF_invalF_rev :
forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2, forall {n1 n2} i1 i2 (A1 : 'E^n1.+1) (A2 : 'E^n2.+1),
A1 i1 = A2 i2 -> A1 i1 = A2 i2 ->
invalF (frameF A1 i1) (frameF A2 i2) -> invalF (skipF i1 A1) (skipF i2 A2). invalF (frameF i1 A1) (frameF i2 A2) -> invalF (skipF i1 A1) (skipF i2 A2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed. Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.
Lemma frameF_invalF_equiv : Lemma frameF_invalF_equiv :
forall {n1 n2} (A1 : 'E^n1.+1) (A2 : 'E^n2.+1) i1 i2, forall {n1 n2} i1 i2 (A1 : 'E^n1.+1) (A2 : 'E^n2.+1),
A1 i1 = A2 i2 -> A1 i1 = A2 i2 ->
invalF (frameF A1 i1) (frameF A2 i2) <-> invalF (frameF i1 A1) (frameF i2 A2) <->
invalF (skipF i1 A1) (skipF i2 A2). invalF (skipF i1 A1) (skipF i2 A2).
Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed. Proof. move=>> H; unfold frameF; rewrite H; apply vectF_invalF. Qed.
Lemma frameF_1 : forall (A : 'E^1), frameF A ord0 = 0. Lemma frameF_1 : forall (A : 'E^1), frameF ord0 A = 0.
Proof. intros; unfold frameF, vectF; apply mapF_nil; easy. Qed. Proof. intros; unfold frameF, vectF; apply mapF_nil; easy. Qed.
Lemma frameF_singleF : forall (A : E), frameF (singleF A) ord0 = 0. Lemma frameF_singleF : forall (A : E), frameF ord0 (singleF A) = 0.
Proof. intros; apply frameF_1. Qed. Proof. intros; apply frameF_1. Qed.
Lemma frameF_2_0 : Lemma frameF_2_0 :
forall (A : 'E^2), frameF A ord0 ord0 = A ord0 --> A ord_max. forall (A : 'E^2), frameF ord0 A ord0 = A ord0 --> A ord_max.
Proof. Proof.
intros; rewrite -(frameF_correct _ _ _ ord_max_not_0) intros; rewrite -(frameF_correct ord_max_not_0) insert_ord_max ord_one; easy.
insert_ord_max ord_one; easy.
Qed. Qed.
Lemma frameF_2_1 : Lemma frameF_2_1 :
forall (A : 'E^2), frameF A ord_max ord0 = A ord_max --> A ord0. forall (A : 'E^2), frameF ord_max A ord0 = A ord_max --> A ord0.
Proof. Proof. intros; rewrite -(frameF_correct ord_0_not_max) insert_ord_0; easy. Qed.
intros; rewrite -(frameF_correct _ _ _ ord_0_not_max) insert_ord_0; easy.
Qed.
Lemma frameF_coupleF_0 : Lemma frameF_coupleF_0 :
forall (A B : E), frameF (coupleF A B) ord0 ord0 = A --> B. forall (A B : E), frameF ord0 (coupleF A B) ord0 = A --> B.
Proof. intros; rewrite frameF_2_0 coupleF_0 coupleF_1; easy. Qed. Proof. intros; rewrite frameF_2_0 coupleF_0 coupleF_1; easy. Qed.
Lemma frameF_coupleF_1 : Lemma frameF_coupleF_1 :
forall (A B : E), frameF (coupleF A B) ord_max ord0 = B --> A. forall (A B : E), frameF ord_max (coupleF A B) ord0 = B --> A.
Proof. intros; rewrite frameF_2_1 coupleF_0 coupleF_1; easy. Qed. Proof. intros; rewrite frameF_2_1 coupleF_0 coupleF_1; easy. Qed.
Lemma frameF_skipF : Lemma frameF_skipF :
forall {n} (A : 'E^n.+2) {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1), forall {n} {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1) (A : 'E^n.+2),
frameF (skipF i0 A) (insert_ord H10) = frameF (insert_ord H10) (skipF i0 A) =
skipF (insert_ord H01) (frameF A i1). skipF (insert_ord H01) (frameF i1 A).
Proof. Proof.
intros n A i0 i1 H10 H01; unfold frameF. intros n i0 i1 H10 H01 A; unfold frameF.
rewrite -vectF_skipF (skipF_correct_alt H10); [| apply skip_insert_ord]. rewrite -vectF_skipF (skipF_correct_alt H10); [| apply skip_insert_ord].
rewrite -skip2F_correct skip2F_equiv_def; easy. rewrite -skip2F_correct skip2F_equiv_def; easy.
Qed. Qed.
Lemma frameF_skipF_alt : Lemma frameF_skipF_alt :
forall {n} (A : 'E^n.+2) {i0 i1} {H10 : i1 <> i0}, forall {n} {i0 i1} {H10 : i1 <> i0} (A : 'E^n.+2),
frameF (skipF i0 A) (insert_ord H10) = frameF (insert_ord H10) (skipF i0 A) =
skipF (insert_ord (not_eq_sym H10)) (frameF A i1). skipF (insert_ord (not_eq_sym H10)) (frameF i1 A).
Proof. intros; apply frameF_skipF. Qed. Proof. intros; apply frameF_skipF. Qed.
Lemma frameF_permutF : Lemma frameF_permutF :
forall {n} {A : 'E^n.+1} {i0} {p} (Hp : injective p), forall {n i0 p} (Hp : injective p) {A : 'E^n.+1},
frameF (permutF p A) i0 = permutF (skip_f_ord Hp i0) (frameF A (p i0)). frameF i0 (permutF p A) = permutF (skip_f_ord Hp i0) (frameF (p i0) A).
Proof. intros; unfold frameF; rewrite skipF_permutF; easy. Qed. Proof. intros; unfold frameF; rewrite skipF_permutF; easy. Qed.
Context {V1 V2 : ModuleSpace K}. Context {V1 V2 : ModuleSpace K}.
...@@ -577,9 +574,9 @@ Lemma fct_translF_eq : ...@@ -577,9 +574,9 @@ Lemma fct_translF_eq :
Proof. intros; extF; rewrite !translF_correct; apply fct_transl_eq. Qed. Proof. intros; extF; rewrite !translF_correct; apply fct_transl_eq. Qed.
Lemma frameF_mapF : Lemma frameF_mapF :
forall {n} {A1 : 'E1^n.+1} {i0} {f : E1 -> E2}, forall {n i0} {f : E1 -> E2} {A1 : 'E1^n.+1},
frameF (mapF f A1) i0 = frameF i0 (mapF f A1) =
mapF (vect (f (A1 i0)) \o f \o transl (A1 i0)) (frameF A1 i0). mapF (vect (f (A1 i0)) \o f \o transl (A1 i0)) (frameF i0 A1).
Proof. Proof.
intros; unfold frameF; rewrite mapF_correct -mapF_skipF. intros; unfold frameF; rewrite mapF_correct -mapF_skipF.
unfold vectF; rewrite -2!mapF_comp {1}comp_assoc -(comp_assoc (vect _)). unfold vectF; rewrite -2!mapF_comp {1}comp_assoc -(comp_assoc (vect _)).
...@@ -602,16 +599,16 @@ Lemma translF_ms_eq : ...@@ -602,16 +599,16 @@ Lemma translF_ms_eq :
Proof. intros; extF; rewrite translF_correct ms_transl_eq; easy. Qed. Proof. intros; extF; rewrite translF_correct ms_transl_eq; easy. Qed.
Lemma frameF_ms_eq : Lemma frameF_ms_eq :
forall {n} (A : 'V^n.+1) i0, frameF A i0 = skipF i0 A - constF n (A i0). forall {n} i0 (A : 'V^n.+1), frameF i0 A = skipF i0 A - constF n (A i0).
Proof. intros; unfold frameF; rewrite vectF_ms_eq; easy. Qed. Proof. intros; unfold frameF; rewrite vectF_ms_eq; easy. Qed.
Lemma inv_frameF_ms_eq : Lemma inv_frameF_ms_eq :
forall {n} (u : 'V^n) (O : V) i0, forall {n} i0 (O : V) (u : 'V^n),
inv_frameF O u i0 = constF n.+1 O + insertF i0 0 u. inv_frameF i0 O u = constF n.+1 O + insert0F i0 u.
Proof. intros; unfold inv_frameF; rewrite translF_ms_eq; easy. Qed. Proof. intros; unfold inv_frameF; rewrite translF_ms_eq; easy. Qed.
Lemma injF_ms_equiv : Lemma injF_ms_equiv :
forall {n} (A : 'V^n.+1), injective A <-> forall i0, ~ inF 0 (frameF A i0). forall {n} (A : 'V^n.+1), injective A <-> forall i0, ~ inF 0 (frameF i0 A).
Proof. Proof.
intros n A; rewrite injF_g_equiv; split; intros H i0; intros n A; rewrite injF_g_equiv; split; intros H i0;
[rewrite frameF_ms_eq | rewrite -frameF_ms_eq]; easy. [rewrite frameF_ms_eq | rewrite -frameF_ms_eq]; easy.
......
Algebra/AffineSpace/AffineSpace_aff_map.v
View file @ 5ba16a8b
...@@ -357,11 +357,11 @@ Context {V : ModuleSpace K}. ...@@ -357,11 +357,11 @@ Context {V : ModuleSpace K}.
Context {E : AffineSpace V}. Context {E : AffineSpace V}.
Lemma insertF_fct_lm : Lemma insertF_fct_lm :
forall {n} x0 i0, forall {n} i0 x0,
fct_lm (fun A : 'E^n => insertF i0 x0 A) (constF n x0) = fct_lm (fun A : 'E^n => insertF i0 x0 A) (constF n x0) =
(fun u : 'V^n => insert0F i0 u). (fun u : 'V^n => insert0F i0 u).
Proof. Proof.
intros n x0 i0; unfold fct_lm; fun_ext u; extF i. intros n i0 x0; unfold fct_lm; fun_ext u; extF i.
rewrite fct_vect_eq insertF_constF constF_correct. rewrite fct_vect_eq insertF_constF constF_correct.
destruct (ord_eq_dec i i0) as [-> | Hi]. destruct (ord_eq_dec i i0) as [-> | Hi].
rewrite !insertF_correct_l//; apply vect_zero. rewrite !insertF_correct_l//; apply vect_zero.
...@@ -369,9 +369,9 @@ rewrite !insertF_correct_r fct_transl_eq constF_correct transl_correct_r; easy. ...@@ -369,9 +369,9 @@ rewrite !insertF_correct_r fct_transl_eq constF_correct transl_correct_r; easy.
Qed. Qed.
Lemma insertF_am : Lemma insertF_am :
forall {n} x0 i0, aff_map (fun A : 'E^n => insertF i0 x0 A). forall {n} i0 x0, aff_map (fun A : 'E^n => insertF i0 x0 A).
Proof. Proof.
intros n x0 i0; apply (am_lm (constF _ x0)). intros n i0 x0; apply (am_lm (constF _ x0)).
rewrite insertF_fct_lm; apply insert0F_lm. rewrite insertF_fct_lm; apply insert0F_lm.
Qed. Qed.
...@@ -777,7 +777,7 @@ End ModuleSpace_AffineSpace_Morphism_R_Facts. ...@@ -777,7 +777,7 @@ End ModuleSpace_AffineSpace_Morphism_R_Facts.
Section Euclidean_space_AffineSpace_Morphism_Facts. Section Euclidean_space_AffineSpace_Morphism_Facts.
Lemma part1F_am : Lemma part1F_am :
forall {n} (i0 : 'I_n.+1), aff_map_ms (part1F^~ i0 : 'R^n -> 'R^n.+1). forall {n} (i0 : 'I_n.+1), aff_map_ms (part1F i0 : 'R^n -> 'R^n.+1).
Proof. intros; apply am_lm_0, part1F_fct_lm. Qed. Proof. intros; apply am_lm_0, part1F_fct_lm. Qed.
End Euclidean_space_AffineSpace_Morphism_Facts. End Euclidean_space_AffineSpace_Morphism_Facts.
......
Algebra/AffineSpace/AffineSpace_baryc.v
View file @ 5ba16a8b
...@@ -262,18 +262,18 @@ Proof. intros; f_equal; easy. Qed. ...@@ -262,18 +262,18 @@ Proof. intros; f_equal; easy. Qed.
Lemma isobaryc_correct : Lemma isobaryc_correct :
forall {n} (A : 'E^n), forall {n} (A : 'E^n),
invertible (plusn1 K n) -> aff_comb 1 A (isobarycenter A). invertible (plusn1 n : K) -> aff_comb 1 A (isobarycenter A).
Proof. intros; apply baryc_correct; easy. Qed. Proof. intros; apply baryc_correct; easy. Qed.
Lemma isobaryc_orig : Lemma isobaryc_orig :
forall {n} (A : 'E^n) O, forall {n} (A : 'E^n) O,
invertible (plusn1 K n) -> invertible (plusn1 n : K) ->
scal (plusn1 K n) (O --> isobarycenter A) = sum (vectF O A). scal (plusn1 n) (O --> isobarycenter A) = sum (vectF O A).
Proof. intros; rewrite -lc_ones_l; apply baryc_orig; easy. Qed. Proof. intros; rewrite -lc_ones_l; apply baryc_orig; easy. Qed.
Lemma isobaryc_equiv : Lemma isobaryc_equiv :
forall {n} (A : 'E^n) G, forall {n} (A : 'E^n) G,
invertible (plusn1 K n) -> invertible (plusn1 n : K) ->
G = isobarycenter A <-> aff_comb 1 A G. G = isobarycenter A <-> aff_comb 1 A G.
Proof. intros; apply baryc_equiv; easy. Qed. Proof. intros; apply baryc_equiv; easy. Qed.
...@@ -362,7 +362,7 @@ Qed. ...@@ -362,7 +362,7 @@ Qed.
Lemma transl_lc : Lemma transl_lc :
forall {n} i0 (A : E) L (u : 'V^n), forall {n} i0 (A : E) L (u : 'V^n),
A +++ lin_comb L u = barycenter (part1F L i0) (insertF i0 A (translF A u)). A +++ lin_comb L u = barycenter (part1F i0 L) (insertF i0 A (translF A u)).
Proof. Proof.
intros n i0 A L u; apply (baryc_orig_equiv A); intros n i0 A L u; apply (baryc_orig_equiv A);
rewrite sum_insertF_baryc; [apply invertible_one |]. rewrite sum_insertF_baryc; [apply invertible_one |].
...@@ -371,62 +371,62 @@ rewrite vect_zero scal_zero_r plus_zero_l vectF_translF; easy. ...@@ -371,62 +371,62 @@ rewrite vect_zero scal_zero_r plus_zero_l vectF_translF; easy.
Qed. Qed.
Lemma baryc_insertF : Lemma baryc_insertF :
forall {n} i0 O (A : 'E^n) L, forall {n} i0 O L (A : 'E^n),
barycenter (part1F L i0) (insertF i0 O A) = O +++ lin_comb L (vectF O A). barycenter (part1F i0 L) (insertF i0 O A) = O +++ lin_comb L (vectF O A).
Proof. intros; rewrite (transl_lc i0) translF_vectF; easy. Qed. Proof. intros; rewrite (transl_lc i0) translF_vectF; easy. Qed.
Lemma vectF_lc : Lemma vectF_lc :
forall {n} i0 O (A : 'E^n) L, forall {n} i0 O L (A : 'E^n),
lin_comb L (vectF O A) = O --> barycenter (part1F L i0) (insertF i0 O A). lin_comb L (vectF O A) = O --> barycenter (part1F i0 L) (insertF i0 O A).
Proof. Proof.
intros n i0 O A L; apply (transl_l_inj O). intros n i0 O L A; apply (transl_l_inj O).
rewrite -(baryc_insertF i0) transl_correct_l; easy. rewrite -(baryc_insertF i0) transl_correct_l; easy.
Qed. Qed.
Lemma vectF_lc_skipF : Lemma vectF_lc_skipF :
forall {n} i0 (A : 'E^n.+1) L, forall {n} i0 L (A : 'E^n.+1),
lin_comb L (vectF (A i0) A) = lin_comb L (vectF (A i0) A) =
lin_comb (skipF i0 L) (vectF (A i0) (skipF i0 A)). lin_comb (skipF i0 L) (vectF (A i0) (skipF i0 A)).
Proof. Proof.
intros n i0 A L; rewrite (lc_skipF i0) vectF_correct vect_zero intros n i0 L A; rewrite (lc_skipF i0) vectF_correct vect_zero
scal_zero_r plus_zero_l; easy. scal_zero_r plus_zero_l; easy.
Qed. Qed.
Lemma vectF_lc_0 : Lemma vectF_lc_0 :
forall {n} (A : 'E^n.+1) L, forall {n} L (A : 'E^n.+1),
lin_comb L (vectF (A ord0) A) = lin_comb L (vectF (A ord0) A) =
lin_comb (liftF_S L) (vectF (A ord0) (liftF_S A)). lin_comb (liftF_S L) (vectF (A ord0) (liftF_S A)).
Proof. intros; rewrite -!skipF_first; apply vectF_lc_skipF. Qed. Proof. intros; rewrite -!skipF_first; apply vectF_lc_skipF. Qed.
Lemma vectF_lc_max : Lemma vectF_lc_max :
forall {n} (A : 'E^n.+1) L, forall {n} L (A : 'E^n.+1),
lin_comb L (vectF (A ord_max) A) = lin_comb L (vectF (A ord_max) A) =
lin_comb (widenF_S L) (vectF (A ord_max) (widenF_S A)). lin_comb (widenF_S L) (vectF (A ord_max) (widenF_S A)).
Proof. intros; rewrite -!skipF_last; apply vectF_lc_skipF. Qed. Proof. intros; rewrite -!skipF_last; apply vectF_lc_skipF. Qed.
Lemma frameF_lc : Lemma frameF_lc :
forall {n} {A : 'E^n.+1} {i0 L}, sum L = 1 -> forall {n i0 L} {A : 'E^n.+1}, sum L = 1 ->
lin_comb L (frameF A i0) = A i0 --> barycenter (part1F L i0) A. lin_comb L (frameF i0 A) = A i0 --> barycenter (part1F i0 L) A.
Proof. Proof.
intros n A i0 L HL; unfold frameF; rewrite (vectF_lc i0) insertF_skipF; easy. intros n i0 L A HL; unfold frameF; rewrite (vectF_lc i0) insertF_skipF; easy.
Qed. Qed.
Lemma baryc_frameF_equiv : Lemma baryc_frameF_equiv :
forall {n L} (A : 'E^n.+1) G i0, sum L = 1 -> forall {n} i0 {L} (A : 'E^n.+1) G, sum L = 1 ->
G = barycenter L A <-> A i0 --> G = lin_comb (skipF i0 L) (frameF A i0). G = barycenter L A <-> A i0 --> G = lin_comb (skipF i0 L) (frameF i0 A).
Proof. Proof.
intros n L A G i0 HL. intros n i0 L A G HL.
assert (HL0 : invertible (sum L)) by now apply invertible_eq_one. assert (HL0 : invertible (sum L)) by now apply invertible_eq_one.
rewrite (baryc_orig_equiv (A i0) _ HL0) HL scal_one_l// vectF_lc_skipF//. rewrite (baryc_orig_equiv (A i0) _ HL0) HL scal_one_l// vectF_lc_skipF//.
Qed. Qed.
Lemma barycenter2_r : Lemma barycenter2_r :
forall {n1 n2} L1 (A1 : 'E^n1) M12 (A2 : 'E^n2), forall {n1 n2} L1 M12 (A1 : 'E^n1) (A2 : 'E^n2),
invertible (sum L1) -> (forall i1, sum (M12 i1) = 1) -> invertible (sum L1) -> (forall i1, sum (M12 i1) = 1) ->
(forall i1, A1 i1 = barycenter (M12 i1) A2) -> (forall i1, A1 i1 = barycenter (M12 i1) A2) ->
barycenter L1 A1 = barycenter (fun i2 => lin_comb L1 (M12^~ i2)) A2. barycenter L1 A1 = barycenter (fun i2 => lin_comb L1 (M12^~ i2)) A2.
Proof. Proof.
intros n1 n2 L1 A1 M12 A2 HL1 HM12 HA1; pose (O := point_of_as E). intros n1 n2 L1 M12 A1 A2 HL1 HM12 HA1; pose (O := point_of_as E).
assert (HLM : sum (fun i2 => lin_comb L1 (M12^~ i2)) = sum L1). assert (HLM : sum (fun i2 => lin_comb L1 (M12^~ i2)) = sum L1).
rewrite -lc_sum_r (lc_ext_r 1). rewrite -lc_sum_r (lc_ext_r 1).
apply lc_ones_r. apply lc_ones_r.
...@@ -439,12 +439,12 @@ rewrite -(lc2_l_alt HA1'); apply baryc_orig; easy. ...@@ -439,12 +439,12 @@ rewrite -(lc2_l_alt HA1'); apply baryc_orig; easy.
Qed. Qed.
Lemma barycenter2_r_alt : Lemma barycenter2_r_alt :
forall {n1 n2} L1 (A1 : 'E^n1) M12 (A2 : 'E^n2), forall {n1 n2} L1 M12 (A1 : 'E^n1) (A2 : 'E^n2),
invertible (sum L1) -> (forall i1, sum (M12 i1) = 1) -> invertible (sum L1) -> (forall i1, sum (M12 i1) = 1) ->
(forall i1, A1 i1 = barycenter (M12 i1) A2) -> (forall i1, A1 i1 = barycenter (M12 i1) A2) ->
barycenter L1 A1 = barycenter (lin_comb L1 M12) A2. barycenter L1 A1 = barycenter (lin_comb L1 M12) A2.
Proof. Proof.
intros n1 n2 L1 A1 M12 A2 HL1 HM12 H; rewrite (barycenter2_r _ _ M12 A2)//. intros n1 n2 L1 M12 A1 A2 HL1 HM12 H; rewrite (barycenter2_r _ M12 _ A2)//.
f_equal; extF; apply eq_sym, fct_lc_r_eq. f_equal; extF; apply eq_sym, fct_lc_r_eq.
Qed. Qed.
...@@ -496,11 +496,11 @@ rewrite lc_3 3!vectF_correct 2!tripleF_0 2!tripleF_1 2!tripleF_2; easy. ...@@ -496,11 +496,11 @@ rewrite lc_3 3!vectF_correct 2!tripleF_0 2!tripleF_1 2!tripleF_2; easy.
Qed. Qed.
Lemma baryc_skip_zero : Lemma baryc_skip_zero :
forall {n} L (A : 'E^n.+1) i0, forall {n} i0 L (A : 'E^n.+1),
invertible (sum L) -> L i0 = 0 -> invertible (sum L) -> L i0 = 0 ->
barycenter L A = barycenter (skipF i0 L) (skipF i0 A). barycenter L A = barycenter (skipF i0 L) (skipF i0 A).
Proof. Proof.
intros n L A i0 HL Hi0; apply baryc_equiv; unfold aff_comb. intros n i0 L A HL Hi0; apply baryc_equiv; unfold aff_comb.
rewrite -(plus_zero_l (sum _)) -Hi0 -sum_skipF; easy. rewrite -(plus_zero_l (sum _)) -Hi0 -sum_skipF; easy.
rewrite -(plus_zero_l (lin_comb _ _)) rewrite -(plus_zero_l (lin_comb _ _))
-{1}(scal_zero_l (barycenter L A --> A i0)) -{1}(scal_zero_l (barycenter L A --> A i0))
...@@ -510,25 +510,23 @@ apply baryc_correct; easy. ...@@ -510,25 +510,23 @@ apply baryc_correct; easy.
Qed. Qed.
Lemma baryc_insert_zero : Lemma baryc_insert_zero :
forall {n} L (A : 'E^n) x0 i0, forall {n} i0 x0 L (A : 'E^n),
invertible (sum L) -> invertible (sum L) ->
barycenter L A = barycenter (insertF i0 0 L) (insertF i0 x0 A). barycenter L A = barycenter (insert0F i0 L) (insertF i0 x0 A).
Proof. Proof.
intros n L A x0 i0 HL; rewrite (baryc_skip_zero (insertF _ _ _) _ i0). intros n i0 x0 L A HL; rewrite (baryc_skip_zero i0).
rewrite !skipF_insertF; easy. rewrite !skipF_insertF; easy.
rewrite sum_insertF plus_zero_l; easy. rewrite sum_insertF plus_zero_l; easy.
apply insertF_correct_l; easy. apply insertF_correct_l; easy.
Qed. Qed.
Lemma baryc_squeezeF : Lemma baryc_squeezeF :
forall {n} {L} {A : 'E^n.+1} {i0 i1}, forall {n} {i0 i1} (H : i1 <> i0) {L} {A : 'E^n.+1},
invertible (sum L) -> i1 <> i0 -> A i1 = A i0 -> invertible (sum L) -> A i1 = A i0 ->
barycenter L A = barycenter (squeezeF i0 i1 L) (skipF i1 A). barycenter L A = barycenter (squeezeF i0 i1 L) (skipF i1 A).
Proof. Proof.
intros n L A i0 i1 HL Hia Hib; apply baryc_equiv. intros; apply baryc_equiv; [apply invertible_sum_squeezeF; easy |].
apply invertible_sum_squeezeF; easy. apply ac_squeezeF; [..| apply baryc_correct]; easy.
apply ac_squeezeF; try easy.
apply baryc_correct; easy.
Qed. Qed.
Lemma baryc_injF_ex : Lemma baryc_injF_ex :
...@@ -553,7 +551,7 @@ destruct (Hn (squeezeF i0 i1 L) (skipF i1 A)) as [m [M [B [H1 [H2 [H3 H4]]]]]]; ...@@ -553,7 +551,7 @@ destruct (Hn (squeezeF i0 i1 L) (skipF i1 A)) as [m [M [B [H1 [H2 [H3 H4]]]]]];
try now apply invertible_sum_squeezeF. try now apply invertible_sum_squeezeF.
exists m, M, B; repeat split; try easy. exists m, M, B; repeat split; try easy.
apply (skipF_monot_r i1); easy. apply (skipF_monot_r i1); easy.
rewrite (baryc_squeezeF _ Hib); easy. rewrite (baryc_squeezeF Hib); easy.
Qed. Qed.
Lemma baryc_filter_n0F : Lemma baryc_filter_n0F :
...@@ -578,9 +576,9 @@ destruct (baryc_normalized ...@@ -578,9 +576,9 @@ destruct (baryc_normalized
rewrite -invertible_sum_equiv//. rewrite -invertible_sum_equiv//.
apply baryc_filter_n0F; easy. apply baryc_filter_n0F; easy.
eexists; exists (scal (/ sum (filter_n0F L)) (filter_n0F L)), eexists; exists (scal (/ sum (filter_n0F L)) (filter_n0F L)),
(filter_n0F_gen L A); repeat split; try easy. (filter_n0F_gen L A); repeat split;
2: apply filterPF_invalF. [easy | | apply filterPF_invalF | easy].
intros; rewrite fct_scal_r_eq scal_eq_K. apply mult_not_zero_l. intros; rewrite fct_scal_r_eq scal_eq_K; apply mult_not_zero_l.
apply inv_invertible; rewrite -invertible_sum_equiv//. apply inv_invertible; rewrite -invertible_sum_equiv//.
apply filter_neqF_correct. apply filter_neqF_correct.
Qed. Qed.
...@@ -911,14 +909,23 @@ rewrite minus_zero_equiv lc_constF_r HL scal_one; easy. ...@@ -911,14 +909,23 @@ rewrite minus_zero_equiv lc_constF_r HL scal_one; easy.
Qed. Qed.
Lemma baryc_frameF_ms_eq : Lemma baryc_frameF_ms_eq :
forall {n L} {A : 'E^n.+1} i0, sum L = 1 -> forall {n} i0 {L} {A : 'E^n.+1}, sum L = 1 ->
barycenter_ms L A = barycenter_ms L A =
A i0 + lin_comb (skipF i0 L) (skipF i0 A - constF n (A i0)). A i0 + lin_comb (skipF i0 L) (skipF i0 A - constF n (A i0)).
Proof. Proof.
intros n L A i0 HL; apply eq_sym, (baryc_frameF_equiv A _ i0 HL). intros n i0 L A HL; apply eq_sym, (baryc_frameF_equiv i0); [easy |].
rewrite frameF_ms_eq; apply: minus_plus_l. rewrite frameF_ms_eq; apply: minus_plus_l.
Qed. Qed.
Lemma isobaryc_ms_eq :
forall {n} (A : 'E^n), invertible (plusn1 n : K) ->
isobarycenter_ms A = scal (/ plusn1 n) (sum A).
Proof.
intros n A Hn; rewrite isobaryc_ms_correct; unfold isobarycenter.
destruct (baryc_normalized 1 A (barycenter 1 A)) as [HL1 ->]; [easy.. |].
rewrite -baryc_ms_correct baryc_ms_eq// lc_scal_l lc_ones_l; easy.
Qed.
End ModuleSpace_AffineSpace. End ModuleSpace_AffineSpace.
......
Algebra/Finite_dim/Finite_dim_AS_aff_basis.v
View file @ 5ba16a8b
...@@ -142,50 +142,50 @@ Lemma has_aff_dim_cas : ...@@ -142,50 +142,50 @@ Lemma has_aff_dim_cas :
Proof. move=>> [B HB]; apply (aff_basis_cas _ HB). Qed. Proof. move=>> [B HB]; apply (aff_basis_cas _ HB). Qed.
Lemma aff_basis_lin_basis : Lemma aff_basis_lin_basis :
forall {PE n} {A : 'E^n.+1} O i0, forall {PE n} i0 O {A : 'E^n.+1},
aff_span A O -> basis (vectP PE O) (frameF A i0) -> aff_basis PE A. aff_span A O -> basis (vectP PE O) (frameF i0 A) -> aff_basis PE A.
Proof. Proof.
move=>> HO; apply modus_ponens_and; move=>> HO; apply modus_ponens_and;
[apply aff_gen_lin_gen; easy | apply aff_indep_lin_indep]. [apply aff_gen_lin_gen; easy | apply aff_indep_lin_indep].
Qed. Qed.
Lemma aff_basis_lin_basis_rev : Lemma aff_basis_lin_basis_rev :
forall {PE : E -> Prop} {n} {A : 'E^n.+1} {O} i0, forall {PE : E -> Prop} {n} i0 {O} {A : 'E^n.+1},
PE O -> aff_basis PE A -> basis (vectP PE O) (frameF A i0). PE O -> aff_basis PE A -> basis (vectP PE O) (frameF i0 A).
Proof. Proof.
move=>> HO; apply modus_ponens_and; move=>> HO; apply modus_ponens_and;
[apply aff_gen_lin_gen_rev; easy | apply aff_indep_lin_indep_rev]. [apply aff_gen_lin_gen_rev; easy | apply aff_indep_lin_indep_rev].
Qed. Qed.
Lemma aff_basis_lin_basis_equiv : Lemma aff_basis_lin_basis_equiv :
forall {PE n} {A : 'E^n.+1} {O} i0, forall {PE n} i0 {O} {A : 'E^n.+1},
PE O -> aff_span A O -> PE O -> aff_span A O ->
aff_basis PE A <-> basis (vectP PE O) (frameF A i0). aff_basis PE A <-> basis (vectP PE O) (frameF i0 A).
Proof. Proof.
intros; apply and_iff_compat; intros; apply and_iff_compat;
[apply aff_gen_lin_gen_equiv; easy | apply aff_indep_lin_indep_equiv]. [apply aff_gen_lin_gen_equiv; easy | apply aff_indep_lin_indep_equiv].
Qed. Qed.
Lemma lin_basis_aff_basis : Lemma lin_basis_aff_basis :
forall {PV n} {B : 'V^n} (O : E) i0, forall {PV n} i0 (O : E) {B : 'V^n},
zero_closed PV -> zero_closed PV ->
aff_basis (translP PV O) (inv_frameF O B i0) -> basis PV B. aff_basis (translP PV O) (inv_frameF i0 O B) -> basis PV B.
Proof. Proof.
move=>> HO; apply modus_ponens_and; move=>> HO; apply modus_ponens_and;
[apply lin_gen_aff_gen; easy | apply lin_indep_aff_indep]. [apply lin_gen_aff_gen; easy | apply lin_indep_aff_indep].
Qed. Qed.
Lemma lin_basis_aff_basis_rev : Lemma lin_basis_aff_basis_rev :
forall {PV n} {B : 'V^n} (O : E) i0, forall {PV n} i0 (O : E) {B : 'V^n},
basis PV B -> aff_basis (translP PV O) (inv_frameF O B i0). basis PV B -> aff_basis (translP PV O) (inv_frameF i0 O B).
Proof. Proof.
move=>>; apply modus_ponens_and; move=>>; apply modus_ponens_and;
[apply lin_gen_aff_gen_rev; easy | apply lin_indep_aff_indep_rev]. [apply lin_gen_aff_gen_rev; easy | apply lin_indep_aff_indep_rev].
Qed. Qed.
Lemma lin_basis_aff_basis_equiv : Lemma lin_basis_aff_basis_equiv :
forall {PV n} {B : 'V^n} (O : E) i0, zero_closed PV -> forall {PV n} i0 (O : E) {B : 'V^n}, zero_closed PV ->
basis PV B <-> aff_basis (translP PV O) (inv_frameF O B i0). basis PV B <-> aff_basis (translP PV O) (inv_frameF i0 O B).
Proof. Proof.
intros; apply and_iff_compat; intros; apply and_iff_compat;
[apply lin_gen_aff_gen_equiv; easy | apply lin_indep_aff_indep_equiv]. [apply lin_gen_aff_gen_equiv; easy | apply lin_indep_aff_indep_equiv].
...@@ -194,7 +194,7 @@ Qed. ...@@ -194,7 +194,7 @@ Qed.
Lemma has_aff_dim_has_dim : Lemma has_aff_dim_has_dim :
forall {PE : E -> Prop} {n} O, has_dim (vectP PE O) n -> has_aff_dim PE n. forall {PE : E -> Prop} {n} O, has_dim (vectP PE O) n -> has_aff_dim PE n.
Proof. Proof.
move=> PE n O [B /(lin_basis_aff_basis_rev O ord0) HB]; move=> PE n O [B /(lin_basis_aff_basis_rev ord0 O) HB];
rewrite translP_vectP in HB; apply (Aff_dim _ _ _ HB). rewrite translP_vectP in HB; apply (Aff_dim _ _ _ HB).
Qed. Qed.
...@@ -225,7 +225,7 @@ Qed. ...@@ -225,7 +225,7 @@ Qed.
Lemma has_dim_has_aff_dim_rev : Lemma has_dim_has_aff_dim_rev :
forall {PV n} (O : E), has_dim PV n -> has_aff_dim (translP PV O) n. forall {PV n} (O : E), has_dim PV n -> has_aff_dim (translP PV O) n.
Proof. Proof.
move=> PV n O [B /(lin_basis_aff_basis_rev O ord0) HB]; move=> PV n O [B /(lin_basis_aff_basis_rev ord0 O) HB];
apply (Aff_dim _ _ _ HB). apply (Aff_dim _ _ _ HB).
Qed. Qed.
...@@ -260,7 +260,7 @@ intros PE n A HPE HA; destruct (has_aff_dim_nonempty HPE) as [O HO]. ...@@ -260,7 +260,7 @@ intros PE n A HPE HA; destruct (has_aff_dim_nonempty HPE) as [O HO].
assert (HO' : aff_span A O) by now rewrite -HA. assert (HO' : aff_span A O) by now rewrite -HA.
move: (has_aff_dim_has_dim_rev HO HPE) => HPE'. move: (has_aff_dim_has_dim_rev HO HPE) => HPE'.
move: (aff_gen_lin_gen_rev ord0 HO HA) => HA'. move: (aff_gen_lin_gen_rev ord0 HO HA) => HA'.
apply (aff_basis_lin_basis _ ord0 HO'). apply (aff_basis_lin_basis ord0 _ HO').
apply (lin_gen_basis HPE' HA'). apply (lin_gen_basis HPE' HA').
Qed. Qed.
...@@ -278,7 +278,7 @@ Lemma aff_indep_aff_gen : ...@@ -278,7 +278,7 @@ Lemma aff_indep_aff_gen :
Proof. Proof.
intros PE n A HPE HA1 HA2. intros PE n A HPE HA1 HA2.
move: (has_aff_dim_has_dim_rev (HA1 ord0) HPE) => HPE'. move: (has_aff_dim_has_dim_rev (HA1 ord0) HPE) => HPE'.
apply (aff_gen_lin_gen (A ord0) ord0). apply (aff_gen_lin_gen ord0 (A ord0)).
apply aff_span_inclF_diag. apply aff_span_inclF_diag.
apply (lin_indep_lin_gen HPE'); try easy. apply (lin_indep_lin_gen HPE'); try easy.
apply frameF_inclF; easy. apply frameF_inclF; easy.
......
Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
View file @ 5ba16a8b
...@@ -100,49 +100,49 @@ Lemma aff_gen_cas : ...@@ -100,49 +100,49 @@ Lemma aff_gen_cas :
Proof. move=>> ->; apply aff_span_cas. Qed. Proof. move=>> ->; apply aff_span_cas. Qed.
Lemma aff_gen_lin_gen : Lemma aff_gen_lin_gen :
forall {PE n} {A : 'E^n.+1} O i0, forall {PE n} i0 O {A : 'E^n.+1},
aff_span A O -> lin_gen (vectP PE O) (frameF A i0) -> aff_gen PE A. aff_span A O -> lin_gen (vectP PE O) (frameF i0 A) -> aff_gen PE A.
Proof. Proof.
intros PE n A O i0 HO HA; apply (vectP_inj O). intros PE n i0 O A HO HA; apply (vectP_inj O).
rewrite (aff_span_lin_span i0 HO) vectP_translP; easy. rewrite (aff_span_lin_span i0 HO) vectP_translP; easy.
Qed. Qed.
Lemma aff_gen_lin_gen_rev : Lemma aff_gen_lin_gen_rev :
forall {PE n} {A : 'E^n.+1} {O} i0, forall {PE n} i0 {O} {A : 'E^n.+1},
PE O -> aff_gen PE A -> lin_gen (vectP PE O) (frameF A i0). PE O -> aff_gen PE A -> lin_gen (vectP PE O) (frameF i0 A).
Proof. Proof.
intros PE n A O i0 HO ->; rewrite (aff_span_lin_span i0 HO) vectP_translP//. intros PE n i0 O A HO ->; rewrite (aff_span_lin_span i0 HO) vectP_translP//.
Qed. Qed.
Lemma aff_gen_lin_gen_equiv : Lemma aff_gen_lin_gen_equiv :
forall {PE n} {A : 'E^n.+1} {O} i0, PE O -> aff_span A O -> forall {PE n} i0 {O} {A : 'E^n.+1}, PE O -> aff_span A O ->
aff_gen PE A <-> lin_gen (vectP PE O) (frameF A i0). aff_gen PE A <-> lin_gen (vectP PE O) (frameF i0 A).
Proof. Proof.
intros; split; [apply aff_gen_lin_gen_rev | apply aff_gen_lin_gen]; easy. intros; split; [apply aff_gen_lin_gen_rev | apply aff_gen_lin_gen]; easy.
Qed. Qed.
Lemma lin_gen_aff_gen : Lemma lin_gen_aff_gen :
forall {PV n} {u : 'V^n} (O : E) i0, forall {PV n} i0 (O : E) {u : 'V^n},
zero_closed PV -> zero_closed PV ->
aff_gen (translP PV O) (inv_frameF O u i0) -> lin_gen PV u. aff_gen (translP PV O) (inv_frameF i0 O u) -> lin_gen PV u.
Proof. Proof.
move=> PV n u O i0 move=> PV n i0 O u
/(translP_zero_closed_equiv O) HO /(aff_gen_lin_gen_rev i0 HO). /(translP_zero_closed_equiv O) HO /(aff_gen_lin_gen_rev i0 HO).
rewrite vectP_translP frameF_inv_frameF; easy. rewrite vectP_translP frameF_inv_frameF; easy.
Qed. Qed.
Lemma lin_gen_aff_gen_rev : Lemma lin_gen_aff_gen_rev :
forall {PV n} {u : 'V^n} (O : E) i0, forall {PV n} i0 (O : E) {u : 'V^n},
lin_gen PV u -> aff_gen (translP PV O) (inv_frameF O u i0). lin_gen PV u -> aff_gen (translP PV O) (inv_frameF i0 O u).
Proof. Proof.
intros PV n u O i0 Hu. intros PV n i0 O u Hu.
apply (aff_gen_lin_gen O i0); try rewrite vectP_translP frameF_inv_frameF//. apply (aff_gen_lin_gen i0 O); try rewrite vectP_translP frameF_inv_frameF//.
apply aff_span_inv_frameF_orig. apply aff_span_inv_frameF_orig.
Qed. Qed.
Lemma lin_gen_aff_gen_equiv : Lemma lin_gen_aff_gen_equiv :
forall {PV n} {u : 'V^n} (O : E) i0, zero_closed PV -> forall {PV n} i0 (O : E) {u : 'V^n}, zero_closed PV ->
lin_gen PV u <-> aff_gen (translP PV O) (inv_frameF O u i0). lin_gen PV u <-> aff_gen (translP PV O) (inv_frameF i0 O u).
Proof. Proof.
intros; split; [apply lin_gen_aff_gen_rev | apply lin_gen_aff_gen; easy]. intros; split; [apply lin_gen_aff_gen_rev | apply lin_gen_aff_gen; easy].
Qed. Qed.
...@@ -183,18 +183,18 @@ Section ModuleSpace_AffineSpace_R_Facts. ...@@ -183,18 +183,18 @@ Section ModuleSpace_AffineSpace_R_Facts.
Context {E : ModuleSpace R_Ring}. Context {E : ModuleSpace R_Ring}.
Lemma aff_gen_lin_gen_ms_equiv : Lemma aff_gen_lin_gen_ms_equiv :
forall {PE : E -> Prop} {n} {A : 'E^n.+1} O i0, PE O -> aff_span_ms A O -> forall {PE : E -> Prop} {n} i0 O {A : 'E^n.+1}, PE O -> aff_span_ms A O ->
aff_gen_ms PE A <-> aff_gen_ms PE A <->
lin_gen (fun u => PE (O + u)) (skipF i0 A - constF n (A i0)). lin_gen (fun u => PE (O + u)) (skipF i0 A - constF n (A i0)).
Proof. Proof.
intros PE n A O i0; rewrite -vectP_ms_eq -frameF_ms_eq; intros PE n i0 O A; rewrite -vectP_ms_eq -frameF_ms_eq;
apply (aff_gen_lin_gen_equiv i0). apply (aff_gen_lin_gen_equiv i0).
Qed. Qed.
Lemma lin_gen_aff_gen_ms_equiv : Lemma lin_gen_aff_gen_ms_equiv :
forall {PE : E -> Prop} {n} {u : 'E^n} (O : E) i0, zero_closed PE -> forall {PE : E -> Prop} {n} i0 (O : E) {u : 'E^n}, zero_closed PE ->
lin_gen PE u <-> lin_gen PE u <->
aff_gen_ms (fun A => PE (A - O)) (constF n.+1 O + insertF i0 0 u). aff_gen_ms (fun A => PE (A - O)) (constF n.+1 O + insert0F i0 u).
Proof. Proof.
move=>>; rewrite -translP_ms_eq -inv_frameF_ms_eq; apply lin_gen_aff_gen_equiv. move=>>; rewrite -translP_ms_eq -inv_frameF_ms_eq; apply lin_gen_aff_gen_equiv.
Qed. Qed.
......
Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
View file @ 5ba16a8b
...@@ -58,10 +58,10 @@ Context {V : ModuleSpace K}. ...@@ -58,10 +58,10 @@ Context {V : ModuleSpace K}.
Context {E : AffineSpace V}. Context {E : AffineSpace V}.
Lemma aff_indep_any : Lemma aff_indep_any :
forall {n} {A : 'E^n.+1} i0 i, forall {n} i0 i {A : 'E^n.+1},
lin_indep (frameF A i0) -> lin_indep (frameF A i). lin_indep (frameF i0 A) -> lin_indep (frameF i A).
Proof. Proof.
intros n A i0 i HA; destruct (ord_eq_dec i i0) as [Hi | Hi]; try now rewrite Hi. intros n i0 i A HA; destruct (ord_eq_dec i i0) as [Hi | Hi]; try now rewrite Hi.
destruct n as [| n]; [contradict Hi; rewrite !ord_one; easy |]. destruct n as [| n]; [contradict Hi; rewrite !ord_one; easy |].
intros L; unfold frameF; rewrite (vectF_change_orig (A i0)) intros L; unfold frameF; rewrite (vectF_change_orig (A i0))
lc_plus_r lc_constF_r scal_opp -vect_sym vectF_skipF. lc_plus_r lc_constF_r scal_opp -vect_sym vectF_skipF.
...@@ -77,60 +77,60 @@ rewrite zeroF skipF_correct insertF_correct_l; easy. ...@@ -77,60 +77,60 @@ rewrite zeroF skipF_correct insertF_correct_l; easy.
Qed. Qed.
Lemma aff_indep_all : Lemma aff_indep_all :
forall {n} {A : 'E^n.+1} i, aff_indep A -> lin_indep (frameF A i). forall {n} i {A : 'E^n.+1}, aff_indep A -> lin_indep (frameF i A).
Proof. move=>>; apply aff_indep_any. Qed. Proof. move=>>; apply aff_indep_any. Qed.
Lemma aff_indep_all_equiv : Lemma aff_indep_all_equiv :
forall {n} {A : 'E^n.+1}, aff_indep A <-> forall i, lin_indep (frameF A i). forall {n} {A : 'E^n.+1}, aff_indep A <-> forall i, lin_indep (frameF i A).
Proof. Proof.
intros; split; [intros; apply aff_indep_all; easy | intros H; apply H]. intros; split; [intros; apply aff_indep_all; easy | intros H; apply H].
Qed. Qed.
Lemma aff_indep_lin_indep : Lemma aff_indep_lin_indep :
forall {n} {A : 'E^n.+1} i0, lin_indep (frameF A i0) -> aff_indep A. forall {n} i0 {A : 'E^n.+1}, lin_indep (frameF i0 A) -> aff_indep A.
Proof. move=> n A i0 /(aff_indep_any i0 ord0); easy. Qed. Proof. move=> n i0 A /(aff_indep_any i0 ord0); easy. Qed.
Lemma aff_indep_lin_indep_rev : Lemma aff_indep_lin_indep_rev :
forall {n} {A : 'E^n.+1} i0, aff_indep A -> lin_indep (frameF A i0). forall {n} i0 {A : 'E^n.+1}, aff_indep A -> lin_indep (frameF i0 A).
Proof. move=>>; apply aff_indep_any. Qed. Proof. move=>>; apply aff_indep_any. Qed.
Lemma aff_indep_lin_indep_equiv : Lemma aff_indep_lin_indep_equiv :
forall {n} {A : 'E^n.+1} i0, aff_indep A <-> lin_indep (frameF A i0). forall {n} i0 {A : 'E^n.+1}, aff_indep A <-> lin_indep (frameF i0 A).
Proof. Proof.
intros; split; [apply aff_indep_lin_indep_rev | apply aff_indep_lin_indep]. intros; split; [apply aff_indep_lin_indep_rev | apply aff_indep_lin_indep].
Qed. Qed.
Lemma lin_indep_aff_indep_equiv : Lemma lin_indep_aff_indep_equiv :
forall {n} {u : 'V^n} (O : E) i0, forall {n} i0 (O : E) {u : 'V^n},
lin_indep u <-> aff_indep (inv_frameF O u i0). lin_indep u <-> aff_indep (inv_frameF i0 O u).
Proof. Proof.
intros n u O i0. rewrite (aff_indep_lin_indep_equiv i0) frameF_inv_frameF//. intros n i0 O u; rewrite (aff_indep_lin_indep_equiv i0) frameF_inv_frameF//.
Qed. Qed.
Lemma lin_indep_aff_indep : Lemma lin_indep_aff_indep :
forall {n} {u : 'V^n} (O : E) i0, forall {n} i0 (O : E) {u : 'V^n},
aff_indep (inv_frameF O u i0) -> lin_indep u. aff_indep (inv_frameF i0 O u) -> lin_indep u.
Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed. Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.
Lemma lin_indep_aff_indep_rev : Lemma lin_indep_aff_indep_rev :
forall {n} {u : 'V^n} (O : E) i0, forall {n} i0 (O : E) {u : 'V^n},
lin_indep u -> aff_indep (inv_frameF O u i0). lin_indep u -> aff_indep (inv_frameF i0 O u).
Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed. Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.
Lemma aff_dep_any : Lemma aff_dep_any :
forall {n} {A : 'E^n.+1} i0, forall {n} i0 {A : 'E^n.+1},
(exists i, lin_dep (frameF A i)) -> lin_dep (frameF A i0). (exists i, lin_dep (frameF i A)) -> lin_dep (frameF i0 A).
Proof. Proof.
intros n A i0; rewrite contra_not_r_equiv not_ex_not_all_equiv. intros n i0 A; rewrite contra_not_r_equiv not_ex_not_all_equiv.
intros; apply (aff_indep_any i0); easy. intros; apply (aff_indep_any i0); easy.
Qed. Qed.
Lemma aff_dep_ex : Lemma aff_dep_ex :
forall {n} {A : 'E^n.+1}, (exists i, lin_dep (frameF A i)) -> aff_dep A. forall {n} {A : 'E^n.+1}, (exists i, lin_dep (frameF i A)) -> aff_dep A.
Proof. move=>>; apply aff_dep_any. Qed. Proof. move=>>; apply aff_dep_any. Qed.
Lemma aff_dep_ex_equiv : Lemma aff_dep_ex_equiv :
forall {n} {A : 'E^n.+1}, aff_dep A <-> exists i, lin_dep (frameF A i). forall {n} {A : 'E^n.+1}, aff_dep A <-> exists i, lin_dep (frameF i A).
Proof. intros; split; [intros H; exists ord0; easy | apply aff_dep_any]. Qed. Proof. intros; split; [intros H; exists ord0; easy | apply aff_dep_any]. Qed.
Lemma aff_indep_decomp_uniq : Lemma aff_indep_decomp_uniq :
...@@ -149,7 +149,7 @@ Lemma aff_indep_decomp_uniq_rev : ...@@ -149,7 +149,7 @@ Lemma aff_indep_decomp_uniq_rev :
Proof. Proof.
intros n A HA L HL; apply (insertF_inj_r ord0 (1 - sum L) 1). intros n A HA L HL; apply (insertF_inj_r ord0 (1 - sum L) 1).
replace (insertF _ _ L) with (part1F0 L) by easy; rewrite -itemF_insertF. replace (insertF _ _ L) with (part1F0 L) by easy; rewrite -itemF_insertF.
assert (H1 : sum (part1F L ord0) = 1) by apply part1F_sum. assert (H1 : sum (part1F ord0 L) = 1) by apply part1F_sum.
assert (H2 : sum (itemF n.+1 ord0 1) = (1 : K)) by now apply sum_itemF. assert (H2 : sum (itemF n.+1 ord0 1) = (1 : K)) by now apply sum_itemF.
apply HA; [easy.. |]; apply (vect_l_inj (A ord0)). apply HA; [easy.. |]; apply (vect_l_inj (A ord0)).
rewrite -(scal_one_l 1 (_ --> barycenter (part1F _ _) _))// -{1}H1 rewrite -(scal_one_l 1 (_ --> barycenter (part1F _ _) _))// -{1}H1
...@@ -213,7 +213,7 @@ Lemma aff_indep_monot : ...@@ -213,7 +213,7 @@ Lemma aff_indep_monot :
injective A1 -> invalF A1 A2 -> aff_indep A2 -> aff_indep A1. injective A1 -> invalF A1 A2 -> aff_indep A2 -> aff_indep A1.
Proof. Proof.
intros n1 n2 A1 A2 HA1 HA HA2; destruct (HA ord0) as [i2 Hi2]. intros n1 n2 A1 A2 HA1 HA HA2; destruct (HA ord0) as [i2 Hi2].
apply (lin_indep_monot (frameF A2 i2)). apply (lin_indep_monot (frameF i2 A2)).
apply frameF_inj_equiv, skipF_inj; easy. apply frameF_inj_equiv, skipF_inj; easy.
apply frameF_invalF_equiv; [| apply skipF_invalF]; easy. apply frameF_invalF_equiv; [| apply skipF_invalF]; easy.
apply aff_indep_all; easy. apply aff_indep_all; easy.
...@@ -244,9 +244,9 @@ Lemma aff_indep_coupleF_equiv : ...@@ -244,9 +244,9 @@ Lemma aff_indep_coupleF_equiv :
Proof. intros; rewrite aff_indep_2_equiv coupleF_0 coupleF_1; easy. Qed. Proof. intros; rewrite aff_indep_2_equiv coupleF_0 coupleF_1; easy. Qed.
Lemma aff_indep_skipF : Lemma aff_indep_skipF :
forall {n} {A : 'E^n.+2} i0, aff_indep A -> aff_indep (skipF i0 A). forall {n} i0 {A : 'E^n.+2}, aff_indep A -> aff_indep (skipF i0 A).
Proof. Proof.
intros n A i0 HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |]. intros n i0 A HA; destruct (ord_eq_dec i0 ord0) as [Hi0 | Hi0]; [subst |].
(* *) (* *)
apply (aff_indep_any ord_max); rewrite -(insert_ord_max ord_max_not_0). apply (aff_indep_any ord_max); rewrite -(insert_ord_max ord_max_not_0).
rewrite frameF_skipF_alt; apply lin_indep_skipF_compat, aff_indep_all; easy. rewrite frameF_skipF_alt; apply lin_indep_skipF_compat, aff_indep_all; easy.
...@@ -256,25 +256,25 @@ rewrite frameF_skipF; apply lin_indep_skipF_compat; easy. ...@@ -256,25 +256,25 @@ rewrite frameF_skipF; apply lin_indep_skipF_compat; easy.
Qed. Qed.
Lemma aff_indep_permutF : Lemma aff_indep_permutF :
forall {n} {A : 'E^n.+1} {p}, forall {n p} {A : 'E^n.+1},
bijective p -> aff_indep A -> aff_indep (permutF p A). bijective p -> aff_indep A -> aff_indep (permutF p A).
Proof. Proof.
intros n A p Hp HA; apply (aff_indep_any (p ord0)). intros n p A Hp HA; apply (aff_indep_any (p ord0)).
rewrite (frameF_permutF (bij_inj Hp)); apply lin_indep_permutF. rewrite (frameF_permutF (bij_inj Hp)); apply lin_indep_permutF.
apply skip_f_ord_bij. apply skip_f_ord_bij.
apply aff_indep_all; easy. apply aff_indep_all; easy.
Qed. Qed.
Lemma aff_indep_permutF_rev : Lemma aff_indep_permutF_rev :
forall {n} {A : 'E^n.+1} p, forall {n p} {A : 'E^n.+1},
bijective p -> aff_indep (permutF p A) -> aff_indep A. bijective p -> aff_indep (permutF p A) -> aff_indep A.
Proof. Proof.
intros n A p Hp; rewrite {2}(permutF_f_inv_l Hp A). intros n p A Hp; rewrite {2}(permutF_f_inv_l Hp A).
apply aff_indep_permutF, f_inv_bij. apply aff_indep_permutF, f_inv_bij.
Qed. Qed.
Lemma aff_indep_permutF_equiv : Lemma aff_indep_permutF_equiv :
forall {n} {A : 'E^n.+1} p, forall {n p} {A : 'E^n.+1},
bijective p -> aff_indep A <-> aff_indep (permutF p A). bijective p -> aff_indep A <-> aff_indep (permutF p A).
Proof. Proof.
intros; split; [apply aff_indep_permutF | apply aff_indep_permutF_rev]; easy. intros; split; [apply aff_indep_permutF | apply aff_indep_permutF_rev]; easy.
......
Algebra/Finite_dim/Finite_dim_AS_aff_map.v
View file @ 5ba16a8b
...@@ -106,7 +106,7 @@ Lemma baryc_bc_baryc : ...@@ -106,7 +106,7 @@ Lemma baryc_bc_baryc :
forall {p} L (B : 'E^p), sum L = 1 -> inclF B (aff_span A) -> forall {p} L (B : 'E^p), sum L = 1 -> inclF B (aff_span A) ->
barycenter (barycenter_ms L (mapF (baryc_coord A) B)) A = barycenter L B. barycenter (barycenter_ms L (mapF (baryc_coord A) B)) A = barycenter L B.
Proof. Proof.
intros p L B HL HB; rewrite baryc_ms_eq// -(barycenter2_r_alt _ B)//. intros p L B HL HB; rewrite baryc_ms_eq// -(barycenter2_r_alt _ _ B)//.
apply invertible_eq_one; easy. apply invertible_eq_one; easy.
1,2: intro; rewrite mapF_correct; apply bc_correct; easy. 1,2: intro; rewrite mapF_correct; apply bc_correct; easy.
Qed. Qed.
......
Algebra/Finite_dim/Finite_dim_AS_aff_span.v
View file @ 5ba16a8b
...@@ -176,9 +176,9 @@ intros; apply subset_ext_equiv; split; apply aff_span_monot_inclF; easy. ...@@ -176,9 +176,9 @@ intros; apply subset_ext_equiv; split; apply aff_span_monot_inclF; easy.
Qed. Qed.
Lemma aff_span_inv_frameF_orig : Lemma aff_span_inv_frameF_orig :
forall {n} (B : 'V^n) (O : E) i0, aff_span (inv_frameF O B i0) O. forall {n} i0 (O : E) (B : 'V^n), aff_span (inv_frameF i0 O B) O.
Proof. Proof.
intros n B O i0; rewrite -{2}(transl_zero O); apply (aff_span_ub _ _ i0). intros n i0 O B; rewrite -{2}(transl_zero O); apply (aff_span_ub _ _ i0).
unfold inv_frameF; rewrite translF_insertF insertF_correct_l; easy. unfold inv_frameF; rewrite translF_insertF insertF_correct_l; easy.
Qed. Qed.
...@@ -285,10 +285,10 @@ intros B HB; apply HB; [apply aff_span_cas | apply aff_span_inclF_diag]. ...@@ -285,10 +285,10 @@ intros B HB; apply HB; [apply aff_span_cas | apply aff_span_inclF_diag].
Qed. Qed.
Lemma lin_span_aff_span_aux : Lemma lin_span_aff_span_aux :
forall {n} {A : 'E^n.+1} {O} i0, aff_span A O -> forall {n} i0 {O} {A : 'E^n.+1}, aff_span A O ->
lin_span (frameF A i0) = vectP (aff_span A) O. lin_span (frameF i0 A) = vectP (aff_span A) O.
Proof. Proof.
intros n A O i0 HO; rewrite (vectP_orig_indep (A i0) HO). intros n i0 O A HO; rewrite (vectP_orig_indep (A i0) HO).
2: { apply cas_cms_equiv_R; try apply aff_span_inclF_diag. 2: { apply cas_cms_equiv_R; try apply aff_span_inclF_diag.
move=>> HL HC; apply aff_span_cas; easy. } move=>> HL HC; apply aff_span_cas; easy. }
apply eq_sym, subset_ext_equiv; split; unfold vectP, preimage; intros u Hu. apply eq_sym, subset_ext_equiv; split; unfold vectP, preimage; intros u Hu.
...@@ -305,8 +305,8 @@ apply Aff_span, invertible_eq_one, sum_insertF_baryc. ...@@ -305,8 +305,8 @@ apply Aff_span, invertible_eq_one, sum_insertF_baryc.
Qed. Qed.
Lemma lin_span_aff_span : Lemma lin_span_aff_span :
forall {n} {u : 'V^n} (O : E) i0, forall {n} i0 (O : E) {u : 'V^n},
lin_span u = vectP (aff_span (inv_frameF O u i0)) O. lin_span u = vectP (aff_span (inv_frameF i0 O u)) O.
Proof. Proof.
intros; rewrite -(lin_span_aff_span_aux i0). intros; rewrite -(lin_span_aff_span_aux i0).
rewrite frameF_inv_frameF; easy. rewrite frameF_inv_frameF; easy.
...@@ -314,11 +314,11 @@ apply aff_span_inv_frameF_orig. ...@@ -314,11 +314,11 @@ apply aff_span_inv_frameF_orig.
Qed. Qed.
Lemma aff_span_lin_span : Lemma aff_span_lin_span :
forall {n} {A : 'E^n.+1} {O} i0, aff_span A O -> forall {n} i0 {O} {A : 'E^n.+1}, aff_span A O ->
aff_span A = translP (lin_span (frameF A i0)) O. aff_span A = translP (lin_span (frameF i0 A)) O.
Proof. Proof.
intros n A O i0 HO; apply (vectP_inj O). intros n i0 O A HO; apply (vectP_inj O).
rewrite vectP_translP (lin_span_aff_span (A i0) i0) inv_frameF_frameF. rewrite vectP_translP (lin_span_aff_span i0 (A i0)) inv_frameF_frameF.
apply vectP_orig_indep; [easy | apply cas_cms]. apply vectP_orig_indep; [easy | apply cas_cms].
apply aff_span_inclF_diag. apply aff_span_inclF_diag.
apply invertible_equiv_R, two_not_zero_R. apply invertible_equiv_R, two_not_zero_R.
...@@ -339,14 +339,14 @@ Lemma aff_span_ext_ms : ...@@ -339,14 +339,14 @@ Lemma aff_span_ext_ms :
Proof. move=>>; apply aff_span_ext. Qed. Proof. move=>>; apply aff_span_ext. Qed.
Lemma lin_span_aff_span_ms : Lemma lin_span_aff_span_ms :
forall {n} {u : 'E^n} O i0, lin_span u = forall {n} i0 O {u : 'E^n}, lin_span u =
fun v => aff_span_ms (constF n.+1 O + insertF i0 0 u) (O + v). fun v => aff_span_ms (constF n.+1 O + insert0F i0 u) (O + v).
Proof. Proof.
intros; rewrite -inv_frameF_ms_eq -vectP_ms_eq; apply lin_span_aff_span. intros; rewrite -inv_frameF_ms_eq -vectP_ms_eq; apply lin_span_aff_span.
Qed. Qed.
Lemma aff_span_lin_span_ms : Lemma aff_span_lin_span_ms :
forall {n} {A : 'E^n.+1} {O} i0, aff_span_ms A O -> forall {n} i0 {O} {A : 'E^n.+1}, aff_span_ms A O ->
aff_span_ms A = fun B => lin_span (skipF i0 A - constF n (A i0)) (B - O). aff_span_ms A = fun B => lin_span (skipF i0 A - constF n (A i0)) (B - O).
Proof. Proof.
intros; rewrite -frameF_ms_eq -translP_ms_eq; apply aff_span_lin_span; easy. intros; rewrite -frameF_ms_eq -translP_ms_eq; apply aff_span_lin_span; easy.
......
Algebra/Finite_dim/Finite_dim_AS_def.v
View file @ 5ba16a8b
...@@ -157,7 +157,7 @@ Lemma aff_gen_ext2 : ...@@ -157,7 +157,7 @@ Lemma aff_gen_ext2 :
PE1 = PE2 -> A1 = A2 -> aff_gen PE1 A1 -> aff_gen PE2 A2. PE1 = PE2 -> A1 = A2 -> aff_gen PE1 A1 -> aff_gen PE2 A2.
Proof. intros; subst; easy. Qed. Proof. intros; subst; easy. Qed.
Definition aff_indep {n} (A : 'E^n.+1) : Prop := lin_indep (frameF A ord0). Definition aff_indep {n} (A : 'E^n.+1) : Prop := lin_indep (frameF ord0 A).
Lemma aff_indep_ext : Lemma aff_indep_ext :
forall {n} (A1 : 'E^n.+1) {A2}, A1 = A2 -> aff_indep A1 -> aff_indep A2. forall {n} (A1 : 'E^n.+1) {A2}, A1 = A2 -> aff_indep A1 -> aff_indep A2.
......
Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
View file @ 5ba16a8b
...@@ -174,18 +174,18 @@ rewrite concatF_correct_l concat_l_first ...@@ -174,18 +174,18 @@ rewrite concatF_correct_l concat_l_first
Qed. Qed.
Lemma lin_dep_insertF_compat : Lemma lin_dep_insertF_compat :
forall {n} {B : 'E^n} x0 i0, lin_dep B -> lin_dep (insertF i0 x0 B). forall {n} i0 x0 {B : 'E^n}, lin_dep B -> lin_dep (insertF i0 x0 B).
Proof. Proof.
intros n B x0 i0; rewrite 2!lin_dep_ex; move=> [L [HL /nextF_rev [i Hi]]]. intros n i0 x0 B; rewrite 2!lin_dep_ex; move=> [L [HL /nextF_rev [i Hi]]].
exists (insertF i0 0 L); split. exists (insertF i0 0 L); split.
rewrite lc_insertF scal_zero_l HL plus_zero_l; easy. rewrite lc_insertF scal_zero_l HL plus_zero_l; easy.
apply nextF; exists (skip_ord i0 i); rewrite insertF_correct; easy. apply nextF; exists (skip_ord i0 i); rewrite insertF_correct; easy.
Qed. Qed.
Lemma lin_dep_skipF_reg : Lemma lin_dep_skipF_reg :
forall {n} {B : 'E^n.+1} i0, lin_dep (skipF i0 B) -> lin_dep B. forall {n} i0 {B : 'E^n.+1}, lin_dep (skipF i0 B) -> lin_dep B.
Proof. Proof.
intros n B i0; rewrite -{2}(insertF_skipF i0 B). intros n i0 B; rewrite -{2}(insertF_skipF i0 B).
apply lin_dep_insertF_compat. apply lin_dep_insertF_compat.
Qed. Qed.
...@@ -308,11 +308,11 @@ intros [H1 H2]; eapply lin_dep_concatF_not_disjF; [apply H1 | easy]. ...@@ -308,11 +308,11 @@ intros [H1 H2]; eapply lin_dep_concatF_not_disjF; [apply H1 | easy].
Qed. Qed.
Lemma lin_indep_insertF_reg : Lemma lin_indep_insertF_reg :
forall {n} {B : 'E^n} x0 i0, lin_indep (insertF i0 x0 B) -> lin_indep B. forall {n} i0 x0 {B : 'E^n}, lin_indep (insertF i0 x0 B) -> lin_indep B.
Proof. move=>>; rewrite contra_equiv; apply lin_dep_insertF_compat. Qed. Proof. move=>>; rewrite contra_equiv; apply lin_dep_insertF_compat. Qed.
Lemma lin_indep_skipF_compat : Lemma lin_indep_skipF_compat :
forall {n} {B : 'E^n.+1} i0, lin_indep B -> lin_indep (skipF i0 B). forall {n} i0 {B : 'E^n.+1}, lin_indep B -> lin_indep (skipF i0 B).
Proof. move=>>; rewrite contra_equiv; apply lin_dep_skipF_reg. Qed. Proof. move=>>; rewrite contra_equiv; apply lin_dep_skipF_reg. Qed.
Lemma lin_indep_not_line : Lemma lin_indep_not_line :
...@@ -423,16 +423,16 @@ Qed. ...@@ -423,16 +423,16 @@ Qed.
#<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A># #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
Th 6.61, pp. 189-190. (=>) *) Th 6.61, pp. 189-190. (=>) *)
Lemma lin_dep_insertF : Lemma lin_dep_insertF :
forall {n} {B : 'E^n} {x0} i0, lin_span B x0 -> lin_dep (insertF i0 x0 B). forall {n} i0 {x0} {B : 'E^n}, lin_span B x0 -> lin_dep (insertF i0 x0 B).
Proof. Proof.
intros n B x0 i0 [L]; apply lin_dep_ex; exists (insertF i0 (- 1%K) L); split. intros n i0 x0 B [L]; apply lin_dep_ex; exists (insertF i0 (- 1%K) L); split.
rewrite lc_insertF scal_opp_l scal_one; apply: plus_opp_l. rewrite lc_insertF scal_opp_l scal_one; apply: plus_opp_l.
rewrite -(insertF_zero i0); apply insertF_nextF_compat_l. rewrite -(insertF_zero i0); apply insertF_nextF_compat_l.
apply one_not_zero in HK; contradict HK; apply opp_inj; rewrite opp_zero; easy. apply one_not_zero in HK; contradict HK; apply opp_inj; rewrite opp_zero; easy.
Qed. Qed.
Lemma lin_indep_insertF_rev : Lemma lin_indep_insertF_rev :
forall {n} {B : 'E^n} {x0} i0, forall {n} i0 {x0} {B : 'E^n},
lin_indep (insertF i0 x0 B) -> ~ lin_span B x0. lin_indep (insertF i0 x0 B) -> ~ lin_span B x0.
Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_insertF. Qed. Proof. move=>>; rewrite contra_not_r_equiv; apply lin_dep_insertF. Qed.
......
Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
View file @ 5ba16a8b
...@@ -265,10 +265,10 @@ Proof. move=>>; rewrite -contra_equiv; apply lin_indep_coupleF_sym. Qed. ...@@ -265,10 +265,10 @@ Proof. move=>>; rewrite -contra_equiv; apply lin_indep_coupleF_sym. Qed.
#<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A># #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
Th 6.61, pp. 189-190. (<=) *) Th 6.61, pp. 189-190. (<=) *)
Lemma lin_dep_insertF_rev : Lemma lin_dep_insertF_rev :
forall {n} {B : 'E^n} {x0} i0, forall {n} i0 {x0} {B : 'E^n},
lin_indep B -> lin_dep (insertF i0 x0 B) -> lin_span B x0. lin_indep B -> lin_dep (insertF i0 x0 B) -> lin_span B x0.
Proof. Proof.
move=> n B x0 i0 HB /lin_dep_ex [L [HL1 HL2]]; move=> n i0 x0 B HB /lin_dep_ex [L [HL1 HL2]];
rewrite lc_insertF_r in HL1. rewrite lc_insertF_r in HL1.
destruct (Hierarchy.eq_dec (L i0) 0) as [HL3 | HL3]. destruct (Hierarchy.eq_dec (L i0) 0) as [HL3 | HL3].
(* *) (* *)
...@@ -288,7 +288,7 @@ Qed. ...@@ -288,7 +288,7 @@ Qed.
#<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A># #<A HREF="##GostiauxT1">#[[GostiauxT1]]#</A>#
Th 6.61, pp. 189-190. (<=>) *) Th 6.61, pp. 189-190. (<=>) *)
Lemma lin_dep_insertF_equiv : Lemma lin_dep_insertF_equiv :
forall {n} {B : 'E^n} {x0} i0, forall {n} i0 {x0} {B : 'E^n},
lin_indep B -> lin_dep (insertF i0 x0 B) <-> lin_span B x0. lin_indep B -> lin_dep (insertF i0 x0 B) <-> lin_span B x0.
Proof. Proof.
intros; split; [apply lin_dep_insertF_rev; easy | intros; split; [apply lin_dep_insertF_rev; easy |
...@@ -296,14 +296,14 @@ intros; split; [apply lin_dep_insertF_rev; easy | ...@@ -296,14 +296,14 @@ intros; split; [apply lin_dep_insertF_rev; easy |
Qed. Qed.
Lemma lin_indep_insertF : Lemma lin_indep_insertF :
forall {n} {B : 'E^n} {x0} i0, forall {n} i0 {x0} {B : 'E^n},
lin_indep B -> ~ lin_span B x0 -> lin_indep (insertF i0 x0 B). lin_indep B -> ~ lin_span B x0 -> lin_indep (insertF i0 x0 B).
Proof. Proof.
move=>> HB; rewrite contra_not_l_equiv; apply lin_dep_insertF_rev; easy. move=>> HB; rewrite contra_not_l_equiv; apply lin_dep_insertF_rev; easy.
Qed. Qed.
Lemma lin_indep_insertF_equiv : Lemma lin_indep_insertF_equiv :
forall {n} {B : 'E^n} {x0} i0, forall {n} i0 {x0} {B : 'E^n},
lin_indep B -> lin_indep (insertF i0 x0 B) <-> ~ lin_span B x0. lin_indep B -> lin_indep (insertF i0 x0 B) <-> ~ lin_span B x0.
Proof. move=>>; rewrite iff_not_r_equiv; apply lin_dep_insertF_equiv. Qed. Proof. move=>>; rewrite iff_not_r_equiv; apply lin_dep_insertF_equiv. Qed.
......
Algebra/Group/Group_compl.v
View file @ 5ba16a8b
...@@ -304,36 +304,36 @@ Lemma concatF_minus : ...@@ -304,36 +304,36 @@ Lemma concatF_minus :
Proof. intros; rewrite !minus_eq concatF_plus concatF_opp; easy. Qed. Proof. intros; rewrite !minus_eq concatF_plus concatF_opp; easy. Qed.
Lemma insertF_opp : Lemma insertF_opp :
forall {n} (A : 'G^n) a0 i0, insertF i0 (-a0) (- A) = - insertF i0 a0 A. forall {n} i0 a0 (A : 'G^n), insertF i0 (-a0) (- A) = - insertF i0 a0 A.
Proof. Proof.
intros n A a i0; extF i; rewrite fct_opp_eq; intros n i0 a A; extF i; rewrite fct_opp_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi]; destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy. [rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed. Qed.
Lemma insertF_minus : Lemma insertF_minus :
forall {n} (A B : 'G^n) a0 b0 i0, forall {n} i0 a0 b0 (A B : 'G^n),
insertF i0 (a0 - b0) (A - B) = insertF i0 a0 A - insertF i0 b0 B. insertF i0 (a0 - b0) (A - B) = insertF i0 a0 A - insertF i0 b0 B.
Proof. intros; rewrite !minus_eq insertF_plus insertF_opp; easy. Qed. Proof. intros; rewrite !minus_eq insertF_plus insertF_opp; easy. Qed.
Lemma skipF_opp : forall {n} (A : 'G^n.+1) i0, skipF i0 (- A) = - skipF i0 A. Lemma skipF_opp : forall {n} i0 (A : 'G^n.+1), skipF i0 (- A) = - skipF i0 A.
Proof. easy. Qed. Proof. easy. Qed.
Lemma skipF_minus : Lemma skipF_minus :
forall {n} (A B : 'G^n.+1) i0, skipF i0 (A - B) = skipF i0 A - skipF i0 B. forall {n} i0 (A B : 'G^n.+1), skipF i0 (A - B) = skipF i0 A - skipF i0 B.
Proof. easy. Qed. Proof. easy. Qed.
Lemma replaceF_opp : Lemma replaceF_opp :
forall {n} (A : 'G^n.+1) a0 i0, forall {n} i0 a0 (A : 'G^n.+1),
replaceF i0 (- a0) (- A) = - replaceF i0 a0 A. replaceF i0 (- a0) (- A) = - replaceF i0 a0 A.
Proof. Proof.
intros n A a0 i0; extF i; rewrite fct_opp_eq; intros n i0 a0 A; extF i; rewrite fct_opp_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi]; destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy. [rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
Qed. Qed.
Lemma replaceF_minus : Lemma replaceF_minus :
forall {n} (A B : 'G^n.+1) a0 b0 i0, forall {n} i0 a0 b0 (A B : 'G^n.+1),
replaceF i0 (a0 - b0) (A - B) = replaceF i0 a0 A - replaceF i0 b0 B. replaceF i0 (a0 - b0) (A - B) = replaceF i0 a0 A - replaceF i0 b0 B.
Proof. intros; rewrite !minus_eq replaceF_plus replaceF_opp; easy. Qed. Proof. intros; rewrite !minus_eq replaceF_plus replaceF_opp; easy. Qed.
...@@ -350,9 +350,9 @@ Proof. easy. Qed. ...@@ -350,9 +350,9 @@ Proof. easy. Qed.
(** [mapF_minus] is [f_minus_compat_mapF] in [Group_morphism]. *) (** [mapF_minus] is [f_minus_compat_mapF] in [Group_morphism]. *)
Lemma sum_squeezeF : Lemma sum_squeezeF :
forall {n} (u : 'G^n.+1) {i0 i1}, i1 <> i0 -> sum (squeezeF i0 i1 u) = sum u. forall {n} {i0 i1} (H : i1 <> i0) (u : 'G^n.+1), sum (squeezeF i0 i1 u) = sum u.
Proof. Proof.
intros n u i0 i1 Hi. intros n i0 i1 Hi u.
apply (plus_reg_l (u i0 + replaceF i0 (u i0 + u i1) u i1)). apply (plus_reg_l (u i0 + replaceF i0 (u i0 + u i1) u i1)).
rewrite -plus_assoc -sum_skipF replaceF_correct_r//. rewrite -plus_assoc -sum_skipF replaceF_correct_r//.
rewrite sum_replaceF; easy. rewrite sum_replaceF; easy.
......
Algebra/ModuleSpace/ModuleSpace_FF_FT.v
View file @ 5ba16a8b
...@@ -267,7 +267,7 @@ Lemma scalF_liftF_S : ...@@ -267,7 +267,7 @@ Lemma scalF_liftF_S :
Proof. easy. Qed. Proof. easy. Qed.
Lemma scalF_insertF : Lemma scalF_insertF :
forall {n} a a0 (u : 'E^n) x0 i0, forall {n} i0 a0 x0 a (u : 'E^n),
scalF (insertF i0 a0 a) (insertF i0 x0 u) = scalF (insertF i0 a0 a) (insertF i0 x0 u) =
insertF i0 (scal a0 x0) (scalF a u). insertF i0 (scal a0 x0) (scalF a u).
Proof. Proof.
...@@ -276,23 +276,23 @@ intros; extF; rewrite scalF_correct; unfold insertF; ...@@ -276,23 +276,23 @@ intros; extF; rewrite scalF_correct; unfold insertF;
Qed. Qed.
Lemma scalF_insert2F : Lemma scalF_insert2F :
forall {n} a a0 a1 (u : 'E^n) x0 x1 {i0 i1} (H : i1 <> i0), forall {n} {i0 i1} (H : i1 <> i0) a0 a1 x0 x1 a (u : 'E^n),
scalF (insert2F H a0 a1 a) (insert2F H x0 x1 u) = scalF (insert2F H a0 a1 a) (insert2F H x0 x1 u) =
insert2F H (scal a0 x0) (scal a1 x1) (scalF a u). insert2F H (scal a0 x0) (scal a1 x1) (scalF a u).
Proof. intros; rewrite 3!insert2F_correct 2!scalF_insertF; easy. Qed. Proof. intros; rewrite 3!insert2F_correct 2!scalF_insertF; easy. Qed.
Lemma scalF_skipF : Lemma scalF_skipF :
forall {n} a (u : 'E^n.+1) i0, forall {n} i0 a (u : 'E^n.+1),
scalF (skipF i0 a) (skipF i0 u) = skipF i0 (scalF a u). scalF (skipF i0 a) (skipF i0 u) = skipF i0 (scalF a u).
Proof. easy. Qed. Proof. easy. Qed.
Lemma scalF_skip2F : Lemma scalF_skip2F :
forall {n} a (u : 'E^n.+2) {i0 i1} (H : i1 <> i0), forall {n} {i0 i1} (H : i1 <> i0) a (u : 'E^n.+2),
scalF (skip2F H a) (skip2F H u) = skip2F H (scalF a u). scalF (skip2F H a) (skip2F H u) = skip2F H (scalF a u).
Proof. easy. Qed. Proof. easy. Qed.
Lemma scalF_replaceF : Lemma scalF_replaceF :
forall {n} a a0 (u : 'E^n) x0 i0, forall {n} i0 a0 x0 a (u : 'E^n),
scalF (replaceF i0 a0 a) (replaceF i0 x0 u) = scalF (replaceF i0 a0 a) (replaceF i0 x0 u) =
replaceF i0 (scal a0 x0) (scalF a u). replaceF i0 (scal a0 x0) (scalF a u).
Proof. Proof.
...@@ -300,7 +300,7 @@ intros; rewrite 3!replaceF_equiv_def_skipF scalF_skipF scalF_insertF; easy. ...@@ -300,7 +300,7 @@ intros; rewrite 3!replaceF_equiv_def_skipF scalF_skipF scalF_insertF; easy.
Qed. Qed.
Lemma scalF_replace2F : Lemma scalF_replace2F :
forall {n} a a0 a1 (u : 'E^n) x0 x1 i0 i1, forall {n} i0 i1 a0 a1 x0 x1 a (u : 'E^n),
scalF (replace2F i0 i1 a0 a1 a) (replace2F i0 i1 x0 x1 u) = scalF (replace2F i0 i1 a0 a1 a) (replace2F i0 i1 x0 x1 u) =
replace2F i0 i1 (scal a0 x0) (scal a1 x1) (scalF a u). replace2F i0 i1 (scal a0 x0) (scal a1 x1) (scalF a u).
Proof. intros; rewrite 2!scalF_replaceF; easy. Qed. Proof. intros; rewrite 2!scalF_replaceF; easy. Qed.
...@@ -459,27 +459,27 @@ intros n1 n2 l A1 A2; extF i; rewrite !fct_scal_eq; ...@@ -459,27 +459,27 @@ intros n1 n2 l A1 A2; extF i; rewrite !fct_scal_eq;
Qed. Qed.
Lemma insertF_scal : Lemma insertF_scal :
forall {n} l (A : 'E^n) a0 i0, forall {n} i0 l a0 (A : 'E^n),
insertF i0 (scal l a0) (scal l A) = scal l insertF i0 a0 A. insertF i0 (scal l a0) (scal l A) = scal l insertF i0 a0 A.
Proof. Proof.
intros n l A a0 i0; extF i; rewrite !fct_scal_eq; intros n i0 l a0 A; extF i; rewrite !fct_scal_eq;
destruct (ord_eq_dec i i0); destruct (ord_eq_dec i i0);
[rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy. [rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed. Qed.
Lemma insert0F_scal : Lemma insert0F_scal :
forall {n} l (A : 'E^n) i0, insert0F i0 (scal l A) = scal l insert0F i0 A. forall {n} i0 l (A : 'E^n), insert0F i0 (scal l A) = scal l insert0F i0 A.
Proof. intros; rewrite -{1}(scal_zero_r l) insertF_scal; easy. Qed. Proof. intros; rewrite -{1}(scal_zero_r l) insertF_scal; easy. Qed.
Lemma skipF_scal : Lemma skipF_scal :
forall {n} l (A : 'E^n.+1) i0, skipF i0 (scal l A) = scal l skipF i0 A. forall {n} i0 l (A : 'E^n.+1), skipF i0 (scal l A) = scal l skipF i0 A.
Proof. easy. Qed. Proof. easy. Qed.
Lemma replaceF_scal : Lemma replaceF_scal :
forall {n} l (A : 'E^n.+1) a0 i0, forall {n} i0 l a0 (A : 'E^n.+1),
replaceF i0 (scal l a0) (scal l A) = scal l replaceF i0 a0 A. replaceF i0 (scal l a0) (scal l A) = scal l replaceF i0 a0 A.
Proof. Proof.
intros n l A a0 i0; extF i; rewrite !fct_scal_eq; intros n i0 l a0 A; extF i; rewrite !fct_scal_eq;
destruct (ord_eq_dec i i0); destruct (ord_eq_dec i i0);
[rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy. [rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
Qed. Qed.
......
Algebra/ModuleSpace/ModuleSpace_R_compl.v
View file @ 5ba16a8b
...@@ -533,7 +533,7 @@ Qed. ...@@ -533,7 +533,7 @@ Qed.
Lemma dot_product_def : forall {n} (u : 'R^n), u ⋅ u = 0 -> u = 0. Lemma dot_product_def : forall {n} (u : 'R^n), u ⋅ u = 0 -> u = 0.
Proof. Proof.
intros n u; induction n as [| n Hn]; [intros; apply hat0F_eq; easy |]. intros n u; induction n as [| n Hn]; [intros; apply hat0F_eq; easy |].
rewrite (dot_product_skipF _ _ ord0); intros Hu. rewrite (dot_product_skipF ord0); intros Hu.
apply Rplus_eq_R0 in Hu; try apply scal_pos_R; try apply dot_product_pos. apply Rplus_eq_R0 in Hu; try apply scal_pos_R; try apply dot_product_pos.
destruct Hu as [Hu0 Hu]. destruct Hu as [Hu0 Hu].
apply (extF_zero_skipF ord0); [apply scal_def_R | apply Hn]; easy. apply (extF_zero_skipF ord0); [apply scal_def_R | apply Hn]; easy.
...@@ -618,7 +618,7 @@ Section Lin_map_Euclidean_space_R_Facts. ...@@ -618,7 +618,7 @@ Section Lin_map_Euclidean_space_R_Facts.
Lemma part1F_fct_lm : Lemma part1F_fct_lm :
forall {n} (i0 : 'I_n.+1), forall {n} (i0 : 'I_n.+1),
lin_map (part1F^~ i0 - (fun=> part1F 0 i0) : 'R^n -> 'R^n.+1). lin_map (part1F i0 - (fun=> part1F i0 0) : 'R^n -> 'R^n.+1).
Proof. Proof.
intros n i0; apply lm_scatter_rev; intros i; split. intros n i0; apply lm_scatter_rev; intros i; split.
(* *) (* *)
......
Algebra/ModuleSpace/ModuleSpace_compl.v
View file @ 5ba16a8b
...@@ -203,6 +203,9 @@ Proof. intros; subst; apply scal_one. Qed. ...@@ -203,6 +203,9 @@ Proof. intros; subst; apply scal_one. Qed.
Lemma scal_one_r : forall (a b : K), b = 1 -> scal a b = a. Lemma scal_one_r : forall (a b : K), b = 1 -> scal a b = a.
Proof. intros; subst; apply mult_one_r. Qed. Proof. intros; subst; apply mult_one_r. Qed.
Lemma scal_ones : forall {n} a (b : 'K^n), b = 1 -> scal a b = constF n a.
Proof. intros; subst; extF; apply scal_one_r; easy. Qed.
Lemma scal_sum_l : Lemma scal_sum_l :
forall {n} (a : 'K^n) (u : E), scal (sum a) u = sum (fun i => scal (a i) u). forall {n} (a : 'K^n) (u : E), scal (sum a) u = sum (fun i => scal (a i) u).
Proof. Proof.
......
Algebra/ModuleSpace/ModuleSpace_lin_comb.v
View file @ 5ba16a8b
...@@ -326,7 +326,7 @@ Proof. intros; rewrite lc_splitF firstF_concatF lastF_concatF; easy. Qed. ...@@ -326,7 +326,7 @@ Proof. intros; rewrite lc_splitF firstF_concatF lastF_concatF; easy. Qed.
Lemma lc_skipF : Lemma lc_skipF :
forall {n} {L} {B : 'E^n.+1} i0, forall {n} {L} {B : 'E^n.+1} i0,
lin_comb L B = scal (L i0) (B i0) + lin_comb (skipF i0 L) (skipF i0 B). lin_comb L B = scal (L i0) (B i0) + lin_comb (skipF i0 L) (skipF i0 B).
Proof. intros n L B i0; unfold lin_comb; rewrite (sum_skipF _ i0); easy. Qed. Proof. intros n L B i0; unfold lin_comb; rewrite (sum_skipF i0); easy. Qed.
Lemma lc_skipF_ex_l : Lemma lc_skipF_ex_l :
forall {n} L0 L1 (B : 'E^n.+1) i0, forall {n} L0 L1 (B : 'E^n.+1) i0,
...@@ -423,76 +423,75 @@ assert (HL1b : skipFmax L1 = L) by apply skipF_insertF. ...@@ -423,76 +423,75 @@ assert (HL1b : skipFmax L1 = L) by apply skipF_insertF.
rewrite -skipF_last -{1}HL1b -lc_skip_zero_l// -insertF_concatF_max; easy. rewrite -skipF_last -{1}HL1b -lc_skip_zero_l// -insertF_concatF_max; easy.
Qed. Qed.
Lemma lc_insertF :
forall {n} i0 a0 x0 L (B : 'E^n),
lin_comb (insertF i0 a0 L) (insertF i0 x0 B) = scal a0 x0 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insertF; apply sum_insertF. Qed.
Lemma lc_insertF_l :
forall {n} i0 a0 L (B : 'E^n.+1),
lin_comb (insertF i0 a0 L) B = scal a0 (B i0) + lin_comb L (skipF i0 B).
Proof.
intros n i0 a0 L B; rewrite -{1}(insertF_skipF i0 B) lc_insertF; easy.
Qed.
Lemma lc_insertF_r :
forall {n} i0 x0 L (B : 'E^n),
lin_comb L (insertF i0 x0 B) = scal (L i0) x0 + lin_comb (skipF i0 L) B.
Proof.
intros n i0 x0 L B; rewrite -{1}(insertF_skipF i0 L) lc_insertF; easy.
Qed.
Lemma lc_insert2F :
forall {n} {i0 i1} (H : i1 <> i0) x0 x1 a0 a1 L (B : 'E^n),
lin_comb (insert2F H a0 a1 L) (insert2F H x0 x1 B) =
scal a0 x0 + scal a1 x1 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insert2F; apply sum_insert2F. Qed.
Lemma lc_skip2F : Lemma lc_skip2F :
forall {n} L (B : 'E^n.+2) {i0 i1} (H : i1 <> i0), forall {n i0 i1} (H : i1 <> i0) L (B : 'E^n.+2),
lin_comb L B = lin_comb L B =
scal (L i0) (B i0) + scal (L i1) (B i1) + scal (L i0) (B i0) + scal (L i1) (B i1) +
lin_comb (skip2F H L) (skip2F H B). lin_comb (skip2F H L) (skip2F H B).
Proof. Proof.
intros n L B i0 i1 H; unfold lin_comb; rewrite (sum_skip2F _ H); easy. intros n i0 i1 H L B; unfold lin_comb; rewrite (sum_skip2F H); easy.
Qed. Qed.
Lemma lc_two : Lemma lc_two :
forall {n L} {B : 'E^n.+2} {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat), forall {n} {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat) {L} {B : 'E^n.+2},
skip2F H (scalF L B) = 0 -> skip2F H (scalF L B) = 0 ->
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1). lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof. move=>>; rewrite -!scalF_correct; apply sum_two. Qed. Proof. move=>>; rewrite -!scalF_correct; apply sum_two. Qed.
Lemma lc_two_l : Lemma lc_two_l :
forall {n L} {B : 'E^n.+2} {i0 i1} (H : i1 <> i0), forall {n i0 i1} (H : i1 <> i0) {L} {B : 'E^n.+2},
skip2F H L = 0 -> skip2F H L = 0 ->
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1). lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof. Proof.
intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F. intros n i0 i1 Hi L B H; apply lc_two with Hi; rewrite -scalF_skip2F.
apply scalF_zero_compat_l; easy. apply scalF_zero_compat_l; easy.
Qed. Qed.
Lemma lc_two_r : Lemma lc_two_r :
forall {n L} {B : 'E^n.+2} {i0 i1} (H : i1 <> i0), forall {n i0 i1} (H : i1 <> i0) {L} {B : 'E^n.+2},
skip2F H B = 0 -> skip2F H B = 0 ->
lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1). lin_comb L B = scal (L i0) (B i0) + scal (L i1) (B i1).
Proof. Proof.
intros n L B i0 i1 Hi H; apply lc_two with Hi; rewrite -scalF_skip2F. intros n i0 i1 Hi L B H; apply lc_two with Hi; rewrite -scalF_skip2F.
apply scalF_zero_compat_r; easy. apply scalF_zero_compat_r; easy.
Qed. Qed.
Lemma lc_insertF :
forall {n} L (B : 'E^n) a0 x0 i0,
lin_comb (insertF i0 a0 L) (insertF i0 x0 B) = scal a0 x0 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insertF; apply sum_insertF. Qed.
Lemma lc_insertF_l :
forall {n} L (B : 'E^n.+1) a0 i0,
lin_comb (insertF i0 a0 L) B = scal a0 (B i0) + lin_comb L (skipF i0 B).
Proof.
intros n L B a0 i0; rewrite -{1}(insertF_skipF i0 B) lc_insertF; easy.
Qed.
Lemma lc_insertF_r :
forall {n} L (B : 'E^n) x0 i0,
lin_comb L (insertF i0 x0 B) = scal (L i0) x0 + lin_comb (skipF i0 L) B.
Proof.
intros n L B x0 i0; rewrite -{1}(insertF_skipF i0 L) lc_insertF; easy.
Qed.
Lemma lc_insert2F :
forall {n} L (B : 'E^n) a0 a1 x0 x1 {i0 i1} (H : i1 <> i0),
lin_comb (insert2F H a0 a1 L) (insert2F H x0 x1 B) =
scal a0 x0 + scal a1 x1 + lin_comb L B.
Proof. intros; unfold lin_comb; rewrite scalF_insert2F; apply sum_insert2F. Qed.
Lemma lc_replaceF : Lemma lc_replaceF :
forall {n} L (B : 'E^n) a0 x0 i0, forall {n} i0 a0 x0 L (B : 'E^n),
scal (L i0) (B i0) + lin_comb (replaceF i0 a0 L) (replaceF i0 x0 B) = scal (L i0) (B i0) + lin_comb (replaceF i0 a0 L) (replaceF i0 x0 B) =
scal a0 x0 + lin_comb L B. scal a0 x0 + lin_comb L B.
Proof. Proof.
intros [| n] L B a0 x0 i0; [destruct i0; easy |]. intros [| n] i0 a0 x0 L B; [destruct i0; easy |].
unfold lin_comb; rewrite scalF_replaceF -scalF_correct; apply sum_replaceF. unfold lin_comb; rewrite scalF_replaceF -scalF_correct; apply sum_replaceF.
Qed. Qed.
Lemma lc_replace2F : Lemma lc_replace2F :
forall {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1}, forall {n} {i0 i1} (H : i1 <> i0) a0 a1 x0 x1 L (B : 'E^n.+2),
i1 <> i0 ->
scal (L i0) (B i0) + scal (L i1) (B i1) + scal (L i0) (B i0) + scal (L i1) (B i1) +
lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) = lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) =
scal a0 x0 + scal a1 x1 + lin_comb L B. scal a0 x0 + scal a1 x1 + lin_comb L B.
...@@ -502,8 +501,7 @@ intros; unfold lin_comb; rewrite scalF_replace2F -!scalF_correct; ...@@ -502,8 +501,7 @@ intros; unfold lin_comb; rewrite scalF_replace2F -!scalF_correct;
Qed. Qed.
Lemma lc_replace2F_eq : Lemma lc_replace2F_eq :
forall {n} L (B : 'E^n.+2) a0 a1 x0 x1 {i0 i1}, forall {n} {i0 i1} (H : i1 = i0) a0 a1 x0 x1 L (B : 'E^n.+2),
i1 = i0 ->
scal (L i1) (B i1) + scal (L i1) (B i1) +
lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) = lin_comb (replace2F i0 i1 a0 a1 L) (replace2F i0 i1 x0 x1 B) =
scal a1 x1 + lin_comb L B. scal a1 x1 + lin_comb L B.
...@@ -1005,12 +1003,12 @@ Lemma dot_product_ind_l : ...@@ -1005,12 +1003,12 @@ Lemma dot_product_ind_l :
Proof. intros; unfold dot_product; rewrite lc_ind_l; easy. Qed. Proof. intros; unfold dot_product; rewrite lc_ind_l; easy. Qed.
Lemma dot_product_insertF : Lemma dot_product_insertF :
forall {n} (u v : 'K^n) a b i0, forall {n} i0 a b (u v : 'K^n),
insertF i0 a u ⋅ insertF i0 b v = a * b + u ⋅ v. insertF i0 a u ⋅ insertF i0 b v = a * b + u ⋅ v.
Proof. intros; unfold dot_product; rewrite lc_insertF; easy. Qed. Proof. intros; unfold dot_product; rewrite lc_insertF; easy. Qed.
Lemma dot_product_skipF : Lemma dot_product_skipF :
forall {n} (u v : 'K^n.+1) i0, forall {n} i0 (u v : 'K^n.+1),
u ⋅ v = scal (u i0) (v i0) + skipF i0 u ⋅ skipF i0 v. u ⋅ v = scal (u i0) (v i0) + skipF i0 u ⋅ skipF i0 v.
Proof. intros; unfold dot_product; apply lc_skipF. Qed. Proof. intros; unfold dot_product; apply lc_skipF. Qed.
......
Algebra/Monoid/MonoidMult.v
View file @ 5ba16a8b
...@@ -110,7 +110,7 @@ Lemma sum_absorbing : ...@@ -110,7 +110,7 @@ Lemma sum_absorbing :
forall x0 {n} (u : 'G^n), absorbing x0 -> inF x0 u -> sum u = x0. forall x0 {n} (u : 'G^n), absorbing x0 -> inF x0 u -> sum u = x0.
Proof. Proof.
intros x0 [| n] u Hx0 [i0 Hu]; [now destruct i0 |]. intros x0 [| n] u Hx0 [i0 Hu]; [now destruct i0 |].
rewrite (sum_skipF _ i0) -Hu; easy. rewrite (sum_skipF i0) -Hu; easy.
Qed. Qed.
End Multiplicative_Monoid_Facts. End Multiplicative_Monoid_Facts.
...@@ -172,7 +172,7 @@ Lemma prod_nat_one_compat : forall {n} (u : 'nat_mul^n), u = 1 -> prod_nat u = 1 ...@@ -172,7 +172,7 @@ Lemma prod_nat_one_compat : forall {n} (u : 'nat_mul^n), u = 1 -> prod_nat u = 1
Proof. move=>>; apply sum_zero_compat. Qed. Proof. move=>>; apply sum_zero_compat. Qed.
Lemma prod_nat_singl : Lemma prod_nat_singl :
forall {n} (u : 'nat_mul^n.+1) i0, skipF i0 u = 1 -> prod_nat u = u i0. forall {n} i0 (u : 'nat_mul^n.+1), skipF i0 u = 1 -> prod_nat u = u i0.
Proof. move=>>; apply sum_one. Qed. Proof. move=>>; apply sum_one. Qed.
Lemma prod_nat_castF : Lemma prod_nat_castF :
...@@ -193,7 +193,7 @@ Lemma prod_nat_concatF : ...@@ -193,7 +193,7 @@ Lemma prod_nat_concatF :
Proof. intros; apply sum_concatF. Qed. Proof. intros; apply sum_concatF. Qed.
Lemma prod_nat_replaceF : Lemma prod_nat_replaceF :
forall {n} (u : 'nat_mul^n.+1) x0 i0, forall {n} i0 x0 (u : 'nat_mul^n.+1),
u i0 * prod_nat (replaceF i0 x0 u) = x0 * prod_nat u. u i0 * prod_nat (replaceF i0 x0 u) = x0 * prod_nat u.
Proof. intros; apply sum_replaceF. Qed. Proof. intros; apply sum_replaceF. Qed.
...@@ -266,7 +266,7 @@ Lemma prod_R_one_compat : forall {n} (u : 'R_mul^n), u = 1 -> prod_R u = 1. ...@@ -266,7 +266,7 @@ Lemma prod_R_one_compat : forall {n} (u : 'R_mul^n), u = 1 -> prod_R u = 1.
Proof. move=>>; apply sum_zero_compat. Qed. Proof. move=>>; apply sum_zero_compat. Qed.
Lemma prod_R_singl : Lemma prod_R_singl :
forall {n} (u : 'R_mul^n.+1) i0, skipF i0 u = 1 -> prod_R u = u i0. forall {n} i0 (u : 'R_mul^n.+1), skipF i0 u = 1 -> prod_R u = u i0.
Proof. move=>>; apply sum_one. Qed. Proof. move=>>; apply sum_one. Qed.
Lemma prod_R_castF : Lemma prod_R_castF :
...@@ -286,7 +286,7 @@ Lemma prod_R_concatF : ...@@ -286,7 +286,7 @@ Lemma prod_R_concatF :
Proof. intros; apply sum_concatF. Qed. Proof. intros; apply sum_concatF. Qed.
Lemma prod_R_replaceF : Lemma prod_R_replaceF :
forall {n} (u : 'R_mul^n.+1) x0 i0, forall {n} i0 x0 (u : 'R_mul^n.+1),
u i0 * prod_R (replaceF i0 x0 u) = x0 * prod_R u. u i0 * prod_R (replaceF i0 x0 u) = x0 * prod_R u.
Proof. intros; apply sum_replaceF. Qed. Proof. intros; apply sum_replaceF. Qed.
......
Algebra/Monoid/Monoid_FF.v
View file @ 5ba16a8b
...@@ -524,7 +524,7 @@ Proof. move=>> HA H0; rewrite HA H0; apply insertF_zero. Qed. ...@@ -524,7 +524,7 @@ Proof. move=>> HA H0; rewrite HA H0; apply insertF_zero. Qed.
Lemma insert2F_zero_compat : Lemma insert2F_zero_compat :
forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n), forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n),
x0 = 0 -> x1 = 0 -> A = 0 ->insert2F H x0 x1 A = 0. x0 = 0 -> x1 = 0 -> A = 0 -> insert2F H x0 x1 A = 0.
Proof. move=>> HA H0 H1; rewrite HA H0 H1; apply insert2F_zero. Qed. Proof. move=>> HA H0 H1; rewrite HA H0 H1; apply insert2F_zero. Qed.
Lemma skipF_zero_compat : Lemma skipF_zero_compat :
......
Algebra/Monoid/Monoid_sum.v
View file @ 5ba16a8b
...@@ -202,9 +202,9 @@ Lemma sum_splitF : ...@@ -202,9 +202,9 @@ Lemma sum_splitF :
forall {n1 n2} (u : 'G^(n1 + n2)), sum u = sum (firstF u) + sum (lastF u). forall {n1 n2} (u : 'G^(n1 + n2)), sum u = sum (firstF u) + sum (lastF u).
Proof. intros n1 n2 u; rewrite {1}(concatF_splitF u); apply sum_concatF. Qed. Proof. intros n1 n2 u; rewrite {1}(concatF_splitF u); apply sum_concatF. Qed.
Lemma sum_skipF : forall {n} (u : 'G^n.+1) i0, sum u = u i0 + sum (skipF i0 u). Lemma sum_skipF : forall {n} i0 (u : 'G^n.+1), sum u = u i0 + sum (skipF i0 u).
Proof. Proof.
intros n u i0. intros n i0 u.
rewrite -(sum_castF (ordS_splitS i0)) sum_splitF sum_ind_r. rewrite -(sum_castF (ordS_splitS i0)) sum_splitF sum_ind_r.
rewrite -(sum_castF (ord_split i0)) sum_splitF. rewrite -(sum_castF (ord_split i0)) sum_splitF.
rewrite plus_assoc (plus_comm (u i0) _). rewrite plus_assoc (plus_comm (u i0) _).
...@@ -215,94 +215,93 @@ rewrite lastF_skipF; easy. ...@@ -215,94 +215,93 @@ rewrite lastF_skipF; easy.
Qed. Qed.
Lemma sum_skipF_compat : Lemma sum_skipF_compat :
forall {n} (u v : 'G^n.+1) i0, forall {n} i0 (u v : 'G^n.+1),
u i0 = v i0 -> sum (skipF i0 u) = sum (skipF i0 v) -> sum u = sum v. u i0 = v i0 -> sum (skipF i0 u) = sum (skipF i0 v) -> sum u = sum v.
Proof. Proof.
intros n u v i0 H0 H1; rewrite !(sum_skipF _ i0) H0; apply plus_compat_l; easy. intros n i0 u v H0 H1; rewrite !(sum_skipF i0) H0; apply plus_compat_l; easy.
Qed. Qed.
Lemma sum_skipF_ex : Lemma sum_skipF_ex :
forall {n} u0 (u1 : 'G^n) i0, forall {n} i0 u0 (u1 : 'G^n),
exists u, sum u = u0 + sum u1 /\ u i0 = u0 /\ skipF i0 u = u1. exists u, sum u = u0 + sum u1 /\ u i0 = u0 /\ skipF i0 u = u1.
Proof. Proof.
intros n u0 u1 i0; destruct (skipF_ex i0 u0 u1) as [u [Hu0 Hu1]]. intros n i0 u0 u1; destruct (skipF_ex i0 u0 u1) as [u [Hu0 Hu1]].
exists u; repeat split; try easy; rewrite -Hu0 -Hu1; apply sum_skipF. exists u; repeat split; try easy; rewrite -Hu0 -Hu1; apply sum_skipF.
Qed. Qed.
Lemma sum_one : forall {n} (u : 'G^n.+1) i0, skipF i0 u = 0 -> sum u = u i0. Lemma sum_one : forall {n} i0 (u : 'G^n.+1), skipF i0 u = 0 -> sum u = u i0.
Proof. Proof.
intros; erewrite sum_skipF, sum_zero_compat; try apply plus_zero_r; easy. intros; erewrite sum_skipF, sum_zero_compat; try apply plus_zero_r; easy.
Qed. Qed.
Lemma sum_skip_zero : Lemma sum_skip_zero :
forall {n} {u : 'G^n.+1} i0, u i0 = 0 -> sum u = sum (skipF i0 u). forall {n} i0 {u : 'G^n.+1}, u i0 = 0 -> sum u = sum (skipF i0 u).
Proof. Proof.
move=>> Hi0; rewrite -(plus_zero_l (sum (skipF _ _))) -Hi0; apply sum_skipF. move=>> Hi0; rewrite -(plus_zero_l (sum (skipF _ _))) -Hi0; apply sum_skipF.
Qed. Qed.
Lemma sum_skip2F : Lemma sum_skip2F :
forall {n} (u : 'G^n.+2) {i0 i1} (H : i1 <> i0), forall {n} {i0 i1} (H : i1 <> i0) (u : 'G^n.+2),
sum u = u i0 + u i1 + sum (skip2F H u). sum u = u i0 + u i1 + sum (skip2F H u).
Proof. Proof.
intros n u i0 i1 H. intros n i0 i1 H u.
rewrite (sum_skipF _ i0) -plus_assoc; f_equal. rewrite (sum_skipF i0) -plus_assoc; f_equal.
rewrite (sum_skipF _ (insert_ord H)) skip2F_correct; f_equal. rewrite (sum_skipF (insert_ord H)) skip2F_correct; f_equal.
rewrite skipF_correct; easy. rewrite skipF_correct; easy.
Qed. Qed.
Lemma sum_two : Lemma sum_two :
forall {n} (u : 'G^n.+2) {i0 i1 : 'I_n.+2} (H : (i1 <> i0)%nat), forall {n} {i0 i1 : 'I_n.+2} (H : i1 <> i0) (u : 'G^n.+2),
skip2F H u = 0 -> sum u = u i0 + u i1. skip2F H u = 0 -> sum u = u i0 + u i1.
Proof. Proof.
move=>> H; erewrite sum_skip2F, sum_zero_compat. apply plus_zero_r. apply H. move=>> H; erewrite sum_skip2F, sum_zero_compat. apply plus_zero_r. apply H.
Qed. Qed.
Lemma sum_insertF : Lemma sum_insertF :
forall {n} (u : 'G^n) x0 i0, sum (insertF i0 x0 u) = x0 + sum u. forall {n} i0 x0 (u : 'G^n), sum (insertF i0 x0 u) = x0 + sum u.
Proof. Proof.
intros; erewrite sum_skipF; rewrite -> insertF_correct_l, skipF_insertF; easy. intros; erewrite sum_skipF; rewrite -> insertF_correct_l, skipF_insertF; easy.
Qed. Qed.
Lemma sum_insert0F : forall {n} (u : 'G^n) i0, sum (insert0F i0 u) = sum u. Lemma sum_insert0F : forall {n} i0 (u : 'G^n), sum (insert0F i0 u) = sum u.
Proof. intros; rewrite sum_insertF plus_zero_l; easy. Qed. Proof. intros; rewrite sum_insertF plus_zero_l; easy. Qed.
Lemma sum_insert2F : Lemma sum_insert2F :
forall {n} (u : 'G^n) x0 x1 {i0 i1} (H : i1 <> i0), forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (u : 'G^n),
sum (insert2F H x0 x1 u) = x0 + x1 + sum u. sum (insert2F H x0 x1 u) = x0 + x1 + sum u.
Proof. intros; rewrite insert2F_correct 2!sum_insertF; apply plus_assoc. Qed. Proof. intros; rewrite insert2F_correct 2!sum_insertF; apply plus_assoc. Qed.
Lemma sum_replaceF : Lemma sum_replaceF :
forall {n} (u : 'G^n.+1) x0 i0, u i0 + sum (replaceF i0 x0 u) = x0 + sum u. forall {n} i0 x0 (u : 'G^n.+1), u i0 + sum (replaceF i0 x0 u) = x0 + sum u.
Proof. Proof.
intros n u x0 i0; rewrite replaceF_equiv_def_insertF sum_insertF (sum_skipF u i0). intros n i0 x0 u; rewrite replaceF_equiv_def_insertF sum_insertF (sum_skipF i0).
rewrite 2!plus_assoc (plus_comm (u i0)); easy. rewrite 2!plus_assoc (plus_comm (u i0)); easy.
Qed. Qed.
Lemma sum_replace0F : Lemma sum_replace0F :
forall {n} (u : 'G^n.+1) i0, forall {n} i0 (u : 'G^n.+1),
u i0 + sum (replace0F i0 u) = u i0 + sum (skipF i0 u). u i0 + sum (replace0F i0 u) = u i0 + sum (skipF i0 u).
Proof. intros; rewrite sum_replaceF -sum_skipF plus_zero_l; easy. Qed. Proof. intros; rewrite sum_replaceF -sum_skipF plus_zero_l; easy. Qed.
Lemma sum_replace2F : Lemma sum_replace2F :
forall {n} (u : 'G^n.+2) x0 x1 {i0 i1}, forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (u : 'G^n.+2),
i1 <> i0 -> u i0 + u i1 + sum (replace2F i0 i1 x0 x1 u) = x0 + x1 + sum u. u i0 + u i1 + sum (replace2F i0 i1 x0 x1 u) = x0 + x1 + sum u.
Proof. Proof.
intros n u x0 x1 i0 i1 H; unfold replace2F. intros n i0 i1 H x0 x1 u; unfold replace2F.
rewrite (plus_comm x0) -plus_assoc -(replaceF_correct_r x0 _ H). rewrite (plus_comm x0) -plus_assoc -(replaceF_correct_r x0 _ H).
rewrite sum_replaceF plus_comm3_l sum_replaceF plus_assoc; easy. rewrite sum_replaceF plus_comm3_l sum_replaceF plus_assoc; easy.
Qed. Qed.
Lemma sum_replace2F_eq : Lemma sum_replace2F_eq :
forall {n} (u : 'G^n.+2) x0 x1 {i0 i1}, forall {n} {i0 i1} (H : i1 = i0) x0 x1 (u : 'G^n.+2),
i1 = i0 -> u i1 + sum (replace2F i0 i1 x0 x1 u) = x1 + sum u. u i1 + sum (replace2F i0 i1 x0 x1 u) = x1 + sum u.
Proof. intros; rewrite -> replace2F_correct_eq, sum_replaceF; easy. Qed. Proof. intros; rewrite replace2F_correct_eq// sum_replaceF; easy. Qed.
Lemma sum_permutF : Lemma sum_permutF :
forall {n} p (u : 'G^n), injective p -> sum (permutF p u) = sum u. forall {n} p (u : 'G^n), injective p -> sum (permutF p u) = sum u.
Proof. Proof.
intros n p u Hp; induction n as [| n]. intros n p u Hp; induction n as [| n]; [rewrite !sum_nil; easy |].
rewrite !sum_nil; easy. rewrite (sum_skipF ord0) (sum_skipF (p ord0)); f_equal.
rewrite (sum_skipF (permutF _ _) ord0) (sum_skipF u (p ord0)); f_equal.
rewrite skipF_permutF IHn; try apply skip_f_ord_inj; easy. rewrite skipF_permutF IHn; try apply skip_f_ord_inj; easy.
Qed. Qed.
...@@ -334,8 +333,8 @@ Qed. ...@@ -334,8 +333,8 @@ Qed.
Lemma sum_itemF : forall {n} (x : G) i0, sum (itemF n i0 x) = x. Lemma sum_itemF : forall {n} (x : G) i0, sum (itemF n i0 x) = x.
Proof. Proof.
intros [| n] x i0; [now destruct i0 |]. intros [| n] x i0; [now destruct i0 |]; unfold itemF.
unfold itemF; generalize (sum_replaceF (0 : 'G^n.+1) x i0). unfold itemF; generalize (sum_replaceF i0 x (0 : 'G^n.+1)).
rewrite sum_zero plus_zero_l plus_zero_r; easy. rewrite sum_zero plus_zero_l plus_zero_r; easy.
Qed. Qed.
...@@ -387,8 +386,8 @@ Proof. ...@@ -387,8 +386,8 @@ Proof.
apply (nat_ind2 (fun m n => apply (nat_ind2 (fun m n =>
forall u : 'G^{m,n}, sum (sum u) = sum (sum (flipT u)))). forall u : 'G^{m,n}, sum (sum u) = sum (sum (flipT u)))).
intros; rewrite 2!sum_nil; easy. intros; rewrite 2!sum_nil; easy.
move=>> H u; rewrite 2!(sum_skipF _ ord0) sum_plus sum_row H -sum_skipTc; easy. move=>> H u; rewrite 2!(sum_skipF ord0) sum_plus sum_row H -sum_skipTc; easy.
move=>> H u; rewrite 2!(sum_skipF _ ord0) sum_plus sum_col -H sum_skipTc; easy. move=>> H u; rewrite 2!(sum_skipF ord0) sum_plus sum_col -H sum_skipTc; easy.
Qed. Qed.
(** Functions to Abelian monoid. *) (** Functions to Abelian monoid. *)
...@@ -430,7 +429,7 @@ Lemma sum_skipF_equiv : ...@@ -430,7 +429,7 @@ Lemma sum_skipF_equiv :
forall {n} {u v : 'G^n.+1} {i0}, forall {n} {u v : 'G^n.+1} {i0},
sum u = sum v -> sum (skipF i0 u) = sum (skipF i0 v) <-> u i0 = v i0. sum u = sum v -> sum (skipF i0 u) = sum (skipF i0 v) <-> u i0 = v i0.
Proof. Proof.
intros n u v i0; rewrite !(sum_skipF _ i0) => H; split; intros H0; intros n u v i0; rewrite !(sum_skipF i0) => H; split; intros H0;
[| apply plus_is_reg_equiv in HG2]; move: H; rewrite H0; apply HG2. [| apply plus_is_reg_equiv in HG2]; move: H; rewrite H0; apply HG2.
Qed. Qed.
...@@ -483,7 +482,7 @@ Lemma sum_nonneg_ub_R : ...@@ -483,7 +482,7 @@ Lemma sum_nonneg_ub_R :
forall {n} (u : 'R^n) i, (forall i, 0 <= u i) -> u i <= sum u. forall {n} (u : 'R^n) i, (forall i, 0 <= u i) -> u i <= sum u.
Proof. Proof.
intros [| n] u i Hx; [now destruct i |]. intros [| n] u i Hx; [now destruct i |].
rewrite (sum_skipF _ i) -{1}(plus_zero_r (u i)); apply Rplus_le_compat; rewrite (sum_skipF i) -{1}(plus_zero_r (u i)); apply Rplus_le_compat;
[apply Rle_refl | apply sum_nonneg_R]. [apply Rle_refl | apply sum_nonneg_R].
intros; unfold skipF; easy. intros; unfold skipF; easy.
Qed. Qed.
...@@ -560,7 +559,7 @@ rewrite replaceF_correct_r; try easy. ...@@ -560,7 +559,7 @@ rewrite replaceF_correct_r; try easy.
rewrite constF_correct; auto with arith. rewrite constF_correct; auto with arith.
rewrite <- (Nat.add_0_l (sum _)). rewrite <- (Nat.add_0_l (sum _)).
replace 0%nat with (constF n.+1 0%nat i) at 1 by easy. replace 0%nat with (constF n.+1 0%nat i) at 1 by easy.
generalize (sum_replaceF (constF n.+1 0) (u i) i). generalize (sum_replaceF i (u i) (constF n.+1 0)).
unfold plus; simpl; intros T; rewrite T. unfold plus; simpl; intros T; rewrite T.
rewrite sum_constF_nat. rewrite sum_constF_nat.
rewrite Nat.mul_0_r; auto with zarith. rewrite Nat.mul_0_r; auto with zarith.
......
Algebra/Monoid/Monomial_order.v
View file @ 5ba16a8b
...@@ -244,11 +244,11 @@ Qed. ...@@ -244,11 +244,11 @@ Qed.
Lemma br_sum_conn_equiv : Lemma br_sum_conn_equiv :
forall {R : G -> G -> Prop}, forall {R : G -> G -> Prop},
monomial_order R -> monomial_order R ->
forall {n} {u v : 'G^n.+1} {i0}, forall {n} {i0} {u v : 'G^n.+1},
sum u = sum v -> sum u = sum v ->
R (u i0) (v i0) <-> R (sum (skipF i0 v)) (sum (skipF i0 u)). R (u i0) (v i0) <-> R (sum (skipF i0 v)) (sum (skipF i0 u)).
Proof. Proof.
move=>> HR n u v i0; rewrite !(sum_skipF _ i0); apply br_plus_conn_equiv; easy. move=>> HR n i0 u v; rewrite !(sum_skipF i0); apply br_plus_conn_equiv; easy.
Qed. Qed.
(** About the [monomial_order] / [monomial_order_ns] compound properties. *) (** About the [monomial_order] / [monomial_order_ns] compound properties. *)
...@@ -1309,7 +1309,7 @@ Proof. intros; split; [apply graded_r_rev | apply graded_r]; easy. Qed. ...@@ -1309,7 +1309,7 @@ Proof. intros; split; [apply graded_r_rev | apply graded_r]; easy. Qed.
(* The proof depends on the plus regularity hypothesis HG2. *) (* The proof depends on the plus regularity hypothesis HG2. *)
Lemma graded_S_r_equiv : Lemma graded_S_r_equiv :
forall R {n} (Rn : 'G^n -> 'G^n -> Prop) (x y : 'G^n.+1) i0, forall R {n} (Rn : 'G^n -> 'G^n -> Prop) i0 (x y : 'G^n.+1),
x i0 = y i0 -> sum x = sum y -> x i0 = y i0 -> sum x = sum y ->
graded R Rn (skipF i0 x) (skipF i0 y) <-> Rn (skipF i0 x) (skipF i0 y). graded R Rn (skipF i0 x) (skipF i0 y) <-> Rn (skipF i0 x) (skipF i0 y).
Proof. intros; apply graded_r_equiv, sum_skipF_equiv; easy. Qed. Proof. intros; apply graded_r_equiv, sum_skipF_equiv; easy. Qed.
...@@ -1814,14 +1814,14 @@ assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R). ...@@ -1814,14 +1814,14 @@ assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R).
rewrite grsymlex_S; apply or_iff_compat_l; apply H0; intros H1; split. rewrite grsymlex_S; apply or_iff_compat_l; apply H0; intros H1; split.
(* *) (* *)
move=> [[/eq_sym_equiv H2 H3] | H2]; [| easy]; apply graded_l. move=> [[/eq_sym_equiv H2 H3] | H2]; [| easy]; apply graded_l.
contradict H2; move: H1; rewrite !(sum_skipF _ ord0) H2; apply HG2'. contradict H2; move: H1; rewrite !(sum_skipF ord0) H2; apply HG2'.
apply br_sum_conn_equiv; easy. apply br_sum_conn_equiv; easy.
(* *) (* *)
intros H2; destruct (HG1 (x ord0) (y ord0)) as [H3 | H3]. intros H2; destruct (HG1 (x ord0) (y ord0)) as [H3 | H3].
right; repeat split; easy. right; repeat split; easy.
left; repeat split; [easy.. |]. left; repeat split; [easy.. |].
apply graded_l_rev, br_sum_conn_equiv in H2; [easy.. |]. apply graded_l_rev, br_sum_conn_equiv in H2; [easy.. |].
contradict H3; move: H1; rewrite !(sum_skipF _ ord0) H3; apply HG2'. contradict H3; move: H1; rewrite !(sum_skipF ord0) H3; apply HG2'.
Qed. Qed.
(* The proof depends on the plus regularity hypothesis HG2. *) (* The proof depends on the plus regularity hypothesis HG2. *)
...@@ -1852,14 +1852,14 @@ assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R). ...@@ -1852,14 +1852,14 @@ assert (HG2' : @plus_is_reg_r G) by now apply (monomial_order_plus_is_reg_r R).
rewrite grevlex_S; apply or_iff_compat_l; apply H0; intros H1; split. rewrite grevlex_S; apply or_iff_compat_l; apply H0; intros H1; split.
(* *) (* *)
move=> [[/eq_sym_equiv H2 H3] | H2]; [| easy]; apply graded_l. move=> [[/eq_sym_equiv H2 H3] | H2]; [| easy]; apply graded_l.
contradict H2; move: H1; rewrite !(sum_skipF _ ord_max) H2; apply HG2'. contradict H2; move: H1; rewrite !(sum_skipF ord_max) H2; apply HG2'.
apply br_sum_conn_equiv; easy. apply br_sum_conn_equiv; easy.
(* *) (* *)
intros H2; destruct (HG1 (x ord_max) (y ord_max)) as [H3 | H3]. intros H2; destruct (HG1 (x ord_max) (y ord_max)) as [H3 | H3].
right; repeat split; easy. right; repeat split; easy.
left; repeat split; [easy.. |]. left; repeat split; [easy.. |].
apply graded_l_rev, br_sum_conn_equiv in H2; [easy.. |]. apply graded_l_rev, br_sum_conn_equiv in H2; [easy.. |].
contradict H3; move: H1; rewrite !(sum_skipF _ ord_max) H3; apply HG2'. contradict H3; move: H1; rewrite !(sum_skipF ord_max) H3; apply HG2'.
Qed. Qed.
......