source: Deliverables/D4.1/Matita/Nat.ma @ 230

Last change on this file since 230 was 230, checked in by mulligan, 9 years ago

Lots of work from today.

File size: 3.6 KB
Line 
1include "Cartesian.ma".
2include "Maybe.ma".
3include "Bool.ma".
4
5include "logic/pts.ma".
6include "Plogic/equality.ma".
7
8ninductive Nat: Type[0] ≝
9  Z: Nat
10| S: Nat → Nat.
11
12nlet rec plus (n: Nat) (o: Nat) on n ≝
13  match n with
14    [ Z ⇒ o
15    | S p ⇒ S (plus p o)
16    ].
17   
18notation "n break + m"
19  right associative with precedence 52
20  for @{ 'plus $n $m }.
21 
22interpretation "Nat plus" 'plus n m = (plus n m).
23   
24nlet rec minus (n: Nat) (o: Nat) on n ≝
25  match n with
26    [ Z ⇒ Z
27    | S p ⇒
28      match o with
29        [ Z ⇒ S p
30        | S q ⇒ minus p q
31        ]
32    ].
33   
34notation "n break - m"
35  right associative with precedence 47
36  for @{ 'minus $n $m }.
37 
38interpretation "Nat minus" 'minus n m = (minus n m).
39   
40nlet rec multiplication (n: Nat) (o: Nat) on n ≝
41  match n with
42    [ Z ⇒ Z
43    | S p ⇒ o + (multiplication p o)
44    ].
45   
46notation "n break * m"
47  right associative with precedence 47
48  for @{ 'multiplication $n $m }.
49 
50interpretation "Nat multiplication" 'times n m = (multiplication n m).
51
52nlemma plus_zero:
53  ∀n: Nat.
54    n + Z = n.
55  #n.
56  nelim n.
57  nnormalize.
58  @.
59  #N H.
60  nnormalize.
61  nrewrite > H.
62  @.
63nqed.
64
65nlemma plus_associative:
66  ∀m, n, o: Nat.
67    (m + n) + o = m + (n + o).
68  #m n o.
69  nelim m.
70  nnormalize.
71  @.
72  #N H.
73  nnormalize.
74  nrewrite > H.
75  @.
76nqed.
77
78nlemma succ_plus:
79  ∀m, n: Nat.
80    S(m + n) = m + S(n).
81  #m n.
82  nelim m.
83  nnormalize.
84  @.
85  #N H.
86  nnormalize.
87  nrewrite > H.
88  @.
89nqed.
90
91nlemma plus_symmetrical:
92  ∀m, n: Nat.
93    m + n = n + m.
94  #m n.
95  nelim m.
96  nnormalize.
97  nelim n.
98  nnormalize.
99  @.
100  #N H.
101  nnormalize.
102  nrewrite < H.
103  @.
104  #N H.
105  nnormalize.
106  nrewrite > H.
107  napplyS succ_plus.
108nqed.
109
110nlemma multiplication_zero_right_neutral:
111  ∀m: Nat.
112    m * Z = Z.
113  #m.
114  nelim m.
115  nnormalize.
116  @.
117  #N H.
118  nnormalize.
119  nrewrite > H.
120  @.
121nqed.
122
123nlemma multiplication_succ:
124  ∀m, n: Nat.
125    m * S(n) = m + (m * n).
126  #m n.
127  nelim m.
128  nnormalize.
129  @.
130  #N H.
131  nnormalize.
132  napplyS plus_symmetrical.
133nqed.
134
135nlemma multiplication_symmetrical:
136  ∀m, n: Nat.
137    m * n = n * m.
138  #m n.
139  nelim m.
140  nnormalize.
141  nelim n.
142  nnormalize.
143  @.
144  #N H.
145  nnormalize.
146  nrewrite < H.
147  @.
148  #N H.
149  nnormalize.
150  nrewrite > H.
151  napplyS multiplication_succ.
152nqed.
153
154nlemma multiplication_succ_zero_left_neutral:
155  ∀m: Nat.
156    (S Z) * m = m.
157  #m.
158  nelim m.
159  nnormalize.
160  @.
161  #N H.
162  nnormalize.
163  napplyS succ_plus.
164nqed.
165
166nlemma multiplication_succ_zero_right_neutral:
167  ∀m: Nat.
168    m * (S Z) = m.
169  #m.
170  nelim m.
171  nnormalize.
172  @.
173  #N H.
174  nnormalize.
175  nrewrite > H.
176  @.
177nqed.
178
179nlemma multiplication_distributes_right_plus:
180  ∀m, n, o: Nat.
181    (m + n) * o = m * o + n * o.
182  #m n o.
183  nelim m.
184  nnormalize.
185  @.
186  #N H.
187  nnormalize.
188  nrewrite > H.
189  napplyS plus_associative.
190nqed.
191
192nlemma multiplication_distributes_left_plus:
193  ∀m, n, o: Nat.
194    o * (m + n) = o * m + o * n.
195  #m n o.
196  napplyS multiplication_symmetrical.
197nqed.
198
199nlemma mutliplication_associative:
200  ∀m, n, o: Nat.
201    m * (n * o) = (m * n) * o.
202  #m n o.
203  nelim m.
204  nnormalize.
205  @.
206  #N H.
207  nnormalize.
208  nrewrite > H.
209  napplyS multiplication_distributes_right_plus.
210nqed.
211
212nlemma minus_minus:
213  ∀n: Nat.
214    n - n = Z.
215  #n.
216  nelim n.
217  nnormalize.
218  @.
219  #N H.
220  nnormalize.
221  nrewrite > H.
222  @.
223nqed.
224
225(*
226nlemma succ_injective:
227  ∀m, n: Nat.
228    S m = S n → m = n.
229  #m n.
230  nelim m.
231  #H.
232  ninversion H.
233  #H.
234  ndestruct
235
236nlemma plus_minus_associate:
237  ∀m, n, o: Nat.
238    (m + n) - o = m + (n - o).
239  #m n o.
240  nelim m.
241  nnormalize.
242  @.
243  #N H.
244 
245
246nlemma plus_minus_inverses:
247  ∀m, n: Nat.
248    (m + n) - n = m.
249  #m n.
250  nelim m.
251  nnormalize.
252  napply minus_minus.
253  #N H.
254*)
Note: See TracBrowser for help on using the repository browser.