← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/embedded/Exercises/Exercise1-2/Exercise1.2.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/embedded/Exercises/Exercise1-2/Exercise1.2.lisp
 
1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2
;;;;
 
3
;;;;               Exercise 1.2
 
4
;;;;
 
5
;;;;   Load with (ld "Exercise1.2.lisp")
 
6
;;;;
 
7
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
8
 
 
9
 
 
10
 
 
11
 
 
12
 
 
13
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
14
;;
 
15
;; The proof is structured in two main phases:
 
16
;; 
 
17
;; 1 - Prove that, given a set of coprimes m and a value m, 
 
18
;;     if each element of m divides v, then the product of the elements of m 
 
19
;;     divides v.
 
20
;; 2 - Prove that, given a set of coprimes m, and given two values v1 and v2 which are 
 
21
;;     congruent modulo m with two sets of values l1 and l2, then l1 and l2 
 
22
;;     are congruent w.r.t. m iff v1 and v2 differ by a multiple of the 
 
23
;;     product of the elements of m. The ``if'' direction of this proof
 
24
;;     exploits the statement obtained in phase 1.
 
25
;;   
 
26
;; Once the statement of phase 2 is proved, the theorem requested in the exercise
 
27
;; is easily proved.
 
28
;;
 
29
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
30
 
 
31
 
 
32
 
 
33
 
 
34
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
35
;;
 
36
;; Phase 1:
 
37
;;
 
38
;; The key facts that are proved are the following (we omit the
 
39
;; statement of some hypothesis here):
 
40
;;
 
41
;; (1) gcd(x,y) = 1 ^  y|v ^ x|v ==> xy|v                     (divides-both)
 
42
;; (2) gcd(x,y) = 1 ^  z|x ^ z|y ==> z = 1                    (only-divisor-of-coprimes-is-1)
 
43
;; (3) gcd(x,y)|x   ^ gcd(x,y)|y                              (gcd-divides-both)
 
44
;; (4) gcd(m,n) = 1 ^ gcd(n,k) = 1 ==> gcd(m,nk) =1           (prime-of-product)
 
45
;; (5) ForAll i: gcd(e,m_i) = 1 ==> gcd(m,Product(m_i)) = 1   (rel-prime-of-product)
 
46
;; (6) ForAll i,j with j<>j: gcd(m_i,m_j) = 1 ^
 
47
;;     ForAll i: m_i|v ==> Product(m_i)|v                     
 
48
;;                             (if-every-coprime-divides-v-then-product-of-coprimes-divides-v)
 
49
;;          
 
50
;;
 
51
;; The proof structure of this phase goes as follows:
 
52
;;
 
53
;;                             (2)     (3)
 
54
;;                               \     /
 
55
;;                                \   /
 
56
;;                                 (4)
 
57
;;                                 /
 
58
;;                                /
 
59
;;                      (1)     (5)
 
60
;;                        \     /
 
61
;;                         \   /
 
62
;;                          (6)
 
63
;;
 
64
;;
 
65
;;
 
66
 
 
67
(in-package "ACL2")
 
68
 
 
69
 
 
70
(include-book "../../../../../arithmetic/mod-gcd")
 
71
 
 
72
(include-book "../../../../../rtl/rel1/lib1/basic")
 
73
 
 
74
(include-book "../../../../../rtl/rel1/support/fp")
 
75
 
 
76
;(local (include-book "../../../../../arithmetic/mod-gcd"))
 
77
 
 
78
;(local (include-book "../../../../../fp/lib/basic"))
 
79
 
 
80
;(local (include-book "../../../../../fp/fp"))
 
81
 
 
82
 
 
83
(defun g-c-d (x y) (nonneg-int-gcd x y))
 
84
 
 
85
 
 
86
(defun rel-prime (x y)
 
87
  (= (g-c-d x y) 1))
 
88
 
 
89
(defun rel-prime-all (x l)
 
90
  (if (endp l)
 
91
      t
 
92
    (and (rel-prime x (car l))
 
93
         (rel-prime-all x (cdr l)))))
 
94
 
 
95
(defun rel-prime-moduli (l)
 
96
  (if (endp l)
 
97
      t
 
98
    (and (integerp (car l))
 
99
         (>= (car l) 2)
 
100
         (rel-prime-all (car l) (cdr l))
 
101
         (rel-prime-moduli (cdr l)))))
 
102
 
 
103
(defun divided-by-all (k m)
 
104
  (if (endp m)
 
105
      t
 
106
    (and
 
107
     (integerp (/ k (car m)))
 
108
     (divided-by-all k (cdr m)))))
 
109
 
 
110
(defun natp-all (l)
 
111
  (if (endp l)
 
112
      t
 
113
    (and (natp (car l))
 
114
         (natp-all (cdr l)))))
 
115
 
 
116
(defun posp-all (l)
 
117
  (if (endp l)
 
118
      t
 
119
    (and (posp (car l))
 
120
         (posp-all (cdr l)))))
 
121
 
 
122
(defun prod (l)
 
123
  (if (endp l)
 
124
      1
 
125
    (* (car l) (prod (cdr l)))))
 
126
 
 
127
 
 
128
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
129
;;
 
130
;; First we prove that, if x and y are positive coprimes, and they both divide v, 
 
131
;; then x * y divides v. We exploit the fact that the g-c-d can be expressed as
 
132
;; a linear combination of two multiplier functions, defined into the mod-gcd book.
 
133
;;
 
134
;; The final lemma is stated by theorem divides-both.
 
135
;;
 
136
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
137
 
 
138
(defun a (x y) (nonneg-int-gcd-multiplier1 x y))
 
139
 
 
140
(defun b (x y) (nonneg-int-gcd-multiplier2 x y))
 
141
 
 
142
 
 
143
(defthm g-c-d-type
 
144
    (implies (and (integerp x) (integerp y))
 
145
             (integerp (g-c-d x y)))
 
146
  :rule-classes (:type-prescription))
 
