module Data.Fin.Occurs

import Data.DPair
import Data.Fin
import Data.Maybe.Properties

-- Utilities -------------------------------------------------------------------

predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
predInjective {n = S n} prf = cong S prf

public export
indexIsSuc : Fin n -> Exists (\k => n = S k)
indexIsSuc FZ = Evidence _ Refl
indexIsSuc (FS x) = Evidence _ Refl

%inline %tcinline
zero : (0 _ : Fin n) -> Fin n
zero x = rewrite snd (indexIsSuc x) in FZ

%inline %tcinline
suc : (_ : Fin (pred n)) -> Fin n
suc x =
  replace {p = Fin}
    (sym $ predInjective $ snd $ indexIsSuc x)
    (FS $ rewrite sym $ snd $ indexIsSuc x in x)

-- Thinning --------------------------------------------------------------------

export
thin : Fin n -> Fin (pred n) -> Fin n
thin FZ y = FS y
thin (FS x) FZ = FZ
thin (FS x) (FS y) = FS (thin x y)

-- Properties

export
thinInjective : (x : Fin n) -> {y, z : Fin (pred n)} -> thin x y = thin x z -> y = z
thinInjective FZ prf = injective prf
thinInjective (FS x) {y = FZ, z = FZ} prf = Refl
thinInjective (FS x) {y = FS y, z = FS z} prf = cong FS $ thinInjective x $ injective prf

export
thinSkips : (x : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x)
thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)

%inline
thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
thinSucZero x = rewrite snd (indexIsSuc x) in Refl

%inline
thinSucSuc : (x : Fin n) -> (z : Fin (pred n)) -> thin (FS x) (suc z) = FS (thin x z)
thinSucSuc FZ FZ = Refl
thinSucSuc FZ (FS z) = Refl
thinSucSuc (FS x) FZ = Refl
thinSucSuc (FS x) (FS z) = Refl

export
thinInverse : (x, y : Fin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
thinInverse FZ FZ neq = void (neq Refl)
thinInverse FZ (FS y) neq = (y ** Refl)
thinInverse (FS x) FZ neq = (zero x ** thinSucZero x)
thinInverse (FS x) (FS y) neq =
  let (z ** prf) = thinInverse x y (neq . cong FS) in
  (suc z ** trans (thinSucSuc x z) (cong FS prf))

-- Thickening ------------------------------------------------------------------

export
thick : Fin n -> Fin n -> Maybe (Fin (pred n))
thick FZ FZ = Nothing
thick FZ (FS y) = Just y
thick (FS x) FZ = Just (zero x)
thick (FS x) (FS y) = suc <$> thick x y

export
thickRefl : (x : Fin n) -> IsNothing (thick x x)
thickRefl FZ = ItIsNothing
thickRefl (FS x) = mapNothing suc (thickRefl x)

export
thickNeq : (x, y : Fin n) -> (0 _ : Not (x = y)) -> IsJust (thick x y)
thickNeq FZ FZ neq = void (neq Refl)
thickNeq FZ (FS y) neq = ItIsJust
thickNeq (FS x) FZ neq = ItIsJust
thickNeq (FS x) (FS y) neq = mapIsJust suc (thickNeq x y (neq . cong FS))

export
thickNothing : (x, y : Fin n) -> (0 _ : IsNothing (thick x y)) -> x = y
thickNothing FZ FZ prf = Refl
thickNothing (FS x) (FS y) prf =
  rewrite thickNothing x y (mapNothingInverse suc (thick x y) prf) in
  Refl

export
thickJust : (x, y : Fin n) -> (0 _ : thick x y = Just z) -> thin x z = y
thickJust FZ (FS y) Refl = Refl
thickJust (FS x) FZ Refl = thinSucZero x
thickJust (FS x) (FS y) prf =
  let 0 z = mapJustInverse suc (thick x y) prf in
  rewrite snd $ z.snd in
  trans (thinSucSuc x z.fst) (cong FS $ thickJust x y (fst $ z.snd))

export
thickThin : (x : Fin n) -> (y : Fin (pred n)) -> thick x (thin x y) = Just y
thickThin x y =
  let neq = thinSkips x y in
  let isJust = thickNeq x (thin x y) (\prf => neq $ sym prf) in
  let zPrf = extractIsJust isJust in
  let z = zPrf.fst in
  let 0 prf1 = zPrf.snd in
  let 0 prf2 = thickJust x (thin x y) prf1 in
  trans prf1 (cong Just $ thinInjective x prf2)