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 = ? --