blob: 3bfaa9484e5d0f84f134132464a1eb6d04cd73d9 (
plain)
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
138
139
140
141
142
143
|
;; P01 (*) Find the last box of a list.
(defun my-last (x)
(declare (xargs :guard (and (true-listp x)
(consp x))))
(if (endp (cdr x))
x
(my-last (cdr x))))
(defthm theorem-of-my-last
(implies (and (true-listp x)
(consp x))
(equal (list (nth (1- (len x)) x))
(my-last x))))
;; P02 (*) Find the last but one box of a list.
(defun my-butlast (x)
(declare (xargs :guard (and (true-listp x)
(consp x))))
(if (endp (cdr x))
nil
(cons (car x)
(my-butlast (cdr x)))))
(defthm my-butlast-my-last
(implies (and (true-listp x)
(consp x))
(equal (append (my-butlast x) (my-last x))
x)))
;; P03 (*) Find the K'th element of a list.
(defun element-at (x i)
(declare (xargs :guard (and (true-listp x)
(natp i)
(< i (len x)))))
(if (zp i)
(car x)
(element-at (cdr x) (1- i))))
(defthm element-at-nil
(equal (element-at nil i)
nil))
(defthm elment-at-equal-nth
(equal (element-at x i)
(nth i x)))
;; P04 (*) Find the number of elements of a list.
(defun my-len (x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
0
(+ 1 (my-len (cdr x)))))
(defun rev-iota (n)
(if (zp n)
nil
(cons (1- n) (rev-iota (1- n)))))
(defthm my-len-rev-iota
(implies (natp n)
(equal (my-len (rev-iota n))
n)))
;; P05 (*) Reverse a list.
(defun app (x y)
(declare (xargs :guard (and (true-listp x)
(true-listp y))))
(if (endp x)
y
(cons (car x)
(app (cdr x) y))))
(defthm true-listp-app
(implies (true-listp y)
(true-listp (app x y))))
(defun rev (x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
nil
(app (rev (cdr x))
(list (car x)))))
(defun revapp (x y)
(declare (xargs :guard (and (true-listp x)
(true-listp y))))
(if (endp x)
y
(revapp (cdr x)
(cons (car x) y))))
(defmacro my-reverse (x)
`(revapp ,x nil))
(defthm associativity-of-app
(equal (app (app x y) z)
(app x (app y z))))
(defthm app-rev-equal-revapp
(equal (revapp x y)
(app (rev x) y)))
(defthm my-reverse-equal-rev
(equal (my-reverse x)
(rev x)))
;; P06 (*) Find out whether a list is a palindrome.
(defmacro palindromep (x)
`(equal (my-reverse ,x) ,x))
(defthm app-nil
(implies (true-listp x)
(equal (app x nil)
x)))
(defthm true-listp-rev
(implies (true-listp x)
(true-listp (rev x))))
(defthm rev-app
(implies (true-listp y)
(equal (rev (app x y))
(app (rev y) (rev x)))))
(defthm rev-rev
(implies (true-listp x)
(equal (rev (rev x))
x)))
(defthm sandwich-palindrome
(implies (and (true-listp y)
(palindromep x))
(palindromep (app y (app x (rev y))))))
;; P07 (**) Flatten a nested list structure.
(defun flatten (x)
(cond
((endp x) x)
((consp (car x))
(app (flatten (car x))
(flatten (cdr x))))
(t (cons (car x)
(flatten (cdr x))))))
|
