← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/arithmetic/arith2.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/arithmetic/arith2.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#|
 
4
This book contains a hodgepodge of useful arithmetic rules.
 
5
It's still kind of a mess.  But it's better now that we have the rules in common-factor.lisp.
 
6
 
 
7
|#
 
8
 
 
9
(include-book "fp2")
 
10
(include-book "predicate")
 
11
(include-book "product")
 
12
(include-book "../../../meta/meta-times-equal")
 
13
(include-book "../../../meta/meta-plus-equal")
 
14
(include-book "../../../meta/meta-plus-lessp")
 
15
 
 
16
 
 
17
;get more rules from arithmetic-2 ?
 
18
 
 
19
 
 
20
 
 
21
 
 
22
;;=================================================================================
 
23
;; Collect leading constants in comparisons.
 
24
;; This section is complete.  [what about products??]
 
25
;;===================================================================================
 
26
 
 
27
(defthm collect-constants-in-equal-of-sums
 
28
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
 
29
                (case-split (acl2-numberp c1))
 
30
                )
 
31
           (and (equal (equal (+ c2 x) c1)
 
32
                       (equal (fix x) (- c1 c2)))
 
33
                (equal (equal c1 (+ c2 x))
 
34
                       (equal (fix x) (- c1 c2))))))
 
35
 
 
36
(defthm collect-constants-in-equal-of-sums-2
 
37
  (implies (syntaxp (and (quotep c1) (quotep c2)))
 
38
           (and (equal (equal (+ c2 x) (+ c1 y))
 
39
                       (equal (fix x) (+ (- c1 c2) y))))))
 
40
 
 
41
(defthm collect-constants-in-<-of-sums
 
42
  (implies (syntaxp (and (quotep c1) (quotep c2)))
 
43
           (and (equal (< (+ c2 x) c1)
 
44
                       (< x (- c1 c2)))
 
45
                (equal (< c1 (+ c2 x))
 
46
                       (< (- c1 c2) x)))))
 
47
 
 
48
(defthm collect-constants-in-<-of-sums-2
 
49
  (implies (syntaxp (and (quotep c1) (quotep c2)))
 
50
           (equal (< (+ c2 x) (+ c1 y))
 
51
                  (< x (+ (- c1 c2) y)))))
 
52
 
 
53
 
 
54
;this book includes (how many?) main types of lemmas
 
55
 
 
56
;there's stuff in inverted-factor too
 
57
 
 
58
 
 
59
;collecting constants
 
60
; equal with sums
 
61
; < with sums
 
62
; < with products
 
63
; equal with products
 
64
 
 
65
;rearranging negative coeffs
 
66
;getting rid of fractional coeffs
 
67
 
 
68
;cancelling factors in comparisons of sums (these sums may each have only 1 addend)
 
69
 
 
70
;misc lemmas (comparing products to 0)
 
71
 
 
72
;see equal-constant-+ in equalities.lisp
 
73
 
 
74
;see also see MULT-BOTH-SIDES-OF-EQUAL
 
75
(defthmd mult-both-sides-of-<-by-positive
 
76
  (implies (and (<= 0 c)
 
77
                (rationalp c)
 
78
                (case-split (< 0 c))
 
79
                )
 
80
           (equal (< (* c a) (* c b))
 
81
                  (< a b))))
 
82
 
 
83
 
 
84
(include-book "../../../meta/meta-times-equal")
 
85
(include-book "../../../meta/meta-plus-equal")
 
86
(include-book "../../../meta/meta-plus-lessp")
 
87
 
 
88
 
 
89
(defthm mult-both-sides-of-equal
 
90
  (implies (and (case-split (acl2-numberp a))
 
91
                (case-split (acl2-numberp b))
 
92
                (case-split (acl2-numberp c))
 
93
                )
 
94
           (equal (equal (* a c) (* b c)) 
 
95
                  (if (equal c 0)
 
96
                      t
 
97
                    (equal a b))))
 
98
  :rule-classes nil)
 
99
 
 
100
 
 
101
 
 
102
#|
 
103
 
 
104
;instead of these, we should just cancel common factors from the constants
 
105
 
 
106
;open question: how to handle (equal (* 2 x) (* 3 y)) -- should we collect the constants or not? 
 
107
;maybe so, since doing so would let us substitue for one of the vars (x or y).
 
108
 
 
109
;don't yet handle negative constants
 
110
;prefers that quotient of the constants be > 1  -perhaps we want the quotient to be < 1???
 
