source: src/utilities/binary/division.ma @ 1528

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

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.

File size: 11.2 KB
Line 
1
2
3
4
5
6
7
8
9include "utilities/binary/Z.ma".
10include "utilities/binary/positive.ma".
11
12
13(* XXX: divides goes to arithmetics *)
14inductive dividesP (n,m:Pos) : Prop ≝
15| witness : ∀p:Pos.m = times n p → dividesP n m.
16interpretation "positive divides" 'divides n m = (dividesP n m).
17interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
18
19definition dividesZ : Z → Z → Prop ≝
20λx,y. match x with
21[ OZ ⇒ False
22| pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
23| neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
24].
25
26interpretation "integer divides" 'divides n m = (dividesZ n m).
27interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
28
29
30
31
32(* division *)
33
34inductive natp : Type[0] ≝
35| pzero : natp
36| ppos  : Pos → natp.
37
38definition natp0 ≝
39λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
40
41definition natp1 ≝
42λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
43
44let rec divide (m,n:Pos) on m ≝
45match m with
46[ one ⇒
47  match n with
48  [ one ⇒ 〈ppos one,pzero〉
49  | _ ⇒ 〈pzero,ppos one〉
50  ]
51| p0 m' ⇒
52  match divide m' n with
53  [ pair q r ⇒
54    match r with
55    [ pzero ⇒ 〈natp0 q,pzero〉
56    | ppos r' ⇒
57      match partial_minus (p0 r') n with
58      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
59      | MinusZero ⇒ 〈natp1 q, pzero〉
60      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
61      ]
62    ]
63  ]
64| p1 m' ⇒
65  match divide m' n with
66  [ pair q r ⇒
67    match r with
68    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
69    | ppos r' ⇒
70      match partial_minus (p1 r') n with
71      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
72      | MinusZero ⇒ 〈natp1 q, pzero〉
73      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
74      ]
75    ]
76  ]
77].
78
79definition div ≝ λm,n. fst ?? (divide m n).
80definition mod ≝ λm,n. snd ?? (divide m n).
81
82lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).
83@pos_elim /3/;
84qed.
85
86lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
87@pos_elim
88[ //
89| #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/;
90] qed.
91
92theorem plus_minus_r:
93∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
94#m #n #p #le >(commutative_plus_pos …)
95>(commutative_plus_pos p ?) @plus_minus //; qed.
96
97lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
98#m #n #p elim m;/2/; qed.
99(*
100lemma le_to_minus: ∀m,n. m≤n → m-n = 0.
101#m #n elim n;
102[ <(minus_n_O …) /2/;
103| #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct;
104    >(eq_minus_S_pred …) >(IH A) /2/
105] qed.
106*)
107lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
108#n #m #p (*elim (decidable_lt n m);*)#lt
109(*[*) @(pos_elim … p) //;#p' #IH
110    <(times_succn_m …) <(times_succn_m …) <(times_succn_m …)
111    >(minus_plus_distrib …)
112    <(plus_minus … lt) <IH
113    >(plus_minus_r …) /2/;
114qed.
115(*|
116lapply (not_lt_to_le … lt); #le
117@(pos_elim … p) //; #p'
118 cut (m-n = one); [ /3/ ]
119  #mn >mn >(times_n_one …) >(times_n_one …)
120  #H <H in ⊢ (???%)
121  @sym_eq @le_n_one_to_eq <H
122  >(minus_plus_distrib …) @monotonic_le_minus_l
123  /2/;
124] qed.
125
126lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
127#m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//;
128#H' lapply (minus_to_plus … H'); /2/;
129<(plus_n_O …) #H'' >H'' in H #H
130@False_ind @(absurd ? H ( not_le_Sn_n n))
131qed.
132*)
133
134let rec natp_plus (n,m:natp) ≝
135match n with
136[ pzero ⇒ m
137| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
138].
139
140let rec natp_times (n,m:natp) ≝
141match n with
142[ pzero ⇒ pzero
143| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
144].
145
146inductive natp_lt : natp → Pos → Prop ≝
147| plt_zero : ∀n. natp_lt pzero n
148| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
149
150lemma lt_p0: ∀n:Pos. one < p0 n.
151#n normalize; /2/; qed.
152
153lemma lt_p1: ∀n:Pos. one < p1 n.
154#n' normalize; >(?:p1 n' = succ (p0 n')) //; qed.
155
156lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
157#m elim m;
158[ //;
159| 2,3: #m' #IH normalize; >IH //;
160] qed.
161
162lemma pos_nonzero2: ∀n. ∀P:Pos→Type[0]. ∀Q:Type[0]. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).
163#n #P #Q @succ_elim /2/; qed.
164
165lemma partial_minus_to_Prop: ∀n,m.
166  match partial_minus n m with
167  [ MinusNeg ⇒ n < m
168  | MinusZero ⇒ n = m
169  | MinusPos r ⇒ n = m+r
170  ].
171#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus_pos n m);
172normalize; cases (partial_minus n m); /2/; qed.
173
174lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
175#n #m #lt elim lt; /2/;
176qed.
177
178lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
179#n #m #lt @(transitive_lt ? (p0 m) ?) /2/;
180qed.
181
182lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
183#n #m #lt inversion lt;
184[ #H >(succ_injective … H) //;
185| #p #H1 #H2 #H3 >(succ_injective … H3)
186    @(transitive_lt ? (p0 p) ?) /2/;
187]
188qed.
189
190lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
191#n #m #lt elim lt; /2/;
192qed.
193
194
195
196lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
197#n #m #lt inversion lt;
198[ #p #H destruct;
199| #n' #m' #lt #e1 #e2 destruct @lt
200] qed.
201
202lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
203#a #b /2/; qed.
204
205lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
206#a #b >(?:p1 b = succ (p0 b)) /2/; qed.
207
208lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
209/2/; qed.
210
211theorem divide_ok : ∀m,n,dv,md.
212 divide m n = 〈dv,md〉 →
213 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
214#m #n @(pos_cases … n)
215[ >(divide_by_one m) #dv #md #H destruct normalize /2/
216| #n' elim m;
217  [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
218  | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?);
219      lapply (refl ? (divide m' (succ n')));
220      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
221      #dv' #md' #DIVr elim (IH … DIVr);
222      whd in ⊢ (? → ? → ??%? → ?);
223      cases md';
224      [ cases dv'; normalize;
225        [ #H destruct
226        | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/
227        ]
228      | cases dv'; [ 2: #dv'' ] @succ_elim
229          normalize; #n #md'' #Hr1 #Hr2
230          lapply (plt_lt … Hr2); #Hr2'
231          lapply (partial_minus_to_Prop md'' n);
232          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
233          #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos
234          [ 1,3,5,7: @double_lt1 /2/;
235          | 2,4: @double_lt3 /2/;
236          | *: @double_lt2 /2/;
237          ]
238      ]
239  | #m' #IH #dv #md whd in ⊢ (??%? → ?);
240      lapply (refl ? (divide m' (succ n')));
241      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
242      #dv' #md' #DIVr elim (IH … DIVr);
243      whd in ⊢ (? → ? → ??%? → ?); cases md';
244      [ cases dv'; normalize;
245        [ #H destruct;
246        | #dv'' #Hr1 #Hr2 #H destruct; /3/;
247        ]
248      | (*cases dv'; [ 2: #dv'' ] @succ_elim
249          normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2
250          lapply (plt_lt … Hr2); #Hr2'
251          whd in ⊢ (??%? → ?);
252          lapply (partial_minus_to_Prop (p0 md'') (succ n'));
253          cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ]
254          cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize
255          #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ]
256          #lt #e [ 1,3,4,6: >lt ]
257          destruct
258          normalize in ⊢ (?(???%)?); % /2/; @plt_pos
259          [ cut (succ n' + r'' < p0 (succ n')); /2/;
260          | cut (succ n' + r'' < p0 (succ n')); /2/; ]]]]
261qed.
262
263lemma mod0_divides: ∀m,n,dv:Pos.
264  divide n m = 〈ppos dv,pzero〉 → m∣n.
265#m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *)
266normalize #H destruct //
267qed.
268
269lemma divides_mod0: ∀dv,m,n:Pos.
270  n = dv*m → divide n m = 〈ppos dv,pzero〉.
271#dv #m #n #DIV lapply (refl ? (divide n m));
272elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE
273lapply (divide_ok … DIVIDE); *;
274cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
275cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
276>DIV in ⊢ (% → ?); #H #lt destruct;
277[ lapply (plus_to_minus_pos … e0);
278    >(commutative_times …) >(commutative_times dv'' …)
279    cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
280    >(minus_times_distrib_l …) //;
281
282 (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ]
283    #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind
284    @(absurd ? B (lt_to_not_le … A))
285
286| @False_ind @(absurd ? (plt_lt … lt) ?) /2/;
287
288| >DIVIDE cut (dv = dv''); /2/;
289]
290qed.
291
292lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
293#m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %);
294#dv #md cases md; cases dv;
295[ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct
296| #dv' #H %1 @mod0_divides /2/;
297| #md' #DIVIDES %2 @nmk *; #dv'
298    >(commutative_times …) #H lapply (divides_mod0 … H);
299    >DIVIDES #H'
300    destruct;
301| #md' #dv' #DIVIDES %2 @nmk *; #dv'
302    >(commutative_times …) #H lapply (divides_mod0 … H);
303    >DIVIDES #H'
304    destruct;
305] qed.
306
307theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
308#p #q cases p;
309[ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ]
310| *: #n cases q; normalize; /2/;
311] qed.
312
313definition natp_to_Z ≝
314λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
315
316definition natp_to_negZ ≝
317λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
318
319(* TODO: check these definitions are right.  They are supposed to be the same
320   as Zdiv/Zmod in Coq. *)
321definition divZ ≝ λx,y.
322  match x with
323  [ OZ ⇒ OZ
324  | pos n ⇒
325    match y with
326    [ OZ ⇒ OZ
327    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
328    | neg m ⇒ match divide n m with [ pair q r ⇒
329                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
330    ]
331  | neg n ⇒
332    match y with
333    [ OZ ⇒ OZ
334    | pos m ⇒ match divide n m with [ pair q r ⇒
335                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
336    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
337    ]
338  ].
339
340definition modZ ≝ λx,y.
341  match x with
342  [ OZ ⇒ OZ
343  | pos n ⇒
344    match y with
345    [ OZ ⇒ OZ
346    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
347    | neg m ⇒ match divide n m with [ pair q r ⇒
348                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
349    ]
350  | neg n ⇒
351    match y with
352    [ OZ ⇒ OZ
353    | pos m ⇒ match divide n m with [ pair q r ⇒
354                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
355    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
356    ]
357  ].
358
359interpretation "natural division" 'divide m n = (div m n).
360interpretation "natural modulus" 'module m n = (mod m n).
361interpretation "integer division" 'divide m n = (divZ m n).
362interpretation "integer modulus" 'module m n = (modZ m n).
363
364
365
366
367
368
369
370theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
371#x #y cases y;
372[ #H @(False_ind … H)
373| #m #_ cases x;
374  [ % //;
375  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
376      cases (divide n m) in ⊢ (???% → %); #dv #md #H
377      elim (divide_ok … H); #e #l elim l; /2/;
378  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
379      cases (divide n m) in ⊢ (???% → %); #dv #md #H
380      elim (divide_ok … H); #e #l elim l;
381      [ /2/;
382      | #md' #m' #l' %
383        [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …)
384            >(pos_compare_lt … l') //;
385        | @Zminus_Zlt //;
386        ]
387      ]
388  ]
389| #m #H @(False_ind … H)
390] qed.
Note: See TracBrowser for help on using the repository browser.