#|
 Copyright © 2018 by Pete Manolios 
 CS 4820 Fall 2018

 Homework 3.
 Due: 10/5 (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 3".

 The group members are:

 ... (put the names of the group members here)

 Provide a proof script that ACL2s accepts and that includes the
 following definitions and theorems.

 Some of the definitions may require measure functions and lemmas
 before they are accepted by ACL2s. See l3.lisp, the code for lecture
 3, for examples on how to provide ccms (for termination). You can get
 the documentation for ccg with the following command:

  :doc acl2::ccg 

 Some of the defthms will require lemmas and they may require
 hints. Use :doc ! For example, if you want to see how to tell the
 theorem prover what induction scheme to use, read:

  :doc acl2::hints 

 Use the method, as covered in class, as well as all of the techniques
 covered for controlling, understanding and programming the theorem
 prover to do your bidding. 

 This homework is designed to give you some experience using ACL2s to
 prove non-trivial things, so expect to spend time trying to understand
 why things don't work, how to query the theorem prover, how to come up
 with good rewrite strategies, etc. Please plan ahead and give
 yourselves plenty of time. Also, ask questions on Piazza.

 We start with the flatten example revisited.

 55 points.

|#

(in-package "ACL2S")

(set-gag-mode nil)

(defmacro tlp (x)
  `(true-listp ,x))

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

(defunc mc-flatten-acc (x a)
  :input-contract (tlp a)
  :output-contract (tlp (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 (tlp (mc-flatten x))
  (mc-flatten-acc x nil))

; You already did this for HWK2, using paper and pencil proofs.
(defthm flatten-mc-flatten
  (equal (mc-flatten x)
         (flatten x)))
  
(defunc gopher (x)
  :input-contract t
  :output-contract t
  (if (or (atom x)
          (atom (car x)))
      x
    (gopher (cons (caar x) (cons (cdar x) (cdr x))))))

(defthm flatten-gopher
  (equal (flatten (gopher x))
	 (flatten x)))

(defunc samefringe (x y)
  :input-contract t
  :output-contract (booleanp (samefringe x y))
  (if (or (atom x)
	  (atom y))
      (equal x y)
    (and (equal (car (gopher x))
		(car (gopher y)))
	 (samefringe (cdr (gopher x))
		     (cdr (gopher y))))))

(defthm correctness-of-samefringe
  (equal (samefringe x y)
         (equal (flatten x)
                (flatten y))))

#|

 Next, a classic example, where we prove that insertion sort and
 quicksort actually sort.

 We are using lexorder and <<, which give us a total order on the ACL2
 universe.

 See :doc acl2::<<

 Try running qsort and isort on lists containing whatever you want,
 e.g., numbers, symbols, strings, other lists, etc.

 The following definitions are automatically accepted.

|#


(defmacro <<= (x y)
  `(acl2::lexorder ,x ,y))

(defmacro << (x y)
  `(acl2::<< ,x ,y))

(defunc insert (a x)
  :input-contract (tlp x)
  :output-contract (tlp (insert a x))
  (cond ((endp x) (list a))
        ((<<= a (first x)) (cons a x))
        (t (cons (first x) (insert a (rest x))))))

(defunc isort (x)
  :input-contract (tlp x)
  :output-contract (tlp (isort x))
  (if (endp x)
      ()
    (insert (first x) (isort (rest x)))))

(defunc less (x lst)
  :input-contract (tlp lst)
  :output-contract (tlp (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 (tlp lst)
  :output-contract (tlp (notless x lst))
  (cond ((endp lst) nil)
        ((<<= x (first lst))
         (cons (first lst) (notless x (rest lst))))
        (t (notless x (rest lst)))))

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

(defunc orderedp (x)
  :input-contract (tlp x)
  :output-contract (booleanp (orderedp x))
  (or (endp x)
      (endp (rest x))
      (and (<<= (first x) (second x))
           (orderedp (rest x)))))

(defunc del (e x)
  :input-contract (tlp x)
  :output-contract (tlp (del e x))
  (cond ((endp x) nil)
        ((equal e (first x)) (rest x))
        (t (cons (first x) (del e (rest x))))))

(defunc perm (x y)
  :input-contract (and (tlp x) (tlp y))
  :output-contract (booleanp (perm x y))
  (if (endp x)
      (endp y)
    (and (member-equal (first x) y)
         (perm (rest x) (del (first x) y)))))

#|

 45 points.

 Uncomment and prove, using ACL2s, three of the following defthms
 (in any order you wish).

 30 points.

 Extra credit: prove all of the following defthms (in any order you
 wish, but you only get extra credit if you prove all the defthms).

 (defthm isort-orderedp
   (implies (tlp x)
            (orderedp (isort x))))

 (defthm qsort-orderedp
   (implies (tlp x)
            (orderedp (qsort x))))

 (defthm isort-perm
   (implies (tlp x)
            (perm (isort x) x)))

 (defthm qsort-perm
   (implies (tlp x)
            (perm (qsort x) x)))

 (defthm qsort-is-isort
   (implies (tlp x)
            (equal (qsort x) (isort x))))
|#