; Try to work this in 3 hours, alone, without using the ACL2 system.

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

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

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

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

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

; Prove

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