module Data.Fin.Occurs

import Data.DPair
import Data.Fin
import Data.Maybe
import Data.Nat

import Syntax.PreorderReasoning

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

export
thin : Fin (S n) -> Fin n -> Fin (S 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 (S n)) -> {y, z : Fin 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 (S n)) -> (y : Fin n) -> Not (thin x y = x)
thinSkips FZ y prf = absurd prf
thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)

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

export
thick : {n : Nat} -> Fin (S n) -> Fin (S n) -> Maybe (Fin n)
thick FZ FZ = Nothing
thick FZ (FS y) = Just y
thick {n = S n} (FS x) FZ = Just FZ
thick {n = S n} (FS x) (FS y) = FS <$> thick x y

public export
data ThickProof : Fin (S n) -> Fin (S n) -> Maybe (Fin n) -> Type where
  Equal : res = Nothing -> ThickProof x x res
  Thinned : (y : Fin n) -> res = Just y -> ThickProof x (thin x y) res

%name ThickProof prf

export
thickProof : {n : Nat} -> (x, y : Fin (S n)) -> ThickProof x y (thick x y)
thickProof FZ FZ = Equal Refl
thickProof FZ (FS y) = Thinned y Refl
thickProof {n = S n} (FS x) FZ = Thinned FZ Refl
thickProof {n = S n} (FS x) (FS y) with (thickProof x y)
  thickProof (FS x) (FS x) | Equal prf = Equal (cong (map FS) prf)
  thickProof (FS x) (FS _) | Thinned y prf = Thinned (FS y) (cong (map FS) prf)

thickRefl' :
  (x, y : Fin (S n)) ->
  (0 _ : x = y) ->
  ThickProof x y (thick x y) ->
  thick x y = Nothing
thickRefl' x x _ (Equal prf) = prf
thickRefl' x (thin x z) prf (Thinned z _) = absurd $ thinSkips x z (sym prf)

export
thickRefl : {n : Nat} -> (x : Fin (S n)) -> thick x x = Nothing
thickRefl x = thickRefl' x x Refl (thickProof x x)

export
thickThin : {n : Nat} -> (x : Fin (S n)) -> (y : Fin n) -> thick x (thin x y) = Just y
thickThin x y with (thin x y) proof prf
  _ | z with (thickProof x z)
    thickThin x y | x | Equal prf' = absurd $ thinSkips x y prf
    thickThin x y | _ | Thinned z prf' = Calc $
      |~ thick x (thin x z)
      ~~ Just z             ...(prf')
      ~~ Just y             ..<(cong Just $ thinInjective x prf)