]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/nat/plus.ma
- main proposition on lsx finally proved!
[helm.git] / matita / matita / nlibrary / nat / plus.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/big_ops.ma".
16 include "algebra/unital_magmas.ma".
17 include "algebra/abelian_magmas.ma".
18
19 nlet rec plus (n:nat) (m:nat) on n : nat ≝
20  match n with
21   [ O ⇒ m
22   | S n' ⇒ S (plus n' m) ].
23
24 interpretation "natural plus" 'plus x y = (plus x y).
25
26 ndefinition plus_magma_type: magma_type.
27  napply mk_magma_type
28   [ napply NAT
29   | napply mk_binary_morphism
30      [ napply plus
31      | #a; #a'; #b; #b'; #Ha; #Hb; nrewrite < Ha; nrewrite < Hb; napply refl ]##]
32 nqed.
33
34 ndefinition plus_abelian_magma_type: abelian_magma_type.
35  napply mk_abelian_magma_type
36   [ napply plus_magma_type
37   | nnormalize; #x;
38      (* nelim non va *) napply (nat_rect_CProp0 ??? x);
39      ##[ #y; napply (nat_rect_CProp0 ??? y) [ napply refl | #n; #H; nnormalize; nrewrite < H; napply refl]
40      ##| #n; #H; #y; nnormalize;
41          (* rewrite qui non va *)
42          napply (eq_rect_CProp0_r ????? (H y));
43          napply (nat_rect_CProp0 ??? y)
44           [ napply refl
45           | #n0; #K; nnormalize in K; nnormalize;
46             napply (eq_rect_CProp0 ????? K); napply refl] ##]
47 nqed.
48
49 ndefinition plus_unital_magma_type: unital_magma_type.
50  napply mk_unital_magma_type
51   [ napply plus_magma_type
52   | napply O
53   | #x; napply refl
54   | #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
55 nqed.
56
57 ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.