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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
|
; Fully Ordered Finite Sets, Version 0.9
; Copyright (C) 2003, 2004 Kookamara LLC
;
; Contact:
;
; Kookamara LLC
; 11410 Windermere Meadows
; Austin, TX 78759, USA
; http://www.kookamara.com/
;
; License: (An MIT/X11-style license)
;
; Permission is hereby granted, free of charge, to any person obtaining a
; copy of this software and associated documentation files (the "Software"),
; to deal in the Software without restriction, including without limitation
; the rights to use, copy, modify, merge, publish, distribute, sublicense,
; and/or sell copies of the Software, and to permit persons to whom the
; Software is furnished to do so, subject to the following conditions:
;
; The above copyright notice and this permission notice shall be included in
; all copies or substantial portions of the Software.
;
; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
; DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis <jared@kookamara.com>
;
; computed-hints.lisp
;
; We provide support for the development of "pick a point" style
; proofs through computed hints.
(in-package "COMPUTED-HINTS")
;;; Introduction
;;;
;;; Suppose we have some predicate, P, of any number of arguments. A
;;; natural operation is to extend this predicate to every element of
;;; a list, set, or other collection. In other words, we would like
;;; to know if every element in the set, list, tree, or whatever has
;;; the property when applied to arguments.
;;;
;;; For example, we might have the predicate:
;;;
;;; (defun integer-lessp (a b)
;;; (and (integerp a)
;;; (< a b)))
;;;
;;; We could now extend this concept to an entire list, to ask if
;;; every element in the list was an integer that is less than b. The
;;; function might be written as:
;;;
;;; (defun list-integer-lessp (a-list b)
;;; (declare (xargs :guard (true-listp a-list)))
;;; (or (endp a-list)
;;; (and (integer-lessp (car a-list) b)
;;; (list-integer-lessp (cdr a-list) b))))
;;;
;;; Similarly, we might want to map the function across sets or other
;;; types of collections.
;;;
;;; Take an abstract mathematical view for a moment. Given some
;;; predicate P, what we would really like to do is be able to express
;;; the idea that given some collection x, every element of x
;;; satisfies P. In other words, we want to define:
;;;
;;; (collection-P x [args]) = forall a in x, (P x [args])
;;;
;;; And indeed, it would be nice to be working with this very abstract
;;; mathematical definition, for which we will not need to make
;;; inductive arguments. Unfortunately, because all variables in
;;; ACL2's rewrite rules are implicitly universally quantified, we
;;; cannot express the above as a rewrite rule.
;;;
;;; However, through the use of constrained function symbols and
;;; functional instantiation, we can effectively accomplish the above
;;; reduction when it suits our purposes. And, the process can be
;;; automated through the use of computed hints. Overall, this is not
;;; as nice as working with a pure rewrite rule, and in fact has some
;;; unfortunate limitations. However, it does turn out to be very
;;; broadly applicable and invaluable for reasoning about set
;;; theoretic concepts, where concepts such as "subset" are really
;;; nothing more than the extension of the predicate "in" across a
;;; set.
;;;
;;; Moreover, the reduction that we set out to achieve will reduce
;;; (collection-P x [args]) to the following implication:
;;;
;;; (implies (in a x)
;;; (P a [args]))
;;;
;;; I call this a "pick a point" reduction, because it is similar to
;;; and takes its inspiration from the well known set theoretic
;;; technique of picking an arbitrary element (or point) in one set,
;;; then showing it is also a member of another set.
;;; Preliminaries
;;;
;;; We will make minor use of the rewriting system developed in
;;; instance.lisp. We also enter program mode, because we are not
;;; interested in reasoning about these functions.
(include-book "instance")
(program)
;;; Tagging
;;;
;;; Suppose that we have (collection-P x a0 a1 ... an) to a simpler
;;; argument. We begin by defining a synonym for collection-P, e.g.,
;;;
;;; (defun collection-P-tag (x a0 a1 ... an)
;;; (collection-P x a0 a1 ... an))
;;;
;;; Now we instruct the theorem prover to rewrite instances of
;;; conclusion into conclusion-tag, as long as we are not backchaining
;;; and as long as conclusion occurs as the goal. For example,
;;;
;;; (defthm tagging-theorem
;;; (implies
;;; (and (syntaxp (rewriting-goal-lit mfc state))
;;; (syntaxp (rewriting-conc-lit `(collection-P ,x ,a0 ... ,an)
;;; mfc state)))
;;; (equal (collection-P x a0 ... an)
;;; (collection-P-tag x a0 ... an))))
;;;
;;; This theorem is trivial to prove, since collection-P-tag is merely
;;; a synonym for collection-P. After the theorem is proven,
;;; collection-P-tag should be disabled.
(defun rewriting-goal-lit (mfc state)
(declare (xargs :stobjs state)
(ignore state))
(null (mfc-ancestors mfc)))
(defun rewriting-conc-lit (term mfc state)
(declare (xargs :stobjs state)
(ignore state))
(let ((clause (mfc-clause mfc)))
(member-equal term (last clause))))
;;; Computing a Hint
;;;
;;; Now, what we are going to do next is create a computed hint that
;;; will look for instances of a trigger, and if it sees one, we will
;;; try to provide a functional instantiation hint. This takes some
;;; work. Our computed hint function is called as ACL2 is working to
;;; simplify terms, and it is allowed to examine the current clause.
;;; The current clause will be a a disjunction of literals. For
;;; example,
;;;
;;; (a ^ b ^ ...) => P is (~a v ~b v ... v P)
;;; (a v b v ...) => P is subgoal1: (~a v P), sg2: (~b v P), ...
;;;
;;; Our first step is to see if our computed hint should even be
;;; applied to this clause. We only allow the hint to be applied if
;;; the current clause is stable under simplification, i.e., if other
;;; attempts to prove it have failed. At that point, we check the
;;; clause to see if our trigger occurs as a term within it. If so,
;;; the tagging theorem has applied and thinks we should try to use
;;; our computed hint!
;;;
;;; We check for the existence of our trigger using the following
;;; function, (harvest-trigger clause trigger-fn), which extracts all
;;; the terms from clause whose function symbol is trigger-fn, and
;;; returns them as a list.
;;;
;;; Now, our intention is to functionally instantiate the theorem in
;;; question. To do this, we need to provide values for the
;;; hypotheses and arguments a0 ... an.
;;;
;;; In order to recover the hypotheses, we first remove from the
;;; clause all of our trigger terms. We then negate each of the
;;; remaining literals as they occur in the clause. And, if there are
;;; more than one of them, we are going to AND their negations
;;; together. This is done by the functions others-to-negated-list,
;;; and others-to-hyps.
;;;
;;; For example, if we originally had the conjecture (a ^ b ^ ...) =>
;;; P Then this became the clause: (~a v ~b v ... v P), which is
;;; represented by the list ((not a) (not b) ... P). Suppose that P
;;; was our trigger term. We remove P from the clause, yielding ((not
;;; a) (not b) ...), and then we negate all of these literals,
;;; creating the list (a b ...). We now and these together, creating
;;; the the term (and a b ...), which was our original hypotheses!
(defun harvest-trigger (clause trigger-fn)
(if (endp clause)
nil
(if (eq (caar clause) trigger-fn)
(cons (car clause) (harvest-trigger (cdr clause) trigger-fn))
(harvest-trigger (cdr clause) trigger-fn))))
(defun others-to-negated-list (others)
(if (endp others)
nil
(if (equal (caar others) 'not) ; don't create ugly double not's
(cons (second (car others))
(others-to-negated-list (cdr others)))
(cons (list 'not (car others))
(others-to-negated-list (cdr others))))))
(defun others-to-hyps (others)
(if (endp others)
t
(let ((negated (others-to-negated-list others)))
(if (endp (cdr negated)) ; don't wrap single literals in and's
(car negated)
(cons 'and (others-to-negated-list others))))))
;;; Absolute Restrictions:
;;;
;;; Collection predicate must have a first argument which is the
;;; collection to traverse!!
;;;
;;; Need to be able to create hint for predicate as well.
;;; Building Hints
;;;
;;; Our ultimate goal now is to be able to create functional
;;; instantiation hints for each trigger which was found. In other
;;; words, we now have a set of triggers which look like the following:
;;;
;;; ((collection-P-tag col1 [extra-args1])
;;; (collection-P-tag col2 [extra-args2])
;;; ...)
;;;
;;; We want to instantiate generic theorems of the form:
;;;
;;; (defthm generic-theorem
;;; (implies (hyps)
;;; (collection-P-tag (collection) [extra-args])))
;;;
;;; Where we have the following generic constraint:
;;;
;;; (implies (hyps)
;;; (implies (in a (collection))
;;; (predicate a)))
;;;
;;; So, the functional instantiation hints we want to create will look
;;; like the following:
;;;
;;; (:functional-instance generic-theorem
;;; (hyps (lambda () [substitution for hyps]))
;;; (collection (lambda () [substitution for collection]))
;;; (predicate (lambda (x) [substitution for predicate]))
;;; (collection-P (lambda (x) [substitution for collection-P])))
;;;
;;; Lets consider how we can build these substitutions for some
;;; trigger = (collection-P-tag col1 [extra-args1]). Some of this
;;; is easy:
;;;
;;; The substitution for hyps is actually built using the process
;;; described above, e.g., they are extracted from the clause and
;;; eventually restored to normal using others-to-hyps, so I will
;;; not spend any time on them.
;;;
;;; The collection is simply (second trigger), since we require that
;;; the collection predicate has the collection as its first
;;; argument.
;;;
;;; The substitution for collection-P is also fairly easy. Since
;;; we require that the collection function's first argument is
;;; the collection under examination, we simply need to write
;;; (lambda (?x) (actual-collection-P ?x [extra-args])), where the
;;; extra arguments are taken from the trigger we are looking at.
;;;
;;; This leaves us with predicate. The substitution for predicate
;;; is difficult, because we want to support very flexible
;;; predicates involving many arguments and various weird terms.
;;; To do this, we will allow the user to provide a rewrite rule
;;; that says how to handle the predicate.
;;;
;;; In other words, given the trigger (trigger-term col a0 a1 a2
;;; ... an) we will create the following "base predicate" to
;;; rewrite:
;;;
;;; (predicate ?x a0 a1 a2 ... an)
;;;
;;; Where "predicate" is literally the name of the generic
;;; predicate. The user can then provide a substitution such
;;; as:
;;;
;;; (predicate ?x ?y) -> (not (integer-lessp ?x ?y))
;;;
;;; And this will transform the above into the desired result.
(defun build-hint (trigger ; list, the actual trigger to use
generic-theorem ; symbol, the name of generic-theorem
generic-hyps ; symbol, the name of (hyps)
generic-collection ; symbol, the name of (collection)
generic-predicate ; symbol, the name of predicate
generic-collection-P ; symbol, the name of collection-P
collection-P-sub ; symbol, name of actual collection-P
hyps-sub ; the computed substitution for hyps
predicate-rewrite) ; rewrite rule for predicate
(let* ((base-pred (cons generic-predicate (cons '?x (cddr trigger))))
(pred-sub (instance-rewrite base-pred predicate-rewrite)))
`(:functional-instance
,generic-theorem
(,generic-hyps
(lambda () ,hyps-sub))
(,generic-collection
(lambda () ,(second trigger)))
(,generic-collection-P
(lambda (?x) ,(cons collection-P-sub (cons '?x (cddr trigger)))))
(,generic-predicate
(lambda (?x) ,pred-sub)))))
(defun build-hints (triggers
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
hyps-sub
predicate-rewrite)
(if (endp triggers)
nil
(cons (build-hint (car triggers)
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
hyps-sub
predicate-rewrite)
(build-hints (cdr triggers)
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
hyps-sub
predicate-rewrite))))
(defconst *message*
"~|~%We suspect this conjecture should be proven by functional ~
instantiation of ~x0. This suspicion is caused by ~x2, so ~
if this is not what you want to do, then you should disable ~
~x2. Accordingly, we suggest the following hint: ~
~%~%~x1~%")
;;; Of course, some of those hints can be computed. Here we write a function
;;; to actually provide these hints and install the computed hint function.
(defun automate-instantiation-fn (new-hint-name
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
predicate-rewrite
trigger-symbol
tagging-theorem)
`(encapsulate ()
(defun ,new-hint-name (id clause world stable)
(declare (xargs :mode :program)
(ignore world))
(if (not stable)
nil
(let ((triggers (harvest-trigger clause ,trigger-symbol)))
(if (not triggers)
nil
(let* ((others (set-difference-equal clause triggers))
(hyps (others-to-hyps others))
(phrase (string-for-tilde-@-clause-id-phrase id))
(fi-hints (build-hints triggers
,generic-theorem
,generic-hyps
,generic-collection
,generic-predicate
,generic-collection-P
,collection-P-sub
hyps
,predicate-rewrite))
(hints (list :use fi-hints
:expand triggers)))
(prog2$ (cw *message*
,generic-theorem
(list phrase hints)
,tagging-theorem)
hints))))))
(add-default-hints!
'((,new-hint-name id clause world stable-under-simplificationp)))
))
(defmacro automate-instantiation (&key new-hint-name
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-predicate
actual-collection-predicate
predicate-rewrite
actual-trigger
tagging-theorem)
(automate-instantiation-fn new-hint-name
(list 'quote generic-theorem)
(list 'quote generic-hyps)
(list 'quote generic-collection)
(list 'quote generic-predicate)
(list 'quote generic-collection-predicate)
(list 'quote actual-collection-predicate)
(list 'quote predicate-rewrite)
(list 'quote actual-trigger)
(list 'quote tagging-theorem)))
|
