;;; 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))))