twanvl/Sorting.agda

## Sorting.agda
module Sorting where
-- See https://www.twanvl.nl/blog/agda/sorting

open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List hiding (merge)
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
open import Data.Nat.Logarithm
open import Data.Nat.Induction
open import Data.Nat.Tactic.RingSolver
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming ([_] to reveal)
open import Function

-----------------------------------------------------------------------------------------
-- Counting monad
-----------------------------------------------------------------------------------------

-- A monad that keeps a natural number counter
module CountingMonad where
  private
    module Dummy where
      infix 1 _in-time_
      data _in-time_ {a} (A : Set a) (n : ℕ) : Set a where
        box : A → A in-time n

    open Dummy

    unbox : ∀ {a} {A : Set a} {n} → A in-time n → A
    unbox (box x) = x

  open Dummy public using (_in-time_)

  infixl 1 _>>=_
  _>>=_ : ∀ {a b} {A : Set a} {B : Set b} → {n m : ℕ} → A in-time n → (A → B in-time m) → B in-time (n + m)
  box x >>= f = box (unbox (f x))

  _=<<_ : ∀ {a b} {A : Set a} {B : Set b} → {n m : ℕ} → (A → B in-time m) → A in-time n → B in-time (n + m)
  _=<<_ = flip _>>=_

  infixr 2 _<$>_
  _<$>_ : ∀ {a b} {A : Set a} {B : Set b} → {n : ℕ} → (A → B) → A in-time n → B in-time n
  f <$> box x = box (f x)

  _<$$>_ : ∀ {a b} {A : Set a} {B : Set b} → {n : ℕ} → A in-time n → (A → B) → B in-time n
  _<$$>_ = flip _<$>_

  return : ∀ {a} {A : Set a} → {n : ℕ} → A → A in-time n
  return = box

  bound-≡ : ∀ {a} {A : Set a} {m n} → (m ≡ n) → A in-time m → A in-time n
  bound-≡ = subst (_in-time_ _)

  bound-+ : ∀ {a} {A : Set a} {m n k} → (m + k ≡ n) → A in-time m → A in-time n
  bound-+ eq x = bound-≡ eq (x >>= return)

  bound-≤ : ∀ {a} {A : Set a} {m n} → (m ≤ n) → A in-time m → A in-time n
  bound-≤ m≤n = bound-+ (m+[n∸m]≡n m≤n)

  bound-≤′ : ∀ {a} {A : Set a} {m n} → (m ≤′ n) → A in-time m → A in-time n
  bound-≤′ ≤′-refl     x = x
  bound-≤′ (≤′-step l) x = return {n = 1} x >>= bound-≤′ l

open CountingMonad


-----------------------------------------------------------------------------------------
-- Permutations
-----------------------------------------------------------------------------------------

1+m+n=m+1+n : (m n : ℕ) → suc (m + n) ≡ m + suc n
1+m+n=m+1+n = solve-∀

