aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--palindrome-sandwich.lisp104
1 files changed, 104 insertions, 0 deletions
diff --git a/palindrome-sandwich.lisp b/palindrome-sandwich.lisp
new file mode 100644
index 0000000..78a9370
--- /dev/null
+++ b/palindrome-sandwich.lisp
@@ -0,0 +1,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-hyp
+ (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))))