Library Algebra.Group.Group_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Complements on the commutative group algebraic structure.
The AbelianGroup algebraic structure (aka commutative group) is defined
in the Coquelicot library, including the canonical structure
prod_AbelianGroup for the cartesian product of commutative groups.
This module mat be used through the import of Algebra.Group.Group,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Usage
From Requisite Require Import stdlib ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Section Group_Facts.
Context {G : AbelianGroup}.
Lemma inhabited_g : inhabited G.
Proof. apply inhabited_m. Qed.
Lemma inhabited_fct_g : ∀ {T : Type}, inhabited (T → G).
Proof. intros; apply inhabited_fct_m. Qed.
Lemma plus_compat_l_equiv : ∀ x x1 x2 : G, x1 = x2 ↔ x + x1 = x + x2.
Proof. intros; split; [apply plus_compat_l | apply plus_reg_l]. Qed.
Lemma plus_compat_r_equiv : ∀ x x1 x2 : G, x1 = x2 ↔ x1 + x = x2 + x.
Proof. intros; split; [apply plus_compat_r | apply plus_reg_r]. Qed.
Lemma plus_is_zero_l : ∀ x y : G, x + y = 0 → x = - y.
Proof. intros x y H; apply (plus_reg_r y); rewrite plus_opp_l; easy. Qed.
Lemma plus_is_zero_l_equiv : ∀ x y : G, x + y = 0 ↔ x = - y.
Proof. intros; split. apply plus_is_zero_l. move⇒ ->; apply plus_opp_l. Qed.
Lemma plus_is_zero_r : ∀ x y : G, x + y = 0 → y = - x.
Proof. move=>>; rewrite plus_comm; apply plus_is_zero_l. Qed.
Lemma plus_is_zero_r_equiv : ∀ x y : G, x + y = 0 ↔ y = - x.
Proof. intros; split. apply plus_is_zero_r. move⇒ ->; apply plus_opp_r. Qed.
Lemma opp_inj : ∀ x y : G, - x = - y → x = y.
Proof. intros x y H; rewrite -(opp_opp x) H; apply opp_opp. Qed.
Lemma opp_eq : ∀ x y : G, x = y → - x = - y.
Proof. apply f_equal. Qed.
Lemma opp_neq_reg : ∀ x y : G, - x ≠ - y → x ≠ y.
Proof. move=>>; rewrite -contra_equiv; apply opp_eq. Qed.
Lemma opp_neq_compat : ∀ x y : G, x ≠ y → - x ≠ - y.
Proof. move=>>; rewrite -contra_equiv; apply opp_inj. Qed.
Lemma opp_sym : ∀ x y : G, x = - y ↔ - x = y.
Proof. intros; split; [move⇒ → | move⇒ <-]; rewrite opp_opp; easy. Qed.
Lemma opp_zero_equiv : ∀ x : G, x = 0 ↔ - x = 0.
Proof. intros; rewrite -opp_sym opp_zero; easy. Qed.
Lemma minus_eq : ∀ x y : G, x - y = x + (-y).
Proof. easy. Qed.
Lemma minus_zero_l : ∀ x : G, 0 - x = - x.
Proof. intros; apply plus_zero_l. Qed.
Lemma minus_reg_l : ∀ x x1 x2 : G, x - x1 = x - x2 → x1 = x2.
Proof. intros x x1 x2 H; apply opp_inj, (plus_reg_l x); easy. Qed.
Lemma minus_reg_r : ∀ x x1 x2 : G, x1 - x = x2 - x → x1 = x2.
Proof. intros x x1 x2 H; apply (plus_reg_r (- x)); easy. Qed.
Lemma minus_compat_l : ∀ x x1 x2 : G, x1 = x2 → x - x1 = x - x2.
Proof. intros; f_equal; easy. Qed.
Lemma minus_compat_r : ∀ x x1 x2 : G, x1 = x2 → x1 - x = x2 - x.
Proof. intros; f_equal; easy. Qed.
Lemma minus_sym : ∀ x y : G, x - y = - y + x.
Proof. intros; apply plus_comm. Qed.
Lemma minus_opp : ∀ x y : G, x - - y = x + y.
Proof. intros; rewrite minus_eq opp_opp; easy. Qed.
Lemma minus_plus_l_eq : ∀ x x1 x2 : G, x1 - x2 = x + x1 - (x + x2).
Proof.
intros x x1 x2; rewrite (minus_trans x x1 x2) !minus_eq opp_plus 2!plus_assoc.
f_equal; rewrite plus_comm plus_assoc; easy.
Qed.
Lemma minus_plus_r_eq : ∀ x x1 x2 : G, x1 - x2 = x1 + x - (x2 + x).
Proof.
intros; rewrite (minus_plus_l_eq x) (plus_comm _ x1) (plus_comm _ x2); easy.
Qed.
Lemma opp_minus : ∀ x y : G, - (x - y) = y - x.
Proof. intros; rewrite opp_plus opp_opp plus_comm; easy. Qed.
Lemma minus2_eq_zero : ∀ x y : G, x + y - x - y = 0.
Proof.
intros; rewrite !minus_eq -(plus_assoc x y) (plus_comm y) plus_assoc
plus_opp_r plus_zero_l plus_opp_r; easy.
Qed.
Lemma minus_plus_l : ∀ x y : G, x + y - x = y.
Proof.
intros; rewrite minus_eq plus_comm plus_assoc plus_opp_l plus_zero_l; easy.
Qed.
Lemma minus_plus_r : ∀ x y : G, x + y - y = x.
Proof. intros; rewrite minus_eq -plus_assoc plus_opp_r plus_zero_r; easy. Qed.
Lemma minus2_l : ∀ x y : G, x - y - x = - y.
Proof. intros; rewrite !minus_eq -minus_eq; apply minus_plus_l. Qed.
Lemma minus2_r : ∀ x y : G, x - (x - y) = y.
Proof.
intros; rewrite !minus_eq opp_plus opp_opp plus_assoc plus_opp_r;
apply plus_zero_l.
Qed.
Lemma plus_minus_l : ∀ x y : G, x - y + y = x.
Proof. intros; rewrite minus_eq -plus_assoc plus_opp_l; apply plus_zero_r. Qed.
Lemma plus_minus_r : ∀ x y : G, x + (y - x) = y.
Proof.
intros; rewrite minus_eq plus_assoc plus_comm plus_assoc
plus_opp_l plus_zero_l; easy.
Qed.
Lemma minus_plus_assoc : ∀ x y z : G, x - (y + z) = x - y - z.
Proof. intros; rewrite !minus_eq opp_plus plus_assoc; easy. Qed.
Lemma plus_minus_assoc : ∀ x y z : G, x + (y - z) = x + y - z.
Proof. intros; rewrite !minus_eq plus_assoc; easy. Qed.
Lemma minus2 : ∀ x y z : G, x - (y - z) = x - y + z.
Proof. intros; rewrite !minus_eq opp_plus opp_opp plus_assoc; easy. Qed.
Lemma minus_zero_reg : ∀ {x y : G}, x - y = 0 → x = y.
Proof. intros x y H; apply (minus_reg_r y); rewrite minus_eq_zero; easy. Qed.
Lemma minus_zero_reg_sym : ∀ {x y : G}, y - x = 0 → x = y.
Proof.
intros; apply minus_zero_reg, opp_inj; rewrite opp_minus opp_zero; easy.
Qed.
Lemma minus_zero_compat : ∀ {x y : G}, x = y → x - y = 0.
Proof. move=>> ->; apply plus_opp_r. Qed.
Lemma minus_zero_equiv : ∀ x y : G, x - y = 0 ↔ x = y.
Proof. intros; split; [apply minus_zero_reg | apply minus_zero_compat]. Qed.
Lemma minus_zero_reg_contra : ∀ {x y : G}, x ≠ y → x - y ≠ 0.
Proof. move=>>; rewrite -contra_equiv; apply minus_zero_reg. Qed.
Lemma minus_zero_reg_sym_contra : ∀ {x y : G}, x ≠ y → y - x ≠ 0.
Proof. move=>>; rewrite -contra_equiv; apply minus_zero_reg_sym. Qed.
Lemma minus_zero_compat_contra : ∀ {x y : G}, x - y ≠ 0 → x ≠ y.
Proof. move=>>; rewrite -contra_equiv; apply minus_zero_compat. Qed.
Lemma minus_zero_equiv_contra : ∀ x y : G, x - y ≠ 0 ↔ x ≠ y.
Proof. move=>>; rewrite -iff_not_equiv; apply minus_zero_equiv. Qed.
Lemma plus_minus_l_equiv : ∀ x y z : G, x = y + z ↔ y = x - z.
Proof.
intros; split; intros H; rewrite H; rewrite minus_eq -plus_assoc.
rewrite plus_opp_r plus_zero_r; easy.
rewrite plus_opp_l plus_zero_r; easy.
Qed.
Lemma plus_minus_r_equiv : ∀ x y z : G, x = y + z ↔ z = x - y.
Proof. intros; rewrite -plus_minus_l_equiv plus_comm; easy. Qed.
Lemma sum_opp : ∀ {n} (u : 'G^n), sum (- u) = - sum u.
Proof.
intros; apply plus_is_zero_l_equiv; rewrite -sum_plus plus_opp_l sum_zero; easy.
Qed.
Lemma sum_minus :
∀ {n} (u1 u2 : 'G^n), sum (u1 - u2) = sum u1 - sum u2.
Proof. intros; rewrite minus_eq -sum_opp; apply sum_plus. Qed.
Lemma sum_minus_zero_equiv :
∀ {n} (u1 u2 : 'G^n), sum (u1 - u2) = 0 ↔ sum u1 = sum u2.
Proof. intros; rewrite sum_minus; apply minus_zero_equiv. Qed.
End Group_Facts.
Section Group_FF_Facts.
Properties with the additional operations of groups (opp, minus).
Context {G : AbelianGroup}.
Lemma constF_opp : ∀ n (x : G), constF n (- x) = - constF n x.
Proof. easy. Qed.
Lemma constF_minus :
∀ n (x y : G), constF n (x - y) = constF n x - constF n y.
Proof. easy. Qed.
Lemma castF_opp :
∀ {n1 n2} (H : n1 = n2) (A1 : 'G^n1), castF H (- A1) = - castF H A1.
Proof. easy. Qed.
Lemma castF_minus :
∀ {n1 n2} (H : n1 = n2) (A1 y1 : 'G^n1),
castF H (A1 - y1) = castF H A1 - castF H y1.
Proof. easy. Qed.
Lemma widenF_S_opp : ∀ {n} (A : 'G^n.+1), widenF_S (- A) = - widenF_S A.
Proof. easy. Qed.
Lemma widenF_S_minus :
∀ {n} (A B : 'G^n.+1), widenF_S (A - B) = widenF_S A - widenF_S B.
Proof. easy. Qed.
Lemma liftF_S_opp : ∀ {n} (A : 'G^n.+1), liftF_S (- A) = - liftF_S A.
Proof. easy. Qed.
Lemma liftF_S_minus :
∀ {n} (A B : 'G^n.+1), liftF_S (A - B) = liftF_S A - liftF_S B.
Proof. easy. Qed.
Lemma widenF_opp :
∀ {n1 n2} (H : n1 ≤ n2) (A2 : 'G^n2), widenF H (- A2) = - widenF H A2.
Proof. easy. Qed.
Lemma widenF_minus :
∀ {n1 n2} (H : n1 ≤ n2) (A2 B2 : 'G^n2),
widenF H (A2 - B2) = widenF H A2 - widenF H B2.
Proof. easy. Qed.
Lemma firstF_opp :
∀ {n1 n2} (A : 'G^(n1 + n2)), firstF (- A) = - firstF A.
Proof. easy. Qed.
Lemma firstF_minus :
∀ {n1 n2} (A B : 'G^(n1 + n2)), firstF (A - B) = firstF A - firstF B.
Proof. easy. Qed.
Lemma lastF_opp : ∀ {n1 n2} (A : 'G^(n1 + n2)), lastF (- A) = - lastF A.
Proof. easy. Qed.
Lemma lastF_minus :
∀ {n1 n2} (A B : 'G^(n1 + n2)), lastF (A - B) = lastF A - lastF B.
Proof. easy. Qed.
Lemma concatF_opp :
∀ {n1 n2} (A1 : 'G^n1) (A2 : 'G^n2),
concatF (- A1) (- A2) = - concatF A1 A2.
Proof.
intros n1 n2 A1 A2; apply extF; intros i; rewrite fct_opp_eq;
destruct (lt_dec i n1) as [Hi | Hi];
[rewrite !concatF_correct_l | rewrite !concatF_correct_r]; easy.
Qed.
Lemma concatF_minus :
∀ {n1 n2} (A1 B1 : 'G^n1) (A2 B2 : 'G^n2),
concatF (A1 - B1) (A2 - B2) = concatF A1 A2 - concatF B1 B2.
Proof. intros; rewrite !minus_eq concatF_plus concatF_opp; easy. Qed.
Lemma insertF_opp :
∀ {n} (A : 'G^n) a i0, insertF (- A) (- a) i0 = - insertF A a i0.
Proof.
intros n A a i0; apply extF; intros i; rewrite fct_opp_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
Qed.
Lemma insertF_minus :
∀ {n} (A B : 'G^n) a0 b0 i0,
insertF (A - B) (a0 - b0) i0 = insertF A a0 i0 - insertF B b0 i0.
Proof. intros; rewrite !minus_eq insertF_plus insertF_opp; easy. Qed.
Lemma skipF_opp : ∀ {n} (A : 'G^n.+1) i0, skipF (- A) i0 = - skipF A i0.
Proof. easy. Qed.
Lemma skipF_minus :
∀ {n} (A B : 'G^n.+1) i0, skipF (A - B) i0 = skipF A i0 - skipF B i0.
Proof. easy. Qed.
Lemma replaceF_opp :
∀ {n} (A : 'G^n.+1) a0 i0,
replaceF (- A) (- a0) i0 = - replaceF A a0 i0.
Proof.
intros n A a0 i0; apply extF; intros i; rewrite fct_opp_eq;
destruct (ord_eq_dec i i0) as [Hi | Hi];
[rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
Qed.
Lemma replaceF_minus :
∀ {n} (A B : 'G^n.+1) a0 b0 i0,
replaceF (A - B) (a0 - b0) i0 = replaceF A a0 i0 - replaceF B b0 i0.
Proof. intros; rewrite !minus_eq replaceF_plus replaceF_opp; easy. Qed.
Lemma permutF_opp :
∀ {n} (p : 'I_[n]) (A : 'G^n), permutF p (- A) = - permutF p A.
Proof. easy. Qed.
Lemma permutF_minus :
∀ {n} (p : 'I_[n]) (A B : 'G^n),
permutF p (A - B) = permutF p A - permutF p B.
Proof. easy. Qed.
Lemma sum_squeezeF :
∀ {n} (u : 'G^n.+1) {i0 i1}, i1 ≠ i0 → sum (squeezeF u i0 i1) = sum u.
Proof.
intros n u i0 i1 Hi.
apply (plus_reg_l (u i0 + replaceF u (u i0 + u i1) i0 i1)).
rewrite -plus_assoc -sum_skipF replaceF_correct_r//.
rewrite sum_replaceF; easy.
Qed.
End Group_FF_Facts.