Library Algebra.Monoid.Monoid_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 monoid algebraic structure.
The AbelianMonoid algebraic structure (aka commutative monoid) is defined
in the Coquelicot library, including the canonical structure
prod_AbelianMonoid for the cartesian product of commutative monoids.
The present module adds :
Let G : AbelianMonoid.
This module may be used through the import of Algebra.Monoid.Monoid,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- support for the zero structure;
Zero structure
- zero_struct G is the predicate stating that G is the singleton type with only element 0];
- nonzero_struct G is the predicate stating that G contains an element distinct from 0.
Used logic axioms
- classic_dec, an alias for excluded_middle_informative, the strong form of excluded middle.
Usage
From Requisite Require Import ssr.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl.
Local Open Scope Monoid_scope.
Section Monoid_Facts.
Definition zero_struct (G : AbelianMonoid) : Prop := unit_type (0 : G).
Definition nonzero_struct (G : AbelianMonoid) : Prop := ∃ x : G, x ≠ 0.
Lemma zero_not_nonzero_struct_equiv :
∀ {G}, zero_struct G ↔ ¬ nonzero_struct G.
Proof. intros; apply iff_sym, not_ex_not_all_equiv. Qed.
Lemma nonzero_not_zero_struct_equiv :
∀ {G}, nonzero_struct G ↔ ¬ zero_struct G.
Proof. intros; apply iff_sym, not_all_ex_not_equiv. Qed.
Lemma zero_struct_dec : ∀ G, { zero_struct G } + { nonzero_struct G }.
Proof.
intros; destruct (classic_dec (zero_struct G));
[left | right; apply nonzero_not_zero_struct_equiv]; easy.
Qed.
Context {G : AbelianMonoid}.
Lemma inhabited_m : inhabited G.
Proof. apply (inhabits 0). Qed.
Lemma inhabited_fct_m : ∀ {T : Type}, inhabited (T → G).
Proof. intros; apply fun_to_nonempty_compat, inhabited_m. Qed.
Lemma plus_compat_l : ∀ x x1 x2 : G, x1 = x2 → x + x1 = x + x2.
Proof. intros; f_equal; easy. Qed.
Lemma plus_compat_r : ∀ x x1 x2 : G, x1 = x2 → x1 + x = x2 + x.
Proof. intros; f_equal; easy. Qed.
Lemma plus_comm3_l : ∀ x y z : G, x + (y + z) = y + (x + z).
Proof. intros x y z; rewrite plus_assoc (plus_comm x) -plus_assoc; easy. Qed.
Lemma plus_comm3_r : ∀ x y z : G, x + (y + z) = z + (y + x).
Proof. intros x y z; rewrite plus_comm -plus_assoc plus_comm3_l; easy. Qed.
Lemma plus_comm4_m :
∀ x y z t : G, (x + y) + (z + t) = (x + z) + (y + t).
Proof.
intros x y z t; rewrite !plus_assoc -(plus_assoc x y) -(plus_assoc x z).
do 2 f_equal; apply plus_comm.
Qed.
Lemma zero_uniq : ∀ z : G, (∀ x, x + z = x) → z = 0.
Proof. intros z H; rewrite -(plus_zero_l z); easy. Qed.
Lemma opposite_uniq : ∀ x y1 y2 : G, y1 + x = 0 → x + y2 = 0 → y1 = y2.
Proof.
intros x y1 y2 Hy1 Hy2.
rewrite -(plus_zero_r y1) -Hy2 plus_assoc Hy1 plus_zero_l; easy.
Qed.
End Monoid_Facts.