{-# OPTIONS --allow-unsolved-metas #-}
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
-- A ⊎ A is NOT the same as A again.
-- For instance, if A contains n elements, then A ⊎ A contains 2n elements.

{-
  The idea of insertion sort:

  To sort 5 ∷ 2 ∷ 10 ∷ 1 ∷ [],

  start with []. Then successively insert additional elements at the correct position.

  []
  5 ∷ []
  2 ∷ 5 ∷ []
  2 ∷ 5 ∷ 10 ∷ []
  1 ∷ 2 ∷ 5 ∷ 10 ∷ []
-}

module Implementation
  {A : Set}
  (_≤_ : A  A  Set)
  (cmp? : (x y : A)  (x  y)  (y  x)) where
  -- For elements x, y : A, we are given a type "x ≤ y" of witnesses
  -- that x is less than or equal to y.
  
  -- "insert x ys" should return the same list as "ys", but with the element "x"
  -- inserted at the correct location.
  insert : 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) 

  cheatsort : List A  List A
  cheatsort xs = []

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₀ = {!!}

  lemma : (x : A) (ys : List A)  IsOrdered ys  IsOrdered (insert x ys)
  lemma x []             empty       = singleton
  lemma x (y  [])       singleton   with cmp? x y
  ... | left  x≤y = cons x≤y singleton
  ... | right y≤x = cons y≤x singleton
  lemma x (y  (z  ys)) (cons y≤z p) = {!!}

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

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

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

  -- "OList l" is the type of ordered lists where all elements are ≥ l.
  -- In other words, "OList l" is the type of ordered lists bounded from below by l.
  data OList (l : A) : Set where
    nil  : OList l
    cons : (x : A)  l  x  OList x  OList l

  forget : {l : A}  OList l  List A
  forget nil           = []
  forget (cons x _ xs) = x  forget xs

  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 -∞
  sort []       = nil
  sort (x  xs) = insert x min (sort xs)

  {-
  _ : {l : A} (xs : OList l) → sort (forget xs) ≡ xs
  _ = ?
  -}