111
;maybe the constant should be by itself?
 
112
(defthm collect-constants-in-product-<-1-of-2-with-1-of-2
 
113
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
 
114
                (rationalp c1)
 
115
                (rationalp c2)
 
116
                (< 0 c1) ;gen
 
117
                (< 0 c2) ;gen
 
118
                (rationalp a)
 
119
                (rationalp b))
 
120
           (equal (< (* c1 a) (* c2 b))
 
121
                  (if (> c1 c2)
 
122
                      (< (* (/ c1 c2) a) b)
 
123
                    (< a (* (/ c2 c1) b)))))
 
124
  :hints (("Goal" :use ((:instance mult-both-sides-of-<-by-positive 
 
125
                                   (a (* c1 a))
 
126
                                   (b (* c2 b))
 
127
                                   (c (/ c1)))
 
128
                        (:instance mult-both-sides-of-<-by-positive 
 
129
                                   (a (* c1 a))
 
130
                                   (b (* c2 b))
 
131
                                   (c (/ c2)))))))
 
132
 
 
133
(defthm collect-constants-in-product-<-1-of-1-with-1-of-2
 
134
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
 
135
                (rationalp c1)
 
136
                (rationalp c2)
 
137
                (< 0 c1) ;gen
 
138
                (< 0 c2) ;gen
 
139
                (rationalp b))
 
140
           (equal (< c1 (* c2 b))
 
141
                  (< (/ c1 c2) b)))
 
142
  :hints (("Goal" :use ((:instance mult-both-sides-of-<-by-positive 
 
143
                                   (a c1)
 
144
                                   (b (* c2 b))
 
145
                                   (c (/ c2)))))))
 
146
 
 
147
(defthm collect-constants-in-product-<-1-of-2-with-1-of-1
 
148
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
 
149
                (rationalp c1)
 
150
                (rationalp c2)
 
151
                (< 0 c1) ;gen
 
152
                (< 0 c2) ;gen
 
153
                (rationalp b))
 
154
           (equal (< (* c2 b) c1)
 
155
                  (< b (/ c1 c2))))
 
156
  :hints (("Goal" :use ((:instance mult-both-sides-of-<-by-positive 
 
157
                                   (b c1)
 
158
                                   (a (* c2 b))
 
159
                                   (c (/ c2)))))))
 
160
 
 
161
 
 
162
|#
 
163
 
 
164
 
 
165
 
 
166
;generalize to acl2-numberp whenever possible
 
167
;make more like these!
 
168
 
 
169
;BOZO generalize this hack
 
170
;drop?
 
171
;is this like rearrange-negative coeffs?
 
172
(defthm rearr-neg-eric
 
173
  (implies (and (rationalp a)
 
174
                (rationalp b)
 
175
                (rationalp c)
 
176
                (rationalp d))
 
177
           (equal (EQUAL (+ a (* -1 b) c)
 
178
                         d)
 
179
                  (equal (+ a c) (+ b d)))))
 
180
 
 
181
;add "equal" to the name?
 
182
;more like this?
 
183
;BOZO bad name...
 
184
(defthm collect-constants-with-division
 
185
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
 
186
                (rationalp c2)
 
187
                (acl2-numberp c1)
 
188
                (not (equal c2 0))
 
189
                (rationalp x))
 
190
           (equal (equal c1 (* c2 x))
 
191
                  (equal (/ c1 c2) x))))
 
192
 
 
193
 
 
194
;; ==================================================================================================
 
195
;;
 
196
;;;comparing a product to 0
 
197
 
 
198
;; may cause case splits (which, for my purposes, is acceptable)
 
199
 
 
200
;; ==================================================================================================
 
201
 
 
202
 
 
203
 
 
204
#|
 
205
;BOZO I have more rules about this in product.lisp !!!
 
206
 
 
207
;case split on the sign of A
 
208
(defthm prod->-0-cancel-pos
 
209
  (implies (and (< 0 a)
 
210
                (rationalp x)
 
211
                (rationalp a)
 
212
                )
 
213
           (equal (< 0 (* a x))
 
214
                  (< 0 x))))
 
215
 
 
216
(defthm prod-<-0-cancel-pos
 
217
  (implies (and (< 0 a)
 
218
                (rationalp x)
 
219
                (rationalp a)
 
220
                )
 
221
           (equal (< (* a x) 0)
 
222
                  (< x 0))))
 
