#|
CS 2800 Homework 6 - 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 hw06.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 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.

- 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/06/<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 hw06.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.

|#

#| 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 1. Substitutions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

In this part you will practice applying and recognizing substitutions.
Recall that a substitution is a list of pairs of the form (<var>
<term>). For an expression phi and a substitution sigma, we denote by
phi|sigma the expression obtained by applying the substitution sigma
to phi. Also remember that substitutions do not apply to quoted
variables.

[a]

Let

  phi = (+ x (* (f n) (+ 'n x)))

and

  sigma = ((x (+ n 2)) (n (+ m 1))) .

Determine phi|sigma .

...

[b]

Let

  phi = (a 'x (a (a (b x) y) (b 'y)))

and

  sigma = ((x (+ z z)) (y (cons v w))) .

Determine phi|sigma.

...

Determine (phi|sigma)|sigma .

...

[c]

Let

  phi = (a (a 'x y) (a (a (a b a) 'a) (b 'y)))

and

  sigma = ((x (+ a b)) (b a) (a b) (y (a x y))) .

Determine phi|sigma.

...

Determine (phi|sigma)|sigma .

...

[d]

For any formula phi and any substitution sigma, (phi|sigma)|sigma =
phi|sigma . Is this claim true or false? If true, explain why. If
false, give a counterexample.

...
...

[e]

Let

  phi = (- (* a b) (+ (* c d) (- d a)))

and

  psi = (- (* b a) (+ (* 71 (f b)) (- (f b) b))) .

Does there exist sigma such that phi|sigma = psi ? If your answer is
yes, give one. If your answer is no, explain why not.

...

[f]

Let phi = (p (+ x y) (* (* 2 x) y)) . Then, for any two substitutions
sigma1 and sigma2, (phi|sigma1)|sigma2 = (phi|sigma2)|sigma1. Is this
claim true or false? If true, explain why. If false, give a
counterexample.

...
...

|#

#|

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

For the following functions, we only know the signature:

f: Nat -> Nat
m: List -> List
c: Nat x List -> List
r: Nat x List -> Nat

[a]

Define functions f, m, c, and r with the above signatures. Your
functions should be as simple as possible! The actual outputs of the
functions are arbitrary, as long as they satisfy the output
contract. For example, for m, you may choose to simply return the
constant nil, which is a list.

|#

(defunc f (x)
  :input-contract ...
  :output-contract ...
  0)

(defunc m (a)
  :input-contract ...
  :output-contract ...
  nil)

(defunc c (x a)
  :input-contract ...
  :output-contract ...
  nil)

(defunc r (x a)
  :input-contract ...
  :output-contract ...
  0)

#|

[b1]

We will now try to define more complex functions by reusing f, m, c,
and r. For each of the definitions, fill in the dots with contracts
such that ACL2 accepts the function.

The added contracts should be minimal. Therefore, do not add any
hypotheses that are enforced by the output contracts of the
participating functions. For instance, if your contract already
imposes the condition (listp a), and (m a) appears in a context where
a list is expected, you contract should not mention (listp (m a)) as
this is guaranteed by the output contract of m.

Sometimes there is no way to satisfy the input contracts of the
functions that appear in an expression. As an example, consider the
following definition:

  (defunc g0 (x)
    :input-contract ...
    :output-contract ...
    (c x x))

By instantiating the input contract of c with the substitution ((x
x) (a x)) , we get (and (natp x) (listp x)) . This formula is
equivalent to nil, because x cannot be a natural number and a list at
the same time! If you encounter such cases, then just comment out the
definition and write a comment explaining why the input contract is
nil.

Your output contracts should be as strong as possible. For example, t
is always a valid output contract, but it does not provide any useful
information.  Also, your output contracts should only depend on the
contracts of f, m, c, and r, and not on the concrete computation that
your implementations happen to perform. For example, consider the
following definition:

  (defunc g0 (x)
    :input-contract ...
    :output-contract ...
    (m x))

The input-contract should be (listp x) because of m's input
contract. The output contract should be (listp (g0 x)), even
though your implementation of m returns nil, because that is the
strongest contract that only depends on m's contract (i.e.  does
not depend on m's body).

|#

(defunc g1 (x y z)
  :input-contract ...
                  ...
                  ...
  :output-contract ...
  (r (f x) (m (c y (m z)))))
...

(defunc g2 (x y)
  :input-contract ...
  :output-contract ...
  (r x (r y (c x y))))
...

(defunc g3 (x y)
  :input-contract ...
                  ...
  :output-contract ...
  (equal (m (c x y))
         (c (f x) (m y))))
...

(defunc g4 (x y z)
  :input-contract ...
  :output-contract ...
  (c x (c y (r x z))))
...
(defunc g5 (x y z w v)
  :input-contract ...
                  ...
                  ...
                  ...
                  ...
  :output-contract ...
  (implies (and (<= (r x (c x y))
                    (r z (c z y)))
                (<= (r z (c z v))
                    (r w (c w v))))
           (equal (c x (c z (c w v))) y)))
...
#|

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 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 use the following function definitions:

(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 list-of-t (n)
  :input-contract (natp n)
  :output-contract (listp (list-of-t n))
  (if (equal n 0)
      nil
      (cons t (list-of-t (- n 1)))))

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

#|

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). Definitional
axioms and contract theorems are there for you to use, as ACL2s has
accepted these functions.

[a]

Prove the following conjecture using equational reasoning:

(implies (and (natp n)
              (> n 0)
              (equal (len (list-of-t (- n 1)))
                     (- n 1)))
         (equal (len (list-of-t n)) n))

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

|#

#|

[b1]

Prove the following conjecture using equational reasoning:

(implies (and (natp m)
              (natp n))
         (and (implies (equal m 0)
                       (equal (app (list-of-t m)
                                   (list-of-t n))
                              (list-of-t (+ m n))))
              (implies (and (> m 0)
                            (equal (app (list-of-t (- m 1))
                                        (list-of-t n))
                                   (list-of-t (+ (- m 1) n))))
                       (equal (app (list-of-t m)
                                   (list-of-t n))
                              (list-of-t (+ m n))))))

Hint: break the conjecture into two parts, and prove them
independently. For both parts, be careful with the context: e.g., you
have to take into account the hypotheses that the outer implication
enforces.

...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
[b2]

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

(implies (and (natp n)
              (natp m))
         (equal (app (list-of-t m)
                     (list-of-t n))
                (list-of-t (+ m n))))

Assume that you proved the theorem above. After all, you did all the
hard work! Prove the following conjecture using equational reasoning:

(implies (and (natp k)
              (natp m)
              (natp n))
         (equal (app (list-of-t k)
                     (app (list-of-t m)
                          (list-of-t n)))
                (list-of-t (+ k (+ m n)))))

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

[c]

Prove the following conjecture using equational reasoning:

(implies (and (natp n)
              (natp k))
         (and (implies (equal k 0)
                       (implies (and (> n 0)
                                     (> k 0))
                                (> (factorial (+ n k))
                                   (factorial n))))
              (implies (equal k 0)
                       (implies (implies (and (> n 0)
                                              (> k 0))
                                         (> (factorial (+ n k))
                                            (factorial n)))
                                (implies (and (> n 0)
                                              (> (+ k 1) 0))
                                         (> (factorial (+ n (+ k 1)))
                                            (factorial n)))))
              (implies (> k 0)
                       (implies (implies (and (> n 0)
                                              (> k 0))
                                         (> (factorial (+ n k))
                                            (factorial n)))
                                (implies (and (> n 0)
                                              (> (+ k 1) 0))
                                         (> (factorial (+ n (+ k 1)))
                                            (factorial n)))))))

For your information, the above conjecture corresponds to our
proof obligation when proving the following theorem by induction:

(implies (and (natp n)
              (natp k)
              (> n 0)
              (> k 0))
         (> (factorial (+ n k)) (factorial n)))

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

|#

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

#|

Please fill out the following feedback form, not as a team, but each team
member individually:

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

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.

|#