← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/adviser/adviser.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/coi/adviser/adviser.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#| coi: Computational Object Inference                                       |#
4
 
#|                                                                           |#
5
 
#|===========================================================================|#
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
6
31
;; adviser.lisp
7
 
;; Jared Davis 
 
32
;; Jared Davis
8
33
 
9
34
(in-package "ADVISER")
10
35
(include-book "misc/symbol-btree" :dir :system)
11
36
(include-book "../symbol-fns/symbol-fns")
12
 
 
13
 
(defdoc Adviser
14
 
  ":Doc-Section Adviser
15
 
 
16
 
   a extensible hint suggestion daemon~/
17
 
 
18
 
   Adviser is a a hint computation service.  When the adviser book is loaded,
19
 
   this service is installed into the ACL2 world as a default hint.  This
20
 
   service is consulted when goals becomes stable under simplification during
21
 
   your proof attempts.  In other words, before destructor elimination,
22
 
   generalization, and so forth are tried, the theorem prover will now first
23
 
   consult the Adviser service and see if any hints is available.  ~/
24
 
 
25
 
   When the Adviser is consulted, it examines the goal that ACL2 is stuck on
26
 
   and checks to see if it can give any suggestions.  To make these
27
 
   suggestions, Adviser consults its own database of rules.  These rules are
28
 
   kept in a new ACL2 ~il[table] that Adviser manages, and efficiently stored
29
 
   using the btree library that comes with ACL2 (see
30
 
   books/misc/symbol-btree.lisp).
31
 
 
32
 
   This database oriented approach has two advantages.  First, users can extend
33
 
   Adviser's knowledge by adding new rules, without having to understand the
34
 
   tricky details of how computed hints work.  (These rules are added through a
35
 
   new event called ~il[defadvice], which intentionally looks a lot like
36
 
   defthm).  Second, by using a database of triggers, a single pass over each
37
 
   goal is sufficient to determine if advice is necessary.  In contrast, if
38
 
   everyone created their own computed hints, we would have multiple passes
39
 
   over the same goal.
40
 
 
41
 
   ~l[defadvice] for information on adding rules to Adviser.")
42
 
 
43
 
(defdoc defadvice
44
 
  ":Doc-Section Adviser
45
 
 
46
 
  adds a rule to the Adviser database~/
47
 
 
48
 
  ~bv[]
 
37
(include-book "xdoc/top" :dir :system)
 
38
(defmacro defxdoc (&rest args)
 
39
  `(acl2::defxdoc ,@args))
 
40
 
 
41
; The following legacy doc strings were replaced Nov. 2014 by
 
42
; auto-generated defxdoc forms below.
 
43
 
 
44
;(defdoc Adviser
 
45
; ":Doc-Section Adviser
 
46
 
 
47
;  a extensible hint suggestion daemon~/
 
48
 
 
49
;  Adviser is a a hint computation service.  When the adviser book is loaded,
 
50
;  this service is installed into the ACL2 world as a default hint.  This
 
51
;  service is consulted when goals becomes stable under simplification during
 
52
;  your proof attempts.  In other words, before destructor elimination,
 
53
;  generalization, and so forth are tried, the theorem prover will now first
 
54
;  consult the Adviser service and see if any hints is available.  ~/
 
55
 
 
56
;  When the Adviser is consulted, it examines the goal that ACL2 is stuck on
 
57
;  and checks to see if it can give any suggestions.  To make these
 
58
;  suggestions, Adviser consults its own database of rules.  These rules are
 
59
;  kept in a new ACL2 ~il[table] that Adviser manages, and efficiently stored
 
60
;  using the btree library that comes with ACL2 (see
 
61
;  books/misc/symbol-btree.lisp).
 
62
 
 
63
;  This database oriented approach has two advantages.  First, users can extend
 
64
;  Adviser's knowledge by adding new rules, without having to understand the
 
65
;  tricky details of how computed hints work.  (These rules are added through a
 
66
;  new event called ~il[adviser::defadvice], which intentionally looks a lot
 
67
;  like defthm).  Second, by using a database of triggers, a single pass over
 
68
;  each goal is sufficient to determine if advice is necessary.  In contrast,
 
69
;  if everyone created their own computed hints, we would have multiple passes
 
70
;  over the same goal.
 
71
 
 
72
;  ~l[adviser::defadvice] for information on adding rules to Adviser.")
 
73
 
 
74
;(defdoc defadvice
 
75
; ":Doc-Section Adviser
 
76
 
 
77
; adds a rule to the Adviser database~/
 
78
 
 
79
; ~bv[]
 
80
; General Form:
 
81
; (defadvice rule-name term
 
82
;   :rule-classes rule-classes)
 
83
; ~ev[]
 
84
 
 
85
; where ~c[name] is a new symbolic name ~l[name], ~c[term] is a term alleged to
 
86
; be a useful piece of advice, and ~c[rule-classes] describe the type of advice
 
87
; being added and when to suggest hints of this nature.~/
 
88
 
 
89
; When Adviser is first loaded, no rules are installed in its database, so it
 
90
; will never suggest any hints.  To make Adviser useful, rules must be added to
 
91
; it using defadvice.  In principle, many types of advice could be added to the
 
92
; Adviser service, and in the future other classes of advice might be added.
 
93
; But, for now, the only understood rule class is :pick-a-point.
 
94
 
 
95
; ~l[adviser::pick-a-point] for documentation and examples about :pick-a-point
 
96
; rules.")
 
97
 
 
98
;(defdoc pick-a-point
 
99
; ":Doc-Section Adviser
 
100
 
 
101
; make some :pick-a-point rules~/
 
102
 
 
103
; ~bv[]
 
104
; Example:
 
105
; (defadvice subbag-by-multiplicity
 
106
;   (implies (bag-hyps)
 
107
;            (subbagp (subbag) (superbag))))
 
108
; ~ev[]~/
 
109
;
 
110
; I described how the pick-a-point method can be useful for proving subsets in
 
111
; the 2004 ACL2 Workshop Paper: Finite Set Theory based on Fully Ordered Lists.
 
112
; Essentially, the idea is to you should be able to prove (subset x y) by just
 
113
; knowing that forall a, (in a x) implies (in a y).  Since writing that paper,
 
114
; I have found the pick a point method to be widely useful in other contexts
 
115
; that involve extending a predicate to some data structure.
 
116
 
 
117
; Often we will have some simple predicate, say ~c[integerp], which we will
 
118
; want to extend over some datastructure, say a list.  The result is a new,
 
119
; recursively defined predicate, say ~c[all-integerp].  Of course, it should be
 
120
; obvious that if every member of the list satisfies ~c[integerp], then the
 
121
; entire list satisfies ~c[all-integerp].  But, we can't write a :rewrite rule
 
122
; such as:
 
123
 
 
124
; ~bv[]
 
125
;   (equal (all-integerp x)
 
126
;          (forall a (implies (member a x) (integerp a))))
 
127
; ~ev[]
 
128
 
 
129
; Because all of the variables in our :rewrite rules must be universally
 
130
; quantified.  The :pick-a-point rules in Adviser are designed to make exactly
 
131
; this kind of reduction.  As an example, I'll now elaborate on how to set up
 
132
; such a reduction for ~c[all-integerp].  You will find that many other ideas,
 
133
; such as subsets, subtree, subbag relations, and so forth, are basically just
 
134
; copies of this idea.
 
135
 
 
136
; We begin with our definition of all-integerp.  (We do not use integer-listp
 
137
; because it requires its argument to be a true-listp.)
 
138
 
 
139
; ~bv[]
 
140
; (defun all-integerp (x)
 
141
;   (if (consp x)
 
142
;       (and (integerp (car x))
 
143
;            (all-integerp (cdr x)))
 
144
;     t))
 
145
; ~ev[]
 
146
 
 
147
; Our first task is to write our ``forall'' statement as a constraint theorem
 
148
; about encapsulated functions.  Becuase we are quantifying over all ``a'', it
 
149
; will be a variable in this constrained theorem.  However, since ``x'' is not
 
150
; being quantified, we will create a constrained function for it.  For reasons
 
151
; we will explain later, we will also have one more constrianed function called
 
152
; ``hyps''.  In all, we come up with the following encapsulate:
 
153
 
 
154
; ~bv[]
 
155
; (encapsulate
 
156
;  (((intlist-hyps) => *)
 
157
;   ((intlist-list) => *))
 
158
;  (local (defun intlist-hyps () nil))
 
159
;  (local (defun intlist-list () nil))
 
160
;  (defthm intlist-constraint
 
161
;    (implies (and (intlist-hyps)
 
162
;                  (member intlist-element (intlist-list)))
 
163
;             (integerp intlist-element))
 
164
;    :rule-classes nil))
 
165
; ~ev[]
 
166
 
 
167
; Our next goal is to prove that, given this constraint, it must be the case
 
168
; that (integer-listp (intlist-list)) is true.  The proof is not entirely
 
169
; straightforward, but follows the same script each time.  Basically, we first
 
170
; set up a ``badguy'' function that will go through and find an element that
 
171
; violates our constraint if one exists.  We show that the badguy finds such
 
172
; an element whenever ``all-integerp'' is not satisifed.  Then, we just use
 
173
; the instance of our constraint to show that all-integerp must be true for
 
174
; (intlist-list).
 
175
 
 
176
; ~bv[]
 
177
; (local (defun badguy (x)
 
178
;          (if (endp x)
 
179
;              nil
 
180
;            (if (integerp (car x))
 
181
;                (badguy (cdr x))
 
182
;              (car x)))))
 
183
;
 
184
; (local (defthm badguy-works
 
185
;          (implies (not (all-integerp x))
 
186
;                   (and (member (badguy x) x)
 
187
;                        (not (integerp (badguy x)))))))
 
188
 
 
189
; (defthm intlist-by-membership-driver
 
190
;   (implies (intlist-hyps)
 
191
;            (all-integerp (intlist-list)))
 
192
;   :rule-classes nil
 
193
;   :hints((\"Goal\"
 
194
;           :use (:instance intlist-constraint
 
195
;                           (intlist-element (badguy (intlist-list)))))))
 
196
; ~ev[]
 
197
;
 
198
; At this point, we have essentially shown ACL2 that ``all-integerp`` can
 
199
; be shown as long as we can show our constraint is true.  The missing step
 
200
; is for ACL2 to actually try this approach for us.  But we can't write a
 
201
; rewrite rule that says ``try to functionally instantiate this theorem
 
202
; whenever you are trying to prove (all-integerp x).''
 
203
 
 
204
; That's where Adviser comes in.  We just give it the following rule:
 
205
 
 
206
; ~bv[]
 
207
; (ADVISER::defadvice intlist-by-membership
 
208
;   (implies (intlist-hyps)
 
209
;            (all-integerp (intlist-list)))
 
210
;   :rule-classes (:pick-a-point :driver intlist-by-membership-driver))
 
211
; ~ev[]
 
212
 
 
213
; Because we used defadvice, rather than defthm, this rule is for Adviser
 
214
; to add to its database.  Adviser will set up a new trigger for
 
215
; all-integerp, and whenever it sees that trigger as the target that we
 
216
; are trying to prove, it will functionally instantiate the driver theorem.
 
217
; We can now conduct membership based proofs of all-integerp.
 
218
 
 
219
; For example, in the following script we can prove that (all-integerp (rev x))
 
220
; exactly when (all-integerp x) without inducting over either function,
 
221
; because we can just consider membership.
 
222
 
 
223
; ~bv[]
 
224
; (defthm equal-of-booleans-rewrite
 
225
;   (implies (and (booleanp x)
 
226
;                 (booleanp y))
 
227
;            (equal (equal x y)
 
228
;                   (iff x y)))
 
229
;   :rule-classes ((:rewrite :backchain-limit-lst 0)))
 
230
 
 
231
; (defthm member-of-all-integerp-1
 
232
;   (implies (and (member a x)
 
233
;                 (all-integerp x))
 
234
;            (integerp a)))
 
235
 
 
236
; (defthm member-of-all-integerp-2
 
237
;   (implies (and (all-integerp x)
 
238
;                 (not (integerp a)))
 
239
;            (not (member a x))))
 
240
 
 
241
; (in-theory (disable all-integerp))
 
242
 
 
243
; (defund rev (x)
 
244
;   (if (endp x)
 
245
;       x
 
246
;     (append (rev (cdr x))
 
247
;             (list (car x)))))
 
248
 
 
249
; (defthm member-of-rev
 
250
;   (iff (member a (rev x))
 
251
;        (member a x))
 
252
;   :hints((\"Goal\" :in-theory (enable rev))))
 
253
 
 
254
; (encapsulate
 
255
;  ()
 
256
 
 
257
;  (local (defthm lemma1
 
258
;           (implies (all-integerp x)
 
259
;                    (all-integerp (rev x)))))
 
260
;
 
261
;  (local (defthm lemma2
 
262
;           (implies (all-integerp (rev x))
 
263
;                    (all-integerp x))
 
264
;           :hints((\"Subgoal 1\" :use (:instance member-of-all-integerp-1
 
265
;                                                 (a intlist-element)
 
266
;                                                 (x (rev x)))))))
 
267
 
 
268
;  (defthm all-integerp-of-rev
 
269
;    (equal (all-integerp (rev x))
 
270
;           (all-integerp x)))
 
271
;  )
 
272
; ~ev[]")
 
273
 
 
274
(defxdoc adviser::adviser
 
275
  :parents (adviser::adviser)
 
276
  :short "A extensible hint suggestion daemon"
 
277
  :long "<p>Adviser is a a hint computation service.  When the adviser book is
 
278
 loaded, this service is installed into the ACL2 world as a default hint.  This
 
279
 service is consulted when goals becomes stable under simplification during
 
280
 your proof attempts.  In other words, before destructor elimination,
 
281
 generalization, and so forth are tried, the theorem prover will now first
 
282
 consult the Adviser service and see if any hints is available.</p>
 
283
 
 
284
 <p>When the Adviser is consulted, it examines the goal that ACL2 is stuck on
 
285
 and checks to see if it can give any suggestions.  To make these suggestions,
 
286
 Adviser consults its own database of rules.  These rules are kept in a new
 
287
 ACL2 @(see table) that Adviser manages, and efficiently stored using the btree
 
288
 library that comes with ACL2 (see books/misc/symbol-btree.lisp).</p>
 
289
 
 
290
 <p>This database oriented approach has two advantages.  First, users can
 
291
 extend Adviser's knowledge by adding new rules, without having to understand
 
292
 the tricky details of how computed hints work.  (These rules are added through
 
293
 a new event called @(see adviser::defadvice), which intentionally looks a lot
 
294
 like defthm).  Second, by using a database of triggers, a single pass over
 
295
 each goal is sufficient to determine if advice is necessary.  In contrast, if
 
296
 everyone created their own computed hints, we would have multiple passes over
 
297
 the same goal.</p>
 
298
 
 
299
 <p>See @(see adviser::defadvice) for information on adding rules to
 
300
 Adviser.</p>")
 
301
 
 
302
(defxdoc adviser::defadvice
 
303
  :parents (adviser::adviser)
 
304
  :short "Adds a rule to the Adviser database"
 
305
  :long "@({
49
306
  General Form:
50
 
  (defadvice rule-name term 
 
307
  (defadvice rule-name term
51
308
    :rule-classes rule-classes)
52
 
  ~ev[]             
53
 
 
54
 
  where ~c[name] is a new symbolic name ~l[name], ~c[term] is a term alleged to
55
 
  be a useful piece of advice, and ~c[rule-classes] describe the type of advice
56
 
  being added and when to suggest hints of this nature.~/
57
 
 
58
 
  When Adviser is first loaded, no rules are installed in its database, so it
59
 
  will never suggest any hints.  To make Adviser useful, rules must be added to
60
 
  it using defadvice.  In principle, many types of advice could be added to the
61
 
  Adviser service, and in the future other classes of advice might be added. 
62
 
  But, for now, the only understood rule class is :pick-a-point.  
63
 
 
64
 
  ~l[pick-a-point] for documentation and examples about :pick-a-point rules.")
65
 
 
66
 
(defdoc pick-a-point
67
 
  ":Doc-Section Adviser
68
 
 
69
 
  make some :pick-a-point rules~/
70
 
        
71
 
  ~bv[]
 
309
 })
 
310
 
 
311
 <p>where @('name') is a new symbolic name See @(see name), @('term') is a term
 
312
 alleged to be a useful piece of advice, and @('rule-classes') describe the
 
313
 type of advice being added and when to suggest hints of this nature.</p>
 
314
 
 
315
 <p>When Adviser is first loaded, no rules are installed in its database, so it
 
316
 will never suggest any hints.  To make Adviser useful, rules must be added to
 
317
 it using defadvice.  In principle, many types of advice could be added to the
 
318
 Adviser service, and in the future other classes of advice might be added.
 
319
 But, for now, the only understood rule class is :pick-a-point.</p>
 
320
 
 
321
 <p>See @(see adviser::pick-a-point) for documentation and examples about
 
322
 :pick-a-point rules.</p>")
 
323
 
 
324
(defxdoc adviser::pick-a-point
 
325
  :parents (adviser::adviser)
 
326
  :short "Make some :pick-a-point rules"
 
327
  :long "@({
72
328
  Example:
73
329
  (defadvice subbag-by-multiplicity
74
330
    (implies (bag-hyps)
75
331
             (subbagp (subbag) (superbag))))
76
 
  ~ev[]~/
77
 
  
78
 
  I described how the pick-a-point method can be useful for proving subsets in
79
 
  the 2004 ACL2 Workshop Paper: Finite Set Theory based on Fully Ordered Lists.
80
 
  Essentially, the idea is to you should be able to prove (subset x y) by just
81
 
  knowing that forall a, (in a x) implies (in a y).  Since writing that paper,
82
 
  I have found the pick a point method to be widely useful in other contexts
83
 
  that involve extending a predicate to some data structure.
84
 
 
85
 
  Often we will have some simple predicate, say ~c[integerp], which we will
86
 
  want to extend over some datastructure, say a list.  The result is a new,
87
 
  recursively defined predicate, say ~c[all-integerp].  Of course, it should be
88
 
  obvious that if every member of the list satisfies ~c[integerp], then the
89
 
  entire list satisfies ~c[all-integerp].  But, we can't write a :rewrite rule
90
 
  such as:
91
 
 
92
 
  ~bv[]
 
332
 })
 
333
 
 
334
 <p>I described how the pick-a-point method can be useful for proving subsets
 
335
 in the 2004 ACL2 Workshop Paper: Finite Set Theory based on Fully Ordered
 
336
 Lists.  Essentially, the idea is to you should be able to prove (subset x y)
 
337
 by just knowing that forall a, (in a x) implies (in a y).  Since writing that
 
338
 paper, I have found the pick a point method to be widely useful in other
 
339
 contexts that involve extending a predicate to some data structure.</p>
 
340
 
 
341
 <p>Often we will have some simple predicate, say @('integerp'), which we will
 
342
 want to extend over some datastructure, say a list.  The result is a new,
 
343
 recursively defined predicate, say @('all-integerp').  Of course, it should be
 
344
 obvious that if every member of the list satisfies @('integerp'), then the
 
345
 entire list satisfies @('all-integerp').  But, we can't write a :rewrite rule
 
346
 such as:</p>
 
347
 
 
348
 @({
93
349
    (equal (all-integerp x)
94
350
           (forall a (implies (member a x) (integerp a))))
95
 
  ~ev[]
96
 
 
97
 
  Because all of the variables in our :rewrite rules must be universally
98
 
  quantified.  The :pick-a-point rules in Adviser are designed to make exactly
99
 
  this kind of reduction.  As an example, I'll now elaborate on how to set up
100
 
  such a reduction for ~c[all-integerp].  You will find that many other ideas,
101
 
  such as subsets, subtree, subbag relations, and so forth, are basically just
102
 
  copies of this idea.
103
 
 
104
 
  We begin with our definition of all-integerp.  (We do not use integer-listp
105
 
  because it requires its argument to be a true-listp.)
106
 
 
107
 
  ~bv[]
 
351
 })
 
352
 
 
353
 <p>Because all of the variables in our :rewrite rules must be universally
 
354
 quantified.  The :pick-a-point rules in Adviser are designed to make exactly
 
355
 this kind of reduction.  As an example, I'll now elaborate on how to set up
 
356
 such a reduction for @('all-integerp').  You will find that many other ideas,
 
357
 such as subsets, subtree, subbag relations, and so forth, are basically just
 
358
 copies of this idea.</p>
 
359
 
 
360
 <p>We begin with our definition of all-integerp.  (We do not use integer-listp
 
361
 because it requires its argument to be a true-listp.)</p>
 
362
 
 
363
 @({
108
364
  (defun all-integerp (x)
109
365
    (if (consp x)
110
366
        (and (integerp (car x))
111
367
             (all-integerp (cdr x)))
112
368
      t))
113
 
  ~ev[]
114
 
 
115
 
  Our first task is to write our ``forall'' statement as a constraint theorem
116
 
  about encapsulated functions.  Becuase we are quantifying over all ``a'', it
117
 
  will be a variable in this constrained theorem.  However, since ``x'' is not
118
 
  being quantified, we will create a constrained function for it.  For reasons
119
 
  we will explain later, we will also have one more constrianed function called
120
 
  ``hyps''.  In all, we come up with the following encapsulate:
121
 
 
122
 
  ~bv[]
 
369
 })
 
370
 
 
371
 <p>Our first task is to write our ``forall'' statement as a constraint theorem
 
372
 about encapsulated functions.  Becuase we are quantifying over all ``a'', it
 
373
 will be a variable in this constrained theorem.  However, since ``x'' is not
 
374
 being quantified, we will create a constrained function for it.  For reasons
 
375
 we will explain later, we will also have one more constrianed function called
 
376
 ``hyps''.  In all, we come up with the following encapsulate:</p>
 
377
 
 
378
 @({
123
379
  (encapsulate
124
380
   (((intlist-hyps) => *)
125
381
    ((intlist-list) => *))
127
383
   (local (defun intlist-list () nil))
128
384
   (defthm intlist-constraint
129
385
     (implies (and (intlist-hyps)
130
 
                   (member intlist-element (intlist-list)))
131
 
              (integerp intlist-element))
 
386
                   (member intlist-element (intlist-list)))
 
387
              (integerp intlist-element))
132
388
     :rule-classes nil))
133
 
  ~ev[]
134
 
 
135
 
  Our next goal is to prove that, given this constraint, it must be the case
136
 
  that (integer-listp (intlist-list)) is true.  The proof is not entirely 
137
 
  straightforward, but follows the same script each time.  Basically, we first
138
 
  set up a ``badguy'' function that will go through and find an element that
139
 
  violates our constraint if one exists.  We show that the badguy finds such
140
 
  an element whenever ``all-integerp'' is not satisifed.  Then, we just use
141
 
  the instance of our constraint to show that all-integerp must be true for 
142
 
  (intlist-list).
143
 
 
144
 
  ~bv[]
 
389
 })
 
390
 
 
391
 <p>Our next goal is to prove that, given this constraint, it must be the case
 
392
 that (integer-listp (intlist-list)) is true.  The proof is not entirely
 
393
 straightforward, but follows the same script each time.  Basically, we first
 
394
 set up a ``badguy'' function that will go through and find an element that
 
395
 violates our constraint if one exists.  We show that the badguy finds such an
 
396
 element whenever ``all-integerp'' is not satisifed.  Then, we just use the
 
397
 instance of our constraint to show that all-integerp must be true for
 
398
 (intlist-list).</p>
 
399
 
 
400
 @({
145
401
  (local (defun badguy (x)
146
402
           (if (endp x)
147
403
               nil
148
404
             (if (integerp (car x))
149
 
                 (badguy (cdr x)) 
 
405
                 (badguy (cdr x))
150
406
               (car x)))))
151
 
             
 
407
 
152
408
  (local (defthm badguy-works
153
409
           (implies (not (all-integerp x))
154
410
                    (and (member (badguy x) x)
158
414
    (implies (intlist-hyps)
159
415
             (all-integerp (intlist-list)))
160
416
    :rule-classes nil
161
 
    :hints((\"Goal\" 
 
417
    :hints((\"Goal\"
162
418
            :use (:instance intlist-constraint
163
419
                            (intlist-element (badguy (intlist-list)))))))
164
 
  ~ev[]
165
 
  
166
 
  At this point, we have essentially shown ACL2 that ``all-integerp`` can
167
 
  be shown as long as we can show our constraint is true.  The missing step
168
 
  is for ACL2 to actually try this approach for us.  But we can't write a 
169
 
  rewrite rule that says ``try to functionally instantiate this theorem 
170
 
  whenever you are trying to prove (all-integerp x).''
171
 
 
172
 
  That's where Adviser comes in.  We just give it the following rule:
173
 
 
174
 
  ~bv[]
 
420
 })
 
421
 
 
422
 <p>
 
423
 
 
424
 At this point, we have essentially shown ACL2 that ``all-integerp`` can be
 
425
 shown as long as we can show our constraint is true.  The missing step is for
 
426
 ACL2 to actually try this approach for us.  But we can't write a rewrite rule
 
427
 that says ``try to functionally instantiate this theorem whenever you are
 
428
 trying to prove (all-integerp x).''</p>
 
429
 
 
430
 <p>That's where Adviser comes in.  We just give it the following rule:</p>
 
431
 
 
432
 @({
175
433
  (ADVISER::defadvice intlist-by-membership
176
434
    (implies (intlist-hyps)
177
435
             (all-integerp (intlist-list)))
178
436
    :rule-classes (:pick-a-point :driver intlist-by-membership-driver))
179
 
  ~ev[]
180
 
 
181
 
  Because we used defadvice, rather than defthm, this rule is for Adviser
182
 
  to add to its database.  Adviser will set up a new trigger for 
183
 
  all-integerp, and whenever it sees that trigger as the target that we 
184
 
  are trying to prove, it will functionally instantiate the driver theorem.
185
 
  We can now conduct membership based proofs of all-integerp.  
186
 
 
187
 
  For example, in the following script we can prove that (all-integerp (rev x))
188
 
  exactly when (all-integerp x) without inducting over either function, 
189
 
  because we can just consider membership.
190
 
 
191
 
  ~bv[]
 
437
 })
 
438
 
 
439
 <p>Because we used defadvice, rather than defthm, this rule is for Adviser to
 
440
 add to its database.  Adviser will set up a new trigger for all-integerp, and
 
441
 whenever it sees that trigger as the target that we are trying to prove, it
 
442
 will functionally instantiate the driver theorem.  We can now conduct
 
443
 membership based proofs of all-integerp.</p>
 
444
 
 
445
 <p>For example, in the following script we can prove that (all-integerp (rev
 
446
 x)) exactly when (all-integerp x) without inducting over either function,
 
447
 because we can just consider membership.</p>
 
448
 
 
449
 @({
192
450
  (defthm equal-of-booleans-rewrite
193
451
    (implies (and (booleanp x)
194
452
                  (booleanp y))
211
469
  (defund rev (x)
212
470
    (if (endp x)
213
471
        x
214
 
      (append (rev (cdr x)) 
 
472
      (append (rev (cdr x))
215
473
              (list (car x)))))
216
474
 
217
475
  (defthm member-of-rev
225
483
   (local (defthm lemma1
226
484
            (implies (all-integerp x)
227
485
                     (all-integerp (rev x)))))
228
 
 
 
486
 
229
487
   (local (defthm lemma2
230
488
            (implies (all-integerp (rev x))
231
489
                     (all-integerp x))
237
495
     (equal (all-integerp (rev x))
238
496
            (all-integerp x)))
239
497
   )
240
 
  ~ev[]")
 
498
 })
 
499
 
 
500
 ")
241
501
 
242
502
(defun rewriting-goal-lit (mfc state)
243
503
  "Ensure that we are rewriting a goal, i.e., not backchaining."
264
524
  (declare (xargs :mode :program))
265
525
  (if (zp n)
266
526
      acc
267
 
    (aux-symbols (1- n) (cons (intern-in-package-of-symbol 
268
 
                               (concatenate 'string "X" 
 
527
    (aux-symbols (1- n) (cons (intern-in-package-of-symbol
 
528
                               (concatenate 'string "X"
269
529
                                            (coerce (explode-atom n 10) 'string))
270
530
                               'defthm)
271
531
                              acc))))
307
567
;;   (implies (hyps)
308
568
;;            (conclusion (arg1) (arg2) ... (argN)))
309
569
;;   :rule-classes (:pick-a-point :driver foo))
310
 
;; 
 
570
;;
311
571
;; Where hyps and each arg are encapsulated functions of no arguments, and
312
572
;; where foo is some defthm which proves exactly this implication for those
313
573
;; constrained functions.
322
582
    (and (true-listp (car x))
323
583
         (equal (len (car x)) 1)
324
584
         (symbolp (first (car x)))
325
 
         (pick-a-point-term-syntax-ok-p1 (cdr x)))))         
 
585
         (pick-a-point-term-syntax-ok-p1 (cdr x)))))
326
586
 
327
587
(defun pick-a-point-term-syntax-ok-p (term)
328
588
  "Check that (implies (hyps) (conclusion ...)) is syntactically ok."
334
594
             (conclusion (third term)))
335
595
         (and (true-listp hypothesis)
336
596
              (equal (len hypothesis) 1)
337
 
              (symbolp (first hypothesis))             
 
597
              (symbolp (first hypothesis))
338
598
              (true-listp conclusion)
339
599
              (consp conclusion)
340
600
              (cond ((eq (car conclusion) 'not)
341
601
                     (let ((conclusion (cadr conclusion)))
342
602
                       (and (<= 2 (len conclusion))
343
603
                            (symbolp (car conclusion))
344
 
                            (pick-a-point-term-syntax-ok-p1 
345
 
                             (cdr conclusion)))))                          
346
 
                    (t 
 
604
                            (pick-a-point-term-syntax-ok-p1
 
605
                             (cdr conclusion)))))
 
606
                    (t
347
607
                     (and (<= 2 (len conclusion))
348
608
                          (symbolp (car conclusion))
349
 
                          (pick-a-point-term-syntax-ok-p1 
 
609
                          (pick-a-point-term-syntax-ok-p1
350
610
                           (cdr conclusion)))))))))
351
611
 
352
612
 
354
614
  "Check that the rule classes are syntactically ok."
355
615
  (declare (xargs :mode :program))
356
616
  (and (true-listp x)
357
 
       (= (length x) 3)       
 
617
       (= (length x) 3)
358
618
       (eq (first x) :pick-a-point)
359
619
       (eq (second x) :driver)
360
620
       (symbolp (third x))))
363
623
  "Check that a pick a point rule satisfies all syntactic requirements."
364
624
  (declare (xargs :mode :program))
365
625
  (cond ((not (symbolp name))
366
 
         (cw "~%Rule name must be a symbol, but it is ~x0.~%" 
 
626
         (cw "~%Rule name must be a symbol, but it is ~x0.~%"
367
627
             name))
368
628
        ((not (pick-a-point-term-syntax-ok-p term))
369
629
         (cw "~%Term must be of the form:~%~%   ~
372
632
              Or else of the form:~%~%   ~
373
633
               (implies (hyps) ~%          ~
374
634
                        (not (conclusion (arg1) (arg2) ... (argN))))~%~%~
375
 
              But instead, the term is:~%~%   ~x0~%" 
 
635
              But instead, the term is:~%~%   ~x0~%"
376
636
             term))
377
637
        ((not (pick-a-point-rule-classes-syntax-ok-p rule-classes))
378
638
         (cw "~%:pick-a-point rules must have :rule-classes ~
394
654
         (negatedp   (if (eq (car conclusion) 'not)
395
655
                         t
396
656
                       nil))
397
 
         (function   (if negatedp 
 
657
         (function   (if negatedp
398
658
                         (first (cadr conclusion))
399
659
                       (first conclusion)))
400
660
         (args       (if negatedp
404
664
          (cons :name name)
405
665
          (cons :negatedp negatedp)
406
666
          (cons :function function)
407
 
          (cons :trigger (symbol-fns::join-symbols 
 
667
          (cons :trigger (symbol-fns::join-symbols
408
668
                          function
409
669
                          "ADVISER-"
410
670
                          (symbol-name function)
413
673
          (cons :hyps (first hypothesis))
414
674
          (cons :args (pairlis$ (symbols (len args))
415
675
                                args)))))
416
 
                                                            
 
676
 
417
677
(defun pick-a-point-rule-installer (parsed-rule)
418
678
  "Take a parsed rule and install it into the table, and set up the trigger."
419
679
  (declare (xargs :mode :program))
437
697
    ;; hypothesis .. which may be undesirable .. so for now we disable it.
438
698
    (defthmd ,name-any
439
699
      (implies (and (syntaxp (rewriting-goal-lit mfc state))
440
 
                    (syntaxp (rewriting-any-lit 
 
700
                    (syntaxp (rewriting-any-lit
441
701
                              ,(if negatedp
442
702
                                   `(list 'not (list ',function ,@(strip-cars args)))
443
703
                                 `(list ',function ,@(strip-cars args)))
446
706
                      (,trigger ,@(strip-cars args))))
447
707
      :hints(("Goal" :in-theory (union-theories (theory 'minimal-theory)
448
708
                                                '((:definition ,trigger))))))
449
 
    
 
709
 
450
710
    ;; Next we create a theorem that rewrites function to our trigger in more
451
711
    ;; appropriate circumstances .. when the term is the conclusion of the goal.
452
712
    (defthm ,name
460
720
                      (,trigger ,@(strip-cars args))))
461
721
      :hints(("Goal" :in-theory (union-theories (theory 'minimal-theory)
462
722
                                                '((:definition ,trigger))))))
463
 
    
 
723
 
464
724
    ;; Finally we add our pattern to the pick a point rules database.
465
725
    (table adviser-table :pick-a-point-rules
466
726
           (let ((rules (pick-a-point-rules world)))
488
748
;; for instances of a trigger, and if it sees one, we will try to provide a
489
749
;; functional instantiation hint.  Our computed hint function is called as ACL2
490
750
;; is working to simplify terms, and it is allowed to examine the current
491
 
;; clause.  
 
751
;; clause.
492
752
;;
493
753
;; Terminology: A clause is a list of disjuncts, e.g.,
494
754
;;
527
787
                             (caadr literal)
528
788
                           (car literal))
529
789
                       nil)))
530
 
      (let ((match (and 
531
 
                    ;; Eric and Doug added this check, since we got an error 
 
790
      (let ((match (and
 
791
                    ;; Eric and Doug added this check, since we got an error
532
792
                    ;; when matchsym was a lambda expression:
533
793
                    (symbolp matchsym)
534
794
                    (ACL2::symbol-btree-lookup matchsym rules))))
535
 
        (pick-a-point-trigger-harvester 
 
795
        (pick-a-point-trigger-harvester
536
796
         (cdr clause)
537
797
         rules
538
798
         (if match (cons literal acc-lit) acc-lit)
539
799
         (if match (cons match acc-rule) acc-rule))))))
540
800
 
541
 
      
 
801
 
542
802
 
543
803
;; If we find any matches, we need to provide appropriate hints.  To do this,
544
804
;; we need to provide values for the hypotheses and arguments.
545
 
;; 
 
805
;;
546
806
;; In order to compute the hypotheses, we first remove from the clause all of
547
807
;; our trigger terms.  This is easy to do, we can just take the
548
808
;; set-difference-equal of the clause with the acc-lit accumulator found above.
560
820
  (declare (xargs :mode :program))
561
821
  (if (endp literals)
562
822
      nil
563
 
    (if (equal (caar literals) 'not)  
 
823
    (if (equal (caar literals) 'not)
564
824
        ;; don't create ugly double not's
565
825
        (cons (second (car literals))
566
826
              (negate-literals (cdr literals)))
579
839
 
580
840
;; Here's an example:
581
841
;;
582
 
;; ADVISER !>(andify-literals 
583
 
;;  (negate-literals '((foo x) 
584
 
;;                     (foo y) 
585
 
;;                     (not (foo a)) 
 
842
;; ADVISER !>(andify-literals
 
843
;;  (negate-literals '((foo x)
 
844
;;                     (foo y)
 
845
;;                     (not (foo a))
586
846
;;                     (not (foo b)))))
587
847
;; (AND (NOT (FOO X))
588
848
;;      (NOT (FOO Y))
596
856
;; as arguments the matching literal and rule, and the hypotheses that were
597
857
;; build using the above strategy.
598
858
;;
599
 
;; Rule is expected to be a parsed rule, which means that it is an alist of 
 
859
;; Rule is expected to be a parsed rule, which means that it is an alist of
600
860
;; components.  We need to build a functional instance hint.  The theorem
601
861
;; to instantiate is stored in :driver.  The name of the generic hypotheses
602
862
;; function is stored in :hyps.  We also need to provide instantiations for
609
869
      nil
610
870
    (cons `(,(car arg-names)
611
871
            (lambda () ,(car actuals)))
612
 
          (make-functional-instance-pairs (cdr arg-names) 
 
872
          (make-functional-instance-pairs (cdr arg-names)
613
873
                                          (cdr actuals)))))
