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
|
; A certain recursive equation renders ACL2 inconsistent.
; Copyright (C) 2001 John R. Cowles, University of Wyoming
; This book is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This book is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by:
; John Cowles
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071-3682 U.S.A.
; Fall 2001.
; Last modified 28 September 2001.
; Modified May 2002 by Robert Krug to account for v2-7 changes. See also
; bad-def1.lisp for an alternate version.
#|
This is an example, due Manolious and Moore, showing there is NO
ACL2 function g that satisfies the recursive equation
(equal (g n)
(if (equal n 0)
nil
(cons nil (g (- n 1))))).
The proof is by contradiction: Adding the above equation as an axiom
allows the proof of NIL, which is ACL2's version of FALSE.
This proof follows the outline of such a proof given by Manolious
and Moore.
|#
(in-package "ACL2")
(defstub
g (*) => *)
(defaxiom
g-axiom
(equal (g n)
(if (equal n 0)
nil
(cons nil (g (- n 1)))))
:rule-classes nil)
(defthm
len-cons
(equal (len (cons x y))(+ 1 (len y))))
(defthm
len-g->-k
(implies (and (not (equal n 0))
(> (len (g (- n 1)))
(- k 1)))
(> (len (g n)) k))
:hints (("Goal"
:use g-axiom)))
(set-irrelevant-formals-ok :warn)
(defun
induct-hint (k n)
(if (zp k)
t
(induct-hint (- k 1)(- n 1))))
(defthm len-g-=-0-==>-n-=-0
(equal (equal (len (g n)) 0)
(equal n 0))
:hints (("Goal" :use g-axiom)))
(defthm
g-at-neg-input
(implies (and (< n 0)
(integerp k))
(> (len (g n)) k))
:rule-classes nil
:hints (("goal"
:induct (induct-hint k n))))
(defthm
contradiction!!
nil
:rule-classes nil
:hints (("Goal"
:use (:instance
g-at-neg-input
(n -1)
(k (len (g -1)))))))
|
