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
|
; (certify-book "convert-perm-to-how-many")
; See Exercise 11.50 in CAR.
; /projects/acl2/v3-1/acl2-sources/books/textbook/chap11/how-many-soln2.lisp
(in-package "ACL2")
(include-book "perm")
(defun how-many (e x)
(cond
((endp x)
0)
((equal e (car x))
(1+ (how-many e (cdr x))))
(t
(how-many e (cdr x)))))
; We aim to prove that (perm x y) is the same as checking that for all e,
; (how-many e x) is (how-many e y). We can do that by defining the function
; (perm-counter-example x y) -- the counterexample generator -- that finds an e that occurs a
; different number of times in x than in y.
; Thus, the following definition is modeled after the definition of perm.
(defun perm-counter-example (x y)
(cond ((atom x)
(car y))
((not (memb (car x) y))
(car x))
(t (perm-counter-example (cdr x) (rm (car x) y)))))
; The right-hand side of the equal term in the last hypothesis suggests the
; following rewrite rule. (We return to this issue later.)
(defthm how-many-rm
(implies (not (equal a b))
(equal (how-many a (rm b x))
(how-many a x))))
(defthm not-memb-implies-rm-is-no-op
(implies (and (not (memb a x))
(true-listp x))
(equal (rm a x) x)))
(defthm true-listp-rm
(implies (true-listp x)
(true-listp (rm a x)))
:rule-classes :type-prescription)
(defthm not-memb-implies-how-many-is-0
(implies (not (memb a x))
(equal (how-many a x)
0)))
(defthm how-many-rm-general
(equal (how-many a (rm b x))
(if (and (equal a b) (memb a x))
(1- (how-many a x))
(how-many a x))))
(defthm perm-counter-example-is-counterexample-for-true-lists
(implies (and (true-listp x)
(true-listp y))
(equal (perm x y)
(equal (how-many (perm-counter-example x y) x)
(how-many (perm-counter-example x y) y))))
:rule-classes nil)
(defun tlfix (x)
(if (endp x)
nil
(cons (car x) (tlfix (cdr x)))))
(defthm perm-tlfix
(perm (tlfix x) x))
(defthm perm-counter-example-tlfix-1
(equal (perm-counter-example (tlfix x) y)
(perm-counter-example x y)))
(defthm rm-tlfix
(equal (rm a (tlfix x))
(tlfix (rm a x))))
(defthm memb-tlfix
(equal (memb a (tlfix x))
(memb a x)))
(defthm perm-counter-example-tlfix-2
(equal (perm-counter-example x (tlfix y))
(perm-counter-example x y)))
(defthm how-many-tlfix
(equal (how-many a (tlfix x))
(how-many a x)))
(defthm convert-perm-to-how-many
(equal (perm x y)
(equal (how-many (perm-counter-example x y) x)
(how-many (perm-counter-example x y) y)))
:hints (("Goal" :use
((:instance perm-counter-example-is-counterexample-for-true-lists
(x (tlfix x))
(y (tlfix y)))))))
|