147
 
 
148
(defthm a-b-thm
 
149
    (implies (and (integerp x) (>= x 0)
 
150
                  (integerp y) (>= y 0))
 
151
             (= (+ (* (a x y) x)
 
152
                   (* (b x y) y))
 
153
                (g-c-d x y)))
 
154
  :hints (("Goal" :use Linear-combination-for-nonneg-int-gcd))
 
155
  :rule-classes ())
 
156
 
 
157
 
 
158
(in-theory (disable g-c-d))
 
159
 
 
160
(defthm hack-1
 
161
        (implies (and (integerp v) (= gcd 1)) (= (* v gcd) v))
 
162
        :rule-classes nil)
 
163
 
 
164
(defthm hack-2 
 
165
 (implies
 
166
  (and
 
167
   (natp x)
 
168
   (natp y)
 
169
   (integerp v)
 
170
   (= (g-c-d x y) 1))
 
171
 (= (* v (+ (* (A X Y) X) (* (B X Y) Y))) v))
 
172
 :hints (("Goal" :in-theory '((:definition natp))
 
173
        :use (a-b-thm
 
174
              (:instance hack-1 (gcd (+ (* (A X Y) X) (* (B X Y) Y)))))))
 
175
 :rule-classes nil)
 
176
 
 
177
 
 
178
(defthm hack-3 
 
179
 (implies
 
180
  (and
 
181
   (integerp a)
 
182
   (integerp b)
 
183
   (natp x)
 
184
   (natp y)
 
185
   (> x 0)
 
186
   (> y 0)
 
187
   (integerp v))
 
188
 (= (* v (+ (* A X) (* B Y)) (/ (* x y)))
 
189
    (+ (* (/ v y) a) (* (/ v x) b))))
 
190
 :rule-classes nil)
 
191
 
 
192
 
 
193
(defthm hack-4
 
194
 (implies
 
195
  (and
 
196
   (natp x)
 
197
   (natp y)
 
198
   (> x 0)
 
199
   (> y 0)
 
200
   (integerp v))
 
201
 (= (* v (+ (* (A X Y) X) (* (B X Y) Y)) (/ (* x y)))
 
202
    (+ (* (/ v y) (a x y)) (* (/ v x) (b x y)))))
 
203
 :hints (("Goal" :use ((:instance hack-3 (a (a x y)) (b (b x y)))
 
204
                       (:type-prescription a)
 
205
                       (:type-prescription b))))
 
206
 :rule-classes nil)
 
207
 
 
208
 
 
209
(defthm hack-5
 
210
 (implies
 
211
   (and 
 
212
     (integerp v1)
 
213
     (integerp v2)
 
214
     (integerp v3)
 
215
     (integerp v4))
 
216
   (integerp (+ (* v1 v2) (* v3 v4))))
 
217
 :rule-classes nil)
 
218
 
 
219
 
 
220
(defthm hack-6
 
221
 (implies
 
222
  (and
 
223
   (integerp (/ v y))
 
224
   (integerp (/ v x)))
 
225
   (integerp (+ (* (/ v y) (a x y)) (* (/ v x) (b x y)))))
 
226
         :hints (("Goal" :use ( (:instance hack-5 (v1 (/ v y)) (v2 (a x y)) (v3 (/ v x)) (v4 (b x y)))
 
227
                       (:type-prescription a)
 
228
                       (:type-prescription b))))
 
229
  :rule-classes nil)
 
230
 
 
231
(defthm hack-7
 
232
(IMPLIES 
 
233
 (AND 
 
234
  (equal decomp-a-b  
 
235
         V)             
 
236
  (equal (* decomp-a-b
 
237
            div)
 
238
         res) 
 
239
  (INTEGERP res))
 
240
 (INTEGERP (* V div)))
 
241
:hints (("Goal" :in-theory nil))
 
242
:rule-classes nil)
 
