From 658812d37e3be083623a63c9839ac056451df1cd Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Mon, 19 Jul 2021 09:42:54 +0900
Subject: Add `palindrome-sandwich.lisp` file.

---
 palindrome-sandwich.lisp | 104 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 104 insertions(+)
 create mode 100644 palindrome-sandwich.lisp

(limited to 'palindrome-sandwich.lisp')

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))))
-- 
cgit v1.2.3