; **************** BEGIN INITIALIZATION FOR ACL2s B MODE ****************** ;
; (Nothing to see here!  Your actual file is after this initialization code);

#|
Pete Manolios
Fri Jan 27 09:39:00 EST 2012
----------------------------

Made changes for spring 2012.


Pete Manolios
Thu Jan 27 18:53:33 EST 2011
----------------------------

The Beginner level is the next level after Bare Bones level.

|#

; Put CCG book first in order, since it seems this results in faster loading of this mode.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "ccg/ccg" :uncertified-okp nil :dir :acl2s-modes :ttags ((:ccg)) :load-compiled-file nil);v4.0 change

;Common base theory for all modes.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "base-theory" :dir :acl2s-modes)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "custom" :dir :acl2s-modes :uncertified-okp nil :ttags :all)

;Settings common to all ACL2s modes
(acl2s-common-settings)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading trace-star and evalable-ld-printing books.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "trace-star" :uncertified-okp nil :dir :acl2s-modes :ttags ((:acl2s-interaction)) :load-compiled-file nil)
(include-book "hacking/evalable-ld-printing" :uncertified-okp nil :dir :system :ttags ((:evalable-ld-printing)) :load-compiled-file nil)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s Beginner mode.") (value :invisible))
;Settings specific to ACL2s Beginner mode.
(acl2s-beginner-settings)

; why why why why
(acl2::xdoc acl2s::defunc) ; almost 3 seconds

