X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fnat%2Fplus.ma;h=75268ffcb4336b3ca709e5134dd51ae00c350a88;hb=2dc6ec0db2156431948014a6498c9901f8759e39;hp=62fe4917a3ecff80a5db88248715a0999e413653;hpb=a0c0e92cee3ed99995e12b02f18e30f018d946ea;p=helm.git diff --git a/helm/software/matita/nlibrary/nat/plus.ma b/helm/software/matita/nlibrary/nat/plus.ma index 62fe4917a..75268ffcb 100644 --- a/helm/software/matita/nlibrary/nat/plus.ma +++ b/helm/software/matita/nlibrary/nat/plus.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) -include "nat/nat.ma". -include "algebra/magmas.ma". +include "nat/big_ops.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,29 @@ 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. \ No newline at end of file +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. + +ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O. \ No newline at end of file