CS 2800 Homework 8 - Spring 2013

This homework does not require ACL2s.

Instructions for using this file:

- Open this file with your editor of choice. Make sure that you save
  your modified file as plain ASCII text. For example, handing in a
  file in Microsoft Word format is not allowed. You can use ACL2s
  if you wish, in which case you can also use it check your
  answers (using acl2::test? for example).

- Insert your solutions into this file where indicated (for instance
  as "..."). This includes equational proofs, explanations, and
  formulas.

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

  svn://dell-server-wahl-1.ccs.neu.edu/cs2800-2013-spring/08/<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 hw08.txt in this directory, add it, and commit.

- 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
=============

Definitions
-----------

We will use the following definitions throughout this homework. You
have seen most of them already.

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

(defunc rotate-left (x n)
  :input-contract (and (listp x) (natp n))
  :output-contract (listp (rotate-left x n))
  (cond ((equal n 0) x)
        ((endp x) x)
        (t (rotate-left (app (rest x) (list (first x)))
                        (- n 1)))))

(defunc exp (n k)
  :input-contract (and (natp n) (natp k))
  :output-contract (natp (exp n k))
  (if (equal k 0)
      1
      (* n (exp n (- k 1)))))

Recall that for each of the defunc's above we have both a definitional
axiom, and a contract theorem. For example for len, we have the
definitional axiom:

(implies t
         (equal (len a)
                (if (atom a)
                    0
                    (+ 1 (len (rest a))))))

which is equivalent to (by propositional logic)

(equal (len a)
       (if (atom a)
           0
           (+ 1 (len (rest a)))))

The contract theorem is:

(implies t (natp (len a)))

which is equivalent to 

(natp (len a))

Recall that you get to use definitional axioms and contract theorems
for free, i.e., you don't have to prove anything to use them.

Trees
-----

We will use the same definition of trees as in the previous homework:

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

The definition above gives raise to a recognizer called treep. 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, the following theorems hold (by construction):

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

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

3. (treep r) => (listp r)

We will use the following functions that operate on 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 tree-depth (r)
  :input-contract (treep r)
  :output-contract (natp (tree-depth r))
  (if (endp r)
      0
      (+ 1 (if (> (tree-depth (first r))
                  (tree-depth (third r)))
               (tree-depth (first r))
               (tree-depth (third r))))))


1.  Equational Reasoning
========================

A. Prove the following conjecture using equational reasoning:

(implies (treep r)
         (and (implies (endp r)
                       (<= (tree-depth r)
                           (tree-size r)))
              (implies (and (consp r)
                            (<= (tree-depth (first r))
                                (tree-size (first r)))
                            (<= (tree-depth (third r))
                                (tree-size (third r))))
                       (<= (tree-depth r)
                           (tree-size r)))))

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

B. Prove the following conjecture using equational reasoning:

(implies (and (natp a)
              (natp b)
              (natp n))
         (and (implies (equal n 0)
                       (equal (exp (* a b) n)
                              (* (exp a n) (exp b n))))
              (implies (and (not (equal n 0))
                            (equal (exp (* a b) (- n 1))
                                   (* (exp a (- n 1))
                                      (exp b (- n 1)))))
                       (equal (exp (* a b) n)
                              (* (exp a n) (exp b n))))))

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

C1. Prove the following conjecture using equational reasoning:

(implies (and (listp x) (listp y))
         (and
          (implies (endp x)
                   (iff (in a (app x y))
                        (or (in a x) (in a y))))
          (implies (and (not (endp x))
                        (not (equal a (first x)))
                        (iff (in a (app (rest x) y))
                             (or (in a (rest x)) (in a y))))
                   (iff (in a (app x y))
                        (or (in a x) (in a y))))
          (implies (and (not (endp x))
                        (equal a (first x))
                        (iff (in a (app (rest x) y))
                             (or (in a (rest x)) (in a y))))
                   (iff (in a (app x y))
                        (or (in a x) (in a y))))))

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

C2. As we will see in class soon, the conjecture in part [C1], which
is now a theorem, corresponds to our proof obligation when proving the
following theorem by induction:

(implies (and (listp x)
              (listp y))
         (iff (in a (app x y))
              (or (in a x) (in a y))))

Assume you have proved the theorem above. Prove the following
conjecture using equational reasoning:

(implies
 (and (listp x)
      (natp n))
 (and
  (implies (equal n 0)
           (equal (in a (rotate-left x n))
                  (in a x)))
  (implies (and (not (equal n 0))
                (iff (in a (rotate-left
                            (app (rest x) (list (first x)))
                            (- n 1)))
                     (in a (app (rest x) (list (first x))))))
           (iff (in a (rotate-left x n))
                (in a x)))))

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

2. Definitional Principle
=========================

Preliminaries
-------------

Recall the "Definitional Principle":

The definition

(defunc f (x1 ... xn)
  :input-contract ic
  :output-contract oc 
  body)

is _admissible_ provided:

I. f is a new function symbol, i.e., there are currently no theorems
or axioms about the function f. Note that this happens in the context
of a history of function definitions.

II. The xi are pairwise distinct variable symbols.

III. body is a term mentioning no free variables other than the
xi. Note that body may use f recursively as a function symbol with the
correct number of arguments. It goes without saying that the xi cannot
be used as function symbols. Also, no undefined function symbols
should be used.

IV. The function is "terminating", i.e., it terminates on all valid
inputs.

V. ic => oc is a theorem.

VI. The body contracts hold under the assumption that ic holds.

If admissible, the logical effect of the definition is to add two new
axioms:

- definitional axiom for f: ic => [(f x1 ... xn) = body].
-     contract axiom for f: ic => oc.

Exercise
--------

For each of the definitions below, check whether it is admissible,
i.e., it satisfies the definitional principle. You can assume that f is
a new function symbol in each case.

If yes,

1. Provide a measure function that can be used to show termination.
2. Explain in English why the contract axiom holds.
3. Explain in English why the body contracts hold.

If no,

1. Identify which of the 6 conditions above are violated.
2. If IV is satisfied, provide a measure function. If IV is violated,
   provide a valid input on which the function does not terminate.

Note that some of the conditions of admissibility make no sense if
certain others are violated. For example, if the function does not
terminate on all inputs (IV is violated), there is no point checking
the contract axiom (V). Similarly, if the body contains free variable
symbols other than the xi, it cannot be evaluated, so the remaining
conditions make no sense.

Assume that all the functions mentioned in this homework are already
defined (search for the text "defunc" above this line). The history of
function definitions additionally contains standard ACL2s definitions,
e.g., listp , natp , endp , first , and rest .

(defunc f (l)
  :input-contract (listp l)
  :output-contract (listp (f l))
  (if (endp l)
      nil
      (g (rest l) (list (first l)))))

...

(defunc f (n a n)
  :input-contract (and (natp n) (listp a))
  :output-contract (natp (f n a n))
  (if (endp a)
      0
      (f n (rest a) n)))

...

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

...

(defunc f (x y)
  :input-contract (and (listp x) (listp y))
  :output-contract (natp (f x y))
  (if (endp x)
    -1
    (f (rest x) (cons 1 y))))

...

(defunc f (x a)
  :input-contract (and (listp x) (natp a))
  :output-contract (natp (f x a))
  (if (endp x)
    a
    (f (rest x) (+ a 1))))

...

(defunc f (x y)
  :input-contract (and (integerp x) (integerp y))
  :output-contract (integerp (f x y))
  (if (equal x 0)
      0
      (+ (* 2 y) (f (- x 1) y))))

...

(defunc f (x a)
  :input-contract (and (integerp  x) (listp a))
  :output-contract (natp (f x a))
  (cond ((< x 0)   (f (len a) (app a a)))
        ((endp a)  0)
        (t         (+ 1 (f x (rest a))))))

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

(defunc f (a n)
  :input-contract (and (listp a) (natp n))
  :output-contract (listp (f a n))
  (if (equal n 0)
      (list n)
      (f (cons (rest a) (first a))
         (- n 1))))

...

(defunc f (x a)
  :input-contract (and (integerp x) (listp a))
  :output-contract (integerp (f x a))
  (cond
   ((endp a)                 68)
   ((equal (len a) x)        71)
   ((equal (len a) (+ x 1))  74)
   ((< x (len a))            (f (+ x 1) (rest a)))
   (t                        (f (- x 1) (cons 1 a)))))

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

(defunc f (a b)
  :input-contract  (and (natp a) (natp b))
  :output-contract (natp (f a b))
  (cond
    ((and (equal a 0) (equal b 0))  0)
    ((< a b)                        (f b a))
    (t                              (f b (- a 1)))))

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


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

#|

Please fill out the following form.

https://docs.google.com/spreadsheet/viewform?formkey=dEZ5aE5jTXd6TGVZRkJOaDFJMkF2MGc6MA

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.

|#