223
 
 
224
 
 
225
(defthm prod-<-0-cancel-neg
 
226
  (implies (and (< a 0)
 
227
                (rationalp x)
 
228
                (rationalp a)
 
229
                )
 
230
           (equal (< (* a x) 0)
 
231
                  (< 0 x))))
 
232
 
 
233
(defthm prod->-0-cancel-neg
 
234
  (implies (and (< a 0)
 
235
                (rationalp x)
 
236
                (rationalp a)
 
237
                )
 
238
           (equal (< 0 (* a x))
 
239
                  (< x 0))))
 
240
 
 
241
 
 
242
;reorder to make the most likely case of the if first?
 
243
(defthm prod->-0-cancel
 
244
  (implies (and (rationalp x)
 
245
                (rationalp a))
 
246
           (equal (< 0 (* a x))
 
247
                  (if (< 0 a)
 
248
                      (< 0 x)
 
249
                    (if (equal 0 a)
 
250
                        nil
 
251
                      (< x 0))))))
 
252
 
 
253
 
 
254
(defthm prod-<-0-cancel
 
255
  (implies (and (rationalp x)
 
256
                (rationalp a))
 
257
           (equal (< (* a x) 0)
 
258
                  (if (equal a 0)
 
259
                      nil
 
260
                    (if (< a 0)
 
261
                        (< 0 x)
 
262
                      (< x 0))))))
 
263
 
 
264
 
 
265
(in-theory (disable prod-<-0-cancel-neg 
 
266
                    prod-<-0-cancel-pos
 
267
                    prod->-0-cancel-neg  
 
268
                    prod->-0-cancel-pos))
 
269
 
 
270
 
 
271
|#
 
272
 
 
273
 
 
274
(defthmd cancel-in-prods-<-case-x->-0
 
275
  (implies (and (rationalp x)
 
276
                (< 0 x)
 
277
                (rationalp a)
 
278
                (rationalp b))
 
279
           (equal  (< (* x a) (* x b))
 
280
                   (< a b)))
 
281
  )
 
282
 
 
283
(defthmd cancel-in-prods-<-case-x-<-0
 
284
  (implies (and (rationalp x)
 
285
                (> 0 x)
 
286
                (rationalp a)
 
287
                (rationalp b))
 
288
           (equal  (< (* x a) (* x b))
 
289
                   (> a b)))
 
290
  )
 
291
 
 
292
;changed the var names 'cause "x" was too heavy
 
293
;disabled, since we have a bind-free rule to cancel
 
294
(defthmd cancel-in-prods-<
 
295
  (implies (and (rationalp a)
 
296
                (rationalp b)
 
297
                (rationalp c))
 
298
           (equal (< (* a b) (* a c))
 
299
                  (if (equal 0 a)
 
300
                      nil
 
301
                    (if (> a 0)
 
302
                        (< b c)
 
303
                      (> b c)))))
 
304
  :hints (("Goal" :in-theory (enable  cancel-in-prods-<-case-x-<-0
 
305
                                      cancel-in-prods-<-case-x->-0)))
 
306
  )
 
307
 
 
308
 
 
309
 
 
310
;it shouldn't be too hard to write a bind-free function for cancelling common factors; that rule could replace
 
311
;many of the cancelling rules below
 
312
 
 
313
 
 
314
;use negative-syntaxp? (or a version of it that operates on single addends only (i.e., has no '+ case)
 
315
;do we need this?
 
316
(defthmd move-a-negative-coeff
 
317
  (equal (< (+ a (* -1 b)) c)
 
318
         (< a (+ b c))))
 
319
  
 
320
;can simplify the *-1 term to have only one var 
 
321
;do we need this?
 
322
(defthm rearr-negative-coeffs-<-sums-blah
 
323
  (equal (< (+ A e (* -1 C)) B)
 
324
         (< (+ A e) (+ (* C) B)))
 
325
  :hints (("Goal" :use (:instance
 
326
                        move-a-negative-coeff (a (+ a e)) (b (* c)) (c b)))))
 
327
 
 
328
(defthm collect-constant-mults-<-1-of-2-with-1-of-2-term-len-2
 
329
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
 
330
                (rationalp c1)
 
331
                (rationalp c2)
 
332
                (rationalp a)
 
333
                (rationalp b)
 
334
                (rationalp c)
 
335
                (rationalp d))
 
336
           (equal (< (+ (* c1 c d) a) (+ (* c2 c d) b))
 
337
                  (< (+ (* (- c1 c2) c d) a) b))))
 
