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