Fin.agda

module Lib.Fin where

open import Lib.Nat
open import Lib.Bool
open import Lib.Id

data Fin : Nat -> Set where
  zero : {n : Nat} -> Fin (suc n)
  suc  : {n : Nat} -> Fin n -> Fin (suc n)

fromNat : (n : Nat) -> Fin (suc n)
fromNat zero    = zero
fromNat (suc n) = suc (fromNat n)

toNat : {n : Nat} -> Fin n -> Nat
toNat zero    = zero
toNat (suc n) = suc (toNat n)

weaken : {n : Nat} -> Fin n -> Fin (suc n)
weaken zero    = zero
weaken (suc n) = suc (weaken n)

lem-toNat-weaken : forall {n} (i : Fin n) -> toNat i ≡ toNat (weaken i)
lem-toNat-weaken zero    = refl
lem-toNat-weaken (suc i) with toNat i | lem-toNat-weaken i
... | .(toNat (weaken i)) | refl = refl

lem-toNat-fromNat : (n : Nat) -> toNat (fromNat n) ≡ n
lem-toNat-fromNat zero = refl
lem-toNat-fromNat (suc n) with toNat (fromNat n) | lem-toNat-fromNat n
... | .n | refl = refl

finEq : {n : Nat} -> Fin n -> Fin n -> Bool
finEq  zero    zero   = true
finEq  zero   (suc _) = false
finEq (suc _)  zero   = false
finEq (suc i) (suc j) = finEq i j

-- A view telling you if a given element is the maximal one.
data MaxView {n : Nat} : Fin (suc n) -> Set where
  theMax : MaxView (fromNat n)
  notMax : (i : Fin n) -> MaxView (weaken i)

maxView : {n : Nat}(i : Fin (suc n)) -> MaxView i
maxView {zero} zero = theMax
maxView {zero} (suc ())
maxView {suc n} zero = notMax zero
maxView {suc n} (suc i) with maxView i
maxView {suc n} (suc .(fromNat n)) | theMax   = theMax
maxView {suc n} (suc .(weaken i))  | notMax i = notMax (suc i)

-- The non zero view

data NonEmptyView : {n : Nat} -> Fin n -> Set where
  ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i

nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
nonEmpty zero    = ne
nonEmpty (suc _) = ne

-- The thinning view

thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
thin zero    j       = suc j
thin (suc i) zero    = zero
thin (suc i) (suc j) = suc (thin i j)

data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
  equal    : {n : Nat}{i : Fin n} -> EqView i i
  notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)

compare : {n : Nat}(i j : Fin n) -> EqView i j
compare zero    zero    = equal
compare zero    (suc j) = notequal j
compare (suc i) zero    with nonEmpty i
...                | ne = notequal zero
compare (suc i) (suc j) with compare i j
compare (suc i) (suc .i)          | equal      = equal
compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)