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
|
; Copyright (C) 2022, Regents of the University of Texas
; Written by Matt Kaufmann and J Moore
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; Many thanks to ForrestHunt, Inc. for supporting the preponderance of this
; work, and for permission to include it here.
; Justification of DO$ Induction
; aka ``the hairbrained induction scheme''
; Suppose you're trying to prove a conjecture p by induction using an
; unverified induction machine, i.e., one in which the measure has not yet been
; shown to decrease. Clearly, the induction proof obligations have to include
; a proof that the measure decreaes. This file shows that you can add an
; arbitrary hypothesis, q, as a hypothesis to that measure theorem, provided
; you can prove that p holds when q is false.
; The motivation for this idea stems from the induction suggested by the loop$
; in
; (defun foo (i)
; (declare (xargs :guard (natp i)))
; (loop$ with i = i
; do
; :guard (natp i)
; (if (equal i 0) (return t) (setq i (- i 1)))))
; This function can be guard verified (proving termination) and can be proved
; to return t when (natp i).
; But consider the induction suggested by the loop$: induct on i with base case
; i=0 and an induction step i/=0 with inductive hypothesis for i-1. Of course
; that can't be proved to terminate. Note futher that as soon as
; (implies (natp i)
; (loop$ with i = i
; do
; :guard (natp i)
; (if (equal i 0) (return t) (setq i (- i 1)))))
; is simplified the :guard (natp i) is eliminated, being logically irrelevant.
; To prove termination, specifically, to prove
; (L< (LEX-FIX (- i 1))
; (LEX-FIX i))
; we need more than just (not (equal i 0)). We need (natp i).
; But the recursive hint function obtained by decompiling the DO$ generated by
; the loop$ is
; (defun hint-fn (i)
; (if (equal i 0)
; t
; (hint-fn (- i 1))))
; and there is no clue that (natp i) should be available.
; Hence, we consider the hairbrained scheme of freely inventing a q, namely
; (natp i), and changing the termination goal from
; (implies (not (equal i 0)) (l< (lex-fix (- i 1)) (lex-fix i)))
; to
; (implies (and (natp i) (not (equal i 0))) (l< (lex-fix (- i 1)) (lex-fix i)))
; So there are two questions. The first is whether this is legal and how else
; is q involved in the scheme? The second is how do we choose q? The second
; question is heuristic.
; Without loss of generality we imagine a simple induction machine in which
; there is one variable, x, one base case recognized by (basep x), one
; induction step recognized by (not (basep x)) with one induction hypothesis
; given by {x <-- (stp x)}. (Here ``stp'' is short for ``step,'' which is in
; the main Lisp package and can't be claimed here.)
; We also assume that the well-founded-relation is L< on the domain LEXP and
; that the measure, m is lex-fix'd before being used. This means we do not
; have to prove that m satisfies lexp every time we induct like this. We just
; prove it once, below.
(in-package "ACL2")
(defthm lexp-lex-fix
(lexp (lex-fix x))
:hints (("Goal" :in-theory (enable nfix-list)))
:otf-flg t)
; So now we'll posit four conditions, labeled [a], [b], [c], and [d], and show
; that if you prove all four then you have proved (p x).
; [a] is our modified termination conjecture with q as a hyp.
; [b] and [c] are the base case and induction step suggested by the
; impoverished induction machine.
; [d] shows that p holds when q doesn't.
(encapsulate ((basep (x) t)
(stp (x) t)
(p (x) t)
(m (x) t)
(q (x) t))
(local (defun basep (x) (equal x nil)))
(local (defun stp (x) (cdr x)))
(local (defun p (x) (declare (ignore x)) t))
(local (defun m (x) (acl2-count x)))
(local (defun q (x) (true-listp x)))
(defthm [a] (implies (and (q x) (not (basep x)))
(l< (lex-fix (m (stp x)))
(lex-fix (m x)))))
(defthm [b] (implies (basep x) (p x)))
(defthm [c] (implies (and (not (basep x)) (p (stp x))) (p x)))
(defthm [d] (implies (not (q x)) (p x))))
; To admit this, we use [a].
(defun induction-hint (x)
(declare (xargs :measure (lex-fix (m x))
:well-founded-relation l<
:hints (("Goal" :in-theory (disable lexp lex-fix l<)))))
(if (q x)
(if (basep x)
(list x)
(induction-hint (stp x)))
(list x)))
; (p x) follows from [b], [c], and [d].
(defthm therefore-p
(p x)
:hints (("Goal" :induct (induction-hint x))))
; The Essay on DO$ Induction and the Selection of Q explains our heuristics for
; choosing q.
|
