PROOF-SortSpec-sortPreservesLength.agda 1.18 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1 2 3 4
-- Agda program using the Iowa Agda library

open import bool

5
module PROOF-SortSpec-sortPreservesLength
Michael Hanus 's avatar
Michael Hanus committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

insert : ℕ → 𝕃 ℕ → 𝕃 ℕ
insert x [] = x :: []
insert y (z :: u) = if y ≤ z then y :: (z :: u) else z :: (insert y u)

sort : 𝕃 ℕ → 𝕃 ℕ
sort [] = []
sort (x :: y) = insert x (sort y)

---------------------------------------------------------------------------

insertIncLength : (x : ℕ) → (xs : 𝕃 ℕ)
                → length (insert x xs) ≡ suc (length xs)
insertIncLength x [] = refl
insertIncLength x (y :: ys) with (x ≤ y)
... | tt = refl
... | ff rewrite insertIncLength x ys = refl

sortPreservesLength : (xs : 𝕃 ℕ) → length (sort xs) ≡ length xs
sortPreservesLength [] = refl
sortPreservesLength (x :: xs)
 rewrite insertIncLength x (sort xs) | sortPreservesLength xs = refl

---------------------------------------------------------------------------