#|

CS 2800 Homework 12 - Spring 2013

Student names:

- For this homework, you are going to use ACL2s to reason about
  tail-recursive function definitions.

- To turn in your solution, check out the directory at

  svn://dell-server-wahl-1.ccs.neu.edu/cs2800-2013-spring/12/<groupname>

  Place your file hw12.lisp in this directory, add it, and commit.

- Your entire solution file must be accepted by ACL2s, in
  BEGINNER mode. If your solution to any question that is to be
  run in ACL2s is incomplete, comment out those portions so that
  the file is accepted by ACL2s.

In this homework, we are going to use ACL2s as a workhorse to do
all the boring reasoning for us, e.g., equational reasoning. This
will free us to focus on the interesting part of proving
theorems, which is coming up with the key insights, encoded as
lemmas.

Here is a quick reminder of what we covered in class.

In ACL2s, if I want to prove a theorem, I do it with defthm. For
example, to ask ACL2s to prove the conjecture

(listp x) => (len (rev x)) = (len x)

I write this:

(defthm len-rev ; the name of the theorem ;
  (implies (listp x)
           (equal (len (rev x))
                  (len x))))

Theorems (like len-rev above) are used by ACL2s as rewrite
rules. What this means is that when ACL2s is reasoning and sees
an expression that matches the lhs (left-hand side) of len-rev,
it wil try to apply the rule by rewriting the lhs to the rhs of
the rule.

For example, suppose ACL2s see the expression

(len (rev (app a b)))

This expression "matches" the lhs of len-rev (see the lecture
notes for the details) and will get rewritten as per the rhs of
the rule to:

(len (app a b))

This was a good thing because the expression was simplified.

If we had written len-rev by swapping the lhs and rhs, we would
have gotten very different  behavior. The expression

(len (rev (app a b)))

would have been rewritten to 

(len (rev (rev (app a b))))

which is not a good thing. 

So the take-home message is to be careful how you write your
defthms. Make sure that the lhs is the more complex side.

|#

; Below are some basic lemmas that will be useful later.

(defthm len-consp
  (implies (and (equal (len x) (len y))
                (listp x) 
                (listp y) 
                (consp x))
           (consp y))
  :rule-classes :forward-chaining)

(defthm rev-tlp
  (implies (listp x)
           (acl2::true-listp (rev x)))
  :rule-classes ((:type-prescription) (:forward-chaining)))

(defthm app-rev
  (implies (and (listp x)
                (listp y))
           (equal (rev (acl2::append x y))
                  (acl2::append (rev y) (rev x)))))

(defthm rev-rev
  (implies (listp x)
           (equal (rev (rev x))
                  x)))

; Here is the definition of revt, the tail recursive version
; of rev that we defined in class.

(defunc revt (x acc) 
  :input-contract (and (listp x) (listp acc)) 
  :output-contract (listp (revt x acc)) 
  (if (endp x)
    acc 
    (revt (rest x) (cons (first x) acc))))

; Here is the definition of rev*, the function that uses revt to
; efficiently compute rev.

(defunc rev* (x) 
  :input-contract (listp x) 
  :output-contract (listp (rev* x)) 
  (revt x ()))

; Q1. Fill in the ...'s below so that both revt-lemma and
; rev*-rev, below, are theorems that ACL2s accepts. Notice that
; for theorems like this that relate the tail recursive version
; of a function with the simple recursive definition, we will
; always use rewrite rules that have the tail recursive function
; on the lhs so that when the rule applies, an expression
; containing the tail recursive function gets turned into an
; expression involving the simple recursive definition. Make sure
; to use the same approach for the rest of the questions in this
; homework.

(defthm revt-lemma 
  (implies (and (listp x) 
                (listp acc))
           (equal (revt x acc) 
                  ...(rev x)...)))

(defthm rev*-rev
  (implies (listp x)
           (equal (rev* x)  
                  (rev x))))

; This is the data definition for a list of lists and
; accompanying theorems.

(defunc listlistp (l)
  :input-contract t
  :output-contract (booleanp (listlistp l))
  (if (atom l) 
    (equal l ())
    (and (listp (first l))
         (listlistp (rest l)))))

(defthm app-listlistp
  (implies (and (listlistp l)
                (listlistp x))
           (listlistp (acl2::append l x))))

(defthm listlistp-listp
  (implies (listlistp l)
           (acl2::true-listp l))
  :rule-classes :forward-chaining)

(defthm rev-listlistp
  (implies (listlistp l)
           (listlistp (rev l))))

; Here is a recursive definition for rev-all, a function that
; given a list of lists, reverses every element of the top-level
; list.

