source: src/utilities/binary/Z.ma @ 697

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

Merge Clight branch of vectors and friends.
Start making stuff build.

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