#|

 Copyright © 2018 by Pete Manolios 
 CS 4820 Fall 2018

 Homework 2.
 Due: 9/21 (Midnight)

 For this assignment, work in groups of 2-3. Send me exactly one
 solution per team and make sure to follow the submission instructions
 on the course Web page. In particular, make sure that the subject of
 your email submission is "CS 4820 HWK 2".

 The group members are:
 ... (put the names of the group members here)


 1. For this problem, I want you to provide a measure for a function we
    saw in class.

 1a. Define a measure function for e3 (defined below) by filing in the
     ...'s in the definition of m.

 1b. Prove that it works with a paper and pencil proof. You don't have
     to submit this proof.

 1c. Make sure your definition works by using ACL2s to check your
     measure with the code below. (30 pts)

 Notice that if you use the default ACL2s termination method
 (:ccg), then ACL2s proves termination automatically.

|#

(set-termination-method :measure)
(set-gag-mode nil)

(defunc m (x y)
  :input-contract (and (natp x) (posp y))
  :output-contract (natp (m x y))
  ...)

(defunc e3 (x y)
  :input-contract (and (natp x) (posp y))
  :output-contract (natp (e3 x y))
  (declare (xargs :measure (if (not (and (natp x) (posp y))) 0 (m x y))))
  (cond ((equal x 0) x)
        ((equal y 1) y)
        ((> x y) (e3 y x))
        (t (e3 x (- y 1)))))

#|

 2. Below is a version of quicksort. 

|#

(set-termination-method :ccg)
(defdata lor (listof rational))

(defunc less (x lst)
  :input-contract (and (rationalp x) (lorp lst))
  :output-contract (lorp (less x lst))
  (cond ((endp lst) ())
        ((< (first lst) x)
         (cons (first lst) (less x (rest lst))))
        (t (less x (rest lst)))))

(defunc notless (x lst)
  :input-contract (and (rationalp x) (lorp lst))
  :output-contract (lorp (notless x lst))
  (cond ((endp lst) nil)
        ((>= (first lst) x)
         (cons (first lst) (notless x (rest lst))))
        (t (notless x (rest lst)))))

(defunc qsort (x)
  :input-contract (lorp x)
  :output-contract (lorp (qsort x))
  (if (endp x) 
      ()
    (append (qsort (less (first x) (rest x)))
            (append (list (first x))
                    (qsort (notless (first x) (rest x)))))))


#|

 ACL2s accepts the above definitions. Your job is to provide a paper
 and pencil proof that qsort is terminating. Do that by providing a
 measure function and a proof that it decreases, as per the RAP lecture
 notes.

 You can assume that less and notless are terminating functions.
 Prove any lemmas you need, using a paper and pencil proof. (40 pts)

 Recall that a measure function, m, for f, has to satisfy the following
 conditions.

 Condition 1. m has the same arguments and the same input contract as f.
 Condition 2. m's output contract is (natp (m ...))
 Condition 3. m is admissible.
 Condition 4. On every recursive call of f, given the input contract and 
    the conditions that lead to that call, m applied to the arguments in
    the call is less than m applied to the original inputs.

 You should do this proof as shown in the lecture notes.

 - Write down formalization of Condition 4.

 - Use equational reasoning to conclude the formula is valid.
   If you need lemmas, identify and prove them.

 Unless clearly stated otherwise, you need to follow these steps for EACH
 recursive call separately.

 Here is an example.

 (defunc f (x y)
   :input-contract (and (true-listp x) (natp y))
   :output-contract (natp (f x y))
   (if (endp x)
     (if (equal y 0) 
       0
       (+ 1 (f x (- y 1))))
     (+ 1 (f (rest x) y))))

 A measure is
 (defunc m (x y)
   :input-contract (and (true-listp x) (natp y))
   :output-contract (natp (m x y))
   (+ (len x) y))

 For the first recursive call in f, the formalization 
 for proving Condition 4 is:

 (implies (and (true-listp x)
               (natp y)
               (endp x)
               (not (equal y 0)))
          (< (m x (- y 1))
             (m x y)))

 This can be rewritten as:

 (implies (and (true-listp x)
               (natp y)
               (endp x)
               (> y 0))
          (< (m x (- y 1))
             (m x y)))

 Proof of Condition 4 for the first recursive call:

 Context
 C1. (true-listp x)
 C2. (natp y)
 C3. (endp x)
 C4. y != 0

 (m x (- y 1))
 = { Def m, C3, Def len, Arithmetic }
 (- y 1)
 < { Arithmetic }
 y
 = { Def m, C3, Def. len, Arithmetic }
 (m x y)

 The formalization for Proof of Condition 4 for the 
 second recursive call:

 (implies (and (true-listp x)
               (natp y)
               (not (endp x)))
          (< (m (rest x) y)
             (m x y)))

 Proof:
 C1. (true-listp x)
 C2. (natp y)
 C3. (not (endp x))

 (m (rest x) y)
 = { Def m, C3 }
 (+ (len (rest x)) y)
 < { Arithmetic, Decreasing len axiom }
 (+ (len x) y)
 = { Def m }
 (m x y)

 Hence f terminates, and m is a measure function for it.


 ...


