#|

CS 2800 Homework 11 - Spring 2013

Student names:

- For this homework, you are required to write induction proofs involving
  tail-recursive functions. This may involve defining functions that are
  admited by ACL2s.

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

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

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

- Your entire solution file must be accepted by ACL2s, in BEGINNER mode. So
  enclose within comments as appropriate. 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.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; I. INDUCTION PROOFS INVOLVING TAIL-RECURSIVE FUNCTIONS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; defining a list of natural numbers
(defdata natlist (listof nat))


;; The following theorems are needed for later proofs
(defthm natlist-app
  (implies (and (natlistp a)
                (natlistp b))
           (natlistp (acl2::append a b))))

(defthm rev-natlist
  (implies (natlistp l)
           (natlistp (rev l))))

;; 1. Define the function get-naturals, which takes a list l and returns
;; the list of natural numbers present in l.

(defunc get-naturals (l)
  :input-contract (listp l)
  :output-contract (natlistp (get-naturals l))
  ...

)

(check= (get-naturals '(a "abc" 1 aw 9)) '(1 9))
(check= (get-naturals '("hj" "abc" aw (1 2 3) 89 lk 1)) '(89 1))
(check= (get-naturals '(q "ab" lk ())) ())

;; 2. Define the function get-naturals-t, which is a tail-recursive version
;; of get-naturals with an accumulator:

(defunc get-naturals-t (l acc)
  :input-contract (and (listp l) (natlistp acc))
  :output-contract (natlistp (get-naturals-t l acc))
  ...

)

;; Write at least 3 check= tests
(check= ...)
(check= ...)
(check= ...)

#|
  3. Define get-naturals*, a NON-RECURSIVE function that calls
  get-naturals-t and returns the same values as get-naturals.
  That is, the following must be a theorem:

  (listp l) => (get-naturals* l) = (get-naturals l)

  Note that get-naturals* has the same arguments and contracts as
  get-naturals.
|#

(defunc get-naturals* (l)
  :input-contract (listp l)
  :output-contract (natlistp (get-naturals* l))
  ...)

#|

4. Identify a lemma that relates get-naturals-t to get-naturals. Remember 
   that this is a generalization step, i.e., all arguments to get-naturals-t
   are variables (no constants). The RHS should include acc.
   DO NOT prove this lemma at this point. (This will be done in step 6.)

  (listp l) /\ ... =>
	(get-naturals-t l acc) = ...

  5. Assuming that lemma in 4 is true and using ONLY equational reasoning,
  prove the main theorem:

  (listp l) => (get-naturals* l) = (get-naturals l)

  You may use the following lemmas without proof.

L1: (listp l) => (app l nil) = l
L2: (listp l) => (rev (rev l)) = l

...

6. Prove the lemma in 4. Use the induction scheme of get-naturals-t. In
   doing so, you may use the following lemma without proof:

   L3: (natp e) /\ (natlistp l) => (natlistp (cons e l))

...

7. Prove any remaining lemmas that you used but didn't prove. If none, say so.
...

|#

;; 8. Define the function how-many, which takes an element a and a list l
;; and returns the number of occurrences of a in l:

(defunc how-many (e l)
  :input-contract (listp l)
  :output-contract (natp (how-many e l))
  ...

)

;;9. Write a function how-many-t, which is a tail-recursive version of how-many
;; with an accumulator:

(defunc how-many-t (e l acc)
  :input-contract (and (listp l) (natp acc))
  :output-contract (natp (how-many-t e l acc))
  ...

)

;; 10. Define how-many*, a NON-RECURSIVE function that calls how-many-t and
;;     returns the same values as how-many. That is, the following must be a
;;     theorem:

;;   (listp l) => (how-many* e l) = (how-many e l)

;;   Note that how-many* has the same arguments and contracts as how-many.

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

#|

11. Identify a lemma that relates how-many-t and how-many. Remember that
    this is a generalization step, i.e., all arguments to how-many-t are
    variables (no constants). The RHS should include acc.

...

12. Assuming that lemma in 11 is true and using ONLY equational reasoning,
    prove the main theorem:

  (listp l) => (how-many* e l) = (how-many e l)

13. Prove the lemma in 11. Use the induction scheme of how-many-t.

...

14. Prove any remaining lemmas that you used but didn't prove. If none, say so.
...

|#

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

(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))

;; Here is a tail-recursive version of positions, named positions-t:

(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))
  (cond ((endp l) acc)
        ((equal (first l) x) (positions-t x (rest l) (+ c 1) (cons c acc)))
        (t                   (positions-t x (rest l) (+ c 1)         acc))))

;; 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. That is the purpose of argument c of positions-t.

;; Now define positions*, a NON-RECURSIVE function that calls positions-t and
;; returns the same values as positions, i.e., this is a theorem:

;; (listp l) => (positions* x l) = (positions x l)

(defunc positions* (x l)
  :input-contract (listp l)
  :output-contract (natlistp (positions* x l))
  ...)

;; Note that positions* has the same arguments and contracts as positions.

#|

16. Identify a lemma that relates positions-t to positions. Remember that
this is a generalization step, i.e., all arguments to positions-t are
variables (no constants). The RHS should include c as well as acc.

Hint: this requires some thought. Evaluate positions-t on some examples to
find out what it should be. The lemma will involve several functions other
than positions-t and positions, including some functions defined earlier in
this homework. Consider the acl2::test? facility to sanity-check your
lemma.

...

17. Assuming that lemma in 16 is true and using ONLY equational reasoning,
    prove the main theorem:

  (listp l) => (positions* x l) = (positions x l)

...

18. Prove the lemma in 16. Use the induction scheme of positions-t. In
    doing so, you may use the following lemmas without proof:

L3: (natp e) /\ (natlistp l) => (natlistp (cons e l))
L4: (listp x) /\ (listp y) => (app (rev x) (rev y)) = (rev (app y x))

There may be other lemmas that you find necessary. Put these on the todo
list, and prove them later.

...

19. Prove any remaining lemmas that you used but didn't prove. If none, say so.

...

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; II. Fibonacci -- Made Efficient
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; First reduce the amount of testing done by ACL2 while it admits a function:
(acl2::acl2s-defaults :set acl2::subgoal-timeout 1)

;; Now recall the definition of the fib function:
(defunc fib (n)
  :input-contract (natp n)
  :output-contract (natp (fib n))
  (if (<= n 1)
    n
    (+ (fib (- n 1))
       (fib (- n 2)))))

;; This is an elegant and very easy to read definition. But it is also very
;; slow. To see why, we trace the recursive calls to fib when processing
;; input. This is done as follows:

(acl2::trace! fib)
(acl2::set-guard-checking :none)

#|

(Hint: you can use (acl2::untrace$ ...) to stop tracing a function.)

Now try fib using some _small_ inputs. Start with n=1, n=2, to get a
feeling for the output produced by trace. A line of the form

 > (FIB 1)

indicates that a call (fib 1) was just encountered and is now being processes, while

 < (FIB 1)

indicates that the call (fib 1) was completed.

1. In the evaluation of (fib  5), how many times is fib called on argument 1 ? ...
   In the evaluation of (fib 10), how many times is fib called on argument 1 ? ...

Hint: you can use the Eclipse editor to count occurrences of certain text
strings, or you can copy the output of trace into your favorite alternative
editor.

Compare the above numbers with the values (fib 5) and (fib 10). What do you
find?

...

2. You saw how long the trace output of (fib 10) is -- for a fairly small
input of 10. Let's see whether we can make fib more efficient, but NOT
using tail-recursion (as we did in the last homework). Our fib-fast
function will be hard for ACL2 to prove terminating, so you are allowed to
write this function in program mode:

|#

:program

#|

The idea is as follows. First write a function fib-help that, for input n,
computes the _list_ of Fibonacci numbers
(fib n), (fib n-1), ..., 8,5,3,2,1,1,0 = (fib 0)
(descending order). See tests below, and also note the output contract,
which is provided for you. Provide 3 more tests.

To minimize the number of recursive calls required to evaluate (fib-help n),
you MUST use (let ...) whenever you need the result of a recursive call
several times. Your solution will be considered incorrect if your code
contains several calls to fib-help with the same arguments.

|#

(defunc fib-help (n)
  :input-contract (natp n)
  :output-contract (and (natlistp (fib-help n)) (equal (len (fib-help n)) (+ n 1)))
  ...

)

(check= (fib-help 0) '(0))
(check= (fib-help 1) '(1 0))
(check= (fib-help 3) '(2 1 1 0))

;; Now write a non-recursive function fib-fast, with contracts as for the
;; (slow) fib function, which calls fib-help to compute (fib n).

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

;; Now let's see whether fib-fast deserves that name. Turn on tracing for
;; the helper function (fib-fast itself is not recursive):

(acl2::trace! fib-help)

#|

In the evaluation of (fib-fast  5), how many times is fib-help called on argument 1 ? ...
In the evaluation of (fib-fast 10), how many times is fib-help called on argument 1 ? ...

Compare your results to those obtained with (fib n).

You can also try fib and fib-fast on input 100. Hint: try fib-fast first!

|#

#|

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

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