338
 
 
339
 
 
340
(include-book "inverted-factor")
 
341
 
 
342
 
 
343
;events in :rule-classes nil which can be :used in hacks
 
344
 
 
345
(defthm <-transitive
 
346
  (implies (and (< a b)
 
347
                (< b c)
 
348
                )
 
349
           (< a c)
 
350
           )
 
351
  :rule-classes nil
 
352
  )
 
353
 
 
354
(defthm <=-transitive
 
355
  (implies (and (<= a b)
 
356
                (<= b c)
 
357
                )
 
358
           (<= a c)
 
359
           )
 
360
  :rule-classes nil
 
361
  )
 
362
 
 
363
;a<b and b<=c together imply a<c
 
364
(defthm <-and-<=-transitivity
 
365
  (implies (and (< a b) 
 
366
                (<= b c)        
 
367
                )
 
368
           (< a c)
 
369
           )
 
370
  :rule-classes nil
 
371
  )
 
372
 
 
373
;a<=b and b<c together imply a<c
 
374
(defthm <=-and-<-transitivity
 
375
  (implies (and (< a b) 
 
376
                (<= b c)        
 
377
                )
 
378
           (< a c)
 
379
           )
 
380
  :rule-classes nil
 
381
  )
 
382
 
 
383
 
 
384
;used only as a hack:
 
385
 
 
386
 
 
387
(defthm equal-transitive
 
388
  (implies (and (equal a b)
 
389
                (equal b c))
 
390
           (equal a c))
 
391
  :rule-classes nil)
 
392
 
 
393
;there's a conflict in my arithmetic normal forms:
 
394
; do we prefer (< (* 2 x) 1) or (< x 1/2) ?
 
395
 
 
396
 
 
397
(defthm collect-again
 
398
  (implies (and (syntaxp (quotep k))
 
399
                (rationalp x)
 
400
                (rationalp y))
 
401
           (equal (< (+ x y) (* k x))
 
402
                  (< y (* (- k 1) x)))))
 
403
 
 
404
 
 
405
 
 
406
;natp is defined here to try to make sure its always enabled
 
407
 
 
408
(defun natp (x)
 
409
  (declare (xargs :guard t))
 
410
  (and (integerp x)
 
411
       (<= 0 x)))
 
412
 
 
413
(in-theory (enable natp))
 
414
 
 
415
;an odd rule
 
416
(defthm two-natps-add-to-1
 
417
  (implies (and (natp n)
 
418
                (natp x))
 
419
           (equal (equal 1 (+ x n))
 
420
                  (or (and (equal x 1) (equal n 0))
 
421
                      (and (equal x 0) (equal n 1))))))
 
422
 
 
423
;backchain-limit?
 
424
;why needed?
 
425
(defthm nonneg-+
 
426
  (implies (and (<= 0 x)
 
427
                (<= 0 y))
 
428
           (not (< (+ x y) 0))))
 
429
 
 
430
;improve this? make the conclusion more type-like?
 
431
(defthm nonneg-+-type
 
432
  (implies (and (<= 0 x)
 
433
                (<= 0 y))
 
434
           (not (< (+ x y) 0)))
 
435
  :rule-classes (:type-prescription))
 
436
 
 
437
(defthm move-negative-constant-1
 
438
  (implies (and (syntaxp (and (quotep k) (< (cadr k) 0)))
 
439
                (acl2-numberp x)
 
440
                (acl2-numberp y))
 
441
           (equal (equal x (+ k y))
 
442
                  (equal (+ x (- k)) y))))
 
443
;move?
 
444
(defthm rationalp-sum
 
445
  (implies (rationalp k)
 
446
           (and (equal (rationalp (+ k x))
 
447
                       (not (complex-rationalp x)))
 
448
                (equal (rationalp (+ x k))
 
449
                       (not (complex-rationalp x))))))
 
450
 
 
451
;move?
 
452
;make rationalp-sum like this?
 
453
(defthm rationalp-prod
 
454
  (implies (and (rationalp k)
 
455
                (case-split (not (equal k 0)))
 
456
                )
 
457
           (and (equal (rationalp (* k x))
 
458
                       (not (complex-rationalp x)))
 
459
                (equal (rationalp (* x k))
 
460
                       (not (complex-rationalp x))))))
 
461
;move?
 
