挿入ソートの証明

Isort.idr

module Isort

-- > idris -p base
import Syntax.PreorderReasoning

%default total
%hide sorted


sorted : List Nat -> Bool
sorted []           = True
sorted (x::[])      = True
sorted (x1::x2::xs) = lte x1 x2 && sorted (x2::xs)

insert : Nat -> List Nat -> List Nat
insert x []      = [x]
insert x (y::ys) = if lte x y then x :: y :: ys
                              else y :: insert x ys
-- 挿入ソート
isort : List Nat -> List Nat
isort = foldr insert []

h : Nat -> Bool -> Bool
h _ b = b


-- sortedの補題
commAnd : (a, b : Bool) -> a && b = b && a
commAnd False False = Refl
commAnd False True  = Refl
commAnd True  False = Refl
commAnd True  True  = Refl

sortedFalse : (xs : List Nat) -> (y : Nat)
  -> sorted xs = False -> sorted (y::xs) = False
sortedFalse []               y p = p
sortedFalse (x1 :: [])       y p = absurd p
sortedFalse (x1 :: x2 :: xs) y p =
  rewrite p in
  rewrite commAnd (lte y x1) False in Refl

-- lteの補題
lteTrans : (x, y, z : Nat)
  -> lte x y = True -> lte y z = True -> lte x z = True
lteTrans Z     _     _     _  _  = Refl
lteTrans (S x) Z     z     p1 p2 = absurd p1
lteTrans (S x) (S y) Z     p1 p2 = p2
lteTrans (S x) (S y) (S z) p1 p2 = lteTrans x y z p1 p2

lteComm : (x, y : Nat)
  -> lte x y = False -> lte y x = True
lteComm Z     _     p = absurd p
lteComm (S x) Z     _ = Refl
lteComm (S x) (S y) p = lteComm x y p


-- fusionの十分条件2つ目
fusionCond2 : sorted [] = True
fusionCond2 = Refl

-- fusionの十分条件3つ目
fusionCond3 : (x : Nat) -> (ys : List Nat) -> sorted (insert x ys) = h x (sorted ys)
fusionCond3 x [] = Refl
fusionCond3 x (y :: ys) with (lte x y) proof p
  fusionCond3 x (y :: ys) | False with (sorted ys) proof p2
    fusionCond3 x (y :: ys) | False | False =
      let l1 = trans (fusionCond3 x ys) (sym p2) in
      rewrite sortedFalse ys y (sym p2) in
      rewrite sortedFalse (insert x ys) y l1 in Refl
    fusionCond3 x (y :: ys) | False | True with (sorted (insert x ys)) proof p3
      fusionCond3 x (y :: ys) | False | True | False =
        let l1 = trans p2 $ sym (trans p3 (fusionCond3 x ys)) in absurd l1
      fusionCond3 x (y :: []) | False | True | True = rewrite lteComm x y (sym p) in Refl
      fusionCond3 x (y :: y2 :: ys) | False | True | True with (lte x y2) proof p4
        fusionCond3 x (y :: y2 :: ys) | False | True | True | False with (lte y y2) proof p5
          fusionCond3 x (y :: y2 :: ys) | False | True | True | False | False = Refl
          fusionCond3 x (y :: y2 :: ys) | False | True | True | False | True =
            rewrite sym p2 in rewrite sym p3 in Refl
        fusionCond3 x (y :: y2 :: ys) | False | True | True | True =
          rewrite sym p2 in
          let l1 = lteComm x y (sym p) in rewrite l1 in
          let l2 = sym p4 in rewrite l2 in
          rewrite lteTrans y x y2 l1 l2 in Refl
  fusionCond3 x (y :: ys) | True = rewrite (sym p) in Refl

-- foldrのfusion則（決め打ち）
postulate fusionFoldr : (zs : List Nat)
  -> sorted [] = True
    -> ((x : Nat) -> (ys : List Nat) -> sorted (insert x ys) = h x (sorted ys))
      -> sorted (foldr insert [] zs) = foldr h True zs

foldrProof : (xs : List Nat) -> foldr Isort.h True xs = True
foldrProof [] = Refl
foldrProof (x :: xs) =
  ( foldr h True (x::xs) )    ={ Refl }=
  ( h x (foldr h True xs) )   ={ foldrProof xs }=
  ( h x True )                ={ Refl }=
  True                        QED

-- 結論
isortIsSorted : (zs : List Nat) -> sorted (isort zs) = True
isortIsSorted zs =
  ( sorted (foldr insert [] zs) )   ={ fusionFoldr zs fusionCond2 fusionCond3 }=
  ( foldr h True zs )               ={ foldrProof zs }=
  True                              QED