#|

CS 2800 Homework 10 - Spring 2013

Student names:

For this homework, you will be writing paper-and-pencil proofs for part I,
and program in part II.

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

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

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

 - Only Part II. uses ACL2s but your entire solution file should be
   accepted by ACL2s, in BEGINNER mode. So enclose within comments as
   appropriate. If your solution to any question of part II. is incomplete,
   comment out those portions so that the file is accepted by ACL2s.

- Whenever convenient, we will use F and T to represent false and true, and
  the following character combinations to represent the Boolean
  connectives:

    NOT        ~

    AND        /\
    OR         \/

    IMPLIES    =>

    EQUIVALENT =
    XOR        <>

  The binding powers of these connectives are as in class: they are listed
  in the above table from highest to lowest. Within one group
  (no blank line), the binding power is the same.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Part I: Induction proofs
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

  For induction proofs, first see if you need to perform conjecture
  contract completion. Then state the induction scheme (IS) you are using,
  by specifying the function that gives rise to it. Write down the proof
  obligations coming out of the IS, and prove them by equational reasoning.

  If you use any lemmas in your proofs, you need to clearly state so. These
  lemmas need to be proved separately, unless they have been proved in this
  or prior homeworks (mention that if you believe this is the case), or the
  homework explicitly states that you can use some property without proof.

  Here are the definitions for the functions used in the problems:

(defunc in (a l)
  :input-contract (listp l)
  :output-contract (booleanp (in a l))
  (if (endp l)
      nil
    (or (equal a (first l))
        (in a (rest l)))))

(defunc subsetp (l1 l2)
  :input-contract (and (listp l1) (listp l2))
  :output-contract (booleanp (subsetp l1 l2))
  (if (endp l1)
      t
    (and (in (first l1) l2)
         (subsetp (rest l1) l2))))

(defunc app (l1 l2)
  :input-contract (and (listp l1) (listp l2))
  :output-contract (listp (app l1 l2))
  (if (endp l1)
      l2
    (cons (first l1) (app (rest l1) l2))))

(defunc rev (l)
  :input-contract (listp l)
  :ouput-contract (listp (rev l))
  (if (endp l)
      nil
    (app (rev (rest l)) (list (first l)))))

(defunc remove-dups (l)
  :input-contract (listp l)
  :output-contract (listp (remove-dups l))
  (if (endp l)
      nil
    (if (in (first l) (rest l))
	(remove-dups (rest l))
      (cons (first l) (remove-dups (rest 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 len (l)
  :input-contract (listp l)
  :output-contract (natp (len l))
  (if (endp l)
      0
    (+ 1 (len (rest l)))))

(defunc del (a l)
  :input-contract (listp l)
  :output-contract (listp (del a l))
  (cond ((endp l) nil)
	((equal a (first l)) (rest l))
	(t (cons (first l) (del a (rest l))))))

Prove the following conjectures using induction.

1. We begin with the lemma we used in Homework 9 without proof. You have by
now learned the tool to prove it: induction. So, go ahead and prove it!

(implies (and (listp l1)
              (listp l2)
              (subsetp l1 l2))
         (subsetp l1 (cons a l2)))

2.

(implies (listp l)
	 (<= (len (del a l))
	     (len l)))

3.

(implies (and (listp l1) (listp l2))
	 (implies (in a l1) 
		  (in a (app l1 l2))))

4.

(implies (and (listp l1) (listp l2))
	 (equal (in a (app l1 l2))
		(or (in a l1)
		    (in a l2))))

5.

(implies (listp l)
	 (equal (in a l)
		(in a (rev l))))

6.

(implies (listp l) 
	 (<= (how-many e (remove-duplicates l)) 
	     (how-many e l)))

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Part II: Tail-recursive functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

7. Consider the function add-to-all (n l), which adds the natural number n
to every element of the list of naturals l, and the function positions (x
l), which determines the list of positions in the list l where x occurs:

|#

(defdata natlist (listof nat))

(defunc add-to-all (n l)
  :input-contract (and (natp n) (natlistp l))
  :output-contract (natlistp (add-to-all n l))
  (if (endp l)
      ()
    (cons (+ (first l) n) (add-to-all n (rest l)))))

(check= (add-to-all 1 '(1 2 3)) '(2 3 4))

(defunc positions (x l)
  :input-contract (listp l)
  :output-contract (natlistp (positions x l))
  (cond ((endp l) ())
        ((equal (first l) x) (cons 0 (add-to-all 1 (positions x (rest l)))))
        (t                           (add-to-all 1 (positions x (rest l))))))

(check= (positions 3 '(3 1 9 7 3 67 34 3))  '(0 4 7))
(check= (positions 3 '(3 1 9 37 6 34 3 32)) '(0 6))
(check= (positions 1 '(3 1 9 7 3 67 34 1))  '(1 7))

#|

a. Define a tail-recursive version positions-t of positions. The
tail-recursive function positions-t walks through the input list from left
to right. Suppose you find an occurrence of x. In order to know what its
position is in the original list, you have to keep track of the number of
elements already processed. Function positions-t should thus have an extra
argument, say c, for that purpose, in addition to the accumulator:

|#

(defunc positions-t (x l c acc)
  :input-contract (and (listp l) (natp c) (natlistp acc))
  :output-contract (natlistp (positions-t x l c acc))
  ...

)

(check= (positions-t 3 '(3 1 9 7 3 67 34 3)  0 '()) '(7 4 0))
(check= (positions-t 3 '(3 1 9 37 6 34 3 32) 0 '()) '(6 0))
(check= (positions-t 1 '(3 1 9 7 3 67 34 1)  0 '()) '(7 1))

#|

b. What is the relationship between positions and positions-t? Fill in the
blanks in the following conjecture. You do not need to prove the conjecture.

Hint: Try out more examples on positions and positions-t if necessary. The
conjecture might involve several functions other than positions-t and
positions, including the add-to-all function from above. There should be no
constants anywhere. Use the acl2::test? facility to sanity-check your
conjecture.

(listp l) /\ (natp c) /\ (natlistp acc) =>
  (positions-t x l c acc) = ...

8. Consider the following function that produces the nth fibonacci number.

|#

(acl2::acl2s-defaults :set acl2::testing-enabled nil) ; we turn off testing

(defunc fib (n)
  :input-contract (natp n)
  :output-contract (natp (fib n))
  (if (<= n 1)
      n
    (+ (fib (- n 1)) (fib (- n 2)))))

(check= (fib 1) 1)
(check= (fib 6) 8)
(check= (fib 8) 21)

;; Now write a tail recursive fibonacci function fib-t. There are several
;; ways to do this. One is for fib-t to have two additional arguments, a
;; and b, such that in the ith recursive call, b contains fib(i) and a
;; contains fib(i+1). That means that after the nth iteration, the result
;; fib(n) will be stored in b. To maintain that invariant, think about how
;; to update a and b in each recursive call.

(defunc fib-t (n a b)
  :input-contract (and (natp n) (natp a) (natp b))
  :output-contract (natp (fib-t n a b))
  ...

)

(check= (fib-t 1 1 1) 1)
(check= (fib-t 6 2 4) 36)
(check= (fib-t 8 1 1) 34)

;; Finally, write a NON-RECURSIVE function fib* that has the same signature
;; as fib, and computes the same value as fib, but uses fib-t, initializing
;; the arguments a and b of fib-t appropriately:

(defunc fib* (n)
  :input-contract ...
  :output-contract ...
  ...)

;; Test that fib* computes the same values as fib above!

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;Feedback Form
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

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