blob: 98f5e649c96a7ddd1dcd77addaf59600ae096fb5 (
about) (
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
|
;;; palindrome-sandwich.lisp
;;; 任意の真リスト x, y について
;;; x を y と y の逆順のリスト (rev y) で連結したものが回文であることと
;;; x が回文であることが同値であることを示す
;;; (defthm palindrome-sandwich
;;; (implies (and (true-listp x)
;;; (true-listp y))
;;; (equal (palindromep (app y (app x (rev y))))
;;; (palindromep x))))
;; 二つのリストを連結する
(defun app (x y)
(if (endp x)
y
(cons (car x)
(app (cdr x) y))))
;; 逆順のリストを返す
(defun rev (x)
(if (endp x)
nil
(app (rev (cdr x)) (list (car x)))))
;; 回文かどうかを判定する
(defmacro palindromep (x)
`(equal (rev ,x) ,x))
;; (app x y) が真リストであることと y が真リストであることは同値
(defthm true-listp-app
(equal (true-listp (app x y))
(true-listp y)))
;; x が真リストなら (rev x) も真リスト
(defthm true-listp-rev
(implies (true-listp x)
(true-listp (rev x))))
;; app の結合法則
(defthm associativity-of-app
(equal (app (app x y) z)
(app x (app y z))))
;; nil を連結しても変わらない
(defthm app-nil
(implies (true-listp x)
(equal (app x nil) x)))
;; (rev (app x y)) と (app (rev y) (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)))
;; (app x y) の長さは x の長さと y の長さの和
(defthm len-app
(equal (len (app x y))
(+ (len x) (len y))))
;; 長さの異なるリストは異なる
(defthm not-euqal-lens-implies-not-equal
(implies (not (equal (len x) (len y)))
(not (equal x y))))
;; sandwich-equal の補助定理
;; 真リスト x が nil でないとき (app x y) は y でない
(defthm sandwich-equal-lemma
(implies (and (consp x)
(true-listp x))
(not (equal (app x y)
y))))
;; sandwich-equal の証明に使用する帰納法
(defun sandwich-equal-induction (x y)
(cond
((endp x) y)
((endp y) x)
(t (sandwich-equal-induction (cdr x) (cdr y)))))
;; 同じものに挟まれたものが等しいことは
;; 挟まれたものが等しいことを意味する
(defthm sandwich-equal
(implies (and (true-listp x)
(true-listp y1)
(true-listp y2)
(true-listp z))
(equal (equal (app x (app y1 z))
(app x (app y2 z)))
(equal y1 y2)))
:hints (("Goal" :induct (sandwich-equal-induction y1 y2))))
;; 任意の真リスト x, y について
;; y を x と x の逆順のリスト (rev x) で連結したものが回文であることと
;; y が回文であることは同値である
(defthm palindrome-sandwich
(implies (and (true-listp x)
(true-listp y))
(equal (palindromep (app y (app x (rev y))))
(palindromep x))))
|