module Permutations {a} (A : Set a) where

  -- x ◂ xs ≡ ys means that ys is equal to xs with x inserted somewhere
  data _◂_≡_ (x : A) : List A → List A → Set a where
    here  : ∀ {xs}           → x ◂ xs ≡ (x ∷ xs)
    there : ∀ {y} {xs} {xys} → (p : x ◂ xs ≡ xys) → x ◂ (y ∷ xs) ≡ (y ∷ xys)

  -- Proof that a list is a permutation of another one
  data IsPermutation : List A → List A → Set a where
    []  : IsPermutation [] []
    _∷_ : ∀ {x xs ys xys}
        → (p : x ◂ ys ≡ xys)
        → (ps : IsPermutation xs ys)
        → IsPermutation (x ∷ xs) xys

  -- Identity permutation
  id-permutation : (xs : List A) → IsPermutation xs xs
  id-permutation [] = []
  id-permutation (x ∷ xs) = here ∷ id-permutation xs

  -- cons on the other side
  insert-permutation : ∀ {x xs ys xys}
                     → x ◂ ys ≡ xys → IsPermutation ys xs → IsPermutation xys (x ∷ xs)
  insert-permutation here p = here ∷ p
  insert-permutation (there y) (p ∷ ps) = there p ∷ insert-permutation y ps

  -- inverse permutations
  inverse-permutation : ∀ {xs ys} -> IsPermutation xs ys → IsPermutation ys xs
  inverse-permutation [] = []
  inverse-permutation (p ∷ ps) = insert-permutation p (inverse-permutation ps)

  swap-inserts : ∀ {x y xs xxs yxxs}
               → (x ◂ xs ≡ xxs) → (y ◂ xxs ≡ yxxs) → ∃ \yxs → (y ◂ xs ≡ yxs) × (x ◂ yxs ≡ yxxs)
  swap-inserts p here = _ , here , there p
  swap-inserts here (there q) = _ , q , here
  swap-inserts (there p) (there q) with swap-inserts p q
  ... | _ , p' , q' = _ , there p' , there q'

  extract-permutation : ∀ {x ys zs zs'}
                      → x ◂ ys ≡ zs → IsPermutation zs zs'
                      → ∃ \ys' → (x ◂ ys' ≡ zs') × IsPermutation ys ys'
  extract-permutation here (q ∷ qs) = _ , q , qs
  extract-permutation (there p) (q ∷ qs) with extract-permutation p qs
  ... | ys' , r , rs with swap-inserts r q
  ...   | ys'' , s , t = ys'' , t , s ∷ rs

  -- composing permutations
  compose-permutation : ∀ {xs ys zs : List A}
                      → IsPermutation xs ys → IsPermutation ys zs → IsPermutation xs zs
  compose-permutation [] [] = []
  compose-permutation (p ∷ ps) qqs with extract-permutation p qqs
  ... | _ , q , qs = q ∷ compose-permutation ps qs

  insert-++₁ : ∀ {x xs ys xxs} → x ◂ xs ≡ xxs → x ◂ (xs ++ ys) ≡ (xxs ++ ys)
  insert-++₁ here = here
  insert-++₁ (there p) = there (insert-++₁ p)

  insert-++₂ : ∀ {y xs ys yys} → y ◂ ys ≡ yys → y ◂ (xs ++ ys) ≡ (xs ++ yys)
  insert-++₂ {xs = []} p = p
  insert-++₂ {xs = _ ∷ xs} p = there (insert-++₂ {xs = xs} p)

  -- Length of permutations
  length-insert : ∀ {x xs xxs} → x ◂ xs ≡ xxs → length xxs ≡ suc (length xs)
  length-insert here = refl
  length-insert (there p) = cong suc (length-insert p)

  length-permutation : ∀ {xs ys} → IsPermutation xs ys → length xs ≡ length ys
  length-permutation [] = refl
  length-permutation (p ∷ ps) = cong suc (length-permutation ps) ⟨ trans ⟩ sym (length-insert p)

  same-perm' : ∀ {x xs xxs ys} → x ◂ xs ≡ xxs → x ◂ ys ≡ xxs → IsPermutation xs ys
  same-perm' here here = id-permutation _
  same-perm' here (there q) = insert-permutation q (id-permutation _)
  same-perm' (there p) here = p ∷ id-permutation _
  same-perm' (there p) (there q) = here ∷ same-perm' p q

  same-perm : ∀ {x xs xxs y ys yys}
            → x ≡ y → IsPermutation xxs yys → x ◂ xs ≡ xxs → y ◂ ys ≡ yys → IsPermutation xs ys
  same-perm refl ps q r with extract-permutation q ps
  ... | l' , q' , ps' = compose-permutation ps' (same-perm' q' r)

-----------------------------------------------------------------------------------------
-- Sorted lists
-----------------------------------------------------------------------------------------

module SortedList
     {a r}
     {A   : Set a}
     {_≤_ : Rel A r}
     (isPartialOrder : IsPartialOrder _≡_ _≤_) where

  open IsPartialOrder isPartialOrder renaming (trans to ≤-trans; refl to ≤-refl)

  -- Less than all values in a list
  data _≤*_ (x : A) : List A → Set (lmax a r) where
    []  : x ≤* []
    _∷_ : ∀ {y ys} → (x ≤ y) → x ≤* ys → x ≤* (y ∷ ys)

  -- Proof that a list is sorted
  data IsSorted : List A → Set (lmax a r) where
    []  : IsSorted []
    _∷_ : ∀ {x xs} → x ≤* xs → IsSorted xs → IsSorted (x ∷ xs)

  ≤*-trans : ∀ {x u us} → x ≤ u → u ≤* us → x ≤* us
  ≤*-trans p []       = []
  ≤*-trans p (y ∷ ys) = ≤-trans p y ∷ ≤*-trans p ys


  -- relation to permutations
  open Permutations A
  less-insert : ∀ {x y xs ys} → y ◂ ys ≡ xs → x ≤* xs → x ≤ y
  less-insert here      (l ∷ _)  = l
  less-insert (there p) (_ ∷ ls) = less-insert p ls

  less-remove : ∀ {x y xs ys} → y ◂ ys ≡ xs → x ≤* xs → x ≤* ys
  less-remove here      (l ∷ ls) = ls
  less-remove (there p) (l ∷ ls) = l ∷ less-remove p ls

  less-perm : ∀ {x xs ys} → IsPermutation xs ys → x ≤* ys → x ≤* xs
  less-perm [] [] = []
  less-perm (p ∷ ps) ss = less-insert p ss ∷ less-perm ps (less-remove p ss)

  -- alternative: insertion instead of selection
  insert-less : ∀ {x y xs ys} → y ◂ ys ≡ xs → x ≤ y → x ≤* ys → x ≤* xs
  insert-less here      l ks = l ∷ ks
  insert-less (there p) l (k ∷ ks) = k ∷ insert-less p l ks

  less-perm' : ∀ {x xs ys} → IsPermutation xs ys → x ≤* xs → x ≤* ys
  less-perm' [] [] = []
  less-perm' (p ∷ ps) (s ∷ ss) = insert-less p s (less-perm' ps ss)

  less-++ : ∀ {x xs ys} → x ≤* xs → x ≤* ys → x ≤* (xs ++ ys)
  less-++ [] ys = ys
  less-++ (x ∷ xs) ys = x ∷ less-++ xs ys

  -- Sorted permutations of xs
  data Sorted : List A → Set (lmax a r) where
    []   : Sorted []
    cons : ∀ x {xs xxs} → (p : x ◂ xs ≡ xxs) → (least : x ≤* xs) → (rest : Sorted xs) → Sorted xxs

  -- Alternative:
  record Sorted' (xs : List A) : Set (lmax a r) where
    constructor sorted'
    field
      list     : List A
      isSorted : IsSorted list
      isPerm   : IsPermutation list xs

  Sorted-to-Sorted' : ∀ {xs} → Sorted xs → Sorted' xs
  Sorted-to-Sorted' [] = sorted' [] [] []
  Sorted-to-Sorted' (cons x p l xs)
      = sorted' (x ∷ list) (IsSorted._∷_ (less-perm isPerm l) isSorted) (p ∷ isPerm)
    where open Sorted' (Sorted-to-Sorted' xs)

  Sorted'-to-Sorted : ∀ {xs} → Sorted' xs → Sorted xs
  Sorted'-to-Sorted (sorted' [] [] []) = []
  Sorted'-to-Sorted (sorted' (x ∷ xs) (l ∷ ls) (p ∷ ps))
    = cons x p (less-perm' ps l) (Sorted'-to-Sorted (sorted' xs ls ps))

  -- Sorted lists are unique
  Sorted-to-List : ∀ {xs} → Sorted xs → List A
  Sorted-to-List [] = []
  Sorted-to-List (cons x _ _ xs) = x ∷ Sorted-to-List xs

  Sorted-unique' : ∀ {xs xs'} → (IsPermutation xs xs') → (ys : Sorted xs) → (zs : Sorted xs')
                 → Sorted-to-List ys ≡ Sorted-to-List zs
  Sorted-unique' [] [] [] = refl
  Sorted-unique' [] (cons _ () _ _) _
  Sorted-unique' [] _ (cons _ () _ _)
  Sorted-unique' (() ∷ _) _ []
  Sorted-unique' ps (cons y yp yl ys) (cons z zp zl zs) = cong₂ _∷_ y=z (Sorted-unique' ps' ys zs)
    where
    y=z : y ≡ z
    y=z = antisym (less-insert zp (less-perm' ps (insert-less yp ≤-refl yl)))
                  (less-insert yp (less-perm  ps (insert-less zp ≤-refl zl)))
    ps' = same-perm y=z ps yp zp

  Sorted-unique : ∀ {xs} → (ys zs : Sorted xs) → Sorted-to-List ys ≡ Sorted-to-List zs
  Sorted-unique = Sorted-unique' (id-permutation _)

-----------------------------------------------------------------------------------------
-- Logarithms
-----------------------------------------------------------------------------------------

module Nat where
  log-split : ∀ n-2 → let n = 2 + n-2 in
              ⌊ n /2⌋ * ⌈log₂ ⌊ n /2⌋ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉)) ≤ n * ⌈log₂ n ⌉
  log-split n-2 = let n = 2 + n-2 in
    begin
      ⌊ n /2⌋ * ⌈log₂ ⌊ n /2⌋ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
    ≤⟨ +-monoˡ-≤ (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
      (*-monoʳ-≤  ⌊ n /2⌋
      (⌈log₂⌉-mono-≤ (⌊n/2⌋≤⌈n/2⌉ n))) ⟩
      ⌊ n /2⌋ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
    ≡⟨ lem  ⌊ n /2⌋  ⌈ n /2⌉  ⌈log₂ ⌈ n /2⌉ ⌉  ⟩
      (⌊ n /2⌋ + ⌈ n /2⌉) * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
    ≡⟨ cong (\nn → nn * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)) (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
      n * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
    ≡⟨ cong (\l → n * (1 + l)) (⌈log₂⌈n/2⌉⌉≡⌈log₂n⌉∸1 n) ⟩
      n * ⌈log₂ n ⌉
    ∎
    where
    open ≤-Reasoning
    lem : ∀ a b c → a * c + (b * c + (a + b)) ≡ (a + b) * (1 + c)
    lem = solve-∀

open Nat

-----------------------------------------------------------------------------------------
-- Sorting algorithms
-----------------------------------------------------------------------------------------

module SortingAlgorithm
    {A : Set}
    {_≤_ : Rel A ℓ₀}
    (isPartialOrder : IsPartialOrder _≡_ _≤_)
    -- testing ordering can be done in 1 operation
    (_≤?_ : (x y : A) → (x ≤ y ⊎ y ≤ x) in-time 1) where

  open Permutations A
  open SortedList isPartialOrder

  ---------------------------------------------------------------------------
  -- Insertion sort
  ---------------------------------------------------------------------------

  -- Insertion sort, O(n^2)
  insert : ∀ {xs} → (x : A) → Sorted xs → Sorted (x ∷ xs) in-time (length xs)
  insert x []
    = return $ cons x here [] []
  insert x (cons u p0 u≤*us us)
    = bound-≡ (sym (length-insert p0))
    $ (x ≤? u) >>= λ
    { (inj₁ p) → return $ cons x here (insert-less p0 p (≤*-trans p u≤*us)) $ cons u p0 u≤*us us
    ; (inj₂ p) → cons u (there p0) (p ∷ u≤*us) <$> insert x us
    }

  insertion-sort : (xs : List A) → Sorted xs in-time length xs ^ 2
  insertion-sort [] = return []
  insertion-sort (x ∷ xs)
    = bound-≡ (lem (length xs)) $
      insertion-sort xs >>= insert x >>= return
    where
      -- lem : ∀ n → (n ^ 2 + n) + (n + 1) ≡ (1 + n) ^ 2
      lem : ∀ n → (n * (n * 1) + n) + (n + 1) ≡ (1 + n) * ((1 + n) * 1)
      lem = solve-∀

  ---------------------------------------------------------------------------
  -- Selection sort
  ---------------------------------------------------------------------------

  import Data.Vec as Vec
  open Vec using (Vec;toList;fromList;_∷_;[])

  -- select least element from a non-empty list x∷xs
  select1 : ∀ {n} (xs : Vec A (suc n))
          → (∃₂ \y ys → (y ◂ toList ys ≡ toList xs) × (y ≤* toList ys)) in-time n
  select1 (x ∷ []) = return $ x , [] , here , []
  select1 {suc n} (x ∷ xs)
    = bound-≡ (lem n) $
      select1 xs >>= \{ (z , zs , perm , least)
      → x ≤? z >>= \
        { (inj₁ p) → return $ x , xs , here , insert-less perm p (≤*-trans p least)
        ; (inj₂ p) → return $ z , (x ∷ zs) , there perm , (p ∷ least)
        }}
    where
    lem : ∀ n → n + 1 ≡ 1 + n
    lem = solve-∀

  selection-sort1 : ∀ {n} (xs : Vec A n) → (Sorted (toList xs)) in-time (n ^ 2)
  selection-sort1 [] = return []
  selection-sort1 {suc n} xs
    = bound-+ (lem n) $
      select1 xs >>= \
      { (y , ys , perm , least)
      → cons y perm least <$> selection-sort1 ys }
    where
      -- Note: ring solver reflection doesn't understand exponents
      --lem : ∀ n → n + (n ^ 2) + (n + 1) ≡ (1 + n) ^ 2
      lem : ∀ n → n + (n * (n * 1)) + (n + 1) ≡ (1 + n) * ((1 + n) * 1)
      lem = solve-∀

  toList∘fromList : ∀ (xs : List A) → toList (fromList xs) ≡ xs
  toList∘fromList [] = refl
  toList∘fromList (x ∷ xs) = cong (_∷_ x) (toList∘fromList xs)

  selection-sort2 : ∀ (xs : List A) → (Sorted xs) in-time (length xs ^ 2)
  selection-sort2 xs = subst Sorted (toList∘fromList xs)
                     <$> selection-sort1 (fromList xs)

  ---------------------------------------------------------------------------
  -- Merge sort
  ---------------------------------------------------------------------------

  xs++[]=xs : ∀ (xs : List A) → xs ++ [] ≡ xs
  xs++[]=xs []       = refl
  xs++[]=xs (x ∷ xs) = cong (_∷_ x) (xs++[]=xs xs)

  length∘toList : ∀ {n} (xs : Vec A n) → length (toList xs) ≡ n
  length∘toList [] = refl
  length∘toList (x ∷ xs) = cong suc (length∘toList xs)

  merge : ∀ {xs ys} → Sorted xs → Sorted ys → (Sorted (xs ++ ys)) in-time (length xs + length ys)
  merge [] sys = return sys
  merge sxs [] = return $ subst Sorted (sym (xs++[]=xs _)) sxs
  merge {xs = []} (cons _ () _ _) _
  merge {ys = []} _ (cons _ () _ _)
  merge {xs = x ∷ xs} {ys = yys} (cons u {xs = xus} up ul us) (cons v {xs = yvs} vp vl vs)
    = go (cons u up ul us) (cons v vp vl vs) =<< (u ≤? v)
    where
    go : Sorted (x ∷ xs) → Sorted yys
       → (u ≤ v) ⊎ (v ≤ u)
       → (Sorted (x ∷ xs ++ yys)) in-time (length xs + length yys)
    go _ vss (inj₁ u≤v)
      = bound-≡ (cong (\l → pred l + length (yys)) (sym $ length-insert up))
      $ merge us vss <$$>
        cons u (insert-++₁ up) (less-++ ul (insert-less vp u≤v (≤*-trans u≤v vl)))
    go uus _ (inj₂ v≤u)
      = bound-≡ (1+m+n=m+1+n (length xs) _ ⟨ trans ⟩
                 cong (\l → length xs + l) (sym $ length-insert vp))
      $ merge uus vs <$$>
        cons v (insert-++₂ {xs = x ∷ xs} vp) (less-++ (insert-less up v≤u (≤*-trans v≤u ul)) vl)

  splitAtVec : ∀ m {n m+n} (xs : Vec A m+n) → m + n ≡ m+n
             → ∃₂ \(ys : Vec A m) (zs : Vec A n) → toList ys ++ toList zs ≡ toList xs
  splitAtVec zero xs refl = [] , xs , refl
  splitAtVec (suc m) [] ()
  splitAtVec (suc m) (x ∷ xs) refl with splitAtVec m xs refl
  ... | us , vs , uvx = x ∷ us , vs , cong (_∷_ x) uvx

  splitHalf' : ∀ {n} → (xs : Vec A n)
             → ∃₂ \(ys : Vec A ⌊ n /2⌋) (zs : Vec A ⌈ n /2⌉) → toList ys ++ toList zs ≡ toList xs
  splitHalf' {n} xs = splitAtVec ⌊ n /2⌋ xs (⌊n/2⌋+⌈n/2⌉≡n n)

  MergeSort : ℕ → Set
  MergeSort = \n → (xs : Vec A n) → (Sorted (toList xs)) in-time (n * ⌈log₂ n ⌉)

  merge-sort' : ∀ n → <-Rec MergeSort n → MergeSort n
  merge-sort' 0             rec []       = return $ []
  merge-sort' 1             rec (x ∷ []) = return $ cons x here [] []
  merge-sort' (suc (suc n)) rec xs with splitHalf' xs
  ... | xs₁ , xs₂ , ok
      = bound-≤ (log-split n)
      $ bound-≡ (cong₂ (\x y → ⌊ 2 + n /2⌋ * ⌈log₂ ⌊ 2 + n /2⌋ ⌉ + (⌈ 2 + n /2⌉ * ⌈log₂ ⌈ 2 + n /2⌉ ⌉ + (x + y)))
                          (length∘toList xs₁)
                          (length∘toList xs₂))
      $ rec _ (s≤s $ s≤s $ ⌊n/2⌋≤n n) xs₁ >>= \sorted₁
      → rec _ (s≤s $ s≤s $ ⌈n/2⌉≤n n) xs₂ >>= \sorted₂
      → subst Sorted ok <$> merge sorted₁ sorted₂

  merge-sort : ∀ xs → (Sorted xs) in-time (length xs * ⌈log₂ length xs ⌉)
  merge-sort xs = subst Sorted (toList∘fromList xs)
              <$> <-rec MergeSort merge-sort' (length xs) (fromList xs)


-----------------------------------------------------------------------------------------
-- Aside: standard library total orders are decidable
-----------------------------------------------------------------------------------------

total-decidable : ∀ {a r} {A : Set a}
                → (_≤_ : Rel A r)
                → IsTotalOrder _≡_ _≤_
                → IsDecTotalOrder _≡_ _≤_
total-decidable {A = A} _≤_ isTotalOrder = record
  { isTotalOrder = isTotalOrder
  ; _≟_ = _≟_
  ; _≤?_ = _≤?_
  }
  where
  open IsTotalOrder isTotalOrder using (reflexive; total; antisym)

  _≟_ : (x y : A) → Dec (x ≡ y)
  _≟_ x y with total x y | total y x | inspect (total x) y | inspect (total y) x
  ... | inj₁ x≤y | inj₁ y≤x | _ | _ = yes (antisym x≤y y≤x)
  ... | inj₂ y≤x | inj₂ x≤y | _ | _ = yes (antisym x≤y y≤x)
  ... | inj₁ _   | inj₂ _   | reveal a | reveal b = no way
      where
      way : ¬ x ≡ y
      way refl with trans (sym a) b
      ... | ()
  ... | inj₂ _   | inj₁ _   | reveal a | reveal b = no way
      where
      way : ¬ x ≡ y
      way refl with trans (sym a) b
      ... | ()

  _≤?_ : (x y : A) → Dec (x ≤ y)
  _≤?_ x y with total x y | x ≟ y
  ... | inj₁ x≤y | _       = yes x≤y
  ... | inj₂ y≤x | yes x=y = yes (reflexive x=y)
  ... | inj₂ y≤x | no  x≠y = no \x≤y → x≠y (antisym x≤y y≤x)
	module Sorting where
	-- See https://www.twanvl.nl/blog/agda/sorting

	open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
	open import Data.List hiding (merge)
	open import Data.List.Properties
	open import Data.Nat hiding (_≟_;_≤?_)
	open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
	open import Data.Nat.Logarithm
	open import Data.Nat.Induction
	open import Data.Nat.Tactic.RingSolver
	open import Data.Product
	open import Data.Sum
	open import Relation.Nullary
	open import Relation.Binary
	open import Relation.Binary.PropositionalEquality renaming ([_] to reveal)
	open import Function

	-----------------------------------------------------------------------------------------
	-- Counting monad
	-----------------------------------------------------------------------------------------

	-- A monad that keeps a natural number counter
	module CountingMonad where
	private
	module Dummy where
	infix 1 _in-time_
	data _in-time_ {a} (A : Set a) (n : ℕ) : Set a where
	box : A → A in-time n

	open Dummy

	unbox : ∀ {a} {A : Set a} {n} → A in-time n → A
	unbox (box x) = x

	open Dummy public using (_in-time_)

	infixl 1 _>>=_
	_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → {n m : ℕ} → A in-time n → (A → B in-time m) → B in-time (n + m)
	box x >>= f = box (unbox (f x))

	_=<<_ : ∀ {a b} {A : Set a} {B : Set b} → {n m : ℕ} → (A → B in-time m) → A in-time n → B in-time (n + m)
	_=<<_ = flip _>>=_

	infixr 2 _<$>_
	_<$>_ : ∀ {a b} {A : Set a} {B : Set b} → {n : ℕ} → (A → B) → A in-time n → B in-time n
	f <$> box x = box (f x)

	_<$$>_ : ∀ {a b} {A : Set a} {B : Set b} → {n : ℕ} → A in-time n → (A → B) → B in-time n
	_<$$>_ = flip _<$>_

	return : ∀ {a} {A : Set a} → {n : ℕ} → A → A in-time n
	return = box

	bound-≡ : ∀ {a} {A : Set a} {m n} → (m ≡ n) → A in-time m → A in-time n
	bound-≡ = subst (_in-time_ _)

	bound-+ : ∀ {a} {A : Set a} {m n k} → (m + k ≡ n) → A in-time m → A in-time n
	bound-+ eq x = bound-≡ eq (x >>= return)

	bound-≤ : ∀ {a} {A : Set a} {m n} → (m ≤ n) → A in-time m → A in-time n
	bound-≤ m≤n = bound-+ (m+[n∸m]≡n m≤n)

	bound-≤′ : ∀ {a} {A : Set a} {m n} → (m ≤′ n) → A in-time m → A in-time n
	bound-≤′ ≤′-refl x = x
	bound-≤′ (≤′-step l) x = return {n = 1} x >>= bound-≤′ l

	open CountingMonad


	-----------------------------------------------------------------------------------------
	-- Permutations
	-----------------------------------------------------------------------------------------

	1+m+n=m+1+n : (m n : ℕ) → suc (m + n) ≡ m + suc n
	1+m+n=m+1+n = solve-∀

	module Permutations {a} (A : Set a) where

	-- x ◂ xs ≡ ys means that ys is equal to xs with x inserted somewhere
	data _◂_≡_ (x : A) : List A → List A → Set a where
	here : ∀ {xs} → x ◂ xs ≡ (x ∷ xs)
	there : ∀ {y} {xs} {xys} → (p : x ◂ xs ≡ xys) → x ◂ (y ∷ xs) ≡ (y ∷ xys)

	-- Proof that a list is a permutation of another one
	data IsPermutation : List A → List A → Set a where
	[] : IsPermutation [] []
	_∷_ : ∀ {x xs ys xys}
	→ (p : x ◂ ys ≡ xys)
	→ (ps : IsPermutation xs ys)
	→ IsPermutation (x ∷ xs) xys

	-- Identity permutation
	id-permutation : (xs : List A) → IsPermutation xs xs
	id-permutation [] = []
	id-permutation (x ∷ xs) = here ∷ id-permutation xs

	-- cons on the other side
	insert-permutation : ∀ {x xs ys xys}
	→ x ◂ ys ≡ xys → IsPermutation ys xs → IsPermutation xys (x ∷ xs)
	insert-permutation here p = here ∷ p
	insert-permutation (there y) (p ∷ ps) = there p ∷ insert-permutation y ps

	-- inverse permutations
	inverse-permutation : ∀ {xs ys} -> IsPermutation xs ys → IsPermutation ys xs
	inverse-permutation [] = []
	inverse-permutation (p ∷ ps) = insert-permutation p (inverse-permutation ps)

	swap-inserts : ∀ {x y xs xxs yxxs}
	→ (x ◂ xs ≡ xxs) → (y ◂ xxs ≡ yxxs) → ∃ \yxs → (y ◂ xs ≡ yxs) × (x ◂ yxs ≡ yxxs)
	swap-inserts p here = _ , here , there p
	swap-inserts here (there q) = _ , q , here
	swap-inserts (there p) (there q) with swap-inserts p q
	... \| _ , p' , q' = _ , there p' , there q'

	extract-permutation : ∀ {x ys zs zs'}
	→ x ◂ ys ≡ zs → IsPermutation zs zs'
	→ ∃ \ys' → (x ◂ ys' ≡ zs') × IsPermutation ys ys'
	extract-permutation here (q ∷ qs) = _ , q , qs
	extract-permutation (there p) (q ∷ qs) with extract-permutation p qs
	... \| ys' , r , rs with swap-inserts r q
	... \| ys'' , s , t = ys'' , t , s ∷ rs

	-- composing permutations
	compose-permutation : ∀ {xs ys zs : List A}
	→ IsPermutation xs ys → IsPermutation ys zs → IsPermutation xs zs
	compose-permutation [] [] = []
	compose-permutation (p ∷ ps) qqs with extract-permutation p qqs
	... \| _ , q , qs = q ∷ compose-permutation ps qs

	insert-++₁ : ∀ {x xs ys xxs} → x ◂ xs ≡ xxs → x ◂ (xs ++ ys) ≡ (xxs ++ ys)
	insert-++₁ here = here
	insert-++₁ (there p) = there (insert-++₁ p)

	insert-++₂ : ∀ {y xs ys yys} → y ◂ ys ≡ yys → y ◂ (xs ++ ys) ≡ (xs ++ yys)
	insert-++₂ {xs = []} p = p
	insert-++₂ {xs = _ ∷ xs} p = there (insert-++₂ {xs = xs} p)

	-- Length of permutations
	length-insert : ∀ {x xs xxs} → x ◂ xs ≡ xxs → length xxs ≡ suc (length xs)
	length-insert here = refl
	length-insert (there p) = cong suc (length-insert p)

	length-permutation : ∀ {xs ys} → IsPermutation xs ys → length xs ≡ length ys
	length-permutation [] = refl
	length-permutation (p ∷ ps) = cong suc (length-permutation ps) ⟨ trans ⟩ sym (length-insert p)

	same-perm' : ∀ {x xs xxs ys} → x ◂ xs ≡ xxs → x ◂ ys ≡ xxs → IsPermutation xs ys
	same-perm' here here = id-permutation _
	same-perm' here (there q) = insert-permutation q (id-permutation _)
	same-perm' (there p) here = p ∷ id-permutation _
	same-perm' (there p) (there q) = here ∷ same-perm' p q

	same-perm : ∀ {x xs xxs y ys yys}
	→ x ≡ y → IsPermutation xxs yys → x ◂ xs ≡ xxs → y ◂ ys ≡ yys → IsPermutation xs ys
	same-perm refl ps q r with extract-permutation q ps
	... \| l' , q' , ps' = compose-permutation ps' (same-perm' q' r)

	-----------------------------------------------------------------------------------------
	-- Sorted lists
	-----------------------------------------------------------------------------------------

	module SortedList
	{a r}
	{A : Set a}
	{_≤_ : Rel A r}
	(isPartialOrder : IsPartialOrder _≡_ _≤_) where

	open IsPartialOrder isPartialOrder renaming (trans to ≤-trans; refl to ≤-refl)

	-- Less than all values in a list
	data _≤*_ (x : A) : List A → Set (lmax a r) where
	[] : x ≤* []
	_∷_ : ∀ {y ys} → (x ≤ y) → x ≤* ys → x ≤* (y ∷ ys)

	-- Proof that a list is sorted
	data IsSorted : List A → Set (lmax a r) where
	[] : IsSorted []
	_∷_ : ∀ {x xs} → x ≤* xs → IsSorted xs → IsSorted (x ∷ xs)

	≤-trans : ∀ {x u us} → x ≤ u → u ≤ us → x ≤* us
	≤*-trans p [] = []
	≤-trans p (y ∷ ys) = ≤-trans p y ∷ ≤-trans p ys


	-- relation to permutations
	open Permutations A
	less-insert : ∀ {x y xs ys} → y ◂ ys ≡ xs → x ≤* xs → x ≤ y
	less-insert here (l ∷ _) = l
	less-insert (there p) (_ ∷ ls) = less-insert p ls

	less-remove : ∀ {x y xs ys} → y ◂ ys ≡ xs → x ≤* xs → x ≤* ys
	less-remove here (l ∷ ls) = ls
	less-remove (there p) (l ∷ ls) = l ∷ less-remove p ls

	less-perm : ∀ {x xs ys} → IsPermutation xs ys → x ≤* ys → x ≤* xs
	less-perm [] [] = []
	less-perm (p ∷ ps) ss = less-insert p ss ∷ less-perm ps (less-remove p ss)

	-- alternative: insertion instead of selection
	insert-less : ∀ {x y xs ys} → y ◂ ys ≡ xs → x ≤ y → x ≤* ys → x ≤* xs
	insert-less here l ks = l ∷ ks
	insert-less (there p) l (k ∷ ks) = k ∷ insert-less p l ks

	less-perm' : ∀ {x xs ys} → IsPermutation xs ys → x ≤* xs → x ≤* ys
	less-perm' [] [] = []
	less-perm' (p ∷ ps) (s ∷ ss) = insert-less p s (less-perm' ps ss)

	less-++ : ∀ {x xs ys} → x ≤* xs → x ≤* ys → x ≤* (xs ++ ys)
	less-++ [] ys = ys
	less-++ (x ∷ xs) ys = x ∷ less-++ xs ys

	-- Sorted permutations of xs
	data Sorted : List A → Set (lmax a r) where
	[] : Sorted []
	cons : ∀ x {xs xxs} → (p : x ◂ xs ≡ xxs) → (least : x ≤* xs) → (rest : Sorted xs) → Sorted xxs

	-- Alternative:
	record Sorted' (xs : List A) : Set (lmax a r) where
	constructor sorted'
	field
	list : List A
	isSorted : IsSorted list
	isPerm : IsPermutation list xs

	Sorted-to-Sorted' : ∀ {xs} → Sorted xs → Sorted' xs
	Sorted-to-Sorted' [] = sorted' [] [] []
	Sorted-to-Sorted' (cons x p l xs)
	= sorted' (x ∷ list) (IsSorted._∷_ (less-perm isPerm l) isSorted) (p ∷ isPerm)
	where open Sorted' (Sorted-to-Sorted' xs)

	Sorted'-to-Sorted : ∀ {xs} → Sorted' xs → Sorted xs
	Sorted'-to-Sorted (sorted' [] [] []) = []
	Sorted'-to-Sorted (sorted' (x ∷ xs) (l ∷ ls) (p ∷ ps))
	= cons x p (less-perm' ps l) (Sorted'-to-Sorted (sorted' xs ls ps))

	-- Sorted lists are unique
	Sorted-to-List : ∀ {xs} → Sorted xs → List A
	Sorted-to-List [] = []
	Sorted-to-List (cons x _ _ xs) = x ∷ Sorted-to-List xs

	Sorted-unique' : ∀ {xs xs'} → (IsPermutation xs xs') → (ys : Sorted xs) → (zs : Sorted xs')
	→ Sorted-to-List ys ≡ Sorted-to-List zs
	Sorted-unique' [] [] [] = refl
	Sorted-unique' [] (cons _ () _ _) _
	Sorted-unique' [] _ (cons _ () _ _)
	Sorted-unique' (() ∷ _) _ []
	Sorted-unique' ps (cons y yp yl ys) (cons z zp zl zs) = cong₂ _∷_ y=z (Sorted-unique' ps' ys zs)
	where
	y=z : y ≡ z
	y=z = antisym (less-insert zp (less-perm' ps (insert-less yp ≤-refl yl)))
	(less-insert yp (less-perm ps (insert-less zp ≤-refl zl)))
	ps' = same-perm y=z ps yp zp

	Sorted-unique : ∀ {xs} → (ys zs : Sorted xs) → Sorted-to-List ys ≡ Sorted-to-List zs
	Sorted-unique = Sorted-unique' (id-permutation _)

	-----------------------------------------------------------------------------------------
	-- Logarithms
	-----------------------------------------------------------------------------------------

	module Nat where
	log-split : ∀ n-2 → let n = 2 + n-2 in
	⌊ n /2⌋ * ⌈log₂ ⌊ n /2⌋ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉)) ≤ n * ⌈log₂ n ⌉
	log-split n-2 = let n = 2 + n-2 in
	begin
	⌊ n /2⌋ * ⌈log₂ ⌊ n /2⌋ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
	≤⟨ +-monoˡ-≤ (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
	(*-monoʳ-≤ ⌊ n /2⌋
	(⌈log₂⌉-mono-≤ (⌊n/2⌋≤⌈n/2⌉ n))) ⟩
	⌊ n /2⌋ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌈ n /2⌉ * ⌈log₂ ⌈ n /2⌉ ⌉ + (⌊ n /2⌋ + ⌈ n /2⌉))
	≡⟨ lem ⌊ n /2⌋ ⌈ n /2⌉ ⌈log₂ ⌈ n /2⌉ ⌉ ⟩
	(⌊ n /2⌋ + ⌈ n /2⌉) * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
	≡⟨ cong (\nn → nn * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)) (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
	n * (1 + ⌈log₂ ⌈ n /2⌉ ⌉)
	≡⟨ cong (\l → n * (1 + l)) (⌈log₂⌈n/2⌉⌉≡⌈log₂n⌉∸1 n) ⟩
	n * ⌈log₂ n ⌉
	∎
	where
	open ≤-Reasoning
	lem : ∀ a b c → a * c + (b * c + (a + b)) ≡ (a + b) * (1 + c)
	lem = solve-∀

	open Nat

	-----------------------------------------------------------------------------------------
	-- Sorting algorithms
	-----------------------------------------------------------------------------------------

	module SortingAlgorithm
	{A : Set}
	{_≤_ : Rel A ℓ₀}
	(isPartialOrder : IsPartialOrder _≡_ _≤_)
	-- testing ordering can be done in 1 operation
	(_≤?_ : (x y : A) → (x ≤ y ⊎ y ≤ x) in-time 1) where

	open Permutations A
	open SortedList isPartialOrder

	---------------------------------------------------------------------------
	-- Insertion sort
	---------------------------------------------------------------------------

	-- Insertion sort, O(n^2)
	insert : ∀ {xs} → (x : A) → Sorted xs → Sorted (x ∷ xs) in-time (length xs)
	insert x []
	= return $ cons x here [] []
	insert x (cons u p0 u≤*us us)
	= bound-≡ (sym (length-insert p0))
	$ (x ≤? u) >>= λ
	{ (inj₁ p) → return $ cons x here (insert-less p0 p (≤-trans p u≤us)) $ cons u p0 u≤*us us
	; (inj₂ p) → cons u (there p0) (p ∷ u≤*us) <$> insert x us
	}

	insertion-sort : (xs : List A) → Sorted xs in-time length xs ^ 2
	insertion-sort [] = return []
	insertion-sort (x ∷ xs)
	= bound-≡ (lem (length xs)) $
	insertion-sort xs >>= insert x >>= return
	where
	-- lem : ∀ n → (n ^ 2 + n) + (n + 1) ≡ (1 + n) ^ 2
	lem : ∀ n → (n * (n * 1) + n) + (n + 1) ≡ (1 + n) * ((1 + n) * 1)
	lem = solve-∀

	---------------------------------------------------------------------------
	-- Selection sort
	---------------------------------------------------------------------------

	import Data.Vec as Vec
	open Vec using (Vec;toList;fromList;_∷_;[])

	-- select least element from a non-empty list x∷xs
	select1 : ∀ {n} (xs : Vec A (suc n))
	→ (∃₂ \y ys → (y ◂ toList ys ≡ toList xs) × (y ≤* toList ys)) in-time n
	select1 (x ∷ []) = return $ x , [] , here , []
	select1 {suc n} (x ∷ xs)
	= bound-≡ (lem n) $
	select1 xs >>= \{ (z , zs , perm , least)
	→ x ≤? z >>= \
	{ (inj₁ p) → return $ x , xs , here , insert-less perm p (≤*-trans p least)
	; (inj₂ p) → return $ z , (x ∷ zs) , there perm , (p ∷ least)
	}}
	where
	lem : ∀ n → n + 1 ≡ 1 + n
	lem = solve-∀

	selection-sort1 : ∀ {n} (xs : Vec A n) → (Sorted (toList xs)) in-time (n ^ 2)
	selection-sort1 [] = return []
	selection-sort1 {suc n} xs
	= bound-+ (lem n) $
	select1 xs >>= \
	{ (y , ys , perm , least)
	→ cons y perm least <$> selection-sort1 ys }
	where
	-- Note: ring solver reflection doesn't understand exponents
	--lem : ∀ n → n + (n ^ 2) + (n + 1) ≡ (1 + n) ^ 2
	lem : ∀ n → n + (n * (n * 1)) + (n + 1) ≡ (1 + n) * ((1 + n) * 1)
	lem = solve-∀

	toList∘fromList : ∀ (xs : List A) → toList (fromList xs) ≡ xs
	toList∘fromList [] = refl
	toList∘fromList (x ∷ xs) = cong (_∷_ x) (toList∘fromList xs)

	selection-sort2 : ∀ (xs : List A) → (Sorted xs) in-time (length xs ^ 2)
	selection-sort2 xs = subst Sorted (toList∘fromList xs)
	<$> selection-sort1 (fromList xs)

	---------------------------------------------------------------------------
	-- Merge sort
	---------------------------------------------------------------------------

	xs++[]=xs : ∀ (xs : List A) → xs ++ [] ≡ xs
	xs++[]=xs [] = refl
	xs++[]=xs (x ∷ xs) = cong (_∷_ x) (xs++[]=xs xs)

	length∘toList : ∀ {n} (xs : Vec A n) → length (toList xs) ≡ n
	length∘toList [] = refl
	length∘toList (x ∷ xs) = cong suc (length∘toList xs)

	merge : ∀ {xs ys} → Sorted xs → Sorted ys → (Sorted (xs ++ ys)) in-time (length xs + length ys)
	merge [] sys = return sys
	merge sxs [] = return $ subst Sorted (sym (xs++[]=xs _)) sxs
	merge {xs = []} (cons _ () _ _) _
	merge {ys = []} _ (cons _ () _ _)
	merge {xs = x ∷ xs} {ys = yys} (cons u {xs = xus} up ul us) (cons v {xs = yvs} vp vl vs)
	= go (cons u up ul us) (cons v vp vl vs) =<< (u ≤? v)
	where
	go : Sorted (x ∷ xs) → Sorted yys
	→ (u ≤ v) ⊎ (v ≤ u)
	→ (Sorted (x ∷ xs ++ yys)) in-time (length xs + length yys)
	go _ vss (inj₁ u≤v)
	= bound-≡ (cong (\l → pred l + length (yys)) (sym $ length-insert up))
	$ merge us vss <$$>
	cons u (insert-++₁ up) (less-++ ul (insert-less vp u≤v (≤*-trans u≤v vl)))
	go uus _ (inj₂ v≤u)
	= bound-≡ (1+m+n=m+1+n (length xs) _ ⟨ trans ⟩
	cong (\l → length xs + l) (sym $ length-insert vp))
	$ merge uus vs <$$>
	cons v (insert-++₂ {xs = x ∷ xs} vp) (less-++ (insert-less up v≤u (≤*-trans v≤u ul)) vl)

	splitAtVec : ∀ m {n m+n} (xs : Vec A m+n) → m + n ≡ m+n
	→ ∃₂ \(ys : Vec A m) (zs : Vec A n) → toList ys ++ toList zs ≡ toList xs
	splitAtVec zero xs refl = [] , xs , refl
	splitAtVec (suc m) [] ()
	splitAtVec (suc m) (x ∷ xs) refl with splitAtVec m xs refl
	... \| us , vs , uvx = x ∷ us , vs , cong (_∷_ x) uvx

	splitHalf' : ∀ {n} → (xs : Vec A n)
	→ ∃₂ \(ys : Vec A ⌊ n /2⌋) (zs : Vec A ⌈ n /2⌉) → toList ys ++ toList zs ≡ toList xs
	splitHalf' {n} xs = splitAtVec ⌊ n /2⌋ xs (⌊n/2⌋+⌈n/2⌉≡n n)

	MergeSort : ℕ → Set
	MergeSort = \n → (xs : Vec A n) → (Sorted (toList xs)) in-time (n * ⌈log₂ n ⌉)

	merge-sort' : ∀ n → <-Rec MergeSort n → MergeSort n
	merge-sort' 0 rec [] = return $ []
	merge-sort' 1 rec (x ∷ []) = return $ cons x here [] []
	merge-sort' (suc (suc n)) rec xs with splitHalf' xs
	... \| xs₁ , xs₂ , ok
	= bound-≤ (log-split n)
	$ bound-≡ (cong₂ (\x y → ⌊ 2 + n /2⌋ * ⌈log₂ ⌊ 2 + n /2⌋ ⌉ + (⌈ 2 + n /2⌉ * ⌈log₂ ⌈ 2 + n /2⌉ ⌉ + (x + y)))
	(length∘toList xs₁)
	(length∘toList xs₂))
	$ rec _ (s≤s $ s≤s $ ⌊n/2⌋≤n n) xs₁ >>= \sorted₁
	→ rec _ (s≤s $ s≤s $ ⌈n/2⌉≤n n) xs₂ >>= \sorted₂
	→ subst Sorted ok <$> merge sorted₁ sorted₂

	merge-sort : ∀ xs → (Sorted xs) in-time (length xs * ⌈log₂ length xs ⌉)
	merge-sort xs = subst Sorted (toList∘fromList xs)
	<$> <-rec MergeSort merge-sort' (length xs) (fromList xs)


	-----------------------------------------------------------------------------------------
	-- Aside: standard library total orders are decidable
	-----------------------------------------------------------------------------------------

	total-decidable : ∀ {a r} {A : Set a}
	→ (_≤_ : Rel A r)
	→ IsTotalOrder _≡_ _≤_
	→ IsDecTotalOrder _≡_ _≤_
	total-decidable {A = A} _≤_ isTotalOrder = record
	{ isTotalOrder = isTotalOrder
	; _≟_ = _≟_
	; _≤?_ = _≤?_
	}
	where
	open IsTotalOrder isTotalOrder using (reflexive; total; antisym)

	_≟_ : (x y : A) → Dec (x ≡ y)
	_≟_ x y with total x y \| total y x \| inspect (total x) y \| inspect (total y) x
	... \| inj₁ x≤y \| inj₁ y≤x \| _ \| _ = yes (antisym x≤y y≤x)
	... \| inj₂ y≤x \| inj₂ x≤y \| _ \| _ = yes (antisym x≤y y≤x)
	... \| inj₁ _ \| inj₂ _ \| reveal a \| reveal b = no way
	where
	way : ¬ x ≡ y
	way refl with trans (sym a) b
	... \| ()
	... \| inj₂ _ \| inj₁ _ \| reveal a \| reveal b = no way
	where
	way : ¬ x ≡ y
	way refl with trans (sym a) b
	... \| ()

	_≤?_ : (x y : A) → Dec (x ≤ y)
	_≤?_ x y with total x y \| x ≟ y
	... \| inj₁ x≤y \| _ = yes x≤y
	... \| inj₂ y≤x \| yes x=y = yes (reflexive x=y)
	... \| inj₂ y≤x \| no x≠y = no \x≤y → x≠y (antisym x≤y y≤x)