#|
CS 2800 Homework 7 - Spring 2013

Student names:

For this homework, you will be using the BEGINNER mode in ACL2s.

Instructions for using this file:

- Open this file in ACL2s as hw07.lisp .

- Set the session mode to "Beginner".

- Insert your solutions into this file where indicated (for instance
  as "..."). This includes contracts, function bodies, and test cases.
  Make sure you provide as many test cases as required
  (in addition to the ones already provided, of course).

- Do not comment in or comment out any existing function definitions
  from this file. Also, do not change the order of any function
  definitions, whether provided by us or defined by you.

- Make sure the entire file is admitted by ACL2s in Beginner
  mode. This means:
  
  * there must be no "..." in the code. If you don't finish some
    problems, comment them out. The same is true for any English text
    that you may add. This file already contains many comments, so you
    can see what the syntax is.
  
  * all check= tests must be satisfied. If any of the provided tests
    fail, your function definition is wrong, and the file will not be
    admitted.  If any of your own tests fail, it may be that your
    function is wrong, but it may also be that your check=
    specification is incorrect.

  Sometimes it may take a while for your function to be admitted. Be
  patient: rest assured that, if your function is correct, the process
  will succeed. If you don't get a success message after 2-3
  mins (depending on your hardware), then probably your definition is
  too complicated or wrong.

  If you remain convinced that your definition is correct, just
  put :program somewhere towards the beginning of the file, e.g.,
  right here:

|#

; :program

#|

  It will turn off static verification of contracts and termination
  analysis.

- Save the file with your additions and turn it in. To do that, check
  out the directory at

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

  where groupname is the name of the group as it was emailed to
  you. Your username and password remain as before.

  Place your file hw07.lisp in this directory, add it, and commit. Do
  NOT submit the session file (ending in .a2s).

- For non-programming problems, include solutions as
  comments. 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.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Preliminaries
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; acl2::test?

#| 

acl2::test? takes a conjecture as input and runs a number of tests to
see whether it can find a counterexample. For example, let us
conjecture that, for positive natural numbers x and y, (x + y)
and (x * y) are different. You can test this conjecture like this:

  (acl2::test?
   (implies (and (posp x) (posp y))
            (not (equal (+ x y) (* x y)))))

acl2::test? may report that it succeeded: no counterexamples were
found. This does not mean you have proved the conjecture! It just
means test? hasn't come across a test that falsifies it. In fact, the
above conjecture is wrong. You can try to find more counterexamples by
increasing the number of tests run, like this:

|#
  
(acl2::acl2s-defaults :set acl2::num-trials 2500)

#|
Now try acl2::test? again!

In general, make sure to perform conjecture contract closure before
passing your conjecture to acl2::test? . For example,

  (acl2::test? (equal (append x y) (append y x)))

will waste time running many useless tests in which x and y are not
lists, and report contract violations. In contrast,

  (acl2::test?
   (implies (and (listp x) (listp y))
            (equal (append x y) (append y x))))

will return a counterexample using lists immediately.

|#

;; Tail-Recursion

#|

A function is said to be tail recursive, if there is nothing to do
after a recursive call occurs, except return its value.

Implementing a tail-recursive function usually amounts to adding an
extra "accumulator" argument that keeps track of the results so far.
For example, here is a tail-recursive implementation of the factorial
function:

|#

(defunc factorial-aux (n acc)
  :input-contract (and (natp n) (natp acc))
  :output-contract (natp (factorial-aux n acc))
  (if (equal n 0)
    acc
    (factorial-aux (- n 1) (* n acc))))

#|

As you can probably guess, to compute factorial of n we call
factorial-aux with acc = 1 . Here is the non-tail-recursive
definition from Homework 6:

|#

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

(acl2::test?
 (implies (natp n)
          (equal (factorial-aux n 1) (factorial n))))

#|

Notice that in factorial-aux, there is nothing to do once we return
from the recursive call, while in the HW6 definition we perform a
multiplication.

|#

;; Standard Definitions

#|

