From 3532e6714b7d0ee10b692e41c356866cfab5c646 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Aug 2009 17:15:57 +0000 Subject: [PATCH] (nat,plus) is an abelian, unital magma --- .../matita/nlibrary/algebra/abelian_magmas.ma | 20 ++++++++++++++ .../matita/nlibrary/algebra/unital_magmas.ma | 27 +++++++++++++++++++ helm/software/matita/nlibrary/depends | 4 ++- .../matita/nlibrary/logic/equality.ma | 10 +++++++ helm/software/matita/nlibrary/nat/plus.ma | 26 +++++++++++++++++- 5 files changed, 85 insertions(+), 2 deletions(-) create mode 100644 helm/software/matita/nlibrary/algebra/abelian_magmas.ma create mode 100644 helm/software/matita/nlibrary/algebra/unital_magmas.ma diff --git a/helm/software/matita/nlibrary/algebra/abelian_magmas.ma b/helm/software/matita/nlibrary/algebra/abelian_magmas.ma new file mode 100644 index 000000000..417409e3c --- /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 index 000000000..027d9e921 --- /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 a7952ea4d..27fb3e081 100644 --- 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 6de962747..ac8a2a20c 100644 --- 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 62fe4917a..809288f2a 100644 --- 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 -- 2.39.2