243
 
 
244
 
 
245
 
 
246
(defthm divides-both 
 
247
 (implies
 
248
  (and
 
249
   (natp x)
 
250
   (natp y)
 
251
   (> x 0)
 
252
   (> y 0)
 
253
   (integerp v)
 
254
   (integerp (/ v y))
 
255
   (integerp (/ v x))
 
256
   (rel-prime x y)) 
 
257
  (integerp (/ v (* x y))))
 
258
 :hints (("Goal" :in-theory (current-theory 'ground-zero) 
 
259
        :use (rel-prime
 
260
              hack-2 
 
261
              hack-4 
 
262
              hack-6
 
263
             (:instance hack-7 (div (/ (* X Y)))
 
264
                                  (res  (+ (* (* V (/ Y)) (A X Y)) (* (* V (/ X)) (B X Y))))
 
265
                                  (decomp-a-b (* V (+ (* (A X Y) X) (* (B X Y) Y)))))))))
 
266
 
 
267
 
 
268
 
 
269
 
 
270
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
271
;;
 
272
;; Now we prove that the only common divisor of two coprimes is 1.
 
273
;;
 
274
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
275
 
 
276
 
 
277
 
 
278
 
 
279
(defthm hack-8
 
280
  (implies
 
281
   (and
 
282
    (natp n)
 
283
    (posp d))
 
284
   (equal (integerp (/ n d)) (equal (nonneg-int-mod n d) 0)))
 
285
  :hints (("Goal" :use (:instance Left-nonneg-int-mod-* (n d) (j (/ n d))))))
 
286
 
 
287
 
 
288
 
 
289
(defthm only-divisor-of-coprimes-is-1
 
290
 (implies
 
291
  (and
 
292
   (natp y)
 
293
   (natp x)
 
294
   (posp z)
 
295
   (rel-prime x y)
 
296
   (integerp (/ x z))
 
297
   (integerp (/ y z)))
 
298
  (= z 1))
 
299
 :hints (("Goal" :use (rel-prime g-c-d 
 
300
                       (:instance Nonneg-int-gcd-is-LARGEST-common-divisor-<= (d z)))))
 
301
 :rule-classes nil)
 
302
 
 
303
 
 
304
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
305
;; 
 
306
;; We now prove that (g-c-d x y) divides both x and y.
 
307
;; This is stated by theorem gcd-divides-both.
 
308
;;
 
309
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
310
 
 
311
(defthm integer-div-of-factor
 
312
 (implies
 
313
  (and
 
314
   (natp a)
 
315
   (natp b)
 
316
   (natp c)
 
317
   (rel-prime a b)
 
318
   (integerp (/ (* b c) a)))
 
319
  (integerp (/ c a)))
 
320
  :hints (("Goal" :use 
 
321
           ((:instance rel-prime (x a) (y b))
 
322
            (:instance g-c-d (x a) (y b))
 
323
            (:instance hack-8 (n c) (d a))
 
324
            (:instance hack-8 (n (* b c)) (d a))
 
325
            (:instance Divisor-of-product-divides-factor (y b) (z a) (x c))))))
 
326
 
 
327
        
 
328
(defthm hack-9 
 
329
 (implies
 
330
  (and 
 
331
   (integerp x)
 
332
   (posp y)
 
333
   (integerp (/ x y)))
 
334
  (= x (* (/ x y) y)))
 
335
 :rule-classes nil)
 
336
 
 
337
(defthm hack-10
 
338
 (implies
 
339
  (and
 
340
   (integerp c)
 
341
   (= (+ (* a x) (* b y)) 1))
 
342
   (= (* c (+ (* a x) (* b y))) c))
 
343
 :rule-classes nil)
 
344
 
 
345
(defthm hack-11
 
346
 (implies
 
347
  (and
 
348
   (integerp c))
 
349
   (= (+ (* c a x) (* c b y)) 
 
350
      (* c (+ (* a x) (* b y)))))
 
351
 :rule-classes nil)
 
352
 
 
353
(defthm hack-12 
 
354
 (implies
 
355
  (and
 
356
   (integerp c)
 
357
   (= (+ (* a x) (* b y)) 1))
 
358
   (= (+ (* c a x) (* c b y)) c)) 
 
359
 :hints (("Goal" :use (hack-10 hack-11)))
 
360
 :rule-classes nil)
 
361
 
 
362
 
 
363
 
 
364
 
 
365
(defthm hack-13
 
366
 (implies
 
367
  (and
 
368
   (natp m)
 
369
   (natp n)
 
370
   (natp k)
 
371
   (rel-prime m n))
 
372
  (= k (+ (* k (a m n) m) (* k (b m n) n))))
 
373
 :hints (("Goal" :use (
 
374
                       (:instance hack-12 (a (a m n)) (b (b m n)) (x m) (y n) (c k))
 
375
                       (:instance a-b-thm (x m) (y n)) 
 
376
                       (:instance rel-prime (x m) (y n)))))
 
377
 :rule-classes nil)
 
378
 
 
379
(defthm hack-14
 
380
 (implies
 
381
  (and
 
382
   (natp m)
 
383
   (natp n)
 
384
   (natp k)
 
385
   (posp cd)
 
386
   (integerp (/ m cd))
 
387
   (integerp (/ (* n k) cd))
 
388
   (rel-prime m n))
 
389
  (= k (+ (* k (a m n) (/ m cd) cd) (* (b m n) (/ (* n k) cd) cd))))
 
390
 :hints (("Goal" :use (
 
391
                       hack-13
 
392
                       (:instance hack-9 (x m) (y cd))
 
393
                       (:instance hack-9 (x (* n k)) (y cd)))))
 
394
 :rule-classes nil)
 
395
 
 
396
(defthm hack-15
 
397
 (implies
 
398
  (and
 
399
   (natp m)
 
400
   (natp n)
 
401
   (natp k)
 
402
   (posp cd)
 
403
   (integerp (/ m cd))
 
404
   (integerp (/ (* n k) cd))
 
405
   (rel-prime m n))
 
406
  (= k (* cd (+ (* k (a m n) (/ m cd) ) (* (b m n) (/ (* n k) cd))))))
 
407
 :hints (("Goal" :use hack-14))
 
408
 :rule-classes nil)
 
409
 
 
410
(defthm hack-16
 
411
 (implies
 
412
  (and
 
413
   (natp m)
 
414
   (natp n)
 
415
   (natp k)
 
416
   (posp cd)
 
417
   (integerp (/ m cd))
 
418
   (integerp (/ (* n k) cd))
 
419
   (rel-prime m n))
 
420
  (integerp (+ (* k (a m n) (/ m cd) ) (* (b m n) (/ (* n k) cd)))))
 
421
 :rule-classes nil)
 
422
 
 
423
(defthm hack-17
 
424
 (implies
 
425
  (and
 
426
   (natp m)
 
427
   (natp n)
 
428
   (natp k)
 
429
   (posp cd)
 
430
   (integerp (/ m cd))
 
431
   (integerp (/ (* n k) cd))
 
432
   (rel-prime m n))
 
433
  (= (/ k cd) (+ (* k (a m n) (/ m cd) ) (* (b m n) (/ (* n k) cd)))))
 
434
 :hints (("Goal" :use ( hack-16 hack-15)))
 
435
 :rule-classes nil)
 
436
 
 
437
 
 
438
(defthm hack-18
 
439
 (implies
 
440
  (and
 
441
   (natp m)
 
442
   (natp n)
 
443
   (natp k)
 
444
   (posp cd)
 
445
   (integerp (/ m cd))
 
446
   (integerp (/ (* n k) cd))
 
447
   (rel-prime m n))
 
448
  (integerp (/ k cd)))
 
449
 :hints (("Goal" :in-theory nil :use ( hack-16 hack-17)))
 
450
 :rule-classes nil)
 
451
 
 
452
 
 
453
        
 
454
(defthm gcd-divides-both
 
455
 (implies
 
456
  (and
 
457
   (natp x)
 
458
   (posp y))
 
459
  (and
 
460
   (integerp (/ x (g-c-d x y)))
 
461
   (integerp (/ y (g-c-d x y)))))
 
462
 :hints (("Goal" :in-theory (enable g-c-d))))
 
463
 
 
464
 
 
465
 
 
466
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
467
;; 
 
468
;; Frome the fact that (g-c-d x y) divides both x and y, we easily 
 
469
;; derive that, if m and n are coprimes, and m and k are coprimes, 
 
470
;; then m and (n * k) are coprimes.
 
471
;; This is stated by prime-of-product.
 
472
;;
 
473
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
474
 
 
475
 
 
476
(defthm hack-19
 
477
  (implies
 
478
  (and
 
479
   (posp x)
 
480
   (posp y)
 
481
   (natp v)
 
482
   (rel-prime v x)
 
483
   (rel-prime v y))
 
484
  (and
 
485
   (integerp (/ v       (g-c-d v (* x y))))
 
486
   (integerp (/ (* x y) (g-c-d v (* x y))))))
 
487
   :hints (("Goal" :use  ((:instance gcd-divides-both (x v) (y (* x y)))))))
 
488
 
 
489
 
 
490
(defthm hack-20
 
491
  (implies
 
492
  (and
 
493
   (posp n)
 
494
   (posp k)
 
495
   (natp m)
 
496
   (rel-prime m n)
 
497
   (rel-prime m k))
 
498
  (and
 
499
   (integerp (/ m       (g-c-d m (* n k))))
 
500
   (integerp (/ k       (g-c-d m (* n k))))))
 
501
   :hints (("Goal" :use  (          
 
502
                          (:instance g-c-d (x m) (y (* n k)))
 
503
                          (:instance Nonneg-int-gcd->-0 (n m) (d (* n k)))
 
504
                          (:instance hack-19 (v m) (x n) (y k))
 
505
                          (:instance hack-18 (cd (g-c-d m (* n k))))))))
 
506
 
 
507
 
 
508
(defthm prime-of-product
 
509
   (implies
 
510
  (and
 
511
   (posp n)
 
512
   (posp k)
 
513
   (natp m)
 
514
   (rel-prime m n)
 
515
   (rel-prime m k))
 
516
  (rel-prime m (* n k)))
 
517
   :hints (("Goal" :in-theory (enable rel-prime)
 
518
           :use ( hack-20
 
519
                  (:instance g-c-d (x m) (y (* n k)))
 
520
                  (:instance Nonneg-int-gcd->-0 (n m) (d (* n k)))
 
521
                  (:instance only-divisor-of-coprimes-is-1 
 
522
                             (z (g-c-d m (* n k)))
 
523
                             (x m)
 
524
                             (y k))))))
 
525
 
 
526
 
 
527
 
 
528
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
529
;;
 
530
;; We now prove that, if el is coprime with every element of a list
 
531
;; l, then it is coprime with their product (prod l).
 
532
;; This is stated by rel-prime-of-product.
 
533
;;
 
534
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
535
 
 
536
 
 
537
(in-theory (enable prod rel-prime rel-prime-moduli))
 
538
 
 
539
(defthm hack-21
 
540
 (implies
 
541
  (and
 
542
   (not (endp m))
 
543
   (posp-all m))
 
544
  (and
 
545
    (posp-all (cdr m))
 
546
    (posp (car m))
 
547
    (posp (prod m))
 
548
    (posp (prod (cdr m)))))
 
549
 :rule-classes nil)
 
550
 
 
551
(defthm hack-22
 
552
 (implies
 
553
  (and
 
554
   (not (endp m))
 
555
   (rel-prime-all el m))
 
556
  (and
 
557
   (rel-prime el (car m))
 
558
   (rel-prime-all el (cdr m))))
 
559
 :hints (("Goal" :use (:instance rel-prime-all (x el) (l m))))
 
560
 :rule-classes nil)
 
561
 
 
562
 
 
563
(defthm rel-prime-of-product
 
564
 (implies
 
565
   (and
 
566
   (posp-all m)
 
567
   (natp el) 
 
568
   (rel-prime-all el m))
 
569
   (rel-prime el (prod m)))
 
570
 :hints ( ("Goal" :in-theory (disable rel-prime natp) :induct (len m))
 
571
          ("Subgoal *1/2''" :use ( (:instance rel-prime (x el) (y 1))
 
572
                                   (:instance g-c-d (x el) (y 1))
 
573
                                   (:instance Nonneg-int-gcd-1-right (x el))))
 
574
          ("Subgoal *1/1'" :use 
 
575
           (hack-21
 
576
            hack-22
 
577
            (:instance prod (l m))
 
578
            (:instance prime-of-product (n (car m)) (k (prod (cdr m))) (m el))))))
 
579
 
 
580
 
 
581
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
582
;;
 
583
;; We prove the main lemma of the first part of the proof,
 
584
;; namely that if m is a list of positive coprimes, and 
 
585
;; every element of m divides v, then the product of the elements
 
586
;; of m, (prod m), divides v.
 
587
;; This is stated by if-every-coprime-divides-v-then-product-of-coprimes-divides-v.
 
588
;;
 
589
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
590
 
 
591
(defthm hack-23
 
592
 (implies
 
593
  (and 
 
594
   (not (endp m))
 
595
   (rel-prime-moduli m))
 
596
  (and
 
597
   (rel-prime-moduli (cdr m))
 
598
   (posp-all (cdr m))
 
599
   (natp (car m))
 
600
   (< 0 (car m)))))
 
601
 
 
602
  
 
603
 
 
604
 
 
605
(defthm if-every-coprime-divides-v-then-product-of-coprimes-divides-v
 
606
  (implies
 
607
   (and
 
608
    (rel-prime-moduli m)
 
609
    (integerp v)
 
610
    (divided-by-all v m))
 
611
  (integerp (/ v (prod m))))
 
612
 :hints (("Goal" :induct (len m))
 
613
         ("Subgoal *1/1" 
 
614
          :in-theory '((:definition posp) (:definition natp))
 
615
          :use 
 
616
          (
 
617
           hack-21
 
618
           hack-23
 
619
           (:instance natp-all (l m))
 
620
           (:instance posp-all (l m))
 
621
           (:instance prod (l m))
 
622
           (:instance rel-prime-moduli (l m))
 
623
           (:instance divided-by-all (k v))
 
624
           (:instance rel-prime-of-product (el (car m)) (m (cdr m)))
 
625
           (:instance divides-both (x (car m)) (y (prod (cdr m))))))))
 
626
 
 
627
 
 
628
 
 
629
 
 
630
 
 
631
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
632
;;
 
633
;; Second part of the proof.
 
634
;;
 
635
;; We start by introducing the notion of congruence of a pair of lists
 
636
;; of numbers w.r.t. a third list of numbers.
 
637
;; Then we prove the following facts (where some hypothesis are omitted, 
 
638
;; ``congruent'' indicates the definition congruent-all-mod, and 
 
639
;; ``congruent-lists'' indicates the definition in
 
640
;; congruant-all-mod-list):
 
641
;;
 
642
;; (7)  ForAll i: m_i|k ==> congruent (x,y,m) ,==> congruent((x mod k),y,m)
 
643
;; (8)  ForAll i,j with j<>j: gcd(m_i,m_j) = 1 ^
 
644
;;      congruent(v1,l1,m) ^ congruent (v2,l2,m) ^
 
645
;;      Product(m_i)|(v1-v2) ==> congruent-lists(l1,l2,m) 
 
646
;; (9)  ForAll i,j with j<>j: gcd(m_i,m_j) = 1 ^
 
647
;;      congruent(v1,l1,m) ^ congruent (v2,l2,m) ^
 
648
;;      congruent-lists(l1,l2,m) ==> Product(m_i)|(v1-v2) 
 
649
;; (10) ForAll i,j with j<>j: gcd(m_i,m_j) = 1 ^
 
650
;;      congruent(v1,l1,m) ^ congruent (v2,l2,m) ==>
 
651
;;      (congruent-lists(l1,l2,m) <==> Product(m_i)|(v1-v2))
 
652
;; (11) (0<=v1<p) ^ (0<=v2<p) ^ p|(v1-v2) ==> v1 = v2
 
653
;; (12) ForAll i,j with j<>j: gcd(m_i,m_j) = 1 ^
 
654
;;      (0<=v1<p) ^ (0<=v2<p) ^ 
 
655
;;      congruent(v1,l,m) ^ congruent(v2,l,m) ==> v1 = v2
 
656
;;
 
657
;;
 
658
;; The proof scheme is the following (where (6) refers to the main statement derived
 
659
;; in phase 1):
 
660
;;
 
661
;;                               (6)      (7)
 
662
;;                                |        |
 
663
;;                                |        |
 
664
;;                               (9)      (8)
 
665
;;                                 \      /
 
666
;;                                  \    /
 
667
;;                                   (10)      (11)
 
668
;;                                      \      /
 
669
;;                                       \    /
 
670
;;                                        (12)
 
671
;;
 
672
 
 
673
 
 
674
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
 
675
 
 
676
(in-theory 
 
677
 (union-theories (current-theory 'ground-zero)
 
678
                 '((:definition prod)
 
679
                   (:definition natp)
 
680
                   (:definition natp-all)
 
681
                   (:definition posp)           
 
682
                   (:executable-counterpart prod)
 
683
                   (:type-prescription prod)
 
684
                   (:induction prod)
 
685
                   (:executable-counterpart posp)
 
686
                   (:type-prescription posp)
 
687
                   (:definition posp-all)       
 
688
                   (:executable-counterpart posp-all)
 
689
                   (:type-prescription posp-all)
 
690
                   (:induction posp-all)
 
691
                   (:definition divided-by-all) 
 
692
                   (:executable-counterpart divided-by-all)
 
693
                   (:type-prescription divided-by-all)
 
694
                   (:induction divided-by-all) )))
 
695
 
 
696
 
 
697
 
 
698
(defun congruent-mod (x y m)
 
699
  (= (mod x m) (mod y m)))
 
700
 
 
701
 
 
702
 
 
703
(defun congruent-all-mod (x a m)
 
704
  (declare (xargs :measure (len m)))
 
705
  (if (endp m)
 
706
      t
 
707
    (and (congruent-mod x (car a) (car m))
 
708
         (congruent-all-mod x (cdr a) (cdr m)))))
 
709
 
 
710
 
 
711
(defun congruent-all-mod-list (l1 l2 m)
 
712
  (declare (xargs :measure (len m)))
 
713
  (if (endp m)
 
714
      t
 
715
    (and
 
716
     (congruent-mod (car l1) (car l2) (car m))
 
717
     (congruent-all-mod-list (cdr l1) (cdr l2) (cdr m)))))
 
718
 
 
719
 
 
720
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
721
;;
 
722
;; We load some books, importing only some key lemmas about
 
723
;; the combination of mod and arithmetic functions.
 
724
;; We prove some additional basic lemmas.
 
725
;;
 
726
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
727
 
 
728
(include-book "../../../../../arithmetic/top-with-meta")
 
729
 
 
730
(include-book "Minimal-Mod-Lemmas")
 
731
 
 
732
(in-theory (disable mod-x-y-=-x-exp))
 
733
 
 
734
(in-theory (disable mod))
 
735
 
 
736
(defthm r-mod-mod
 
737
  (implies
 
738
   (and
 
739
    (integerp x)
 
740
    (integerp z)
 
741
    (integerp i)
 
742
    (> i 0)
 
743
    (> z 0))
 
744
   (equal (mod (mod x (* i z)) z)
 
745
          (mod x z)))
 
746
  :hints (("Goal" :use (:instance rewrite-mod-mod-exp (y (* i z))))))
 
747
 
 
748
(defthm r-mod-mod-cancel
 
749
 (implies
 
750
   (and
 
751
    (integerp x)
 
752
    (integerp z)
 
753
    (> z 0))
 
754
   (equal (mod (mod x z) z) (mod x z))))
 
755
 
 
756
 
 
757
 
 
758
(defthm product-divided-by-all
 
759
 (implies 
 
760
  (posp-all m)
 
761
  (divided-by-all (prod m) m))
 
762
 :hints (("Subgoal *1/1.2''"
 
763
          :induct t)
 
764
         ("Goal" 
 
765
          :in-theory (disable commutativity-of-*)
 
766
          :induct (len m))))
 
767
 
 
768
 
 
769
 
 
770
(defthm prod-is-pos
 
771
 (implies
 
772
  (posp-all m)
 
773
  (posp (prod m))))
 
774
 
 
775
 
 
776
 
 
777
 
 
778
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
779
;;
 
780
;; Here we prove that, if two values v1 and v2 differ by the product 
 
781
;; of a list of coprimes m, then lists congruent to them are congruent w.r.t. m.
 
782
;; This is stated by if-values-differ-by-product-of-m-then-cong-lists-are-congruent-wrt-m.
 
783
;;
 
784
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
785
 
 
786
(defthm if-k-is-divided-by-all-then-x-and-x-mod-k-have-same-congruence
 
787
 (implies
 
788
  (and
 
789
   (equal (len y) (len m))
 
790
   (integerp x)
 
791
   (posp k)
 
792
   (posp-all m)
 
793
   (divided-by-all k m))
 
794
  (equal
 
795
   (congruent-all-mod (mod x k) y m)
 
796
   (congruent-all-mod x y m))))
 
797
 
 
798
 
 
799
(defthm modulo-prod-has-same-congruence
 
800
 (implies
 
801
  (and
 
802
   (equal (len y) (len m))
 
803
   (integerp x)
 
804
   (posp-all m))
 
805
  (equal
 
806
   (congruent-all-mod (mod x (prod m)) y m)
 
807
   (congruent-all-mod x y m))))
 
808
 
 
809
 
 
810
 
 
811
 
 
812
(defthm express-mod-changing-arg-sign
 
813
  (implies 
 
814
   (and 
 
815
    (integerp x)
 
816
    (integerp y)
 
817
    (not (integerp (/ x y)))) 
 
818
   (equal (mod (- x) y) (- y (mod x y))))
 
819
  :hints (("Goal" :in-theory (enable mod)))
 
820
  :rule-classes nil)
 
821
 
 
822
(defthm mod-0-allows-changing-arg-sign
 
823
  (implies 
 
824
   (and 
 
825
    (integerp x) 
 
826
    (integerp y) 
 
827
    (not (equal y 0))
 
828
    (integerp (/ x y)))
 
829
   (and
 
830
    (equal (mod x y) 0)
 
831
    (equal (mod (- x) y) 0)))
 
832
  :rule-classes nil)
 
833
 
 
834
 
 
835
 
 
836
 
 
837
 
 
838
(defthm hack-24
 
839
  (implies
 
840
   (and (integerp x)
 
841
        (integerp y)
 
842
        (integerp z)
 
843
        (not (integerp (/ y z)))
 
844
        (not (equal z 0)))
 
845
   (equal (mod (- x y) z)
 
846
          (mod (- (mod x z) (mod y z)) z)))
 
847
  :hints (("Goal"
 
848
         :use ( 
 
849
                 (:instance mod-+-exp (y (- y)))
 
850
                 (:instance express-mod-changing-arg-sign (x y) (y z))
 
851
                 (:instance cancel-mod-+-exp 
 
852
                            (i (/ z z))
 
853
                            (x z)
 
854
                            (y (- (mod x z) (mod y z))))
 
855
                 (:instance integerp-mod-exp (i x) (j z))
 
856
                 (:instance integerp-mod-exp (i y) (j z)) )
 
857
         :in-theory '(
 
858
                      (:rewrite inverse-of-*)
 
859
                      (:rewrite associativity-of-+)
 
860
                      (:rewrite commutativity-of-+))))
 
861
  :rule-classes nil)
 