|#



#|

 3. Provide a paper and pencil proof of the defthm below. 
    (30 pts)

    The functions flatten and mc-flatten take anything as input and
    return a list containing all of the atoms appearing in the
    input. If the input is an atom, a singleton list containing the
    atom is returned. If the input is a cons, then the atoms in the car
    are appended with the atoms in the cdr. For example, applying
    flatten to the list

    (1 (2 (3 . 4)) 5)

    returns 

    (1 2 3 4 NIL 5 NIL)

    because, the input is equal to the following tree

    (1 . ((2 . ((3 . 4) . nil)) . (5 . nil)))

    and so if we create a list of the atoms of this tree, we get

    (1 2 3 4 nil 5 nil)

|#

(defunc flatten (x)
  :input-contract t
  :output-contract (true-listp (flatten x))
  (cond ((atom x) (list x))
        (t (append (flatten (car x)) (flatten (cdr x))))))

(defunc mc-flatten-acc (x a)
  :input-contract (true-listp a)
  :output-contract (true-listp (mc-flatten-acc x a))
  (cond ((atom x) (cons x a))
        (t (mc-flatten-acc (car x)
                       (mc-flatten-acc (cdr x) a)))))

(defunc mc-flatten (x)
  :input-contract t
  :output-contract (true-listp (mc-flatten x))
  (mc-flatten-acc x nil))

(defthm flatten-mc-flatten
  (equal (mc-flatten x)
         (flatten x)))

#|

...

|#


#|

 Extra Credit (30 pts)

 4. For this problem, I want you to prove termination of an interesting
    function that flattens if statements. 

    Consider the following ACL2s defdata form, along with the examples.

|#


(defdata if-expr (oneof symbol (list 'if if-expr if-expr if-expr)))

(check= (if-exprp 'a) t)
(check= (if-exprp '(if a b c)) t)
(check= (if-exprp '(if a 1 2)) nil)
(check= (if-exprp '(iff a b c)) nil)
(check= (if-exprp '(if a b)) nil)
(check= (if-exprp '(if a b c d)) nil)
(check= (if-exprp '(if (if a b c) a b)) t)

(defthm if-expr-args-b
  (implies (if-exprp (list* a b c))
           (if-exprp b))
  :rule-classes :forward-chaining)

(defthm if-expr-args-c
  (implies (if-exprp (list* a b c d))
           (if-exprp c))
  :rule-classes :forward-chaining)

(defthm if-expr-args-d
  (implies (if-exprp (list* a b c d e))
           (if-exprp d))
  :rule-classes :forward-chaining)


#|

Since ACL2s cannot prove termination without help, let's use program
mode.

|#

:program

(defunc if-flat (x)
  :input-contract (if-exprp x)
  :output-contract (if-exprp (if-flat x))
  (if (symbolp x)
      x
    (let ((test (second x))
          (true-branch (third x))
          (false-branch (fourth x)))
      (if (symbolp test)
          (list 'if test (if-flat true-branch) (if-flat false-branch))
        (if-flat (list 'if (second test)
                       (list 'if (third test) true-branch false-branch)
                       (list 'if (fourth test) true-branch false-branch)))))))

(check= (if-flat '(if a b c)) '(if a b c))
(check= (if-flat 'x) 'x)
(check= (if-flat '(if (if a b c) d e)) '(if a (if b d e) (if c d e)))

#|

 The function if-flat is a terminating function. Show this by defining
 an appropriate measure function. Fill in the ...'s below and prove
 termination with a paper and pencil proof.  If you want to double
 check your work, you can use ACL2s to check whether your measure
 function works.

|#

:ubt! :x-1

(defunc if-flat-measure (x)
  :input-contract (if-exprp x)
  :output-contract (natp (if-flat-measure x))
  ...)

(set-termination-method :measure)

(defunc if-flat (x)
  :input-contract (if-exprp x)
  :output-contract (if-exprp (if-flat x))
  (declare (xargs :measure (if (not (if-exprp x)) 0 (if-flat-measure x))))
  (if (symbolp x)
      x
    (let ((test (second x))
          (true-branch (third x))
          (false-branch (fourth x)))
      (if (symbolp test)
          (list 'if test (if-flat true-branch) (if-flat false-branch))
        (if-flat (list 'if
                       (second test)
                       (list 'if (third test) true-branch false-branch)
                       (list 'if (fourth test) true-branch false-branch)))))))

#|

 ...

|#