Submission for SPLG exam 2013.

Exam.agda

-- SPLG Exam 2013: Christian Harrington <cnha@itu.dk>
-- 20. December 2013

module Exam where
  open import Prelude
  -- http://www.itu.dk/courses/SPLG/E2013/Prelude.agda
  open import Lecture3Delivery 
  -- http://www.itu.dk/courses/SPLG/E2013/Lecture3Delivery.agda

  open Nats
  open Lists
  open Sum
  open LessThan
  open BagEquality
  open Isomorphisms
  open IsomorphismSyntax

  -- Copied from mini project 3
  min : (n m : Nat) -> Either (n <= m) (m <= n)
  min zero zero = left zero<=
  min zero (suc m) = left zero<=
  min (suc n) zero = right zero<=
  min (suc n) (suc m) with min n m
  min (suc n) (suc m) | left x = left (suc<= x)
  min (suc n) (suc m) | right x = right (suc<= x)

  -- Assignment 1

  -- Inserts a nat into a list, so that it is to the right of 
  -- all lower nats. 
  insertElement : Nat → List Nat → List Nat
  insertElement x [] = x :: []
  insertElement x (y :: xs) with min x y
  insertElement x (y :: xs) | left  x<=y = x :: y :: xs
  insertElement x (y :: xs) | right y<=x = y :: (insertElement x xs)

  -- Sorts a list, then inserts a nat in the correct place
  insertionSort : List Nat → List Nat
  insertionSort [] = []
  insertionSort (x :: xs) = insertElement x (insertionSort xs)

  -- Extrinsic proof

  -- Simple lemma showing that a ∨ (b ∨ c) <-> b ∨ (a ∨ c)
  -- Uses commutativity, associativity and congruence rules for Either.
  a∨b∨c<->b∨a∨c : ∀ a b c → Either a (Either b c) <-> Either b (Either a c)
  a∨b∨c<->b∨a∨c a b c = 
    Either a (Either b c) <->[ Either-comm ] 
    Either (Either b c) a <->[ Either-assoc ]
    Either b (Either c a) <->[ Either-cong iso-refl Either-comm ] 
    Either b (Either a c) QED

  -- Lemma showing that if (_==_ z) holds for a list xs with an x in front,
  -- it also holds for that list with the x inserted via insertElement.
  -- Done via induction on xs. 
  insert<->cons : ∀ z x xs → Any (_==_ z) (insertElement x xs) <-> Any (_==_ z) (x :: xs)
  insert<->cons z x [] = iso-refl
  insert<->cons z x (y :: xs) with min x y
  insert<->cons z x (y :: xs) | left  x<=y = iso-refl
  insert<->cons z x (y :: xs) | right y<=x = 
    Either (z == y) (Any (_==_ z) (insertElement x xs)) 
      <->[ Either-cong iso-refl (insert<->cons z x xs) ] 
    Either (z == y) (Either (z == x) (Any (_==_ z) xs))
      <->[ a∨b∨c<->b∨a∨c (z == y) (z == x) (Any (_==_ z) xs) ]
    iso-refl

  -- Lemma showing that if to lists xs and ys are bag equal, then x :: xs 
  -- and ys with x inserted via insertElement are also bag equal.
  cons=baginsert : ∀ x xs ys → xs =bag ys → (x :: xs) =bag insertElement x ys
  cons=baginsert x xs ys xs=bagys = λ z → iso-sym (iso-trans (insert<->cons z x ys) 
                                                  (Either-cong iso-refl (iso-sym (xs=bagys z))))

  -- The main proof. Shows that the list xs is bag equal to the sorted list
  -- xs. Done by induction on xs.
  insertionSortBag : (xs : List Nat) → xs =bag (insertionSort xs)
  insertionSortBag [] = =bag-refl
  insertionSortBag (x :: xs) = cons=baginsert x xs (insertionSort xs) (insertionSortBag xs)

  -- Assignment 2

  open Sigma

  -- Uses the insertion sort from above along with the proof that insertion
  -- sort preserves elements, and returns the sorted list along with
  -- a proof that the sorted list is bag equal to the original.
  is : (xs : List Nat) → List Nat ** λ sXs → xs =bag sXs
  is xs with insertionSortBag xs
  ... | p = (insertionSort xs) , (λ z → p z)