module SortedList where

open import Data.Sum
open import Data.Product
open import Data.List
import Data.Unit
open Data.Unit hiding (total; _≤_)

module External 
  (A     : Set)
  (_≤_   : A → A → Set)
  (total : ∀ a b → a ≤ b ⊎ b ≤ a)
  where
  
  insert : A → List A → List A
  insert a [] = [ a ]
  insert a (x ∷ xs) with total a x
  ... | inj₁ _ = a ∷ x ∷ xs
  ... | inj₂ _ = x ∷ insert a xs

  Sorted : List A → Set
  Sorted []           = ⊤
  Sorted (_ ∷ [])     = ⊤
  Sorted (x ∷ y ∷ xs) = (x ≤ y) × Sorted (y ∷ xs)

  sorted : (a : A) → (xs : List A) → Sorted xs → Sorted (insert a xs)
  sorted a [] _ = tt
  sorted a (x ∷ []) _ with total a x
  ... | inj₁ a≤x = (a≤x , tt)
  ... | inj₂ x≤a = (x≤a , tt)
  sorted a (x ∷ y ∷ xs) (x≤y , sorted-y∷xs) with total a x
  ... | inj₁ a≤x = ( a≤x , ( x≤y , sorted-y∷xs ) )
  ... | inj₂ x≤a = lemma x a y xs x≤a x≤y sorted-y∷xs
    where
      lemma : (a b x : A) → (xs : List A) → a ≤ b → a ≤ x 
              → Sorted (x ∷ xs) → Sorted (a ∷ insert b (x ∷ xs))
      lemma a b x [] a≤b a≤x _ with total b x
      -- (a ≤ b) × Sorted (b ∷ x ∷ [])
      ... | inj₁ b≤x = ( a≤b , b≤x , tt )
      -- (a ≤ x) × Sorted (x ∷ insert b [])
      ... | inj₂ x≤b = ( a≤x , x≤b , tt )
      lemma a b x (y ∷ xs) a≤b a≤x ( x≤y , sorted-y∷xs ) with total b x
      -- (a ≤ b) × Sorted (b ∷ x ∷ xs)
      ... | inj₁ b≤x = ( a≤b , b≤x , (x≤y , sorted-y∷xs ) )
      -- (a ≤ x) × Sorted (x ∷ insert b (y ∷ xs))
      ... | inj₂ x≤b = ( a≤x , lemma x b y xs x≤b x≤y sorted-y∷xs )

  -- Insertion sort
  isort : List A → List A
  isort = foldr insert []
  
  -- Proof that our sort works.
  isort-sorted : (xs : List A) → Sorted (isort xs)
  isort-sorted []       = tt
  isort-sorted (x ∷ xs) = sorted x (isort xs) (isort-sorted xs)

module Internal 
  (A     : Set)
  (_≤_   : A → A → Set)
  (total : ∀ a b → a ≤ b ⊎ b ≤ a)
  (trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c)
  where
   
  mutual
    data SList : Set where
      nil  : SList
      cons : (a : A) → (xs : SList) → a ≤L xs → SList
      
    _≤L_ : A → SList → Set
    a ≤L nil           = ⊤
    a ≤L (cons x xs _) = (a ≤ x) × (a ≤L xs)

  mutual
    sinsert : (a : A) → SList → SList
    sinsert a nil = cons a nil tt
    sinsert a (cons x xs x≤Lxs) with total a x
    ... | inj₁ a≤x = cons a (cons x xs x≤Lxs) (a≤x , lemma₁ a x xs a≤x x≤Lxs)
      where
        lemma₁ : (a x : A) → (xs : SList) → a ≤ x → x ≤L xs → a ≤L xs
        lemma₁ _ _ nil _ _ = tt 
        lemma₁ a x (cons y xs y≤Lxs) a≤x (x≤y , x≤Lxs) =
          (trans a≤x x≤y , lemma₁ a x xs a≤x x≤Lxs)
    ... | inj₂ x≤a = cons x (sinsert a xs) (lemma₂ a x xs x≤a x≤Lxs)

    lemma₂ : (a x : A) → (xs : SList) → x ≤ a → x ≤L xs → x ≤L sinsert a xs
    lemma₂ _ _ nil x≤a _ = (x≤a , tt)
    lemma₂ a x (cons y xs y≤Lxs) x≤a (x≤y , x≤Lxs) with total a y
    -- (x ≤ a) × (x ≤ y) & (x ≤L xs)
    ... | inj₁ a≤y = (x≤a , (x≤y , x≤Lxs))
    -- (x ≤ y) × (x ≤L sinsert a xs)
    ... | inj₂ y≤a = (x≤y , lemma₂ a x xs x≤a x≤Lxs)
    
  -- No further proofs are needed!
  isort′ : List A → SList
  isort′ = foldr sinsert nil

private
  open import Relation.Binary
  open import Data.Nat
  open DecTotalOrder Data.Nat.decTotalOrder
  open External carrier Data.Nat._≤_ total
  open Internal carrier Data.Nat._≤_ total trans

  ex0 = isort  ( ∷  ∷  ∷  ∷ [])
  ex1 = isort′ ( ∷  ∷  ∷  ∷ [])