(defunc rev-all (l)
  :input-contract (listlistp l)
  :output-contract (listlistp (rev-all l))
  (if (endp l)
      ()
    (cons (rev (first l)) 
          (rev-all (rest l)))))

; A few lemmas

(defthm revall-listlistp
  (implies (listlistp x)
           (listlistp (rev-all x)))
  :rule-classes ((:type-prescription) (:forward-chaining)))

(defthm revall-tlp
  (implies (listlistp x)
           (acl2::true-listp (rev-all x)))
  :rule-classes ((:type-prescription) (:forward-chaining)))

; Here is the tail recursive definition. 

(defunc rev-all-t (l acc)
  :input-contract (and (listlistp l) (listlistp acc))
  :output-contract (listlistp (rev-all-t l acc))
  (if (endp l)
    acc
    (rev-all-t (rest l) (cons (rev (first l)) acc))))

(defthm revall-t-tlp
  (implies (and (listlistp l)
                (listlistp acc))
           (acl2::true-listp (rev-all-t l acc)))
  :rule-classes ((:type-prescription) (:forward-chaining)))

(defunc rev-all* (l)
  :input-contract (listlistp l)
  :output-contract (listlistp (rev-all* l))
  (rev (rev-all-t l ())))  

; Q2. Fill in the ...'s below so that ACL2s accepts
; rev-all-t-lemma and rev-all*-rev-all. See the comment before Q1 
; regarding how to write such lemmas.

(defthm rev-all-t-lemma
  (implies (and (listlistp l) (listlistp acc))
           (equal ...
                  ...)))

(defthm rev-all*-rev-all
  (implies (listlistp l)
           (equal (rev-all* l)
                  (rev-all l))))

(defdata natlist (listof nat))

(defthm natlistp-natp
  (implies (and (natp x)
                (natlistp y))
           (natlistp (cons x y))))

(defunc sum-of-squares (l)
  :input-contract (natlistp l)
  :output-contract (natp (sum-of-squares l))
  (if (endp l)
    0
    (+ (* (first l) (first l))
       (sum-of-squares (rest l)))))

(defunc sum-of-squares-t (l acc)
  :input-contract (and (natlistp l) (natp acc))
  :output-contract (natp (sum-of-squares-t l acc))
  (if (endp l)
    acc
    (sum-of-squares-t (rest l) (+ acc (* (first l) (first l))))))

(defunc sum-of-squares* (l)
  :input-contract (natlistp l)
  :output-contract (natp (sum-of-squares* l))
  (sum-of-squares-t l 0))

; Q3. Fill in the ...'s below so that ACL2s accepts
; sum-of-squares-t-lemma and sum-of-squares*-sos.

(defthm sum-of-squares-t-lemma
  (implies ...
           (equal ...
                  ...)))

(defthm sum-of-squares*-sos
  (implies (natlistp l) 
           (equal (sum-of-squares* l) 
                  (sum-of-squares l))))

(defunc delete (x l)
  :input-contract (listp l)
  :output-contract (listp (delete x l))
  (cond ((endp l) ())
        ((equal x (first l)) (delete x (rest l)))
        (t (cons (first l) (delete x (rest l))))))

(defunc delete-t (x l acc)
  :input-contract (and (listp l) (listp acc))
  :output-contract (listp (delete-t x l acc))
  (cond ((endp l) acc)
        ((equal x (first l)) (delete-t x (rest l) acc))
        (t (delete-t x (rest l) (app acc (list (first l)))))))

(defunc delete* (x l)
  :input-contract (listp l)
  :output-contract (listp (delete* x l))
  (delete-t x l ()))

; Q4. Fill in the ...'s below so that ACL2s accepts
; delete-t-lemma and delete*-delete.

(defthm delete-t-lemma
  (implies ...
           (equal ...
                  ...)))

(defthm delete*-delete
  (implies (listp l) 
           (equal (delete* x l) 
                  (delete x l))))


(defunc how-many (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many e l))
  (if (endp l)
    0
    (+ (if (equal e (first l)) 1 0)
       (how-many e (rest l)))))

(defunc how-many-t (e l acc)
  :input-contract (and (listp l) (natp acc))
  :output-contract (natp (how-many-t e l acc))
  (if (endp l)
    acc
    (how-many-t e (rest l) (+ (if (equal e (first l)) 1 0) acc))))

(defunc how-many* (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many* e l))
  (how-many-t e l 0))

; Q5. Fill in the ...'s below so that ACL2s accepts
; how-many-t-lemma and how-many*-how-many.

