{-# OPTIONS --allow-unsolved-metas #-}
{-
  Task: Implement insertion sort.

  For instance,

      sort (5 ∷ 3 ∷ 10 ∷ 1 ∷ [])

  will yield the list

      1 ∷ 3 ∷ 5 ∷ 10 ∷ [].
-}

data _⊎_ (X Y : Set) : Set where
  left  : X → X ⊎ Y
  right : Y → X ⊎ Y

-- "Let a set A be fixed."
module Implementation
  (A : Set)
  (_≤_ : A → A → Set)   -- "x ≤ y" is the type of
                        -- witnesses that x is less than
                        -- or equal to y
  (cmp? : (x y : A) → (x ≤ y) ⊎ (y ≤ x)) where
  -- For instance, in the case that "A" is the type ℕ
  -- and "_≤_" is the usual ordering relation,
  -- "cmp? 5 10" should be something of the form "left ...",
  -- "cmp? 10 5" should be something of the form "right ...".

  data List : Set where
    []  : List
    _∷_ : A → List → List

  -- If the list "ys" is already sorted (ascendingly),
  -- the list "insert x ys" should be the same as "ys",
  -- but with the element "x" inserted at the appropriate
  -- location.
  -- For instance: "insert 5 (2 ∷ 10 ∷ 20 ∷ [])" should
  -- yield "2 ∷ 5 ∷ 10 ∷ 20 ∷ []".
  insert : A → List → List
  insert x []       = x ∷ []
  insert x (y ∷ ys) with cmp? x y
  ... | left  x≤y = x ∷ (y ∷ ys)
  ... | right y≤x = y ∷ insert x ys
  -- There are two options: The correct result might by
  -- (a)    x ∷ y ∷ ys       (this is correct if x ≤ y)
  -- (b)    y ∷ insert x ys  (this is correct if y ≤ x)

  sort : List → List
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

module Verification
  (A : Set)
  (_≤_ : A → A → Set)   -- "x ≤ y" is the type of
                        -- witnesses that x is less than
                        -- or equal to y
  (cmp? : (x y : A) → (x ≤ y) ⊎ (y ≤ x)) where

  open Implementation A _≤_ cmp?

  -- The type "IsSorted xs" should consist of witnesses that
  -- the list "xs" is sorted.
  data IsSorted : List → Set where
    empty     : IsSorted []
    singleton : {x : A} → IsSorted (x ∷ [])
    cons      : {x y : A} {ys : List} → IsSorted (y ∷ ys) → x ≤ y → IsSorted (x ∷ (y ∷ ys))

  lemma₀ : (x y : A) (ys : List) → y ≤ x → IsSorted (y ∷ ys) → IsSorted (y ∷ insert x ys)
  lemma₀ = {!!}

  lemma : (x : A) (ys : List) → IsSorted ys → IsSorted (insert x ys)
  lemma x []       p = singleton
  lemma x (y ∷ ys) p with cmp? x y
  ... | left  x≤y = cons {x} {y} {ys} p x≤y
  ... | right y≤x = lemma₀ x y ys y≤x p

  -- Logical reading: For every list "xs", it is a fact that "sort xs" is sorted.
  -- Computational reading: "theorem" is a function which reads a list "xs"
  -- as input and outputs a witness that "sort xs" is sorted.
  theorem : (xs : List) → IsSorted (sort xs)
  theorem []       = empty
  theorem (x ∷ xs) = lemma x (sort xs) (theorem xs)

  cheatsort : List → List
  cheatsort xs = []

  cheattheorem : (xs : List) → IsSorted (cheatsort xs)
  cheattheorem xs = empty

module CorrectByConstruction
  (A : Set)
  (_≤_ : A → A → Set)   -- "x ≤ y" is the type of
                        -- witnesses that x is less than
                        -- or equal to y
  (-∞ : A)
  (is-min : {x : A} → -∞ ≤ x)
  (cmp? : (x y : A) → (x ≤ y) ⊎ (y ≤ x)) where

  data List : Set where
    []  : List
    _∷_ : A → List → List

  -- "SList l" is the type of sorted lists whose elements are bounded
  -- from below by l. For instance, the numbers 10, 20 and 30 are
  -- bounded from below by 5.
  data SList (l : A) : Set where
    nil  : SList l
    cons : (x : A) → (xs : SList x) → l ≤ x → SList l

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

  sort : List → SList -∞
  sort []       = nil
  sort (x ∷ xs) = insert x (sort xs) is-min