#|

CS 2800 Homework 6 - Summer 2015

This homework is done in groups. The rules are:

 * ALL group members must submit the homework file (this file)

 * The file submitted must be THE SAME for all group members (we
   use this to confirm that alleged group members agree to be
   members of that group)

 * You must list the names of ALL group members below using the
   format below. If you fail to follow instructions, that costs
   us time and it will cost you points, so please read carefully.

Names of ALL group members: Thomas Pedbereznak, Sean Johnsen, Brian Roth

Note: There will be a 10 pt penalty if your names do not follow
this format.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; A -- Conjecture Contract Checking / Contract Completion
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

The following conjectures are incomplete (irrespective of whether they are
true or 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 output should be

h1 /\ h2 => c

The added hypotheses should be minimal. Therefore:

- do not add any hypotheses that are enforced by the output contracts of
the participating functions. For instance, if the expression (f (g x))
appears in your conjecture, and g : type1 -> type2 and f : type2 -> type3,
then do not add (type2p (g x)) as a hypothesis: this is guaranteed by the
output contract of g.

- simplify the conjecture hypotheses as much as possible. In the above
example, suppose h1 => h2 is valid (say h1 = (equal x nil) and h2 = (listp x)).
Then the conjunction h1 /\ h2 is equivalent to h1 ; thus, simplify your
output to

h1 => c

The examples below may contain some unknown functions (whose signature will
be provided), and known functions such as + . The input contracts of _all_
functions need to be enforced by the hypotheses.

1. Given

foo: List x List -> List
bar:  All x List -> List

the conjecture c is

  (foo (bar (+ x y) l) z)   =   (bar (+ y x) (foo l z))

Conjecture with hypotheses:

c1: (rationalp x)
c2: (rationapl y)
c3: (listp l)
c4: (listp z)

(rationalp x) /\ (rationalp y) /\ (listp l) /\ (listp z) => (foo (bar (+ x y) l) z) = (bar (+ y x) (foo l z))

2. Consider the following two definitions, the first of which gives rise to
a recognizer natlistp:

|#

(defdata natlist (listof nat))

(defunc evenlistp (l)
  :input-contract t
  :output-contract (booleanp (evenlistp l))
  (if (listp l)
    (integerp (/ (len l) 2))
    nil))

#|

For the following functions we only know the signature:

d: List -> All
m: Nat x List -> NatList
f: List -> Nat
s: EvenList -> List

the conjecture c is

(d (m x l)) = (f (s l))

Conjecture with hypotheses:

c1: (natp x)
c2: (evenlistp l)

(natp x) /\ (evenlistp x) => (d (m x l)) = (f (s l))

Now define four functions d, m, f, s (as simple as possible) with the above
signatures. 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 natlist.

|#

; d: List -> All
(defunc d (l)
  :input-contract (listp l)
  :output-contract t
  0)

(check= (d nil) 0)
(check= (d '(1)) 0)
(check= (d '(1 v)) 0)
(check= (d '(a b c)) 0)

; m: Nat x List -> Natlist
(defunc m (n l)
  :input-contract (and (natp n) (listp l))
  :output-contract (natlistp (m n l))
  nil)

(check= (m 0 nil) nil)
(check= (m 1 '(1)) nil)
(check= (m 1 '(a b 1)) nil)
(check= (m 11 '(11111)) nil)

; f: List -> Nat
(defunc f (l)
  :input-contract (listp l)
  :output-contract (natp (f l))
  1)

(check= (f nil) 1)
(check= (f '(1)) 1)
(check= (f '(2 2)) 1)
(check= (f '(24 a b)) 1)

; s: EvenList -> List
(defunc s (el)
  :input-contract (evenlistp el)
  :output-contract (listp (s el))
  nil)

(check= (s nil) nil)
(check= (s '(1 2)) nil)
(check= (s '(1 1 b 1)) nil)
(check= (s '(a b d f g f)) nil)

; Suppose we want to write a function that tests our conjecture:

(defunc dummy (x l)
  :input-contract (and (natp x) (evenlistp l))
  :output-contract (booleanp (dummy x l))
  (equal (d (m x l)) (f (s l))))

(check= (dummy 1 '(1 1)) nil)
(check= (dummy 0 nil) nil)
(check= (dummy 2 '(a b c d)) nil)
(check= (dummy 8 '(a 1)) nil)

#|

Complete the function definition. That is, replace the first ... with the
hypotheses you found, and the second ... with an appropriate output
contract. Make sure this definition is accepted by ACL2! Test this function
on at least one input.

3. Given function signatures for d, m, f, s as above in 2, the conjecture c
now is

(d (m x l)) = (f (s x))

Conjecture with hypotheses:

c1: (natp x)
c2: (listp l)
c3: (evenlistp x)

(natp x) /\ (listp l) /\ (evenlistp x) => (d (m x l)) = (f (s x))

Suppose again we want to write a function that tests our conjecture:

|#

(defunc dummy-new (x l)
  :input-contract (and (listp l) (natp x) (evenlistp x))
  :output-contract (booleanp (dummy-new x l))
  (equal (d (m x l)) (f (s x))))

;(check= (dummy-new nil nil) t)

#|

I wrote this check= and ACL2 yelled at me. This is because the input contract / hypotheses
will never be satified because it is impossible for an Any to be a nat and an evenlist at the same time.
This makes the conjecture true, due the the fact that we will never get valid input.

|#

#|

Using the same examples for d, m, f, s as above, complete the function
definition. That is, replace the first ... with the hypotheses you found,
and the second ... with an appropriate output contract. Make sure this
definition is accepted by ACL2! Test this function on at least one
input. Explain what happens. Is the conjecture true or false?

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; B -- Equational reasoning
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

The following questions ask for "equational proofs" (the type of proofs we
have been doing to far) about ACL2s programs. When writing your proofs be
sure to justify each step in the style shown in class. You can use basic
arithmetic facts for free, but in the justification write "arithmetic",
e.g.,

    (first x) + (len (rest x)) + 0

= { Arithmetic }

    (len (rest x)) + (first x)

You may use infix notation (like x+y+z) for arithmetic operators (as done
above), instead of the LISP style prefix notation (like (+ x (+ y z))).

Here are the common definitions used for the remainder of the questions.

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

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

(defunc not (a)
  :input-contract (booleanp a)
  :output-contract (booleanp (not a))
  (if a nil t))

(defunc listp (l)
  :input-contract t
  :output-contract (booleanp (listp l))
  (or (equal l ())
      (consp l)))

(defunc endp (a)
  :input-contract (listp a)
  :output-contract (booleanp (endp a))
  (not (consp a)))

(defunc twice (l)
  :input-contract (listp l)
  :output-contract (listp (twice l))
  (if (endp l)
    nil
    (cons (first l) (cons (first l) (twice (rest l))))))

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

(defunc rev (x)
  :input-contract (listp x)
  :output-contract (and (listp (rev x)) (equal (len x) (len (rev x))))
  (if (endp x)
    nil
    (app (rev (rest x)) (list (first x)))))

Recall that for each of the defunc's above we get both a definitional
axiom (ic => function application = function body), and a contract
theorem (ic => oc). Definitional axioms and contract theorems are there for
you to use, as ACL2s has accepted these functions.

For the following claims, run some tests to conjecture whether they are
true or false. In the former case, prove them using equational reasoning.
In the latter case, disprove them by means of a counterexample. A
counterexample is an assignment to ALL free variables in the conjecture
that makes the conjecture evaluate to false. Do not give "partial
counterexamples" (leaving it to us to complete them).

The Lecture Notes, section "3.1 Testing Conjectures" describes how to test
conjectures.

(a)

(implies (listp y)
         (equal (len (rev (cons x y)))
                (+ 1 (len (rev y)))))

Hint: output contract of rev. If you make use of that, make sure you quote
an appropriate theorem or axiom.


(test? (implies (listp y)
                (equal (len (rev (cons x y)))
                       (+ 1 (len (rev y))))))

The test passed, here is the proof:

c1: (listp y)
c2: (listp (cons x y)) {c1, Def cons}

(len (rev (cons x y)))
= {Contract theorem Rev, c1, c2}
(len (cons x y))
= {Def len, instantiation}
(if (atom (cons x y)) 0 (+ 1 (len (rest (cons x y)))))
= {Def atom}
(if (not (consp (cons x y))) 0 (+ 1 (len (rest (cons x y)))))
= {if axioms, Def not, Def consp, c1, c2}
(+ 1 (len (rest (cons x y))))
= {first-rest axioms, Def Cons}
(+ 1 (len y))
= {Contract theorem Rev, c1}
(+ 1 (len (rev y)))

LHS = RHS      Q.E.D.

(b)


(implies (and (listp x)
              (listp y)
              (listp z))
         (implies (equal (twice (app      x     z)) (app (twice      x    ) (twice z)))
                  (equal (twice (app (cons x y) z)) (app (twice (cons x y)) (twice y)))))

Can be rewriten to:

(implies (and (listp x)
              (listp y)
              (listp z)
              (equal (twice (app x z)) (app (twice x) (twice z))))
          (equal (twice (app (cons x y) z)) (app (twice (cons x y)) (twice y))))


(test? (implies (and (listp x)
                     (listp y)
                     (listp z))
                (implies (equal (twice (app x z)) (app (twice x) (twice z)))
                         (equal (twice (app (cons x y) z)) (app (twice (cons x y)) (twice y))))))



ACL2 Showed this conjecture to be false througha counter example.

One such example we will show through instantation:

(equal (twice (app (cons x y) z)) (app (twice (cons x y)) (twice y)))
= {Instantation ((x nil) (y nil) (z '(1 2 3)))}
(equal (twice (app (cons nil nil) '(1 2 3))) (app (twice (cons nil nil)) (twice nil)))
= {Def twice, Def app, if axioms}
(equal '(1 1 2 2 3 3) nil)
= {Def equal}
false


(c)

(implies (listp x)
         (and (implies (endp x)
                       (equal (len (twice x))
                              (* 2 (len x))))
              (implies (and (not (endp x))
                            (equal (len (twice (rest x)))
                                   (* 2 (len (rest x)))))
                       (equal (len (twice x))
                              (* 2 (len x))))))


(test? (implies (listp x)
                (and (implies (endp x)
                              (equal (len (twice x))
                                     (* 2 (len x))))
                     (implies (and (not (endp x))
                                   (equal (len (twice (rest x)))
                                          (* 2 (len (rest x)))))
                              (equal (len (twice x))
                                     (* 2 (len x)))))))

The test passed, here is the proof:

Part 1:

(implies (and (listp x)
              (endp x))
         (equal (len (twice x))
                (* 2 (len x))))

c1: (listp x)
c2: (endp x)
c3 x = nil {c1, c2, def list, def endp}

(len (twice x))
= {Def twice, if axioms, c3}
(len nil)
= {Def len, if axioms}
0
= {Arithmetic}
(* 2 0)
= {Def len, if axioms}
(* 2 (len nil))
= {c3}
(* 2 (len x))

RHS = LHS

Part 2:

(implies (and (listp x)
              (not (endp x))
              (equal (len (twice (rest x)))
                     (* 2 (len (rest x))))))

c1: (listp x)
c2: (not (endp x))
c3: (equal (len (twice x))
           (*2 (len x)))


(len (twice x))
= {Def twice, c2}
(len (cons (first x) (cons (first x) (twice (rest x)))))
= {Def len, cons axiom, def atom, if axioms}
(+ 1 (len (cons (first x) (twice (rest x)))))
= {Def len, cons axiom, def atom, if axioms}
(+ 1 (+ 1 (len (twice (rest x)))))
= {Arithmetic}
(+ 2 (len (twice (rest x))))
= {c3}
(+ 2 (* 2 (rest x)))
= {Arithmetic}
(* 2 (+ 1 (len (rest x))))
= {c1, c2, Def len, if axioms, Def atom}
(* 2 (len x))

RHS = LHS

(Part 1) /\ (Part 2) == True

Q.E.D.


|#