(defthm how-many-t-lemma
  (implies ...
           (equal ...
                  ...)))

(defthm how-many*-how-many
  (implies (listp l) 
           (equal (how-many* x l) 
                  (how-many x l))))

(defunc ! (n)
  :input-contract (natp n)
  :output-contract (posp (! n))
  (if (equal n 0)
    1
    (* n (! (- n 1)))))

(defunc !-t (n acc)
  :input-contract (and (natp n) (posp acc))
  :output-contract (posp (!-t n acc))
  (if (equal n 0)
    acc
    (!-t (- n 1) (* n acc))))

; Q6. Fill in the ...'s in the next *two* forms below so that
; ACL2s accepts !*, !-t-lemma, !*-!.

(defunc !* (n)
  :input-contract (natp n)
  :output-contract (posp (! n))
  (!-t n ...))

(defthm !-t-lemma
   ...)

(defthm !*-!
  (implies (natp n)
           (equal (!* n) 
                  (! n))))

(defunc pair (x y)
  :input-contract (and (listp x) (listp y) 
                       (equal (len x) (len y)))
  :output-contract (listp (pair x y))
  (if (endp x)
    ()
    (cons (list (first x) (first y)) (pair (rest x) (rest y)))))

(defunc pair-t (x y acc)
  :input-contract (and (listp x) (listp y) (listp acc) 
                       (equal (len x) (len y)))
  :output-contract (listp (pair-t x y acc))
  (if (endp x)
    acc
    (pair-t (rest x) (rest y) (cons (list (first x) (first y)) acc))))

; Q7. Fill in the ...'s in the next *two* forms below so that
; ACL2s accepts pair*, pair-t-lemma, and pair*-pair.

(defunc pair* (x y)
  :input-contract (and (listp x) (listp y) 
                       (equal (len x) (len y)))
  :output-contract (listp (pair* x y))
  ...)


(defthm pair-t-lemma
  ...)

(defthm pair*-pair
  (implies (and (listp x) (listp y) 
                (equal (len x) (len y)))
           (equal (pair* x y)
                  (pair x y))))

(defunc merge-lists (x y)
  :input-contract (and (natlistp x) (natlistp y))
  :output-contract t
  (cond  ((endp x) y)
         ((endp y) x)
         ((< (first x) (first y))
          (cons (first x) (merge-lists (rest x) y)))
         (t (cons (first y) (merge-lists x (rest y))))))

(defthm merge-lists-output
  (implies (and (natlistp x) (natlistp y))
           (natlistp (merge-lists x y)))
  :hints (("goal" :induct (merge-lists-induction-scheme-from-definition x y))))

; Q8. Fill in the ...'s in the next *three* forms below so that
; ACL2s accepts merge-lists-t, merge-lists*, merge-lists-t-lemma,
; and merge-lists*-merge-lists.

(defunc merge-lists-t (x y acc)
  :input-contract (and (natlistp x) (natlistp y) (natlistp acc))
  :output-contract (natlistp (merge-lists-t x y acc))
  (cond  ((and (endp x) (endp y)) acc)
         ((endp x) ...)
         ((endp y) ...)
         ((< (first x) (first y))
          (merge-lists-t (rest x) y (cons (first x) acc)))
         (t (merge-lists-t x (rest y) (cons (first y) acc)))))


(defunc merge-lists* (x y)
  :input-contract (and (natlistp x) (natlistp y))
  :output-contract (natlistp (merge-lists x y))
  (rev (merge-lists-t x y ())))

(defthm merge-lists-t-lemma
  (implies (and (natlistp x) 
                (natlistp y)
                (natlistp acc))
           (equal (merge-lists-t x y acc)
                  ...)))

(defthm merge-lists*-merge-lists 
  (implies (and (natlistp x) (natlistp y))
           (equal (merge-lists* x y)
                  (merge-lists x y))))

#|

Please fill out the following form:
https://docs.google.com/spreadsheet/viewform?formkey=dDYzR1dLZmduamhaU19HSWt0dGp5T0E6MA

Confirm here whom of the team members filled out the form:

Name 1 ...
Name 2 ...
(Name 3 ...)

Everyone who filled out the form gets credit worth 1 quiz.

The form is anonymous, to encourage you to write what you think about this
class. (If you want to stay anonymous, do not reveal your name on the
feedback form.) On the other hand, we must rely on your honesty in stating
whether you filled out the form or not, and in NOT filling out the form
several times (why would you do that??). We do not want to find
discrepancies in the number of entries on the form, and the number of
people claiming to have filled out the form.

|#