862
 
 
863
 
 
864
(defthm hack-25
 
865
  (implies
 
866
   (and (integerp x)
 
867
        (integerp y)
 
868
        (integerp z)
 
869
        (integerp (/ y z))
 
870
        (not (equal z 0)))
 
871
   (equal (mod (- x y) z)
 
872
          (mod (- (mod x z) (mod y z)) z)))
 
873
  :hints (("Goal" :in-theory (enable mod)))
 
874
  :rule-classes nil)
 
875
 
 
876
(defthm mod--
 
877
  (implies
 
878
   (and (force (integerp x))
 
879
        (force (integerp y))
 
880
        (force (integerp z))
 
881
        (force (not (equal z 0))))
 
882
   (equal (mod (- x y) z)
 
883
          (mod (- (mod x z) (mod y z)) z)))
 
884
  :hints (("Goal" :use (hack-24 hack-25))))
 
885
 
 
886
 
 
887
 
 
888
(defthm cong-all-mod-implies-cong-all-mod-list 
 
889
 (implies
 
890
  (and
 
891
   (congruent-all-mod v1 l1 m)
 
892
   (congruent-all-mod v1 l2 m))
 
893
  (congruent-all-mod-list l1 l2 m)))
 
894
 
 
895
 
 
896
(defthm hack-26
 
897
 (implies 
 
898
  (rel-prime-moduli m)
 
899
  (and
 
900
   (posp-all m)
 
901
   (posp (prod m))))
 
902
 :hints (("Goal" :in-theory (enable rel-prime-moduli)))
 
903
 :rule-classes :forward-chaining)
 
