source: C-semantics/binary/Z.ma @ 10

Last change on this file since 10 was 10, checked in by campbell, 10 years ago

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File size: 18.9 KB
Line 
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(* This includes a lot of copied code from arithmetics/Z.ma, so some of the
16   comments may no longer be applicable. *)
17
18include "arithmetics/compare.ma".
19include "binary/positive.ma".
20
21ninductive Z : Type ≝
22  OZ  : Z
23| pos : Pos → Z
24| neg : Pos → Z.
25
26interpretation "Integers" 'Z = Z.
27
28ndefinition Z_of_nat ≝
29λn. match n with
30[ O ⇒ OZ
31| S n ⇒ pos (succ_pos_of_nat n)].
32
33ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
34
35ndefinition neg_Z_of_nat \def
36λn. match n with
37[ O ⇒ OZ
38| S n ⇒ neg (succ_pos_of_nat n)].
39
40ndefinition abs ≝
41λz.match z with
42[ OZ ⇒ O
43| pos n ⇒ nat_of_pos n
44| neg n ⇒ nat_of_pos n].
45
46ndefinition OZ_test ≝
47λz.match z with
48[ OZ ⇒ true
49| pos _ ⇒ false
50| neg _ ⇒ false].
51
52ntheorem OZ_test_to_Prop : ∀z:Z.
53  match OZ_test z with
54  [true ⇒ z=OZ
55  |false ⇒ z ≠ OZ].
56#z;ncases z
57##[napply refl
58##|##*:#z1;napply nmk;#H;ndestruct]
59nqed.
60
61(* discrimination *)
62ntheorem injective_pos: injective Pos Z pos.
63#n;#m;#H;ndestruct;//;
64nqed.
65
66(* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
67\def injective_pos. *)
68
69ntheorem injective_neg: injective Pos Z neg.
70#n;#m;#H;ndestruct;//;
71nqed.
72
73(* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
74\def injective_neg. *)
75
76ntheorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n.
77#n;napply nmk;#H;ndestruct;
78nqed.
79
80ntheorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n.
81#n;napply nmk;#H;ndestruct;
82nqed.
83
84ntheorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m.
85#n;#m;napply nmk;#H;ndestruct;
86nqed.
87
88ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
89#x;#y;ncases x;
90##[ncases y;
91   ##[@;//
92   ##|##*:#n;@2;napply nmk;#H;ndestruct]
93##|#n;ncases y;
94   ##[@2;napply nmk;#H;ndestruct;
95   ##|#m;ncases (decidable_eq_pos n m);#H;
96      ##[nrewrite > H;@;//
97      ##|@2;napply nmk;#H2;nelim H;
98         (* bug if you don't introduce H3 *)#H3;ndestruct;
99         napply H3;@]
100   ##|#m;@2;napply nmk;#H;ndestruct]
101##|#n;ncases y;
102   ##[@2;napply nmk;#H;ndestruct;
103   ##|#m;@2;napply nmk;#H;ndestruct
104   ##|#m;ncases (decidable_eq_pos n m);#H;
105      ##[nrewrite > H;@;//
106      ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
107         napply H3;@]##]##]
108nqed.
109
110ndefinition Zsucc ≝
111λz. match z with
112[ OZ ⇒ pos one
113| pos n ⇒ pos (succ n)
114| neg n ⇒
115          match n with
116          [ one ⇒ OZ
117          | _ ⇒ neg (pred n)]].
118
119ndefinition Zpred ≝
120λz. match z with
121[ OZ ⇒ neg one
122| pos n ⇒
123          match n with
124          [ one ⇒ OZ
125          | _ ⇒ pos (pred n)]
126| neg n ⇒ neg (succ n)].
127
128nlemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))).
129//; nqed.
130
131ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
132#z;ncases z;
133##[ //
134##| #n; nnormalize; ncases n; /2/;
135##| #n; ncases n; //; #n';
136    nrewrite > (pred_succ_unfold_hack …); nrewrite < (succ_pred_n …); //;
137    @; #H; ndestruct;
138nqed.
139
140nlemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))).
141//; nqed.
142
143ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
144#z;ncases z
145##[ //
146##| #n; ncases n;//; #n';
147    nrewrite > (succ_pred_unfold_hack …); nrewrite < (succ_pred_n …); //;
148    @; #H; ndestruct;
149##| #n; ncases n;/3/;
150##]
151nqed.
152
153ndefinition Zle : Z → Z → Prop ≝
154λx,y:Z.
155  match x with
156  [ OZ ⇒
157    match y with
158    [ OZ ⇒ True
159    | pos m ⇒ True
160    | neg m ⇒ False ]
161  | pos n ⇒
162    match y with
163    [ OZ ⇒ False
164    | pos m ⇒ n ≤ m
165    | neg m ⇒ False ]
166  | neg n ⇒
167    match y with
168    [ OZ ⇒ True
169    | pos m ⇒ True
170    | neg m ⇒ m ≤ n ]].
171
172interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
173interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
174
175ndefinition Zlt : Z → Z → Prop ≝
176λx,y:Z.
177  match x with
178  [ OZ ⇒
179    match y with
180    [ OZ ⇒ False
181    | pos m ⇒ True
182    | neg m ⇒ False ]
183  | pos n ⇒
184    match y with
185    [ OZ ⇒ False
186    | pos m ⇒ n<m
187    | neg m ⇒ False ]
188  | neg n ⇒
189    match y with
190    [ OZ ⇒ True
191    | pos m ⇒ True
192    | neg m ⇒ m<n ]].
193   
194interpretation "integer 'less than'" 'lt x y = (Zlt x y).
195interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
196
197ntheorem irreflexive_Zlt: irreflexive Z Zlt.
198#x;ncases x
199##[napply nmk;//
200##|##*:#n;napply (not_le_succ_n n) (* XXX: auto?? *)]
201nqed.
202
203(* transitivity *)
204ntheorem transitive_Zle : transitive Z Zle.
205#x;#y;#z;ncases x
206##[ncases y
207   ##[//
208   ##|##*:#n;ncases z;//]
209##|#n;ncases y
210   ##[#H;ncases H
211   ##|(*##*:#m;#Hl;ncases z;//;*)
212      #m;#Hl;ncases z;//;#p;#Hr;
213      napply (transitive_le n m p);//; (* XXX: auto??? *)
214   ##|#m;#Hl;ncases Hl]
215##|#n;ncases y
216   ##[#Hl;ncases z
217      ##[##1,2://
218      ##|#m;#Hr;ncases Hr]
219   ##|#m;#Hl;ncases z;
220      ##[##1,2://
221      ##|#p;#Hr;ncases Hr]
222   ##|#m;#Hl;ncases z;//;#p;#Hr;
223      napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
224nqed.
225
226(* variant trans_Zle: transitive Z Zle
227\def transitive_Zle.*)
228
229ntheorem transitive_Zlt: transitive Z Zlt.
230#x;#y;#z;ncases x
231##[ncases y
232   ##[//
233   ##|#n;ncases z
234      ##[#_;#Hr;ncases Hr
235      ##|//
236      ##|#m;#_;#Hr;ncases Hr]
237   ##|#n;#Hl;ncases Hl]
238##|#n;ncases y
239   ##[#Hl;ncases Hl
240   ##|#m;ncases z
241      ##[//
242      ##|#p;napply transitive_lt (* XXX: auto??? *)
243      ##|//##]
244   ##|#m;#Hl;ncases Hl]
245##|#n;ncases y
246   ##[ncases z;
247      ##[##1,2://
248      ##|#m;#_;#Hr;ncases Hr]
249   ##|#m;ncases z;
250      ##[##1,2://
251      ##|#p;#_;#Hr;ncases Hr]
252   ##|#m;ncases z
253      ##[##1,2://
254      ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
255   ##]
256##]
257nqed.     
258
259(* variant trans_Zlt: transitive Z Zlt
260\def transitive_Zlt.
261theorem irrefl_Zlt: irreflexive Z Zlt
262\def irreflexive_Zlt.*)
263
264ntheorem Zlt_neg_neg_to_lt:
265  ∀n,m:Pos. neg n < neg m → m < n.
266//;
267nqed.
268
269ntheorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m.
270//;
271nqed.
272
273ntheorem Zlt_pos_pos_to_lt:
274  ∀n,m:Pos. pos n < pos m → n < m.
275//;
276nqed.
277
278ntheorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m.
279//;
280nqed.
281
282nlemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n.
283#n; nnormalize; nrewrite < (pred_succ_n n); ncases n; //; nqed.
284
285ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
286#x;#y;ncases x
287##[ncases y
288   ##[#H;ncases H
289   ##|//;
290   ##|#p;#H;ncases H]
291##|#n;ncases y
292   ##[#H;ncases H
293   ##|#p;nnormalize;//
294   ##|#p;#H;ncases H]
295##|#n;ncases y
296   ##[##1,2:ncases n;//
297   ##|#p;napply (pos_cases … n);
298      ##[#H;nelim (not_le_succ_one p);#H2;napply H2;napply H (*//;*) (* XXX: auto? *)
299      ##|#m;nrewrite > (Zsucc_neg_succ m);napply le_S_S_to_le; (* XXX: auto? *)
300      ##]
301   ##]
302##]
303nqed.
304
305(*** COMPARE ***)
306
307(* boolean equality *)
308ndefinition eqZb : Z → Z → bool ≝
309λx,y:Z.
310  match x with
311  [ OZ ⇒
312      match y with
313        [ OZ ⇒ true
314        | pos q ⇒ false
315        | neg q ⇒ false]
316  | pos p ⇒
317      match y with
318        [ OZ ⇒ false
319        | pos q ⇒ eqb p q
320        | neg q ⇒ false]     
321  | neg p ⇒
322      match y with
323        [ OZ ⇒ false
324        | pos q ⇒ false
325        | neg q ⇒ eqb p q]].
326
327ntheorem eqZb_to_Prop:
328  ∀x,y:Z.
329    match eqZb x y with
330    [ true ⇒ x=y
331    | false ⇒ x ≠ y].
332#x;#y;ncases x
333##[ncases y;
334   ##[//
335   ##|napply not_eq_OZ_pos (* XXX: auto? *)
336   ##|napply not_eq_OZ_neg (* XXX: auto? *)]
337##|#n;ncases y;
338   ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
339   ##|#m;napply eqb_elim;
340      ##[//
341      ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
342   ##|#m;napply not_eq_pos_neg]
343##|#n;ncases y
344   ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
345   ##|#m;napply nmk;#H;ndestruct
346   ##|#m;napply eqb_elim;
347      ##[//
348      ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
349   ##]
350##]
351nqed.
352
353ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
354  (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
355#x;#y;#P;#HP1;#HP2;
356ncut
357(match (eqZb x y) with
358[ true ⇒ x=y
359| false ⇒ x ≠ y] → P (eqZb x y))
360##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
361   ##[napply HP1
362   ##|napply HP2]
363##|#Hcut;napply Hcut;napply eqZb_to_Prop]
364nqed.
365
366ndefinition Z_compare : Z → Z → compare ≝
367λx,y:Z.
368  match x with
369  [ OZ ⇒
370    match y with
371    [ OZ ⇒ EQ
372    | pos m ⇒ LT
373    | neg m ⇒ GT ]
374  | pos n ⇒
375    match y with
376    [ OZ ⇒ GT
377    | pos m ⇒ pos_compare n m
378    | neg m ⇒ GT]
379  | neg n ⇒
380    match y with
381    [ OZ ⇒ LT
382    | pos m ⇒ LT
383    | neg m ⇒ pos_compare m n ]].
384
385ntheorem Z_compare_to_Prop :
386∀x,y:Z. match (Z_compare x y) with
387[ LT ⇒ x < y
388| EQ ⇒ x=y
389| GT ⇒ y < x].
390#x;#y;nelim x
391##[nelim y;//;
392##|nelim y
393   ##[##1,3://
394   ##|#n;#m;nnormalize;
395      ncut (match (pos_compare m n) with
396      [ LT ⇒ m < n
397      | EQ ⇒ m = n
398      | GT ⇒ n < m ] →
399      match (pos_compare m n) with
400      [ LT ⇒ (succ m)  ≤ n
401      | EQ ⇒ pos m = pos n
402      | GT ⇒ (succ n)  ≤ m])
403      ##[ncases (pos_compare m n);//
404      ##|#Hcut;napply Hcut;napply pos_compare_to_Prop]
405   ##]
406##|nelim y
407   ##[#n;//
408   ##|nnormalize;//
409   ##|nnormalize;#n;#m;
410      ncut (match (pos_compare n m) with
411        [ LT ⇒ n < m
412        | EQ ⇒ n = m
413        | GT ⇒ m < n] →
414      match (pos_compare n m) with
415      [ LT ⇒ (succ n) ≤ m
416      | EQ ⇒ neg m = neg n
417      | GT ⇒ (succ m) ≤ n])
418      ##[ncases (pos_compare n m);//
419      ##|#Hcut;napply Hcut;napply pos_compare_to_Prop]
420   ##]
421##]
422nqed.
423
424ndefinition Zplus : Z → Z → Z ≝
425  λx,y. match x with
426    [ OZ ⇒ y
427    | pos m ⇒
428        match y with
429         [ OZ ⇒ x
430         | pos n ⇒ (pos (m + n))
431         | neg n ⇒
432              match pos_compare m n with
433                [ LT ⇒ (neg (n-m))
434                | EQ ⇒ OZ
435                | GT ⇒ (pos (m-n))] ]
436    | neg m ⇒
437        match y with
438         [ OZ ⇒ x
439         | pos n ⇒
440              match pos_compare m n with
441                [ LT ⇒ (pos (n-m))
442                | EQ ⇒ OZ
443                | GT ⇒ (neg (m-n))]     
444         | neg n ⇒ (neg (m + n))] ].
445
446interpretation "integer plus" 'plus x y = (Zplus x y).
447
448ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
449#n;#m;ncases n
450##[//
451##|#p;ncases m
452   ##[nnormalize;//
453   ##|#m';nnormalize;nrewrite > (nat_plus_pos_plus …);nrewrite > (succ_nat_pos ?);/2/]
454nqed.
455
456ntheorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m.
457//; nqed.
458
459ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
460#z;ncases z;//;
461nqed.
462
463ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
464#x;#y;ncases x;
465##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
466##|#p;ncases y
467   ##[//
468   ##|nnormalize;//
469   ##|#q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*);
470      ncases (pos_compare q p);//]
471##|#p;ncases y
472   ##[//;
473   ##|#q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*);
474      ncases (pos_compare q p);//
475   ##|nnormalize;//]
476##]
477nqed.
478
479ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z.
480#z;ncases z
481##[//
482##|##*:#n;ncases n;//]
483nqed.
484
485ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z.
486#z;ncases z
487##[//
488##|##*:#n;ncases n;//]
489nqed.
490
491nlemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n.
492#n; nnormalize; ncases n; /2/; nqed.
493
494ntheorem Zplus_pos_pos:
495  ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
496#n;#m;napply (pos_cases … n);
497##[ napply (pos_cases … m); //;
498##|#p;napply (pos_cases … m);
499   ##[nnormalize; nrewrite < (succ_plus_one …); //;
500   ##|#q; nrewrite > (Zsucc_Zplus_pos_O …); nrewrite > (Zpred_pos_succ ?);
501      nnormalize; /2/;
502   ##]
503##]
504nqed.
505
506ntheorem Zplus_pos_neg:
507  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
508#n m;
509nnormalize;
510nrewrite < (pos_compare_S_S …);
511nrewrite > (partialminus_S_S …);
512nrewrite > (partialminus_S_S …); //;
513nqed.
514
515nlemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n.
516#A P Q n; napply succ_elim; //; nqed.
517
518nlemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n.
519#n; ncases n; //;
520#n'; nwhd in ⊢ (??%?); nnormalize; nrewrite < (pred_succ_n …);
521napply succ_elim; //; nqed.
522
523ntheorem Zplus_neg_pos :
524  ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
525#n m; napply (pos_cases … n); napply (pos_cases … m);
526##[ //;
527##| #m'; nrewrite > (Zpred_pos_succ …);
528    nrewrite > (?:pos (succ m') = Zsucc (pos m')); //;
529##| #m'; nnormalize; nrewrite > (pos_compare_S_one …); nnormalize;
530    nrewrite > (partial_minus_S_one …); nnormalize; nrewrite > (pos_nonzero …);
531    nrewrite < (pred_succ_n …); //;
532##| #m'; #n'; nnormalize; nrewrite < (pos_compare_S_S …);
533    nrewrite > (partialminus_S_S …);
534    nrewrite > (partialminus_S_S …);
535    nrewrite > (pos_nonzero …);
536    nrewrite > (pos_nonzero …);
537    nrewrite < (pred_succ_n …);
538    nrewrite < (pred_succ_n …);
539    nnormalize; //;
540##] nqed.
541
542ntheorem Zplus_neg_neg:
543  ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
544#n m; napply (pos_cases … n); napply (pos_cases … m);
545##[ ##1,2: //;
546##| #n'; nnormalize in ⊢ (???(?%?));
547    nrewrite > (pos_nonzero …);
548    nrewrite < (pred_succ_n …); nnormalize; //;
549##| #m';#n'; nnormalize; nrewrite > (pos_nonzero …);
550    nrewrite < (pred_succ_n …); nnormalize; //;
551##] nqed.
552
553ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
554#x;#y;ncases x
555##[ncases y
556   ##[//
557   ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
558   ##|#p;nrewrite < (Zsucc_Zplus_pos_O …); //]
559##|ncases y;/2/; #p; nrewrite > (sym_Zplus … (Zpred OZ));
560   nrewrite < (Zpred_Zplus_neg_O …); //;
561##|ncases y
562   ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
563      nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
564   ##|##*:/2/]
565nqed.
566
567ntheorem Zplus_Zsucc_pos_pos :
568  ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
569#n m;nrewrite > (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zplus_pos_O ?);//;
570nqed.
571
572ntheorem Zplus_Zsucc_pos_neg:
573  ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
574#n;#m;
575napply (pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
576##[#n1;nelim n1
577   ##[//
578   ##|##*:#n2;#IH;nelim n2;//]
579##|#n'; nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?);
580   nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?);
581   nrewrite > (Zpred_Zsucc …);  /2/
582##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nrewrite > IH;
583nrewrite < (Zplus_pos_neg …); //]
584nqed.
585
586ntheorem Zplus_Zsucc_neg_neg :
587  ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
588#n;#m;
589napply (pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
590##[napply pos_elim;
591   ##[//
592   ##|#n2;#IH;nnormalize;nrewrite < (pred_succ_n …); nrewrite > (pos_nonzero …); //]
593##| #n'; nnormalize;
594   nrewrite > (pos_nonzero …);
595   nrewrite < (pred_succ_n …); nnormalize;
596   nrewrite < (succ_plus_one …);
597   nrewrite < (succ_plus_one …); nrewrite > (pos_nonzero …); //;
598##| #n' m' IH; nnormalize;
599   nrewrite > (pos_nonzero …); nnormalize;
600   nrewrite < (pluss_succn_m …);
601   nrewrite > (pos_nonzero …); //;
602##]
603nqed.
604
605nlemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
606#n m; nnormalize; nrewrite < (pos_compare_S_S …);
607nrewrite > (partialminus_S_S …);
608nrewrite > (partialminus_S_S …);
609 //; nqed.
610
611
612ntheorem Zplus_Zsucc_neg_pos:
613  ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
614#n;#m;
615napply (pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m)))
616##[napply pos_elim;
617   ##[//
618   ##|#n2;#IH;nnormalize; nrewrite > (pos_nonzero …); nnormalize;
619      nrewrite > (partial_minus_S_one …); //]
620##| #n';
621    nrewrite > (sym_Zplus …);
622    nrewrite < (Zsucc_Zplus_pos_O …);
623    nrewrite > (sym_Zplus …);
624    nrewrite < (Zsucc_Zplus_pos_O …); //;
625##|#n' m' IH;
626   nrewrite > (neg_pos_succ …); //;
627##] nqed.
628
629ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
630#x;#y;ncases x
631##[ncases y;//;(*#n;nnormalize;ncases n;//;*)
632##|##*:#n;ncases y;//;#m;napply Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)]
633nqed.
634
635ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
636#x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
637##[nrewrite > (Zsucc_Zpred ?);//
638##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]
639nqed.
640
641nlemma eq_rect_Type0_r:
642 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
643 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption.
644nqed.
645
646ntheorem associative_Zplus: associative Z Zplus.
647(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
648#x;#y;#z;ncases x
649##[//
650##|napply pos_elim;
651   ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
652   ##|#n1;#IH;
653      nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
654      nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
655##|napply pos_elim;
656   ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
657   ##|#n1;#IH;
658      nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
659      nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
660##]
661nqed.
662
663(* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
664\def associative_Zplus. *)
665
666(* Zopp *)
667ndefinition Zopp : Z → Z ≝
668  λx:Z. match x with
669  [ OZ ⇒ OZ
670  | pos n ⇒ neg n
671  | neg n ⇒ pos n ].
672
673interpretation "integer unary minus" 'uminus x = (Zopp x).
674
675ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
676//;
677nqed.
678
679ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
680#x;#y;ncases x
681##[ncases y;//
682##|##*:#n;ncases y;//;#m;nnormalize;napply pos_compare_elim;nnormalize;//]
683nqed.
684
685ntheorem Zopp_Zopp: ∀x:Z. --x = x.
686#x;ncases x;//;
687nqed.
688
689ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
690#x;ncases x
691##[//
692##|##*:#n;nnormalize;nrewrite > (pos_compare_n_n ?);//]
693nqed.
694
695ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
696#x;#z;#y;#H;
697nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
698nrewrite < (Zplus_Zopp x);
699nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
700//;
701nqed.
702
703ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
704#x;#z;#y;#H;
705napply (injective_Zplus_l x);
706nrewrite < (sym_Zplus ??);
707//;
708nqed.
709
710(* minus *)
711ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
712
713interpretation "integer minus" 'minus x y = (Zminus x y).
714
715
716
717ndefinition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n).
718ndefinition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n).
719ndefinition two_p : Z → Z ≝
720λz.match z with
721[ OZ ⇒ pos one
722| pos p ⇒ pos (two_power_pos p)
723| neg _ ⇒ OZ  (* same fib as Coq *)
724].
Note: See TracBrowser for help on using the repository browser.