module Data.Fin.Occurs

import Data.DPair
import Data.Fin.Strong
import Data.Maybe
import Data.Maybe.Properties
import Data.Nat

import Syntax.PreorderReasoning

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

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

-- Properties

export
thinInjective : (x : SFin n) -> {y, z : SFin (pred n)} -> thin x y = thin x z -> y = z
thinInjective FZ prf = injective {f = FS'} 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 : SFin n) -> (y : SFin (pred n)) -> Not (thin x y = x)
thinSkips FZ y prf = sucNonZero y prf
thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)

thinSuc : {n : Nat} -> (x : SFin (S n)) -> (y : SFin n) -> thin (FS x) (FS' y) = FS (thin x y)
thinSuc {n = S n} x y = rewrite sucIsFS y in Refl

export
thinInverse : (x, y : SFin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
thinInverse FZ FZ neq = void (neq Refl)
thinInverse FZ (FS y) neq = (y ** sucIsFS y)
thinInverse (FS x) FZ neq = (FZ ** Refl)
thinInverse (FS x) (FS y) neq =
  let (z ** prf) = thinInverse x y (\prf => neq $ cong FS prf) in
  (FS' z ** trans (thinSuc x z) (cong FS $ prf))

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

export
thick : SFin n -> SFin n -> Maybe (SFin (pred n))
thick FZ FZ = Nothing
thick FZ (FS y) = Just y
thick (FS x) FZ = Just FZ
thick (FS x) (FS y) = FS' <$> thick x y

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

export
thickNeq : (x, y : SFin 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 FS' (thickNeq x y (\prf => neq $ cong FS prf))

export
thickNothing : (x, y : SFin n) -> (0 _ : IsNothing (thick x y)) -> x = y
thickNothing FZ FZ prf = Refl
thickNothing (FS x) (FS y) prf =
  cong FS (thickNothing x y (mapNothingInverse FS' (thick x y) prf))

export thickJust : (x : SFin n) -> (y : SFin n) -> (0 _ : thick x y = Just z) -> thin x z = y
thickJust FZ (FS y) Refl = sucIsFS y
thickJust (FS x) FZ Refl = Refl
thickJust (FS x) (FS y) prf =
  let invertJust = mapJustInverse FS' (thick x y) prf in
  Calc $
    |~ thin (FS x) z
    ~~ thin (FS x) (FS' invertJust.fst) ...(cong (thin (FS x)) $ snd invertJust.snd)
    ~~ FS (thin x invertJust.fst)       ...(thinSuc x invertJust.fst)
    ~~ FS y                             ...(cong FS $ thickJust x y (fst invertJust.snd))

export
thickThin : (x : SFin n) -> (y : SFin (pred n)) -> thick x (thin x y) = Just y
thickThin x y =
  let
    fromJust =
      extractIsJust $
      thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf)
  in
  Calc $
    |~ thick x (thin x y)
    ~~ Just fromJust.fst  ...(fromJust.snd)
    ~~ Just y             ...(cong Just $ thinInjective x $ thickJust x (thin x y) fromJust.snd)