#|

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

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

Sorting is used everywhere!

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

#|
In class, we proved:

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

Review your notes and the professional method before continuing.

|#

#|

In this lab, we will define the notion of a permutation
and prove

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

|#

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

#|

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.

|#

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

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