Fin.agda

module Data.Fin where

open import Data.Nat hiding (_==_; _<_)
open import Data.Bool
open import Logic.Identity
open import Logic.Base

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

pred : {n : Nat} -> Fin (suc (suc n)) -> Fin (suc n)
pred fzero    = fzero
pred (fsuc i) = i

fzero≠fsuc : {n : Nat}{i : Fin n} -> fzero ≢ fsuc i
fzero≠fsuc ()

fsuc-inj : {n : Nat}{i j : Fin n} -> fsuc i ≡ fsuc j -> i ≡ j
fsuc-inj refl = refl

_==_ : {n : Nat}(i j : Fin n) -> (i ≡ j) \/ (i ≢ j)
fzero  == fzero  = \/-IL refl
fzero  == fsuc j = \/-IR fzero≠fsuc
fsuc i == fzero  = \/-IR (sym≢ fzero≠fsuc)
fsuc i == fsuc j = aux i j (i == j)
  where
    aux : {n : Nat}(i j : Fin n) -> (i ≡ j) \/ (i ≢ j) -> (fsuc i ≡ fsuc j) \/ (fsuc i ≢ fsuc j)
    aux i .i (\/-IL refl) = \/-IL refl
    aux i j  (\/-IR i≠j)  = \/-IR \si=sj -> i≠j (fsuc-inj si=sj)

_<_ : {n : Nat} -> Fin n -> Fin n -> Bool
_      < fzero  = false
fzero  < fsuc j = true
fsuc i < fsuc j = i < j

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

liftSuc : {n : Nat} -> Fin n -> Fin (suc n)
liftSuc  fzero   = fzero
liftSuc (fsuc i) = fsuc (liftSuc i)

lift+ : {n : Nat}(m : Nat) -> Fin n -> Fin (m + n)
lift+  zero   i = i
lift+ (suc m) i = liftSuc (lift+ m i)

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

-- Two elements of Fin n are either the same or one is the thinning of
-- something with respect to the other.
data ThinView : {n : Nat}(i j : Fin n) -> Set where
  same : {n : Nat}{i : Fin n}                  -> ThinView i i
  diff : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> ThinView i (thin i j)

thinView : {n : Nat}(i j : Fin n) -> ThinView i j
thinView {suc _}       fzero     fzero    = same
thinView {suc _}       fzero     (fsuc j) = diff j
thinView {suc zero}    (fsuc ()) fzero
thinView {suc (suc _)} (fsuc i)  fzero    = diff fzero
thinView               (fsuc i)  (fsuc j) = aux i j (thinView i j)
  where
    aux : {n : Nat}(i j : Fin n) -> ThinView i j -> ThinView (fsuc i) (fsuc j)
    aux i .i           same    = same
    aux i .(thin i j) (diff j) = diff (fsuc j)

thin-ij≠i : {n : Nat}(i : Fin (suc n))(j : Fin n) -> thin i j ≢ i
thin-ij≠i  fzero    j     ()
thin-ij≠i (fsuc i)  fzero   ()
thin-ij≠i (fsuc i) (fsuc j) eq = thin-ij≠i i j (fsuc-inj eq)

-- Thickening.
--    thin i (thick i j) ≡ j  ?
--    thick i (thin i j) ≡ j
thick : {n : Nat}(i j : Fin (suc n)) -> i ≢ j -> Fin n
thick i j i≠j = thick' i j i≠j (thinView i j) where
  thick' : {n : Nat}(i j : Fin (suc n)) -> i ≢ j -> ThinView i j -> Fin n
  thick' i .i          i≠i same          = elim-False (i≠i refl)
  thick' i .(thin i j) _  (diff j) = j

-- thin∘thick=id : {n : Nat}(i j : Fin (suc n))(p : i ≢ j) ->
--              thin i (thick i j p) ≡ j
-- thin∘thick=id i j p = ?
--
-- thick∘thin=id : {n : Nat}(i : Fin (suc n))(j : Fin n) ->
--              thick i (thin i j) (sym≢ (thin-ij≠i i j)) ≡ j
-- thick∘thin=id i j = ?
--