source: Deliverables/D3.1/C-semantics/binary/Z.ma @ 405

Last change on this file since 405 was 400, checked in by campbell, 9 years ago

Minor changes for the new version of matita.

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