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

Last change on this file since 1599 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

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