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
138
139
140
141
142
143
144
145
146
147
148
149
|
; See the top-level arithmetic-2 LICENSE file for authorship,
; copyright, and license information.
;;
;; 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"))
(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)))))
(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)))))
:hints (("Goal" :use ((:instance <-*-right-cancel
(x x)
(y (/ y))
(z y))
(:instance right-cancellation-for-*
(x x)
(y (/ y))
(z y)))
:in-theory (disable equal-/))))
(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)))))
:hints (("Goal" :use ((:instance <-*-right-cancel
(x (/ y))
(y x)
(z y))
(:instance right-cancellation-for-*
(x (/ y))
(y x)
(z y)))
:in-theory (disable equal-/ normalize-<-/-to-*-1))))
(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)))))
:hints (("Goal" :use ((:instance <-*-right-cancel
(x x)
(y (* y (/ z)))
(z z))))))
(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)))))
:hints (("Goal" :use ((:instance <-*-right-cancel
(x (* y (/ z)))
(y x)
(z z)))
:in-theory (disable NORMALIZE-<-/-TO-*-3-1))))
(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-/))
|
