; 1.  In this problem you may need the following familiar functions
; and lemmas.  Note that rev-rev, below, is stated more powerfully
; than we normally see it. You may, of course, define other functions
; and prove other lemmas.  You may, of course, use arithmetic.

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

(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))

(defthm len-app
  (equal (len (app a b))
         (+ (len a) (len b))))

(defthm len-rev
  (equal (len (rev x))
         (len x)))

(defthm true-listp-rev
  (true-listp (rev x)))

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

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

(defthm rev-app
  (equal (rev (app a b))
         (app (rev b) (rev a))))

(defthm rev-rev
  (equal (rev (rev x))
         (app x nil)))

; Ok, here's the problem.  Given:

(defun xtr (map lst)
  (if (consp map)
      (cons (nth (car map) lst)
            (xtr (cdr map) lst))
    nil))

(defun nats (n)
  (if (zp n)
      nil
    (cons (- n 1) (nats (- n 1)))))

; Prove:

; (defthm xtr-nats
;   (equal (xtr (nats (len x)) x) (rev x)))

; Be sure to prove every lemma you need other than the ones noted
; above.

; Here is my answer.

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

(include-book "arithmetic/top-with-meta" :dir :system)

(defthm nth-app
  (implies (natp n)
           (equal (nth n (app x y))
                  (if (< n (len x))
                      (nth n x)
                    (nth (- n (len x)) y)))))


(defthm xtr-nats-gen
  (equal (xtr (nats (len x)) (app (rev x) y))
         (app x nil))
  :hints (("Goal" :induct (rev1 x y)))
  :rule-classes nil)

(defun marker (x)
  (if (consp x)
      (marker (cdr x))
    x))
  
(defthm app-marker
  (equal (app x (marker x)) x))

(defthm xtr-nats
  (equal (xtr (nats (len x)) x) (rev x))
  :hints (("Goal" :use (:instance xtr-nats-gen
                                  (x (rev x))
                                  (y (marker x))))))


; 2.  (defun f (x) (f x)) is an example of a definition that is
; inadmissible.  But it is satisfied by an infinite number of
; functions.  (We say a definition for f is satisfied by a function g
; when the definitional axiom for f is a theorem when all calls of f
; are replaced by calls of g.)  For example, the definitional axiom
; for the defun above is (equal (f x) (f x)) and this is satisfied by
; any function of one argument.

; Show an inadmissible definition of f that is satisfied by exactly
; two admissible functions.  Suppose the functions in question are
; named g and h.  Show the definitions of g and h.  You need not show
; any proofs.

; Here is my answer.

; My inadmissible defun will be
; (defun f (x) (if (f x) t nil))

; Here are two functions that satisfy the definitional equation above.

(defun g (x) (declare (ignore x)) t)  
(defun h (x) (declare (ignore x)) nil)  

; You'd get full credit if you did just that much.  Below I show that
; my answers are right.

; Here I prove that g and h both satisfy the equation.

(defthm g-and-h-satisfy-f-equation
  (and (equal (g x) (if (g x) t nil))
       (equal (h x) (if (h x) t nil)))
  :rule-classes nil)

; Here I constrain f to satisfy that equation.

(encapsulate ((f (x) t))
             (local (defun f (x) (declare (ignore x)) t)  )
             (defthm f-def
               (equal (f x) (if (f x) t nil))
               :rule-classes nil))

; And finally I show that g and h are the only solutions.

(defthm f-is-only-satisfied-by-g-and-h
  (or (equal (f x) (g x))
      (equal (f x) (h x)))
  :hints (("Goal" :use f-def))
  :rule-classes nil)





; 3.  Suppose ff is a function of two arguments.  You don't know
; anything about what ff returns.  Given the two definitions

(defstub ff (x y) t)

(defun fn1 (x a)
  (if (consp x)
      (fn1 (cdr x) (ff (car x) a))
    a))

(defun fn2 (x a)
  (if (consp x)
      (ff (car x) (fn2 (cdr x) a))
    a))

; Prove

; (defthm fn1-fn2
;   (equal (fn1 x a) (fn2 (rev x) a)))


(defthm fn2-app
  (equal (fn2 (app u v) a)
         (fn2 u (fn2 v a))))

(defthm fn1-fn2
  (equal (fn1 x a) (fn2 (rev x) a)))