1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
; Arithmetic-5 Library
; Written by Robert Krug
; Copyright/License:
; See the LICENSE file at the top level of the arithmetic-5 library.
;;
;; prefer-times.lisp
;;
;
; This is a small theory of rules that eliminate / from equalites and
; inequalities in favor of *, e.g., x < y/z is rewritten to x*y < z for
; positive z. This theory is compatible with the other theories, i.e.,
; it should not cause looping.
;
; These rules are not included by default bacause it is not clear
; that we should prefer x*y < z to x < y/z, or x*y = z to x = y/z';
; in fact, the whole point of the proofs using these libraries may
; have to do with a representation involving /.
;
; So, unless someone provides a convincing reason to the contrary,
; these rules will remain separate from the rest of the theory.
;
; Note, however, that in certain cases this theory is just the thing that
; needs to be ENABLEd to make the proofs work. Keep it in mind.
;
(in-package "ACL2")
(local (include-book "basic-arithmetic"))
(local (include-book "inequalities"))
(set-default-hints
'((nonlinearp-default-hint-pass1 stable-under-simplificationp
hist pspv)))
(local
(defthm iff-equal
(equal (equal (< w x) (< y z))
(iff (< w x) (< y z)))))
(defthm equal-*-/-1
(equal (equal (* (/ x) y) z)
(if (equal (fix x) 0)
(equal z 0)
(and (acl2-numberp z)
(equal (fix y) (* x z))))))
(defthm equal-*-/-2
(equal (equal (* y (/ x)) z)
(if (equal (fix x) 0)
(equal z 0)
(and (acl2-numberp z)
(equal (fix y) (* z x))))))
(local
(defthm times-one
(implies (acl2-numberp x)
(equal (* 1 x)
x))))
(local
(defthm times-minus-one
(implies (acl2-numberp x)
(equal (* -1 x)
(- x)))))
(local
(in-arithmetic-theory '((:rewrite COMMUTATIVITY-OF-*)
(:REWRITE COMMUTATIVITY-2-OF-*)
(:REWRITE INVERSE-OF-*)
(:REWRITE TIMES-ONE)
(:REWRITE TIMES-MINUS-ONE))))
(defthm normalize-<-/-to-*-1
(implies (and (real/rationalp x)
(real/rationalp y))
(equal (< x (/ y))
(cond ((< y 0) (< 1 (* x y)))
((< 0 y) (< (* x y) 1))
(t (< x 0))))))
(defthm normalize-<-/-to-*-2
(implies (and (real/rationalp x)
(real/rationalp y))
(equal (< (/ y) x)
(cond ((< y 0) (< (* x y) 1))
((< 0 y) (< 1 (* x y)))
(t (< 0 x))))))
(defthm normalize-<-/-to-*-3-1
(implies (and (real/rationalp x)
(real/rationalp y)
(real/rationalp z))
(equal (< x (* y (/ z)))
(cond ((< z 0) (< y (* x z)))
((< 0 z) (< (* x z) y))
(t (< x 0))))))
(defthm normalize-<-/-to-*-3-2
(implies (and (real/rationalp x)
(real/rationalp y)
(real/rationalp z))
(equal (< x (* (/ z) y))
(cond ((< z 0) (< y (* x z)))
((< 0 z) (< (* x z) y))
(t (< x 0))))))
(defthm normalize-<-/-to-*-3-3
(implies (and (real/rationalp x)
(real/rationalp y)
(real/rationalp z))
(equal (< (* y (/ z)) x)
(cond ((< z 0) (< (* x z) y))
((< 0 z) (< y (* x z)))
(t (< 0 x))))))
(defthm normalize-<-/-to-*-3-4
(implies (and (real/rationalp x)
(real/rationalp y)
(real/rationalp z))
(equal (< (* (/ z) y) x)
(cond ((< z 0) (< (* x z) y))
((< 0 z) (< y (* x z)))
(t (< 0 x))))))
(deftheory prefer-*-to-/
'(equal-*-/-1 equal-*-/-2
normalize-<-/-to-*-1 normalize-<-/-to-*-2
normalize-<-/-to-*-3-1 normalize-<-/-to-*-3-2
normalize-<-/-to-*-3-3 normalize-<-/-to-*-3-4))
(in-theory (disable prefer-*-to-/))
|