904
 
 
905
 
 
906
(defthm hack-27
 
907
 (implies
 
908
  (integerp (/ a b))
 
909
  (integerp (/ (- a) b)))
 
910
 :rule-classes nil)
 
911
 
 
912
 
 
913
(defthm hack-28
 
914
  (implies
 
915
   (and
 
916
    (integerp v1)
 
917
    (integerp v2)
 
918
    (posp (prod m))
 
919
    (integerp (/ (- v1 v2) (prod m))))
 
920
   (and
 
921
    (integerp (/ (- v2 v1) (prod m)))
 
922
    (equal  v2 (+ v1 (* (/ (- v2 v1) (prod m)) (prod m))))))
 
923
  :hints (("Goal" :use (:instance hack-27 (a (- v1 v2)) (b (prod m)))))
 
924
  :rule-classes nil)
 
925
 
 
926
 
 
927
(defthm if-values-differ-by-product-of-m-then-cong-lists-are-congruent-wrt-m
 
928
  (implies
 
929
   (and
 
930
    (rel-prime-moduli m)
 
931
    (integerp v1)
 
932
    (integerp v2)
 
933
    (natp-all l1)
 
934
    (natp-all l2)
 
935
    (equal (len l1) (len m))
 
936
    (equal (len l2) (len m))
 
937
    (congruent-all-mod v1 l1 m)
 
938
    (congruent-all-mod v2 l2 m)
 
939
    (integerp (/ (- v1 v2) (prod m))))
 
940
   (congruent-all-mod-list l1 l2 m))
 
941
  :hints (("Goal" 
 
942
           :in-theory '((:definition posp) 
 
943
                        (:rewrite unicity-of-1))
 
944
           :use 
 
945
           ( hack-28
 
946
             hack-26
 
947
             cong-all-mod-implies-cong-all-mod-list
 
948
             (:instance mod-x+i*y-y-exp (i (/ (- v2 v1) (prod m))) (x v1) (y (prod m)))
 
949
             (:instance r-mod-mod (x v1) (i 1) (z (prod m)))
 
950
             (:instance modulo-prod-has-same-congruence (x v1) (y l2))
 
951
             (:instance modulo-prod-has-same-congruence (x v2) (y l2))))))
 
