module FunOrn.Example where
open import Function
open import Relation.Binary.PropositionalEquality
-- Nat to List, and its reornament Vec
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
data List (A : Set) : Set where
nil : List A
cons : (a : A)(xs : List A) → List A
forgetList : ∀{A} → List A → ℕ
forgetList nil = zero
forgetList (cons a xs) = suc (forgetList xs)
data Vec (A : Set) : ℕ → Set where
nil : Vec A zero
cons : ∀{n} → (a : A)(xs : Vec A n) → Vec A (suc n)
makeVec : ∀{A} → (xs : List A) → Vec A (forgetList xs)
makeVec nil = nil
makeVec (cons a xs) = cons a (makeVec xs)
-- Bool to Maybe, and its reornament IMaybe
data Bool : Set where
true false : Bool
data Maybe (A : Set) : Set where
just : (a : A) → Maybe A
nothing : Maybe A
forgetMaybe : ∀{A} → Maybe A → Bool
forgetMaybe nothing = false
forgetMaybe (just a) = true
data IMaybe (A : Set) : Bool → Set where
just : (a : A) → IMaybe A true
nothing : IMaybe A false
forgetIMaybe : ∀{A b} → IMaybe A b → Maybe A
forgetIMaybe {b = false} nothing = nothing
forgetIMaybe {b = true} (just a) = just a
coh-IMaybe : ∀{A b} → (ma : IMaybe A b) → forgetMaybe (forgetIMaybe ma) ≡ b
coh-IMaybe nothing = refl
coh-IMaybe (just a) = refl
-- Less than
_<_ : ℕ → ℕ → Bool
m < zero = false
zero < suc n = true
suc m < suc n = m < n
-- Coq-style implementation and proof of lookup
lookup' : ∀{A} → ℕ → List A → Maybe A
lookup' n nil = nothing
lookup' zero (cons a xs) = just a
lookup' (suc n) (cons a xs) = lookup' n xs
coh-lookup' : ∀{A} → (m : ℕ)(xs : List A) →
forgetMaybe (lookup' m xs) ≡ m < (forgetList xs)
coh-lookup' m nil = refl
coh-lookup' zero (cons a xs) = refl
coh-lookup' (suc m) (cons a xs) = coh-lookup' m xs
-- Correct-by-construction lookup
ilookup : ∀{A} → (m : ℕ) →
{n : ℕ} → Vec A n →
IMaybe A (m < n)
ilookup m nil = nothing
ilookup zero (cons a ys) = just a
ilookup (suc m) (cons a ys) = ilookup m ys
lookup : ∀{A} → ℕ → List A → Maybe A
lookup n xs = forgetIMaybe (ilookup n (makeVec xs))
coh-lookup : ∀{A} → (m : ℕ)(xs : List A) →
forgetMaybe (lookup m xs) ≡ m < (forgetList xs)
coh-lookup m = coh-IMaybe ∘ (ilookup m) ∘ makeVec