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

Last change on this file since 3257 was 1523, checked in by campbell, 8 years ago

Separate out positive and Z definitions from extralib.ma.
Minor syntax updates.

File size: 23.0 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 @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 @(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 normalize @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 normalize @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 //
462|#p cases y
463   [//
464   |//
465   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
466      cases (pos_compare q p);//]
467|#p cases y
468   [//;
469   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
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
505whd in ⊢ (??%%);
506<(pos_compare_S_S …)
507>(minus_S_S …)
508>(minus_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    change with (Zsucc (pos m')) in ⊢ (??(??%)?);
525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
526| #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
527    >partial_minus_S_one normalize; >pos_nonzero
528    <pred_succ_n //
529| #m' #n' whd in ⊢ (??%%); <pos_compare_S_S
530    >minus_S_S
531    >minus_S_S normalize
532    >pos_nonzero
533    >pos_nonzero
534    <pred_succ_n
535    <pred_succ_n
536    normalize; //;
537] qed.
538
539theorem Zplus_neg_neg:
540  ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
541#n #m @(pos_cases … n) @(pos_cases … m)
542[ 1,2: //;
543| #n' normalize in ⊢ (???(?%?));
544    >(pos_nonzero …)
545    <(pred_succ_n …) normalize; //;
546| #m' #n' normalize; >(pos_nonzero …)
547    <(pred_succ_n …) normalize; //;
548] qed.
549
550theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
551#x #y cases x
552[cases y
553   [//
554   |#n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) //
555   |#p <(Zsucc_Zplus_pos_O …) //]
556|cases y;/2/; #p >(sym_Zplus ? (Zpred OZ))
557   <Zpred_Zplus_neg_O //;
558|cases y
559   [#n <(sym_Zplus ??) <(sym_Zplus (Zpred OZ) ?)
560      <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc ?) //
561   |*:/2/]
562qed.
563
564theorem Zplus_Zsucc_pos_pos :
565  ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
566#n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //;
567qed.
568
569theorem Zplus_Zsucc_pos_neg:
570  ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
571#n #m
572@(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
573[#n1 elim n1
574   [//
575   |*:#n2 #IH elim n2;//]
576|#n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?)
577   >(sym_Zplus …) <(Zpred_Zplus_neg_O ?)
578   >(Zpred_Zsucc …)  /2/
579|#n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH
580<(Zplus_pos_neg …) //]
581qed.
582
583theorem Zplus_Zsucc_neg_neg :
584  ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
585#n #m
586@(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
587[@pos_elim
588   [//
589   |#n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //]
590| #n' normalize;
591   >(pos_nonzero …)
592   <(pred_succ_n …) normalize;
593   <(succ_plus_one …)
594   <(succ_plus_one …) >(pos_nonzero …) //;
595| #n' #m' #IH normalize;
596   >(pos_nonzero …) normalize;
597   <(pluss_succn_m …)
598   >(pos_nonzero …) //;
599]
600qed.
601
602lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
603#n #m whd in ⊢ (??%%); <pos_compare_S_S
604>minus_S_S >minus_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
637theorem associative_Zplus: associative Z Zplus.
638(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
639#x #y #z cases x
640[//
641|@pos_elim
642   [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //;
643   |#n1 #IH
644      >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?)
645      >(Zplus_Zsucc ((pos n1)+y) ?) //]
646|@pos_elim
647   [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //;
648   |#n1 #IH
649      >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?)
650      >(Zplus_Zpred ((neg n1)+y) ?) //]
651]
652qed.
653
654(* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
655\def associative_Zplus. *)
656
657(* Zopp *)
658definition Zopp : Z → Z ≝
659  λx:Z. match x with
660  [ OZ ⇒ OZ
661  | pos n ⇒ neg n
662  | neg n ⇒ pos n ].
663
664interpretation "integer unary minus" 'uminus x = (Zopp x).
665
666theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
667//;
668qed.
669
670theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
671#x #y cases x
672[cases y;//
673|*:#n cases y;//;#m whd in ⊢ (??(?%)%); @pos_compare_elim normalize;//]
674qed.
675
676theorem Zopp_Zopp: ∀x:Z. --x = x.
677#x cases x;//;
678qed.
679
680theorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
681#x cases x
682[//
683|*:#n whd in ⊢ (??%?); >pos_compare_n_n //]
684qed.
685
686theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
687#x #z #y #H
688<(Zplus_z_OZ z) <(Zplus_z_OZ y)
689<(Zplus_Zopp x)
690<(associative_Zplus ???) <(associative_Zplus ???)
691//;
692qed.
693
694theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
695#x #z #y #H
696@(injective_Zplus_l x)
697<(sym_Zplus ??)
698//;
699qed.
700
701(* minus *)
702definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
703
704interpretation "integer minus" 'minus x y = (Zminus x y).
705
706
707
708definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n).
709definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n).
710definition two_p : Z → Z ≝
711λz.match z with
712[ OZ ⇒ pos one
713| pos p ⇒ pos (two_power_pos p)
714| neg _ ⇒ OZ  (* same fib as Coq *)
715].
716
717
718
719lemma eqZb_z_z : ∀z.eqZb z z = true.
720#z cases z;normalize;//;
721qed.
722
723
724
725lemma injective_Z_of_nat : injective ? ? Z_of_nat.
726normalize;
727#n #m cases n;cases m;normalize;//;
728[ 1,2: #n' #H destruct
729| #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
730] qed.
731
732lemma reflexive_Zle : reflexive ? Zle.
733#x cases x; //; qed.
734
735lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
736#n cases n;normalize;//;qed.
737
738lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
739#x cases x; //;
740#n cases n; //; qed.
741
742lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
743#x #y
744@pos_elim
745 [ 2: #n' #IH ]
746>(Zplus_Zsucc_Zpred y ?)
747[ >(Zpred_Zsucc (pos n'))
748 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
749    @Zsucc_le
750| #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
751] qed.
752
753theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
754#x #y cases x;
755[ cases y;
756  [ 1,2: //
757  | #n @False_ind
758  ]
759| #n cases y;
760  [ normalize; @False_ind
761  | #m @(pos_cases … n) /2/;
762  | #m normalize; @False_ind
763  ]
764| #n cases y; /2/;
765] qed.
766   
767theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
768#n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
769@(transitive_Zle … Hle) /2/;
770qed.
771
772include "basics/types.ma".
773
774definition decidable_eq_Z_Type : ∀z1,z2:Z. (z1 = z2) + (z1 ≠ z2).
775#z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
776[% //
777|%2 //]
778qed.
779
780lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
781#z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
782#H #H' @False_ind @(absurd ? H H')
783qed.
784
785(* Z.ma *)
786
787definition Zge: Z → Z → Prop ≝
788λn,m:Z.m ≤ n.
789
790interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
791
792definition Zgt: Z → Z → Prop ≝
793λn,m:Z.m<n.
794
795interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
796
797interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
798
799let rec Zleb (x:Z) (y:Z) : bool ≝
800  match x with
801  [ OZ ⇒
802    match y with
803    [ OZ ⇒ true
804    | pos m ⇒ true
805    | neg m ⇒ false ]
806  | pos n ⇒
807    match y with
808    [ OZ ⇒ false
809    | pos m ⇒ leb n m
810    | neg m ⇒ false ]
811  | neg n ⇒
812    match y with
813    [ OZ ⇒ true
814    | pos m ⇒ true
815    | neg m ⇒ leb m n ]].
816   
817let rec Zltb (x:Z) (y:Z) : bool ≝
818  match x with
819  [ OZ ⇒
820    match y with
821    [ OZ ⇒ false
822    | pos m ⇒ true
823    | neg m ⇒ false ]
824  | pos n ⇒
825    match y with
826    [ OZ ⇒ false
827    | pos m ⇒ leb (succ n) m
828    | neg m ⇒ false ]
829  | neg n ⇒
830    match y with
831    [ OZ ⇒ true
832    | pos m ⇒ true
833    | neg m ⇒ leb (succ m) n ]].
834
835
836
837theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
838#n #m cases n;cases m; //;
839[ 1,2: #m' normalize; #H @(False_ind ? H)
840| 3,5: #n' #m' normalize; @le_to_leb_true
841| 4: #n' #m' normalize; #H @(False_ind ? H)
842] qed.
843
844theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
845#n #m cases n;cases m; //;
846[ 1,2: #m' normalize; #H destruct
847| 3,5: #n' #m' normalize; @leb_true_to_le
848| 4: #n' #m' normalize; #H destruct
849] qed.
850
851theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
852#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
853qed.
854
855theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
856#n #m cases n;cases m; //;
857[ normalize; #H @(False_ind ? H)
858| 2,3: #m' normalize; #H @(False_ind ? H)
859| 4,6: #n' #m' normalize; @le_to_leb_true
860| #n' #m' normalize; #H @(False_ind ? H)
861] qed.
862
863theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
864#n #m cases n;cases m; //;
865[ normalize; #H destruct
866| 2,3: #m' normalize; #H destruct
867| 4,6: #n' #m' @leb_true_to_le
868| #n' #m' normalize; #H destruct
869] qed.
870
871theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
872#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
873qed.
874
875theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
876(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
877#n #m #P #Hle #Hnle
878lapply (refl ? (Zleb n m));
879elim (Zleb n m) in ⊢ ((???%)→%);
880#Hb
881[ @Hle @(Zleb_true_to_Zle … Hb)
882| @Hnle @(Zleb_false_to_not_Zle … Hb)
883] qed.
884
885theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
886(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
887#n #m #P #Hlt #Hnlt
888lapply (refl ? (Zltb n m));
889elim (Zltb n m) in ⊢ ((???%)→%);
890#Hb
891[ @Hlt @(Zltb_true_to_Zlt … Hb)
892| @Hnlt @(Zltb_false_to_not_Zlt … Hb)
893] qed.
894
895lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
896#x #y cases x; cases y; /2/;
897#n #m @(pos_cases … n) @(pos_cases … m)
898[ //;
899| #n' /2/;
900| #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
901| #n' #m' #H normalize in H;
902    >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
903] qed.
904
905lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
906#x #y cases x; cases y;
907[ 1,2,7,8,9: /2/;
908| 3,4: #m normalize; *;
909| #m #n @(pos_cases … n) @(pos_cases … m)
910  [ 1,2: /2/;
911  | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
912  | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
913  ]
914| #m #n normalize; *;
915] qed.
916
917lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
918#n cases n; //; #n' #a #b #H
919[ @(pos_elim … n')
920  [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
921  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
922      >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
923  ]
924| @(pos_elim … n')
925  [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
926  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
927      >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
928  ]
929] qed.
930
931lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
932/2/; qed.
933
934let rec Z_times (x:Z) (y:Z) : Z ≝
935match x with
936[ OZ ⇒ OZ
937| pos n ⇒
938  match y with
939  [ OZ ⇒ OZ
940  | pos m ⇒ pos (n*m)
941  | neg m ⇒ neg (n*m)
942  ]
943| neg n ⇒
944  match y with
945  [ OZ ⇒ OZ
946  | pos m ⇒ neg (n*m)
947  | neg m ⇒ pos (n*m)
948  ]
949].
950interpretation "integer multiplication" 'times x y = (Z_times x y).
951
952
953
954definition Zmax : Z → Z → Z ≝
955  λx,y.match Z_compare x y with
956  [ LT ⇒ y
957  | _ ⇒ x ].
958
959lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
960#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
961/3/ qed.
962
963lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
964#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
965whd in ⊢ (% → ??%); /3/ qed.
966
967
968lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
969#x #y cases y;
970[ #H @(False_ind … H)
971| #m #_ cases x; //; #n
972    whd in ⊢ (?%?);
973    lapply (pos_compare_to_Prop n m);
974    cases (pos_compare n m); /2/
975    #lt whd <(minus_Sn_m … lt) /2/;
976| #m #H @(False_ind … H)
977] qed.
978
Note: See TracBrowser for help on using the repository browser.