(cw "~@0Beginner mode loaded.~%~@1"
    #+acl2s-startup "${NoMoReSnIp}$~%" #-acl2s-startup ""
    #+acl2s-startup "${SnIpMeHeRe}$~%" #-acl2s-startup "")


(acl2::in-package "ACL2S B")

; ***************** END INITIALIZATION FOR ACL2s B MODE ******************* ;
;$ACL2s-SMode$;Beginner
#|

CS 2800 Homework 9 - Spring 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: FirstName1 LastName1, FirstName2 LastName2, ...

There will be a 10 pt penalty if your names do not follow this format.
All names must be on one line.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For (parts of) this homework you will need to use ACL2s.

Technical instructions:

- open this file in ACL2s as hw09.lisp

- make sure you are in BEGINNER mode. This is essential! Note that you can
  only change the mode when the session is not running, so set the correct
  mode before starting the session.

- only add to the file. Do not remove or comment out anything pre-existing.

- insert your solutions into this file where indicated (usually as "...")

- make sure the entire file is accepted by ACL2s. In particular, there must
  be no "..." left in the code. If you don't finish all problems, comment
  the unfinished ones out. Comments should also be used for any English
  text that you may add. This file already contains many comments, so you
  can see what the syntax is.

- when done, save your file and submit it as hw09.lisp

- avoid submitting the session file (which shows your interaction with the
  theorem prover). This is not part of your solution. Only submit the lisp
  file.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Instructions for programming problems:

For each function definition, you must provide both contracts and a body.

You must also ALWAYS supply your own tests. This is in addition to the
tests sometimes provided. Make sure you produce sufficiently many new test
cases. This means: cover at least the possible scenarios according to the
data definitions of the involved types. For example, a function taking two
lists should have at least 4 tests: all combinations of each list being
empty and non-empty.

Beyond that, the number of tests should reflect the difficulty of the
function. For very simple ones, the above coverage of the data definition
cases may be sufficient. For complex functions with numerical output, you
want to test whether it produces the correct output on a reasonable
number if inputs.

Use good judgment. For unreasonably few test cases we will deduct points.

We will use ACL2s' check= function for tests. This is a two-argument
function that rejects two inputs that do not evaluate equal. You can think
of check= roughly as defined like this:

(defunc check= (x y)
  :input-contract (equal x y)
  :output-contract (equal (check= x y) t)
  t)

That is, check= only accepts two inputs with equal value. For such inputs, t
(or "pass") is returned. For other inputs, you get an error. If any check=
test in your file does not pass, your file will be rejected.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Induction schemes
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


#|

Below you are given the proof obligations generated by
induction schemes. Your job is to define functions, using defunc
that give rise to these induction schemes. phi|(...) denotes phi
under substitution ... . Make sure that ACL2s accepts your
function definitions.

For these functions (f1-f5) you do not need to provide
tests (i.e., no check= forms are required).

|#


#|

1. (not (natp x)) => phi
2. (and (natp x) (equal x 0)) => phi
3. (and (natp x) (not (equal x 0)) phi|((x (- x 1))))  => phi

|#

(defunc f1 (x)
:input-contract (natp x)
:output-contract (natp (f1 x))
(if (equal x 0)
    0
  (f1 (- x 1))))

#|

1. (not (posp x)) => phi
2. (and (posp x) (equal x 1)) => phi
3. (and (posp x) (equal x 2)) => phi
4. (and (posp x) (not (equal x 1)) (not (equal x 2)) phi|((x (- x 2))))  => phi

|#

(defunc f2 (x)
:input-contract (posp x)
:output-contract (posp (f2 x))
(cond ((equal x 1) 1)
      ((equal x 2) 2)
      (t (f2 (- x 2)))))

#|

1. (not (listp x)) => phi
2. (and (listp x) (endp x)) => phi
3. (and (listp x) (not (endp x)) phi|((x (rest x))))  => phi

|#

(defunc f3 (x)
:input-contract (listp x)
:output-contract (natp (f3 x))
(if (endp x)
    0
    (+ 1 (f3 (rest x)))))

#|

1. (not (listp x)) => phi
2. (and (listp x) (endp x)) => phi
3. (and (listp x) (not (endp x)) (endp (rest x))) => phi
4. (and (listp x) (not (endp x)) (not (endp (rest x)))
        phi|((x (rest x))) phi|((x (rest (rest x)))))  => phi

|#

(defunc f4 (x)
:input-contract (listp x)
:output-contract (natp (f4 x))
(cond ((endp x) 0)
      ((endp (rest x)) 1)
      (t (+ (f4 (rest x)) (f4 (rest (rest x)))))))

#|

1. (not (and (listp x) (posp y))) => phi
2. (and (listp x) (posp y) (endp x) (equal y 1)) => phi
3. (and (listp x) (posp y) (not (and (endp x) (equal y 1)))
        (endp x) phi|((y (- y 1))) phi|((x (cons 1 x)) (y (- y 1)))) => phi
4. (and (listp x) (posp y) (not (and (endp x) (equal y 1)))
        (not (endp x)) (equal y 1) phi|((x (rest x)))  => phi
5. (and (listp x) (posp y) (not (and (endp x) (equal y 1)))
        (not (endp x)) (not (equal y 1)) phi|((x (rest x)))
        phi|((y (- y 1))))  => phi

Hint: phi|((a (rest a)) (b b)) is the same as
      phi|((a (rest a)))
|#


#|
f5 timed out

(defunc f5 (x y)
:input-contract (and (listp x) (posp y))
:output-contract (natp (f5 x y))
(cond ((and (endp x) (equal y 1)) y)
      ((endp x) (+ (f5 x (- y 1)) (f5 (cons 1 x) (- y 1))))
      ((equal y 1) (f5 (rest x) y))
      (t (+ (f5 (rest x) y) (f5 x (- y 1))))))
|#


#|

We start with some familiar definitions. You will be asked to
define functions later on. Make sure to use defunc.

(defunc listp (x)
  :input-contract t
  :output-contract (booleanp (listp x))
  (if (consp x)
      (listp (rest x))
    (equal x nil)))

(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 (a)
  :input-contract (listp a)
  :output-contract (listp (rev a))
  (if (endp a)
      nil
    (app (rev (rest a)) (list (first a)))))

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

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

|#


#|

Use defdata to define a lor, a list of rational numbers.

|#

(defdata lor (listof rational))

#|

Define orderedp: a function that given a lorp returns a
boolean. orderedp check to see if the list of rationals is
ordered, ie, if each element is <= the elements that come after it.

|#

(defunc orderedp (l)
  :input-contract (lorp l)
  :output-contract (booleanp (orderedp l))
  (cond ((endp l) t)
        ((endp (rest l)) t)
        (t (and (<= (first l) (second l))
                (orderedp (rest l))))))

(check= (orderedp '()) t)
(check= (orderedp '(4)) t)
(check= (orderedp '(0 4 2)) nil)
(check= (orderedp '(0 3 5 6)) t)
(check= (orderedp '(1 0)) nil)


#|

Define insert, a function that is given as input e and l. e
is a rational number and l is a lorp.  Insert traverses l until
it finds a number >= e and inserts e right before this number.
For example (insert 3 '(2 5 6)) is '(2 3 5 6)
|#

(defunc insert (e l)
  :input-contract (and (lorp l) (rationalp e))
  :output-contract (lorp (insert e l))
  (cond ((endp l) (list e))
        ((>= (first l) e) (cons e l))
        (t (cons (first l) (insert e (rest l))))))

(check= (insert 3 '()) '(3))
(check= (insert 3 '(1 2)) '(1 2 3))
(check= (insert 3 '(1 4 5)) '(1 3 4 5))
(check= (insert 3 '(4 5)) '(3 4 5))

#|

Formalize and prove (by hand) the following conjecture:

(insert e l) returns a list whose length is 1 more than the
length of l.

For this and all subsequent questions where you are asked to
prove a theorem by hand, use the proof format introduced in class
and write your answer in a comment. If you are using induction,
clearly identify the function you are using to generate an
induction scheme.

|#

#|

T1:
    (implies (and (listp l)
                  (rationalp e))
             (equal (+ 1 (len l))
                    (len (insert e l))))

Proof:
    This function's induction scheme is

    1. ~(and (listp l) (rationalp e)) => phi
    2. (and (listp l) (rationalp e) (endp l)) => phi
    3. (and (listp l) (rationalp e) ~(endp l) (e < (first l)) (phi | (l (rest l))))
    3. (and (listp l) (rationalp e) ~(endp l) (e > (first l)) (phi | (l (rest l))))

    obligation 1:

    c1: (listp l)
    c1: (rationalp e)

    ~(and (listp l) (rationalp e)) => phi

    ={c1, c2}
    nil => phi

    ={implies}
    t

    obligation 2:

    c1: (listp l)
    c2: (rationalp e)
    c3: (endp l)

    (and (listp l) (rationalp e) (endp l)) => phi


    ={c1, c2, c3, def phi}
    (equal (+ 1 (len l))
            (len (insert e l)))

    ={def insert, c2, c3}
    (equal (+ 1 (len (nil)))
            (len (list e)))

    ={def len, c3}
    (equal (+ 1 0)
            (1))

    ={arith, def equal}
    t

    obligation 3:
    c1: (listp l)
    c2: (rationalp e)
    c3: ~(endp l)
    c4. e < (first l)
    c5: (phi | (l (rest l)))


    derived context
    ={c1,c2,c3,c4,c5}
    c6: (equal (+ 1 (len (rest l)))
                    (len (insert e (rest l))))

    ={def insert, c1, c2, c3, c4}
    (equal (+ 1 (len (rest l)))
            (len (cons e (rest l))))

    ={def len}
    (equal (+ 1 (len (rest l)))
           (+ 1 (len (rest l))))

    ={arith, equal}
    t

    obligation 4:

    c1: (listp l)
    c2: (rationalp e)
    c3: ~(endp l)
    c4. e > (first l)
    c5: (phi | (l (rest l)))


    derived context
    ={c1,c2,c3,c4,c5}
    c6: (equal (+ 1 (len (rest l)))
                    (len (insert e (rest l))))

    ={def insert, c1, c2, c3, c4}
    (equal (+ 1 (len (rest l)))
            (len (cons (first (rest l) (insert e ((rest (rest l))))))))

    ={def len, c1, c2, c3}
    (equal (+ 1 (len (rest l)))
            (+ 1 (len (insert e ((rest (rest l))))))))


    1. ~(and (listp l) (rationalp e)) => phi
    2. (and (listp l) (rationalp e) (endp l)) => phi
    3. (and (listp l) (rationalp e) ~(endp l) (e < (first l)) (phi | (l (rest l))))
    3. (and (listp l) (rationalp e) ~(endp l) (e > (first l)) (phi | (l (rest l))))

    given the above, phi is valid for all l and e
|#

#|

Define isort, a function that is given as input a lorp, and
sorts using insertion sort: if l is empty, return nil. If not,
insert the first into the result of sorting the rest.

|#

(defunc isort (l)
  :input-contract (lorp l)
  :output-contract (lorp (isort l))
  (cond ((endp l) l)
        (t (insert (first l)
                   (isort (rest l))))))

(check= (isort '()) '())
(check= (isort '(0)) '(0))
(check= (isort '(1 2)) '(1 2))
(check= (isort '(2 1)) '(1 2))
(check= (isort '(2 84 0 -9 3)) '(-9 0 2 3 84))


#|

Formalize and prove (by hand) the following conjecture:

(isort l) returns a list whose length is equal to the length of l.

Use the proof format introduced in class and write your answer in
this comment.

|#

#|

Here is the formalization:

(implies (lorp l)
           (equal (len (isort l))
                  (len l))))

Here is the proof:

proof obligations:

1. ~(lorp l) => phi
2. (and (lorp l) (endp l)) => phi
3. (and (lorp l) ~(endp l) (phi | (l (rest l)))) => phi

1.

c1. (lorp l)
~(lorp l) => phi

={c1}
nil => phi

={implies}
t

2.

c1. (lorp l)
c2. (endp l)

(and (lorp l) (endp l)) => (equal (len (isort l))
                  (len l))

={c1, c2}
(equal (len (isort l)) (len l))

={c2, def isort, def len, arith}
0

3.

c1. (lorp l)
c2. ~(endp l)
c3. (phi | (l (rest l)))

={c1,c2}
c4. (consp l)

={c3, phi}
c5. (equal (len (isort (rest l)))
           (len (rest l)))

(equal (len (isort l))
       (len l)))

={def isort, c2}
(equal (len (insert (first l)
                    (isort (rest l))))
       (len l)))

={def len, c4, T1}
(equal (+ 1 (len (isort (rest l))))
       (+ 1 (len (rest l))))

={arith, c5}
t

given the above, phi is valid for all l

|#

#|

Formalize and prove (by hand) the following conjecture:

If l is a lorp, then (isort l) is ordered (satisfies orderedp).

Use the proof format introduced in class and write your answer in
this comment.

Hint: You will need a lemma.

Warning: This proof is not hard, but you will have to discover
and prove a lemma, so the proof will be long. Give yourself
plenty of time to complete this problem. Coming up with the lemma
is going to require some insight!

|#



#|

Here is the formalization:

(implies (lorp l)
         (orderedp (isort l)))


Here is the proof:


proof lemma:

(implies (and (rationalp e) (lorp l) (orderedp l))
         (orderedp (insert e l)))

proof contract:
1. ~(and (lorp l) (rationalp e)) => phi
2. (and (lorp l) (rationalp e) (endp l)) => phi
3. (and (lorp l) (rationalp e) ~(endp l) (>= (first l) e)) => phi
4. (and (lorp l) (rationalp e) ~(endp l) ~(>= (first l) e) (phi | (l (rest l)))) => phi


obligation 1:

c1. (lorp l)

proof:
~(and (lorp l) (rationalp e)) => phi

={c1, implies}
t

obligation 2:

c1. (lorp l)
c2. (rationalp e)
c3. (endp l)

proof:

(orderedp (insert e l))

={def insert, c3}
(orderedp (list e))

={def orderedp}
t

obligation 3:

c1. (lorp l)
c2. (rationalp e)
c3. ~(endp l)
c4. (>= (first l) e))
c5. (orderedp l)

proof:
(orderedp (insert e l))

={def insert, c3, c4}
(ordered (cons e l))

={def orderedp, c4}
(and (<= e (first l))
     (orderedp (rest (cons e l))))

={arith, def rest}
(and t
     (orderedp l))

={c5}
t

obligation 4:

c1. (lorp l)
c2. (rationalp e)
c3. ~(endp l)
c4. ~(>= (first l) e))
c5. (orderedp l)
c6. (phi | (l | (rest l)))

={c5, phi}
c6.(orderedp (insert e (rest l)))

proof:
(orderedp (insert e l))

={def insert, c3, c4}
(orderedp (cons (first l) (insert e (rest l))))

={def orderedp, c3, def cons}
(and (<= (first l) (first (insert e (rest l))))
     (orderedp (insert e (rest l))))

={c6, boolean logic}
(<= (first l) (first (insert e (rest l))))

={c5, c4}
t

due to the above,
(implies (and (rationalp e) (lorp l) (orderedp l))
         (orderedp (insert e l)))


proof Theorem:
(implies (lorp l)
         (orderedp (isort l)))

proof obligations:
1. ~(lorp l) => phi
2. (and (lorp l) (endp l)) => phi
3. (and (lorp l) ~(endp l) (phi | (l (rest l)))) => phi

obligation 1:

c1: (lorp l)

(lorp l) => phi

={c1}
t

obligation 2:
c1: (lorp l)
c2: (endp l)

(orderedp (isort l))

={def isort, c2}
(orderedp '())

={def orderedp}
t

obligation 3:
c1: (lorp l)
c2: ~(endp l)
c3: (phi | (l (rest l)))

={c3, phi, c2}
c4: (orderedp (isort (rest l)))


(orderedp (isort l))

={def isort, c2}
(orderedp (insert (first l)
                  (isort (rest l))))

={(lemma | (e (first l)) (l (rest l)), c4,c2,c3,c1}
t

due to the above, (implies (lorp l) (orderedp (isort l)))

|#


#|

Extra credit.

Get ACL2s to prove all of the theorems you were asked to prove by
hand, including the lemma you had to discover. Here is how you
do that.

Suppose that the theorem you want to prove is

(listp x) => (app x nil) = x

First, turn it into a legal ACL2s expression and second use
the "defthm" form, which requires giving the theorem a name. Here
is what the defthm will look like:

(defthm app-x-nil-thm
  (implies (listp x)
           (equal (app x nil)
                  x)))

One thing to keep in mind is that if you have a defthm of
the form

(1) hyp1 /\ hyp2 /\ ... /\ hypn => (f ...) = (g ...)

then you could write it as

(2) hyp1 /\ hyp2 /\ ... /\ hypn => (g ...) = (f ...)

Logically there is no difference, but in ACL2s there is a big
difference. Put the more "complicated" of (g ...) and (f ...) on
the left of the equality because ACL2s uses the defthms as what
are called rewrite rules, i.e., if you defthm is of form (1) then
ACL2s replaces (f ...) by (g ...) but not the other way around.

Another minor issue: replace every occurrence of the function len with
acl2::len, so instead of (len x) write (acl2::len x).

Finally place the defthms in the same order as you were asked to
prove them and lemmas that were used in the proof of a theorem
should come before the theorem.

If you do it right, this should be easy. Also, you should try
this even if you didn't do all the proofs.

|#

(defthm T1
  (implies (and (rationalp e) (lorp l))
           (equal (+ 1 (acl2::len l))
                  (acl2::len (insert e l)))))


(defthm lemma1
  (implies (and (rationalp e) (lorp l) (orderedp l))
           (orderedp (insert e l))))

(defthm T3
  (implies (lorp l)
           (orderedp (isort l))))


"this is the second theorem.  It doesn't finish evaluating, but we believe it to be correct"
#|ACL2s-ToDo-Line|#
(defthm T2
  (implies (lorp l)
           (equal (acl2::len (isort l))
                  (acl2::len l))))