|
|
|---|
|
|
|
|---|
Compute hints based on a term that gets simplified along with the rest of the goal.
When a theory doesn't lend itself well to rewriting, you might just use a lot of hints to get through a proof. But this can become brittle and unwieldy: you might get through the proof by piling on :use hints, but if that proof later fails it can be very difficult to debug. An unstructured pile of hints doesn't give many clues for how the proof is supposed to work and how to fix it if it breaks. Use-termhint provides a different way to structure proofs that require a lot of hints. Also see termhint-seq for a way to give hints in sequence throughout a termhint term.
As a very simple example, suppose that we have axioms ax1 through ax3, and we want to prove th:
(defstub p1 (x) t) (defstub p2 (x y z) t) (defstub p3 (x y) t) (defstub p4 (x) t) (defstub b (x) t) (defstub c (x) t) (defstub d (x) t) (defaxiom t1 (implies (p1 a) (p2 a (b a) (c a)))) (defaxiom t2 (implies (p2 a b c) (p3 a (d c)))) (defaxiom t3 (implies (p3 a d) (p4 a))) (defthm th (implies (p1 a) (p4 a)))
We could do this using some unstructured :use hints (in this case perhaps only one would suffice). But we can be more explicit about how the proof precedes by using use-termhint, as follows.
First, we write a function that follows the process of the proof and provides hints at certain endpoints:
;; A computed hint to use later -- see below. (defun my-use-t3-inst-hint (d) `(:use ((:instance t3 (d ,d))))) (defun hint-for-th (a) (b* ((b (b a)) (c (c a)) ;; The first thing that we want to conclude is (p2 a b c) for some b, c, ;; namely, the ones given by t1. ((unless (p2 a b c)) ;; The unless here causes a case split. In one case, we assume (p2 a ;; b c). In the other case, we arrive here, and we return a hint that ;; proves the subgoal by proving (p2 a b c). This hint is ;; double-quoted because in general we return the quotation of a ;; computed hint expression; in this case, the computed hint we want ;; is '(:use t1). ''(:use t1)) ;; Now we can assume (p2 a b c). Next we want to show (p3 a d) for some d, ;; by t2. (d (d c)) ((unless (p3 a d)) ;; In the case where we're assuming (not (p3 a d)), prove it by using t2. ;; Notice the uses of (hq ...) below: these are specially processed by ;; use-termhint, so that (hq b) will be replaced by whatever the term ;; bound to b has been rewritten to. This will produce the hint: ;; :use ((:instance t2 ;; (b (b a)) ;; (c (c a)))) ;; But notice that we don't have to write out (b a) and (c a); instead we ;; use the (hq ...) of variables bound to those terms. `'(:use ((:instance t2 (b ,(hq b)) (c ,(hq c))))))) ;; Finally, we have (p3 a d), so we just use t3 to get our conclusion. ;; We could use the following: ;; `'(:use ((:instance t3 (d ,(hq d))))) ;; but instead we'll do this, just to show that you can use arbitrary ;; computed hints: `(my-use-t3-inst-hint ',(hq d))))
Now, we submit th with the following hints:
(defthm th (implies (p1 a) (p4 a)) :hints (("goal" :in-theory (disable t1 t2 t3)) (use-termhint (hint-for-th a))))
which suffices to prove it.
Use-termhint produces a sequence of two computed hints: an initial :use hint
that adds a
In the above example, the hypothesis added to the goal is
The
Other quote-like symbols can be added to this list. In particular, it may be useful to add symbols that have certain congruences or rewriting properties. For example, if you want to expand a certain function call and that function has a congruence on its first argument, you may want to introduce an HQ-like symbol that has the same congruence:
(defun my-hq (x) (my-fix x)) (defcong my-equiv equal (my-hq x) 1) (in-theory (disable my-hq (my-hq) (:t my-hq))) (termhint-add-quotesym my-hq) (defthm ... :hints ((use-termhint (let ((arg ...)) `(:expand ((my-fn ,(my-hq arg))))))))