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
|
<html>
<head><title>DEFUN-SK-EXAMPLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>DEFUN-SK-EXAMPLE</h3>a simple example using <code><a href="DEFUN-SK.html">defun-sk</a></code>
<pre>Major Section: <a href="DEFUN-SK.html">DEFUN-SK</a>
</pre><p>
<p>
The following example illustrates how to do proofs about functions defined
with <code><a href="DEFUN-SK.html">defun-sk</a></code>. The events below can be put into a certifiable book
(see <a href="BOOKS.html">books</a>). The example is contrived and rather silly, in that it shows
how to prove that a quantified notion implies itself, where the antecedent
and conclusion are defined with different <code><a href="DEFUN-SK.html">defun-sk</a></code> events. But it
illustrates the formulas that are generated by <code><a href="DEFUN-SK.html">defun-sk</a></code>, and how to use
them. Thanks to Julien Schmaltz for presenting this example as a challenge.
<pre>
(in-package "ACL2")<p>
(encapsulate
(((p *) => *)
((expr *) => *))<p>
(local (defun p (x) x))
(local (defun expr (x) x)))<p>
(defun-sk forall-expr1 (x)
(forall (y) (implies (p x) (expr y))))<p>
(defun-sk forall-expr2 (x)
(forall (y) (implies (p x) (expr y)))))<p>
; We want to prove the theorem my-theorem below. What axioms are there that
; can help us? If you submit the command<p>
; :pcb! forall-expr1<p>
; then you will see the following two key events. (They are completely
; analogous of course for FORALL-EXPR2.)<p>
#|
(DEFUN FORALL-EXPR1 (X)
(LET ((Y (FORALL-EXPR1-WITNESS X)))
(IMPLIES (P X) (EXPR Y))))<p>
(DEFTHM FORALL-EXPR1-NECC
(IMPLIES (NOT (IMPLIES (P X) (EXPR Y)))
(NOT (FORALL-EXPR1 X)))
:HINTS
(("Goal" :USE FORALL-EXPR1-WITNESS)))
|#<p>
; We see that the latter has value when FORALL-EXPR1 occurs negated in a
; conclusion, or (therefore) positively in a hypothesis. A good rule to
; remember is that the former has value in the opposite circumstance: negated
; in a hypothesis or positively in a conclusion.<p>
; In our theorem, FORALL-EXPR2 occurs positively in the conclusion, so its
; definition should be of use. We therefore leave its definition enabled,
; and disable the definition of FORALL-EXPR1.<p>
#|
(thm
(implies (and (p x) (forall-expr1 x))
(forall-expr2 x))
:hints (("Goal" :in-theory (disable forall-expr1))))<p>
; which yields this unproved subgoal:<p>
(IMPLIES (AND (P X) (FORALL-EXPR1 X))
(EXPR (FORALL-EXPR2-WITNESS X)))
|#<p>
; Now we can see how to use FORALL-EXPR1-NECC to complete the proof, by
; binding y to (FORALL-EXPR2-WITNESS X).<p>
; We use defthmd below so that the following doesn't interfere with the
; second proof, in my-theorem-again that follows.
(defthmd my-theorem
(implies (and (p x) (forall-expr1 x))
(forall-expr2 x))
:hints (("Goal"
:use ((:instance forall-expr1-necc
(x x)
(y (forall-expr2-witness x)))))))<p>
; The following illustrates a more advanced technique to consider in such
; cases. If we disable forall-expr1, then we can similarly succeed by having
; FORALL-EXPR1-NECC applied as a :rewrite rule, with an appropriate hint in how
; to instantiate its free variable. See :doc hints.<p>
(defthm my-theorem-again
(implies (and (P x) (forall-expr1 x))
(forall-expr2 x))
:hints (("Goal"
:in-theory (disable forall-expr1)
:restrict ((forall-expr1-necc
((y (forall-expr2-witness x))))))))
</pre>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
