{-# OPTIONS --allow-unsolved-metas #-}
-- AGDA IN PADOVA 2023
-- Exercise sheet 5

infixr 5 _∷_

data List (A : Set) : Set where
  []  : List A
  _∷_ : A  List A  List A

data _⊎_ (A B : Set) : Set where
  left  : A  A  B
  right : B  A  B

module Implementation
  {A : Set}
  (_≤_ : A  A  Set)
  (cmp : (x y : A)  (x  y)  (y  x)) where

  -- Given an ordered list "ys", "insert x ys" is the same as "ys",
  -- but with "x" inserted at the correct place to ensure that the
  -- resulting list is again ordered.
  insert : (x : A)  List A  List A
  insert x []       = x  []
  insert x (y  ys) with cmp x y
  ... | left  x≤y = x  y  ys
  ... | right y≤x = y  insert x ys

  sort : List A  List A
  sort []       = []
  sort (x  xs) = insert x (sort xs)

-- TWO METHODS FOR VERIFYING CORRECTNESS:
-- (a) first implement, then separately verify correctness
-- (b) correct by construction

module Verification₁ {A : Set} (_≤_ : A  A  Set) (cmp : (x y : A)  (x  y)  (y  x)) where
  open Implementation _≤_ cmp

  data IsOrdered : List A  Set where
    empty     : IsOrdered []
    singleton : {x : A}  IsOrdered (x  [])
    cons      : {x y : A} {ys : List A}  x  y  IsOrdered (y  ys)  IsOrdered (x  y  ys)

  lemma₀ : (x y : A) (ys : List A)  y  x  IsOrdered (y  ys)  IsOrdered (y  insert x ys)
  lemma₀ x y []       y≤x p = cons y≤x singleton
  lemma₀ x y (z  ys) y≤x (cons y≤z q) with cmp x z
  ... | left  x≤z = cons y≤x (cons x≤z q)
  ... | right z≤x = cons y≤z (lemma₀ x z ys z≤x q)

  lemma : (x : A) (ys : List A)  IsOrdered ys  IsOrdered (insert x ys)
  lemma x []       p = singleton
  lemma x (y  ys) p with cmp x y
  ... | left  x≤y = cons x≤y p
  ... | right y≤x = lemma₀ x y ys y≤x p

  theorem : (xs : List A)  IsOrdered (sort xs)
  theorem []       = empty
  theorem (x  xs) = lemma x (sort xs) (theorem xs)

  cheatsort : List A  List A
  cheatsort xs = []

  cheattheorem : (xs : List A)  IsOrdered (cheatsort xs)
  cheattheorem xs = empty

module Verification₂ {A : Set} (_≤_ : A  A  Set) (cmp : (x y : A)  (x  y)  (y  x)) where
  open Implementation _≤_ cmp

  -- "(x ◂ ys ↝ xys)" should be the type of witnesses that inserting "x" into "ys" somewhere
  -- yields the list "xys".     -- ◂\t  ↝\leadsto
  data _◂_↝_ : A  List A  List A  Set where
    here  : {x : A} {xs : List A}  x  xs  (x  xs)
    there : {x y : A} {ys xys : List A}  x  ys  xys  x  (y  ys)  (y  xys)

  -- "IsPerm xs ys" should be the type of witnesses that the two lists "xs" and "ys"
  -- are permutations of each other, that is, contain exactly the same elements just
  -- perhaps in different order.
  data IsPerm : List A  List A  Set where
    empty : IsPerm [] []
    cons  : {x : A} {xs ys xys : List A}  (x  ys  xys)  IsPerm xs ys  IsPerm (x  xs) xys

  -- EXERCISE: Make sense of the preceding two definitions.

  -- EXERCISE: Fill in this hole.
  example : (x y z : A)  IsPerm (x  y  z  []) (z  x  y  [])
  example x y z = {!!}

  -- EXERCISE: Verify this lemma.
  lemma : (x : A) (ys : List A)  x  ys  insert x ys
  lemma x ys = {!!}

  -- EXERCISE: Deduce this theorem.
  theorem : (xs : List A)  IsPerm xs (sort xs)
  theorem xs = {!!}

module CorrectByConstruction₀
  {A : Set} (_≤_ : A  A  Set)
  (max : A) (≤max : {x : A}  x  max)
  (cmp : (x y : A)  (x  y)  (y  x)) where

  -- "OList l" is the type of ordered lists of elements of A.
  data OList : Set
  -- The usual "where" is missing because the definition of "OList"
  -- mutually depends on the following function extracting the head
  -- of an ordered list.

  head : OList  A
  -- This is just a declaration. The definition will follow once
  -- the constructors of "OList" have been introduced.

  data OList where
    nil  : OList
    cons : (x : A) (xs : OList)  x  head xs  OList

  head nil           = max
  head (cons x xs _) = x

  insert : A  OList  OList
  insert x ys = {!!}

  sort : List A  OList
  sort []       = nil
  sort (x  xs) = insert x (sort xs)

module CorrectByConstruction₁
  {A : Set} (_≤_ : A  A  Set)
  (min : A) (min≤ : {x : A}  min  x)
  (cmp : (x y : A)  (x  y)  (y  x)) where

  -- "OList l" is the type of ordered lists of elements of A which are bounded from below by l.
  data OList (l : A) : Set where
    nil  : OList l
    cons : (x : A)  l  x  OList x  OList l

  insert : {l : A}  (x : A)  l  x  OList l  OList l
  insert x l≤x nil             = cons x l≤x nil
  insert x l≤x (cons y l≤y ys) with cmp x y
  ... | left  x≤y = cons x l≤x (cons y x≤y ys)
  ... | right y≤x = cons y l≤y (insert x y≤x ys)

  sort : List A  OList min
  sort []       = nil
  sort (x  xs) = insert x min≤ (sort xs) 

module CorrectByConstruction₂
  {A : Set} (_≤_ : A  A  Set)
  (min : A) (min≤ : {x : A}  min  x)
  (cmp : (x y : A)  (x  y)  (y  x)) where

  -- As in module Verification₂ above
  data _◂_↝_ : A  List A  List A  Set where
    here  : {x : A} {xs : List A}  x  xs  (x  xs)
    there : {x y : A} {ys xys : List A}  x  ys  xys  x  (y  ys)  (y  xys)

  -- "OPList l xs" is the type of ordered lists whose elements are bounded from below by l
  -- and which are permutations of xs
  
  data OPList (l : A) : List A  Set where
    nil  : OPList l []
    cons : {ys xys : List A}  (x : A)  OPList x ys  l  x  (x  ys  xys)  OPList l xys

  -- EXERCISE: Fill this in.
  insert : {!!}
  insert = {!!}

  -- EXERCISE: Fill this in.
  sort : (xs : List A)  OPList min xs
  sort = {!!}

-- The modules CorrectByConstruction₁ and CorrectByConstruction₂ require a least element "min".
-- EXERCISE: Define for any type A together with a relation _≤_ on A a new
-- type "* A" which is A adjoined by a new least element -∞. Use
-- this construction to get rid of the additional requirement.
data *_ (A : Set) : Set where
  -- EXERCISE: fill this in

module Lift {A : Set} (_≤_ : A  A  Set) where
  -- EXERCISE: Define a relation _≼_ on * A.
  -- EXERCISE: Verify that there is a least element for this relation.
  -- EXERCISE: Verify that if we have a function cmp for A then we also have such a function for * A.
  -- EXERCISE: Define a correct-by-construction sort function for A, by using * A.