952
 
 
953
 
 
954
 
 
955
 
 
956
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
957
;;
 
958
;; Now we prove that, given two values v1 and v2, if lists congruent to 
 
959
;; them are congruent w.r.t. m, then v1 and v2 differ by the product 
 
960
;; of the elements of m.
 
961
;;
 
962
;; This is stated by 
 
963
;; if-values-are-congruent-wrt-m-via-cong-lists-then-they-differ-by-a-multiple-of-prod-m.
 
964
;;
 
965
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
966
 
 
967
 
 
968
 
 
969
(defthm same-congruence-over-conglist
 
970
 (implies
 
971
  (congruent-all-mod-list l1 l2 m)
 
972
 (equal
 
973
    (congruent-all-mod v l1 m)
 
974
    (congruent-all-mod v l2 m)))
 
975
 :rule-classes nil)
 
976
 
 
977
(defun cong-sg-val (v1 v2 m)
 
978
  (if
 
979
      (endp m)
 
980
      t
 
981
    (and
 
982
     (congruent-mod v1 v2 (car m))
 
983
     (cong-sg-val   v1 v2 (cdr m)))))
 
984
 
 
985
 
 
986
(defthm same-cong-lists-means-same-mods
 
987
 (implies
 
988
  (and
 
989
   (equal (len l) (len m))
 
990
   (congruent-all-mod v1 l m)
 
991
   (congruent-all-mod v2 l m))
 
992
  (cong-sg-val v1 v2 m)))
 