We will use the following definitions throughout this homework. 
(They're already defined in Beginner mode.)

(defunc atom (a) 
  :input-contract t
  :output-contract (booleanp (atom a))
  (not (consp a)))

(defunc len (a)
  :input-contract t
  :output-contract (natp (len a))
  (if (atom a)
      0
      (+ 1 (len (rest a)))))

(defunc app (a b)
  :input-contract (and (listp a) (listp b))
  :output-contract (and (listp (app a b))
                        (equal (len (app a b))
                               (+ (len a) (len b))))
  (if (endp a)
      b
      (cons (first a) (app (rest a) b))))

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

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 1. Specification-Driven Programming
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

In this part of the homework, you will have to write programs that
meet given specifications. Specifications will come in two forms.
First, you will be given input and output contracts. Additionally, we
will use the acl2::test? mechanism.

Consider the following definition:

|#

(defunc count-list (a x)
  :input-contract (listp x)
  :output-contract (natp (count-list a x))
  (if (endp x)
    0
    (+ (if (equal (first x) a) 1 0)
       (count-list a (rest x)))))

#|

[a]

Provide a tail-recursive implementation of count-list:

|#

(defunc count-list-aux (a x acc)
  :input-contract (and (listp x) (natp acc))
  :output-contract (natp (count-list-aux a x acc))
  ...
  ...
  ...
  ...
  ...)


#|

Make sure the following definitions and tests go through:

|#

(defunc count-list1 (a x)
  :input-contract (listp x)
  :output-contract (natp (count-list1 a x))
  (count-list-aux a x 0))

(acl2::test?
 (implies (and (listp x)
               (equal (count-list1 a x) 0))
          (not (in a x))))

(acl2::test?
 (implies (and (listp x)
               (listp y))
          (<= (count-list1 a x)
              (count-list1 a (app x y)))))

#|

In fact, we can have a very precise specification of
count-list1 (which just calls the tail-recursive function): it
should be equal to count-list ! Specifications are not always that
strict, as you will see later.

Make sure the following test goes through:

|#

(acl2::test?
 (implies (and (natp a)
               (listp x))
          (equal (count-list1 a x)
                 (count-list a x))))

#|

[b]

We are not really done with count-list1 ! It differs from count-list 
in a very important way. To see this, first define a tail-recursive
function f-aux that constructs a list of a given length.

We will use this function to provide "malicious" (i.e., really long)
inputs for count-list and count-list1 .

|#

(defunc f-aux (n acc)
  :input-contract (and (natp n) (listp acc))
  :output-contract (and (listp (f-aux n acc))
                        (equal (len (f-aux n acc))
                               (+ (len acc) n)))
  ...
  ...
  ...)

(defunc f (n)
  :input-contract (natp n)
  :output-contract (equal (len (f n)) n)
  (f-aux n nil))

#|

For different natural numbers n , try

  (count-list 1 (f n))

in the ACL2s prompt. 

What is the largest number, x, for which the count-list expression above
can be evaluated? 

...

Note: this can change on different runs so a number in the right
ballpark is OK.

Now try evaluating 

  (count-list1 1 (f n))

in the ACL2s prompt. 

Can you evaluate the count-list1 expression above with n=100x?

...

Explain what is going on. If you do not know what is going on, 
do some research on tail recursion and cite your sources in the answer below.

...
...
...

|#

#|

[c]

In this part, we will deal with trees. A tree is a collection of
nodes, starting at a root node. Each node consists of a value (of any
type), along with a left and right node ("children"). A node can also
be nil. We use the terms "tree" and "node" interchangeably: a node "n"
can be viewed as the tree with "n" as the root. Here is the ACL2s
definition:

|#

(defdata tree
  (oneof nil
         (list tree all tree)))

#|

For example, the following tree:

      1
     / \
    3   5
   / \   \
  2   0   3

is represented in ACL2 as follows (defconst just gives a name to a
constant):

|#

(defconst *some-tree*
  (list (list (list nil
                    2
                    nil)
              3
              (list nil
                    0
                    nil))
        1
        (list nil
              5
              (list nil
                    3
                    nil))))
  
(acl2::test? (treep *some-tree*))

#|

To prove facts about trees, you can rely on the fact that if both
(treep r) and (consp r) hold, then r is a list with exactly three
elements. Also,

  (treep r) /\ (consp r) => (treep (first r))

and
 
  (treep r) /\ (consp r) => (treep (third r)) .

Finally,

  (treep r) => (listp r) .

Do not comment the theorems below. They will be required for
contract and termination proofs in what follows.

|#


(defthm consp-rest-tree
  (implies (and (treep r)
                (consp r))
           (consp (acl2::rest r)))
  :rule-classes (:type-prescription :forward-chaining))

(defthm consp-rest-rest-tree
  (implies (and (treep r)
                (consp r))
           (consp (acl2::rest (acl2::rest r))))
  :rule-classes (:type-prescription :forward-chaining))

(defthm tree-first
  (implies (and (treep r)
                (consp r))
           (treep (acl2::first r)))
  :rule-classes (:forward-chaining))

(defthm tree-third
  (implies (and (treep r)
                (consp r))
           (treep (acl2::third r)))
  :rule-classes (:forward-chaining))

(acl2::in-theory (acl2::disable acl2::integerp-minus-x))

#|

Here are a few helpful functions to deal with trees.

|#

(defunc tree-size (r)
  :input-contract (treep r)
  :output-contract (natp (tree-size r))
  (if (endp r)
    0
    (+ 1
       (+ (tree-size (first r))
          (tree-size (third r))))))

(defunc in-tree (a r)
  :input-contract (treep r)
  :output-contract (booleanp (in-tree a r))
  (if (endp r)
    nil
    (or (equal (second r) a)
        (in-tree a (first r))
        (in-tree a (third r)))))

(defunc count-tree (a r)
  :input-contract (treep r)
  :output-contract (natp (count-tree a r))
  (if (endp r)
    0
    (+ (if (equal (second r) a) 1 0)
       (+ (count-tree a (first r))
          (count-tree a (third r))))))

#|

There are multiple ways to walk through the nodes of a tree. Here is
a function that walks through a tree in some particular way, visits
each node once, and collects all values:

|#

(defunc tree-to-list (r)
  :input-contract (treep r)
  :output-contract (listp (tree-to-list r))
  (if (endp r)
    nil
    (app (cons (second r)
               (tree-to-list (first r)))
         (tree-to-list (third r)))))

#|

For the tree given above ( *some-tree* ), tree-to-list returns
(1 3 2 0 5 3) . Try it! This is not the only possible answer, e.g.,  
(2 3 0 1 5 3) would be perfectly fine. A value can (and should!)
appear multiple times in the output, if it appears in multiple
nodes of the tree. For instance, (2 3 0 1 5) would not be an
acceptable answer.

The formal properties below correspond to our informal specification
above.

|#

(acl2::test?
 (implies (and (treep r)
               (in-tree a r))
          (in a (tree-to-list r))))

(acl2::test?
  (implies (treep r)
           (equal (count-tree a r)
                  (count-list a (tree-to-list r)))))

#|

Provide another implementation of tree-to-list that visits
nodes in a different order. The new function should satisfy the
same properties as tree-to-list ; in other words, the tests below
the definition should pass!

|#

(defunc tree-to-list1 (r)
  :input-contract (treep r)
  :output-contract (listp (tree-to-list1 r))
  ...
  ...
  ...
  ...
  ...)


(check= (equal (tree-to-list1 *some-tree*) 
               (tree-to-list *some-tree*))
        nil)

(acl2::test?
 (implies (and (treep r)
               (in-tree a r))
          (in a (tree-to-list1 r))))

(acl2::test?
  (implies (treep r)
           (equal (count-tree a r)
                  (count-list a (tree-to-list1 r)))))

#|

Now, provide a tail-recursive implementation.

Here is how to achieve this: one of your arguments will be a list of
subtrees to be visited (a list of trees). Another argument will
collect the values, just as before. Instead of recurring on subtrees,
you put them in the list. You recur on the list, until it gets empty.

Fill in the definition of tree-to-list2-aux, and make sure all
definitions and tests below it work. 

|#

(defdata treelist (listof tree))

(defunc tree-to-list2-aux (l acc)
  :input-contract (and (treelistp l) (listp acc))
  :output-contract (listp (tree-to-list2-aux l acc))
  ...
  ...
  ...
  ...
  ...
  ...
  ...)

(defunc tree-to-list2 (r)
  :input-contract (treep r)
  :output-contract (listp (tree-to-list2 r))
  (tree-to-list2-aux (list r) nil))

(acl2::test?
 (implies (and (treep r)
               (in-tree a r))
          (in a (tree-to-list2 r))))

(acl2::test?
  (implies (treep r)
           (equal (count-tree x r)
                  (count-list x (tree-to-list2 r)))))

#|

All implementations should meet the properties given, but this
does not mean that they should provide the same answers! Fill in
the dots below, i.e., provide two different input trees on which
the implementations disagree.

|#

(acl2::test?
 (let ((r ...))
   (and (treep r)
        (not (equal (tree-to-list r)
                    (tree-to-list1 r))))))

(acl2::test?
 (let ((r ...))
   (and (treep r)
        (not (equal (tree-to-list r)
                    (tree-to-list2 r))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 2. Conjecture Contract Completion
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

The conjectures in this Section are incomplete (irrespective of
whether they are true of false): they are lacking hypotheses that make
sure the functions involved are called only on arguments that satisfy
the functions' input contracts. Make the conjectures meaningful by
adding the necessary contract hypotheses. For example, given a
conjecture c , if you think hypotheses h1 and h2 (and nothing else)
are necessary to ensure the input contracts of all functions occurring
in c are satisfied, your answer should be

  (implies (and h1 h2) c)

Simplify the conjecture hypotheses as much as possible. In the above
example, suppose h1 => h2 is valid. Then the conjunction h1 /\ h2 is
equivalent to h1 ; thus, simplify your output to

  (implies h1 c)

Sometimes there is no way to satisfy the input contracts of the
functions that appear in an expression. For example, different
contracts may force some variable to be both a natural number and a
list at the same time. Of course, (natp x) /\ (listp x) is
unsatisfiable. If you encounter a conjecture where this happens, then
the conjecture is meaningless, since there is no way to satisfy its
hypotheses; just comment out the conjecture and write a comment
explaining why.

[a]

Add the required hypotheses to the following conjectures, by filling
in the dots. We re-use functions from Part 1.

1.

(implies ...
         (equal (factorial-aux n 1)
                (factorial n)))

2.
                
(implies ...
         (equal (len (tree-to-list2-aux q (tree-size r)))
                (tree-size r)))

3.

(implies ...
         (equal (tree-size (list a b c))
                (+ (tree-size a)
                   (+ 1 (tree-size b)))))

4.

(implies ...
         (and (equal (len r) k)
              (> (count-tree a r) k)))

5.

(implies ...
         (not (in r (tree-to-list r))))

6.

(implies ...
         (equal (tree-size (cons a b))
                (+ (tree-size a)
                   (tree-size b))))

7.

(implies ...
         (> (count-tree a r) (count-list a r)))

8.

(implies ...
         (<= (+ (count-tree a (first r)) (count-tree a (third r)))
             (count-tree a r)))
                   
[b]

Test the conjectures you produced above, by using acl2::test? .
Ignore the non-meaningful conjectures, i.e., the ones that inevitably
lead to a contract violation. 

Which of the functions are candidate theorems? Provide counterexamples
for the rest.

|#

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 3. Equational Reasoning
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

The following questions ask for equational proofs about ACL2s
programs. Follow the steps introduced in class:

- Perform conjecture contract closure, adding hypotheses (if
  necessary).

- Use propositional reasoning to rewrite the conjecture into one or
  more implications with a conjunction of hypotheses in the antecedent
  and a single expression in the conclusion (if necessary).

- Extract the context (the hypotheses), and determine the derived
  context: anything that follows immediately from the context
  expressions. Remember that you cannot instantiate context
  expressions -- these are not theorems!

- Now write your equational reasoning proof. Be sure to justify each
  step in the style shown in class, e.g.,

      (len (list x))
  = { def. len, first/rest axioms, def list }
      1

  You can use basic arithmetic facts for free. In the justification,
  write "arithmetic", e.g.,

      (len (rest x)) + 2 + (first x) + 1
  = { Arithmetic }
      (first x) + (len (rest x)) + 3

  You can use the same format for proving inequalities. For example,
  you could prove that (len (cons a b)) > (len b) as follows:

      (len (cons a b))
  = { def. len, if axioms, def. atom, consp axioms }
      (+ 1 (len (rest (cons a b))))
  = { rest-cons axioms }
      (+ 1 (len b))
  > { arithmetic }
      (len b)

You can of course also use previously (in class or in homework) proved
theorems! In this case, cite the theorem in the justification, and
give the substitution that shows how you instantiated the theorem.

We will re-use definitions from parts 1 and 2 of this homework.

Recall that for each of the defunc's above we get both a definitional
axiom (input contract => function application = function body), and a
contract theorem (input contract => output contract). 

You can freely use both definitional axioms and contract theorems in 
what follows, as ACL2s has accepted these functions.

|#


















#|

[a]

Prove the following conjecture using equational reasoning:

(implies (treep r)
         (and (implies (and (consp r)
                            (equal (len (tree-to-list (first r)))
                                   (tree-size (first r)))
                            (equal (len (tree-to-list (third r)))
                                   (tree-size (third r))))
                       (equal (len (tree-to-list r))
                              (tree-size r)))
              (implies (endp r)
                       (equal (len (tree-to-list r))
                              (tree-size r)))))
                              
Hints:

- Use Theorem 3.1 from the lecture notes. We quote it for your
  convenience:

    (listp y) /\ (listp z) =>
    (app (cons x y) z) = (cons x (app y z))
  
- Exploit the output contract of app, which relates app and len .

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...

|#

#|
    
[b]

Prove the following conjecture using equational reasoning:

(implies (and (listp x) (listp y))
         (and (implies (endp x)
                       (equal (count-list a (app x y))
                              (+ (count-list a x)
                                 (count-list a y))))
              (implies (and (consp x)
                            (equal (count-list a (app (rest x) y))
                                   (+ (count-list a (rest x))
                                      (count-list a y))))
                       (equal (count-list a (app x y))
                              (+ (count-list a x)
                                 (count-list a y))))))

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...

|#

#|

[c]

Prove the following conjecture using equational reasoning:

(and
 (implies (and (treep r) (endp r))
          (iff (> (count-tree a r) 0)
               (in-tree a r)))
 (implies (and (treep r)
               (consp r)
               (iff (> (count-tree a (first r)) 0)
                    (in-tree a (first r)))
               (iff (> (count-tree a (third r)) 0)
                    (in-tree a (third r))))
          (iff (> (count-tree a r) 0)
               (in-tree a r))))
               
Hint: there are multiple ways to prove a bidirectional implication
(iff). You can start from one side and prove that it is equivalent to
the other, very similar to what we do for equalities.  Alternatively,
you can prove the two directions of the bidirectional implication
independently: to prove F <=> G , you need to show that F => G , and
also that G => F . You could also start with the whole iff expression,
and prove that it is equal to t . You are free to apply any of these
strategies.

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

Please fill out the following form.

https://docs.google.com/spreadsheet/viewform?rm=full&formkey=dE80bmVQSkl5TmtydlF1SzRHNDFmVUE6MA

We do not keep track of who submitted what, so please be honest. Each
individual student should fill out the form, e.g., if there are two
people on a team, then each of these people should fill out the form.

Notice that you can actually fill out the form many times. Don't do
that because we have no idea who submitted what and can't identify
multiple submissions from the same person.

After you fill out the form, write your name below in this file, not
on the questionnaire. We have no way of checking if you submitted the
file, but by writing your name below you are claiming that you did,
and we'll take your word for it.

10 EXP points out of the total 100 for the homework will be awarded if
every member of your team fills out the form. If you cannot get a hold
of a team member, then indicate that and we'll give everyone who
claims to have filled out the questionnaire EXP.

|#