; JVM Problem Set 2
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
; ===============================================================
; This problem set focuses on simple inductive proofs.  Sometimes 
; the formula given is not actually a theorem.  But a similar 
; formula can be proved, e.g., after adding some restrictive 
; hypothesis.  Get ACL2 to prove each of these ``suggested'' 
; theorems.   You will find this trivial, once you've hit upon the
; right theorem, because ACL2 is very good at these ``simple'' 
; proofs.  But make sure you understand the proof that ACL2 does.

; Before proceeding, define the following functions from the last
; problem set.

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

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

(defun ln (x)
  (if (consp x)
      (+ 1 (ln (cdr x)))
    0))

(defun sum (x)
  (if (consp x)
      (+ (car x) (sum (cdr x)))
    0))

(defun tmark (x)
  (if (consp x)
      (tmark (cdr x))
    x))

(defun all-ints (x)
  (if (consp x)
      (and (integerp (car x))
           (all-ints (cdr x)))
    t))

(defun some-int (x)
  (if (consp x)
      (or (integerp (car x))
          (some-int (cdr x)))
    nil))

(defun all-ints-counterexample (x)
  (if (consp x)
      (if (integerp (car x))
          (all-ints-counterexample (cdr x))
        (car x))
    23))

(defun cp (x)
  (if (consp x)
      (cons (car x) (cp (cdr x)))
    x))

(defun rep (e x)
  (if (consp x)
      (cons e (rep e (cdr x)))
    x))

; Do not include any ACL2 books.

; Problem 2.1
(defthm len-app
  (equal (len (app x y))
         (+ (len x) (len y))))

; Problem 2.2
(defthm app-left-id
  (equal (app nil a) a)) 

; Problem 2.3
(defthm app-right-id
  (equal (app a nil) a))

; Problem 2.4
(defthm sum-app
  (equal (sum (app u v))
         (+ (sum u) (sum v))))

; Problem 2.5
(defthm sum-app-commutes
  (equal (sum (app a b))
         (sum (app b a))))

; Problem 2.6
(defthm all-ints-app
  (equal (all-ints (app u v))
         (and (all-ints u) (all-ints v))))

; Problem 2.7
(defthm all-ints-app-commutes
  (equal (all-ints (app x y))
         (all-ints (app y x))))

; Problem 2.8
(defthm cp-identity
  (equal (cp x) x))

; Problem 2.9
(defthm rep-app
  (equal (rep e (app b c))
         (app (rep e b) (rep e c))))

; Problem 2.10
(defthm rep-rep
  (equal (rep e (rep d x))
         (rep e x)))

; Problem 2.11
(defthm sum-rep-1
  (equal (sum (rep 1 a)) (ln a)))

; Problem 2.12
(defthm ln-app
  (equal (ln (app a b))
         (+ (ln a) (ln b))))

; Problem 2.13
(defthm ln-rep
  (equal (ln (rep e u)) (ln u)))

; Problem 2.14
(defthm tmark-tmark
  (equal (tmark (tmark x)) (tmark x)))

; Problem 2.15
(defthm tmark-app
  (equal (tmark (app a b))
         (tmark b)))

; Problem 2.16
(defthm tmark-rep
  (equal (tmark (rep e a))
         (tmark a)))

; Problem 2.17
(defthm sum-rep-n
  (equal (sum (rep n b))
         (* n (ln b))))

; Problem 2.18
(defthm Problem-2-18
  (equal (sum (rep (ln a) b))
         (* (ln a) (ln b)))
  :rule-classes nil)

; Problem 2.19
(defthm Problem-2-19
  (equal (sum (rep 1
                   (app (app (rep 0 a) (rep 1 b))
                        (rep 2 c))))
         (ln (rep e (cp (app (cp a) (app b c))))))
  :rule-classes nil)

; Problem 2.20
(defthm problem-2-20
  (equal (tmark (app a (rep (ln x) (app b c))))
         (app (tmark a) (tmark (app c (tmark (rep 3 c))))))
  :rule-classes nil)

; In the event below, I disable tmark-app.  This prevents ACL2
; from using it.  The proof with fail.  Study the failed proof
; -- but read no further than the announcement that induction
; will be tried.  Intuitively, we don't think this theorem 
; requires induction, so when we see the induction message, we
; know something is wrong.  Look at the formula that the system
; needs to prove.  To me it cries out for a lemma like tmark-app
; (the lemma we disabled).  Learn how to look at formulas and spot
; the ``missing lemmas.''

; This isn't an official problem.  But be ready to discuss this
; proof in class.

(defthm problem-2-20-sort-of
  (equal (tmark (app a (rep (ln a) (app a a))))
         (app (tmark a) (tmark (app a (tmark (rep 3 a))))))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable tmark-app))))

; Problem 2.21
; Define the following function.

(defun surround (x)
  (if (endp x)
      x
    (cons (list (car x))
          (surround (cdr x)))))

; You might test surround on a few examples, like 
; (surround '(1 2 3)).

; Now figure out what lemmas you need to prove the one below. 
; To get this proof to go through you will need to add at least
; one defthm here.

(defthm problem-2-21
  (equal (tmark (surround (app a a)))
         (tmark a))
  :rule-classes nil)