993
 
 
994
(defthm mod-of-0
 
995
 (implies (posp carm) (equal (mod 0 carm) 0))
 
996
 :rule-classes nil)
 
997
 
 
998
 
 
999
(defthm same-cong-vals-implies-diff-has-cong-to-zero
 
1000
 (implies
 
1001
  (and
 
1002
   (posp-all m)
 
1003
   (integerp v1)
 
1004
   (integerp v2))
 
1005
   (implies
 
1006
    (cong-sg-val v1 v2 m)
 
1007
    (cong-sg-val (- v1 v2) 0 m)))
 
1008
 :hints (("Goal" 
 
1009
          :in-theory (disable mod-=-0-exp 
 
1010
                              mod-- 
 
1011
                              mod-+-exp 
 
1012
                              cancel-mod-+-exp 
 
1013
                              rewrite-mod-mod-exp 
 
1014
                              r-mod-mod-cancel 
 
1015
                              integerp-mod-exp)
 
1016
          :induct (len m))
 
1017
         ("Subgoal *1/1" :use  (
 
1018
                                (:instance mod-of-0 (carm (car m)))
 
1019
                                (:instance mod-- (x v1) (y v2) (z (car m)))))))
 
1020
 
 
1021
 
 
1022
(defthm cong-0-is-divided-by-all
 
1023
 (implies
 
1024
  (and
 
1025
   (integerp v)
 
1026
   (posp-all m))
 
1027
  (equal (cong-sg-val v 0 m) (divided-by-all v m)))
 
1028
 :hints (("Goal" :induct (len m))
 
1029
         ("Subgoal *1/1" :use ((:instance mod-of-0 (carm (car m)))
 
1030
                               (:instance mod-=-0-exp (x v) (y (car m))))
 
1031
                         :in-theory (disable MOD-=-0-EXP)))
 
1032
 :rule-classes nil)
 
1033
 
 
1034
 
 
1035
 
 
1036
 
 
1037
(in-theory (enable if-every-coprime-divides-v-then-product-of-coprimes-divides-v))
 
