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.

Brief description

Complements on the commutative monoid algebraic structure.

Description

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 :
  • support for the zero structure;

Zero structure

Let G : AbelianMonoid.
  • 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

Usage

This module may be used through the import of Algebra.Monoid.Monoid, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

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.