462
(defthm complex-rationalp-prod
 
463
  (implies (and (rationalp k)
 
464
                (case-split (not (equal k 0)))
 
465
                )
 
466
           (and (equal (complex-rationalp (* k x))
 
467
                       (complex-rationalp x))
 
468
                (equal (complex-rationalp (* x k))
 
469
                       (complex-rationalp x)))))
 
470
 
 
471
 
 
472
 
 
473
(defthm collect-1
 
474
  (implies (and (syntaxp (and (quotep k) (quotep j)))
 
475
                (rationalp k)
 
476
                (rationalp j)
 
477
                (rationalp x)
 
478
                (rationalp y)
 
479
                )
 
480
           (equal (< (+ y (* k x)) (* j x))
 
481
                  (< (+ (* (- k j) x) y) 0))))
 
482
 
 
483
(defthm collect-2
 
484
  (implies (and (syntaxp (and (quotep k) (quotep j)))
 
485
                (rationalp k)
 
486
                (rationalp j)
 
487
                (rationalp x)
 
488
                (rationalp y)
 
489
                )
 
490
           (equal (< (+ (* k x) y) (* j x))
 
491
                  (< (+ (* (- k j) x) y) 0))))
 
492
 
 
493
(defthm collect-another
 
494
  (implies (and (syntaxp (and (quotep k) (quotep j)))
 
495
                (rationalp k)
 
496
                (rationalp j)
 
497
                (rationalp x)
 
498
                (rationalp y)
 
499
                (rationalp z))
 
500
           (equal (< (+ (* k x) y) (+ (* j x) z))
 
501
                  (< (+ (* (- k j) x) y) z))))
 
502
 
 
503
 
 
504
;simplify this
 
505
(defthm collect-in-<-of-sums-2
 
506
  (implies (syntaxp (and (quotep k) (quotep j)))
 
507
           (equal (< (+ a (* k x) d) (+ b e (* j       x) f))
 
508
                  (< (+ a         d) (+ b e (* (- j k) x) f)))))
 
509
 
 
510
(defthm collect-in-<-of-sums-1
 
511
  (implies (syntaxp (and (quotep k) (quotep j)))
 
512
           (equal (< (+ a d (* k x) y) (+ b e f z (* j       x) g))
 
513
                  (< (+ a d         y) (+ b e f z (* (- j k) x) g)))))
 
514
 
 
515
 
 
516
(defthm cancel-in-sum-equal-zero-1
 
517
  (implies (and (rationalp y)
 
518
                (case-split (not (equal 0 y)))
 
519
                (rationalp x1)
 
520
                (rationalp x2)
 
521
                (rationalp x3)
 
522
                (rationalp x4)
 
523
                (rationalp x5)
 
524
                (rationalp x6))
 
525
           (equal (EQUAL 0 (+ (* Y x1)
 
526
                              (* x2 Y x3)
 
527
                              (* Y x4)
 
528
                              (* x5 Y x6)))
 
529
                  (equal 0 (+ x1 (* x2 x3) x4 (* x5 x6)))))
 
530
  :hints (("Goal" :in-theory (disable product-equal-zero)
 
531
           :use (:instance product-equal-zero (x y) (y (+ x1 (* x2 x3) x4 (* x5 x6))))))
 
532
  
 
533
  )
 
534
 
 
535
;expensive?
 
536
(defthm integerp-implies-not-complex-rationalp
 
537
  (implies (integerp x)
 
538
           (not (complex-rationalp x))))
 
539
 
 
540
;don't need this if we have frac-coeff rules?
 
541
;move to unary-/ ?
 
542
(defthm <-of-two-inverses
 
543
  (implies (and (rationalp x)
 
544
                (rationalp y)
 
545
                (< 0 y)
 
546
                (< 0 x)
 
547
                )
 
548
           (equal (< (/ x) (/ y))
 
549
                  (< y x))))
 
550
 
 
551
 
 
552
#|
 
553
;move up?
 
554
(defthm pos*
 
555
  (implies (and (rationalp x)
 
556
                (rationalp y)
 
557
                (> x 0)
 
558
                (> y 0))
 
559
           (> (* x y) 0))
 
560
  :rule-classes ())
 
561
 
 
562
;bad name
 
563
;find a way to make this a rewrite rule wihtout looping?
 
564
(defthm tighten-integer-bound
 
565
  (implies (and (< x (expt 2 i))
 
566
                (integerp x)
 
567
                (case-split (natp i))
 
568
                )
 
569
           (<= x (+ -1 (expt 2 i))))
 
570
  :rule-classes :linear
 
571
  )
 
572
 
 
573
|#