#|

In this lab you will gain some more experience in doing proofs by
induction like a professional.

Sorting is used everywhere!

In class, we defined insertion sort and proved that it returns an
ordered list. 

We will continue with the exploration of reasoning about sorting
algorithms in this lab.

Here are the definitions and the theorems we proved.

|#

(defdata lor (listof rational))

(definec insert (e :rational L :lor) :lor
  (cond ((endp L) (list e))
        ((<= e (car L)) (cons e L))
        (t (cons (car L) (insert e (cdr L))))))

(definec isort (L :lor) :lor
  (if (endp L)
      L
    (insert (car L) (isort (cdr L)))))

(definec orderedp (L :lor) :bool
  (or (endp (cdr L))
      (and (<= (car L) (second L))
           (orderedp (cdr L)))))

#|
State and prove the following theorems:

L1. (rationalp e) ^ (lorp L) ^ (orderedp L) => (orderedp (insert e L))
L2. (lorp L) => (orderedp (isort L))

Some of this may have been done in class already. 
Make sure you are able to do it alone also!

|#

(defthm insert-ordered
  (implies (and (rationalp e) (lorp L) (orderedp L))
           (orderedp (insert e L))))

(defthm isort-ordered
  (implies (lorp L)
           (orderedp (isort L))))

#|

We will next define the notion of a permutation
|#

"
This function is predefined:
(definec in (a :rational L :lor) :bool
  (and (consp L)
       (or (equal a (car l))
           (in a (cdr L)))))
"

(definec del (a :rational L :lor) :lor
  (cond ((endp L) L)
        ((equal a (car L)) (cdr L))
        (t (cons (car L) (del a (cdr L))))))

(definec permp (x :lor y :lor) :bool
  (if (endp x)
      (endp y)
    (and (in (car x) y)
         (permp (cdr x) (del (car x) y)))))


#|
We now want to prove

L3. (lorp L) => (permp (isort L) L)

Use the professional method to prove L3, which will require lemmas.
You can use any previously proven theorems and can assume that all of
the functions in this file are admissible so that you can use their
definitional axioms and contract theorems.

|#


#|

Extra problem:

If I used the following definitions, then L3 still holds. Prove it.

|#

" Alternative definition of in:

(definec in (a :all L :tl) :bool
  (and (consp L)
       (or (equal a (car l))
           (in a (cdr L)))))
"

(rrev (rrev x)) = x
(definec del (a :all L :tl) :tl
  (cond ((endp L) L)
        ((equal a (car L)) (cdr L))
        (t (cons (car L) (del a (cdr L))))))

(definec permp (x :tl y :tl) :bool
  (if (endp x)
      (endp y)
    (and (in (car x) y)
         (permp (cdr x) (del (car x) y)))))