1038
 
 
1039
 
 
1040
 
 
1041
 
 
1042
(defthm if-values-are-congruent-wrt-m-via-cong-lists-then-they-differ-by-a-multiple-of-prod-m
 
1043
  (implies
 
1044
   (and
 
1045
    (rel-prime-moduli m)
 
1046
    (integerp v1)
 
1047
    (integerp v2)
 
1048
    (natp-all l1)
 
1049
    (natp-all l2)
 
1050
    (equal (len l1) (len m))
 
1051
    (equal (len l2) (len m))
 
1052
    (congruent-all-mod v1 l1 m)
 
1053
    (congruent-all-mod v2 l2 m)
 
1054
    (congruent-all-mod-list l1 l2 m))
 
1055
  (integerp (/ (- v1 v2) (prod m))))
 
1056
  :hints (("Goal" :use ( hack-26
 
1057
                         (:instance cong-0-is-divided-by-all (v (- v1 v2)))
 
1058
                         (:instance same-congruence-over-conglist (v v2))
 
1059
                         (:instance same-cong-vals-implies-diff-has-cong-to-zero (v1 v1) (v2 v2))
 
1060
                         (:instance if-every-coprime-divides-v-then-product-of-coprimes-divides-v 
 
1061
                                    (v (- v1 v2)))))))
 
1062
 
 
1063
 
 
1064
 
 
1065
 
 
1066
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1067
;;
 
1068
;; We prove that congruence w.r.t. m is equivalent to checking that the difference
 
1069
;; of two values is a multiple of the product of the elements of l.
 
1070
;; This follows easily from the ``if'' and ``only if'' lemmas proved above.
 
1071
;;
 
1072
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1073
 
 
1074
 
 
1075
(defthm congruence-of-cong-lists-is-equivalent-to-dividabilty-by-prod-m
 
1076
  (implies
 
1077
   (and
 
1078
    (rel-prime-moduli m)
 
1079
    (integerp v1)
 
1080
    (integerp v2)
 
1081
    (natp-all l1)
 
1082
    (natp-all l2)
 
1083
    (equal (len l1) (len m))
 
1084
    (equal (len l2) (len m))
 
1085
    (congruent-all-mod v1 l1 m)
 
1086
    (congruent-all-mod v2 l2 m))
 
1087
   (equal
 
1088
    (congruent-all-mod-list l1 l2 m) 
 
1089
    (integerp (/ (- v1 v2) (prod m)))))
 
1090
  :hints (("Goal" 
 
1091
           :use (if-values-differ-by-product-of-m-then-cong-lists-are-congruent-wrt-m 
 
1092
                 if-values-are-congruent-wrt-m-via-cong-lists-then-they-differ-by-a-multiple-of-prod-m))))
 
1093
 
 
1094
 
 
1095
 
 
1096
 
 
1097
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1098
;;
 
1099
;; Here we prove a basic lemma: if two numbers differ by a multiple of a fixed number prod,
 
1100
;; and they both are in the range [0,prod), then they are equal.
 
1101
;;
 
1102
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1103
 
 
1104
(defthm hack-29
 
1105
 (implies
 
1106
  (and
 
1107
   (posp prod)
 
1108
   (integerp resdiv))
 
1109
  (and
 
1110
   (implies (equal resdiv 0) (equal (* resdiv prod) 0))
 
1111
   (implies (< resdiv 0)     (<     (* resdiv prod) 0))
 
1112
   (implies (> resdiv 0)     (>=    (* resdiv prod) prod)))))
 
1113
   
 
1114
 
 
1115
(defthm hack-30
 
1116
 (implies
 
1117
  (and
 
1118
    (natp v)
 
1119
    (posp prod)
 
1120
    (< v prod)
 
1121
    (integerp (/ v prod)))
 
1122
  (equal v 0))
 
1123
 :hints (("Goal''" :use (:instance hack-29 (resdiv (/ v prod)))))
 
1124
 :rule-classes nil)
 
1125
 
 
1126
 
 
1127
(defthm hack-31
 
1128
 (implies
 
1129
  (and
 
1130
    (posp prod)
 
1131
    (natp v1)
 
1132
    (natp v2)
 
1133
    (< v1 prod)
 
1134
    (< v2 prod)
 
1135
    (integerp (/ (abs (- v1 v2)) prod)))
 
1136
  (equal v1 v2))
 
1137
 :hints (("Goal" :use (:instance hack-30 (v (abs (- v1 v2))))))
 
1138
 :rule-classes nil)
 
1139
 
 
1140
 
 
1141
(defthm hack-32
 
1142
  (iff (integerp (/ (abs a) b)) (integerp (/ a b)))
 
1143
  :rule-classes nil)
 
1144
 
 
1145
(defthm equality-in-range
 
1146
 (implies
 
1147
  (and
 
1148
    (posp prod)
 
1149
    (natp v1)
 
1150
    (natp v2)
 
1151
    (< v1 prod)
 
1152
    (< v2 prod)
 
1153
    (integerp (/ (- v1 v2) prod)))
 
1154
  (equal v1 v2))
 
1155
 :hints (("Goal" :use (hack-31
 
1156
                       (:instance hack-32 (a (- v1 v2)) (b prod)))))
 
1157
 :rule-classes nil)
 
1158
 
 
1159
 
 
1160
 
 
1161
 
 
1162
 
 
1163
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1164
;;
 
1165
;; Required statement
 
1166
;;
 
1167
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1168
 
 
1169
 
 
1170
 
 
1171
(defthm unique-inversion
 
1172
  (implies
 
1173
   (and
 
1174
    (rel-prime-moduli m)
 
1175
    (natp v1)
 
1176
    (natp v2)
 
1177
    (< v1 (prod m))
 
1178
    (< v2 (prod m))
 
1179
    (natp-all l)
 
1180
    (equal (len l) (len m))
 
1181
    (congruent-all-mod v1 l m)
 
1182
    (congruent-all-mod v2 l m))
 
1183
   (equal v1 v2))
 
1184
  :hints (("Goal" :use
 
1185
           ( (:instance congruence-of-cong-lists-is-equivalent-to-dividabilty-by-prod-m (l1 l) (l2 l))
 
1186
             (:instance equality-in-range (prod (prod m))))))
 
1187
  :rule-classes nil)
 
1188
 
 
1189
 
 
1190
 
 
1191
 
 
1192