614
874
 
615
875
(defun build-hint (literal rule hyps)
637
897
                       acc))))
638
898
 
639
899
(defconst *pick-a-point-message*
640
 
  "~|~%[Adviser]: We suspect this conjecture sould be proven by functional ~
 
900
  "~|~%[Adviser]: We suspect this conjecture should be proven by functional ~
641
901
  instantiation of the following, generic theorems: ~x0.  We only make this ~
642
902
  suggestion because of following triggering rules: ~x1.  If you do not want ~
643
903
  to use functional instantiation here, you should disable these triggering ~
649
909
      nil
650
910
    (cons (cdr (assoc :driver (car rules)))
651
911
          (get-thms (cdr rules)))))
652
 
              
 
912
 
653
913
(defun get-names (rules)
654
914
  (declare (xargs :mode :program))
655
915
  (if (endp rules)
663
923
      nil
664
924
    (let ((lit (first literals)))
665
925
      (if (equal (car lit) 'not)
666
 
          (cons (cadr lit) 
 
926
          (cons (cadr lit)
667
927
                (build-expand-hint (rest literals)))
668
928
        (cons lit (build-expand-hint (rest literals)))))))
669
929
 
683
943
  (let ((rules (pick-a-point-rules world)))
684
944
    (if (null rules)
685
945
        nil
686
 
      (mv-let (literals rules) 
 
946
      (mv-let (literals rules)
687
947
              (pick-a-point-trigger-harvester clause rules nil nil)
688
948
              (if (null literals)
689
949
                  nil
691
951
                       (hyps (andify-literals
692
952
                              (negate-literals others)))
693
953
                       (use   `(:use ,(build-hints literals rules hyps nil)))
694
 
                       (hints `(:computed-hint-replacement 
 
954
                       (hints `(:computed-hint-replacement
695
955
                                ('(:computed-hint-replacement
696
956
                                   ((adviser-default-hint id clause world stable-under-simplificationp)) ; ',(current-theory :here)))
697
957
                                   ,@use))
708
968
  (if (not stable)
709
969
      nil
710
970
;;     (if theory
711
 
;;      `(:computed-hint-replacement 
 
971
;;      `(:computed-hint-replacement
712
972
;;        ((adviser-default-hint id clause world stable-under-simplificationp 'nil))
713
973
;;        :expand nil
714
974
;;        :in-theory ',theory)
717
977
 
718
978
(add-default-hints!
719
979
 '((adviser-default-hint id clause world stable-under-simplificationp))) ;; 'nil)))
720
 
          
721
 
           
 
980
 
 
981
 
722
982
 
723
983
 
724
984
 
728
988
;;
729
989
;; ----------------------------------------------------------------------------
730
990
 
731
 
(defconst *supported-rule-classes* 
 
991
(defconst *supported-rule-classes*
732
992
  '(:pick-a-point))
733
993
 
734
994
(defmacro defadvice (name term &key rule-classes)
735
995
  (if (and (consp rule-classes)
736
996
           (member (car rule-classes) *supported-rule-classes*))
737
997
      (case (car rule-classes)
738
 
        (:pick-a-point 
 
998
        (:pick-a-point
739
999
         (pick-a-point-rule-defadvice name term rule-classes))
740
1000
        (otherwise
741
 
         (er hard 'defadvice 
 
1001
         (er hard 'defadvice
742
1002
             ":rule-classes ~x0 is allegedly supported, but has not ~
743
1003
             been implemented!~%" (car rule-classes))))
744
 
    (er hard 'defadvice 
 
1004
    (er hard 'defadvice
745
1005
        ":rule-classes must be a list, e.g., (:pick-a-point :driver thm), ~
746
 
        but is ~x0.~%" rule-classes)))
747
 
 
 
1006
        but is ~x0.~%" rule-classes)))
 
 
b'\\ No newline at end of file'