hanoi

(in-package "HANOI")

(defun mem
  (e x)
  (if (consp x)
    (if (equal e (car x))
      x
      (mem e (cdr x)))
    nil))

(defun app
  (x y)
  (if (consp x)
    (cons (car x) (app (cdr x) y))
    y))

(defun del
  (e x)
  (if (consp x)
    (if (equal e (car x))
      (cdr x)
      (cons (car x) (del e (cdr x))))
    nil))

(defun perm
  (x y)
  (if (consp x)
    (and (mem (car x) y)
      (perm (cdr x)
        (del (car x) y)))
    (not (consp y))))

(defthm perm-opener
  (equal (perm (list a b c) '(0 1 2))
    (and (integerp a)
      (<= 0 a)
      (<= a 2)
      (integerp b)
      (<= 0 b)
      (<= b 2)
      (integerp c)
      (<= 0 c)
      (<= c 2)
      (not (equal a b))
      (not (equal a c))
      (not (equal b c)))))

(defthm app-assoc
  (equal (app (app a b) c)
    (app a (app b c))))

(defthm app-right-id
  (implies (true-listp x)
    (equal (app x nil) x)))

(defun get
  (n x)
  (if (zp n)
    (car x)
    (get (- n 1) (cdr x))))

(defun put
  (v n x)
  (if (zp n)
    (cons v (cdr x))
    (cons (car x)
      (put v (- n 1) (cdr x)))))

(defthm get-put
  (implies (and (natp i) (natp j))
    (equal (get i (put v j x))
      (if (equal i j)
        v
        (get i x)))))

(defthm put-get
  (implies (and (equal x (get n s))
      (natp n)
      (< n (len s)))
    (equal (put x n s) s)))

(defthm put-put-1
  (implies (and (natp i)
      (natp j)
      (not (equal i j)))
    (equal (put v
        i
        (put u j s))
      (put u
        j
        (put v i s))))
  :rule-classes ((:rewrite :loop-stopper ((i j)))))

(defthm put-put-2
  (equal (put v
      i
      (put w i s))
    (put v i s)))

(defthm true-listp-put
  (implies (and (natp n)
      (< n (len x)))
    (equal (true-listp (put v n x))
      (true-listp x))))

(defthm len-put
  (implies (and (natp n)
      (< n (len x)))
    (equal (len (put v n x))
      (len x))))

(defun push (e x) (cons e x))

(defun pop (x) (cdr x))

(defun top (x) (car x))

(defun h
  (i j k n)
  (if (zp n)
    nil
    (app (h i k j (- n 1))
      (cons (list 'move i k)
        (h j i k (- n 1))))))

(defun hanoi (n) (h 0 1 2 n))

(defun a (m) (get 1 m))

(defun b (m) (get 2 m))

(defun legal-syntaxp
  (m)
  (and (true-listp m)
    (equal (car m) 'move)
    (equal (len m) 3)
    (mem (a m) '(0 1 2))
    (mem (b m) '(0 1 2))
    (not (equal (a m) (b m)))))

(defun legal-movep
  (m s)
  (and (legal-syntaxp m)
    (consp (get (a m) s))
    (if (consp (get (b m) s))
      (< (car (get (a m) s))
        (car (get (b m) s)))
      t)))

(defun do-move
  (m s)
  (let ((stacka (get (a m) s)) (stackb (get (b m) s)))
    (put (pop stacka)
      (a m)
      (put (push (top stacka) stackb)
        (b m)
        s))))

(defun play
  (moves s)
  (if (consp moves)
    (if (legal-movep (car moves) s)
      (play (cdr moves)
        (do-move (car moves) s))
      nil)
    s))

(defun tower
  (n)
  (if (zp n)
    nil
    (app (tower (- n 1)) (list n))))

(defthm examples
  (and (equal (play (hanoi 7)
        (list (tower 7) nil nil))
      (list nil nil (tower 7)))
    (equal (play (hanoi 2)
        (list (tower 3) nil '(4)))
      '((3) nil (1 2 4)))
    (equal (play (hanoi 3) '((1 2 3) (0) nil))
      nil)))

(defthm true-listp-tower
  (true-listp (tower n)))

(defthm play-app
  (equal (play (app moves1 moves2)
      s)
    (play moves2
      (play moves1 s))))

(defun big-tops
  (a b c n s)
  (and (or (endp (get a s))
      (< n (car (get a s))))
    (or (endp (get b s))
      (< n (car (get b s))))
    (or (endp (get c s))
      (< n (car (get c s))))))

(defun induction-hint
  (a b c n s)
  (if (zp n)
    (list a b c n s)
    (list (induction-hint a
        c
        b
        (- n 1)
        (put (push n (get a s))
          a
          s))
      (induction-hint b
        a
        c
        (- n 1)
        (put (push n (get c s))
          c
          s)))))

(defthm h-lemma
  (implies (and (natp n)
      (true-listp s)
      (equal (len s) 3)
      (perm (list a b c) '(0 1 2))
      (big-tops a
        b
        c
        n
        s))
    (equal (play (h a b c n)
        (put (app (tower n) (get a s))
          a
          s))
      (put (app (tower n) (get c s))
        c
        s)))
  :rule-classes nil
  :hints (("Goal" :induct (induction-hint a
       b
       c
       n
       s))))

(defthm hanoi-correct
  (equal (play (hanoi n)
      (list (tower n) nil nil))
    (list nil nil (tower n)))
  :hints (("Goal" :use (:instance h-lemma
       (a 0)
       (b 1)
       (c 2)
       (s (list nil nil nil))))))