(nat,plus) is an abelian, unital magma

diff --git a/helm/software/matita/nlibrary/algebra/abelian_magmas.ma b/helm/software/matita/nlibrary/algebra/abelian_magmas.ma
new file mode 100644 (file)
index 0000000..417409e
--- /dev/null
+++ b/helm/software/matita/nlibrary/algebra/abelian_magmas.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "algebra/magmas.ma".
+
+nrecord abelian_magma_type: Type[1] ≝
+ { amt_magma:> magma_type;
+   symm: ∀x,y: amt_magma. op ? x y = op ? y x
+ }.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/algebra/unital_magmas.ma b/helm/software/matita/nlibrary/algebra/unital_magmas.ma
new file mode 100644 (file)
index 0000000..027d9e9
--- /dev/null
+++ b/helm/software/matita/nlibrary/algebra/unital_magmas.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "algebra/magmas.ma".
+
+nrecord unital_magma_type : Type[1] ≝
+ { umt_magma:> magma_type;
+   unit: umt_magma;
+   umt_is_neutral_l: ∀x. op ? unit x = x;
+   umt_is_neutral_r: ∀x. op ? x unit = x
+ }.
+
+nrecord unital_magma (A: unital_magma_type) : Type[1] ≝
+ { um_magma:> magma A;
+   neutral_closed: unit A ∈ um_magma
+ }.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index a7952ea4d575ee9b0d6e453c7983a80722db32e6..27fb3e081c9ad4064773a07768b088895034117c 100644 (file)
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -4,9 +4,11 @@ sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 sets/setoids.ma logic/connectives.ma properties/relations.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
 logic/connectives.ma logic/pts.ma
-nat/plus.ma algebra/magmas.ma nat/nat.ma
+algebra/abelian_magmas.ma algebra/magmas.ma
+nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/nat.ma
 algebra/magmas.ma sets/sets.ma
 nat/nat.ma logic/equality.ma sets/setoids.ma
 properties/relations1.ma logic/pts.ma
 properties/relations.ma logic/pts.ma
+algebra/unital_magmas.ma algebra/magmas.ma
 logic/pts.ma 

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 6de962747e31baa5776de06e853ec5ad87cdbe45..ac8a2a20c7ddf7934997f2e80c87d5eb86833840 100644 (file)
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -18,6 +18,16 @@ include "properties/relations.ma".
 ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  refl: eq A a a.
 
+nlemma eq_rect_CProp0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #x; #p; #x0; #p0; napply eq_rect_CProp0_r'; nassumption.
+nqed.
+
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).

diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma
index 62fe4917a3ecff80a5db88248715a0999e413653..809288f2a7bb7d6be2f39ab211811db124164a0b 100644 (file)
--- a/helm/software/matita/nlibrary/nat/plus.ma
+++ b/helm/software/matita/nlibrary/nat/plus.ma
@@ -13,7 +13,8 @@
 (**************************************************************************)
 
 include "nat/nat.ma".
-include "algebra/magmas.ma".
+include "algebra/unital_magmas.ma".
+include "algebra/abelian_magmas.ma".
 
 nlet rec plus (n:nat) (m:nat) on n : nat ≝
  match n with
@@ -26,4 +27,27 @@ ndefinition plus_magma_type: magma_type.
   | napply mk_binary_morphism
      [ napply plus
      | #a; #a'; #b; #b'; #Ha; #Hb; nrewrite < Ha; nrewrite < Hb; napply refl ]##]
+nqed.
+
+ndefinition plus_abelian_magma_type: abelian_magma_type.
+ napply mk_abelian_magma_type
+  [ napply plus_magma_type
+  | nnormalize; #x;
+     (* nelim non va *) napply (nat_rect_CProp0 ??? x);
+     ##[ #y; napply (nat_rect_CProp0 ??? y) [ napply refl | #n; #H; nnormalize; nrewrite < H; napply refl]
+     ##| #n; #H; #y; nnormalize;
+         (* rewrite qui non va *)
+         napply (eq_rect_CProp0_r ????? (H y));
+         napply (nat_rect_CProp0 ??? y)
+          [ napply refl
+          | #n0; #K; nnormalize in K; nnormalize;
+            napply (eq_rect_CProp0 ????? K); napply refl] ##]
+nqed.
+
+ndefinition plus_unital_magma_type: unital_magma_type.
+ napply mk_unital_magma_type
+  [ napply plus_magma_type
+  | napply O
+  | #x; napply refl
+  | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
 nqed.
\ No newline at end of file