module Fin where import Nat import Bool open Nat hiding (_==_; _<_) open Bool data FZero : Set where data FSuc (A : Set) : Set where fz : FSuc A fs : A -> FSuc A mutual Fin' : Nat -> Set Fin' zero = FZero Fin' (suc n) = FSuc (Fin n) data Fin (n : Nat) : Set where fin : Fin' n -> Fin n fzero : {n : Nat} -> Fin (suc n) fzero = fin fz fsuc : {n : Nat} -> Fin n -> Fin (suc n) fsuc n = fin (fs n) _==_ : {n : Nat} -> Fin n -> Fin n -> Bool _==_ {zero} (fin ()) (fin ()) _==_ {suc n} (fin fz) (fin fz) = true _==_ {suc n} (fin (fs i)) (fin (fs j)) = i == j _==_ {suc n} (fin fz) (fin (fs j)) = false _==_ {suc n} (fin (fs i)) (fin fz) = false subst : {n : Nat}{i j : Fin n} -> (P : Fin n -> Set) -> IsTrue (i == j) -> P i -> P j subst {zero} {fin ()} {fin ()} P _ _ subst {suc n} {fin fz} {fin fz} P eq pi = pi subst {suc n} {fin (fs i)} {fin (fs j)} P eq pi = subst (\z -> P (fsuc z)) eq pi subst {suc n} {fin fz} {fin (fs j)} P () _ subst {suc n} {fin (fs i)} {fin fz} P () _ _<_ : {n : Nat} -> Fin n -> Fin n -> Bool _<_ {zero} (fin ()) (fin ()) _<_ {suc n} _ (fin fz) = false _<_ {suc n} (fin fz) (fin (fs j)) = true _<_ {suc n} (fin (fs i)) (fin (fs 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 {zero} (fin ()) liftSuc {suc n} (fin fz) = fin fz liftSuc {suc n} (fin (fs 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)