module Core.Thinning

import Data.Fin

-- Definition ------------------------------------------------------------------

data Thinner : Nat -> Nat -> Type where
  IsBase : Thinner n (S n)
  IsDrop : Thinner m n -> Thinner m (S n)
  IsKeep : Thinner m n -> Thinner (S m) (S n)

export
data Thins : Nat -> Nat -> Type where
  IsId : n `Thins` n
  IsThinner : Thinner m n -> m `Thins` n

%name Thinner thin
%name Thins thin

-- Constructors ----------------------------------------------------------------

export
id : (0 n : Nat) -> n `Thins` n
id n = IsId

export
drop : m `Thins` n -> m `Thins` S n
drop IsId = IsThinner IsBase
drop (IsThinner thin) = IsThinner (IsDrop thin)

export
keep : m `Thins` n -> S m `Thins` S n
keep IsId = IsId
keep (IsThinner thin) = IsThinner (IsKeep thin)

public export
wkn1 : (0 n : Nat) -> n `Thins` S n
wkn1 n = drop (id n)

-- Properties

export
keepIdIsId : (0 n : Nat) -> keep (id n) = id (S n)
keepIdIsId n = Refl

-- Non-Identity ----------------------------------------------------------------

export
data IsNotId : m `Thins` n -> Type where
  ItIsThinner : IsNotId (IsThinner thin)

%name IsNotId prf

-- Views -----------------------------------------------------------------------

public export
data View : m `Thins` n -> Type where
  Id : (0 n : Nat) -> View (id n)
  Drop : (thin : m `Thins` n) -> View (drop thin)
  Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)

%name Thinning.View view

export
view : (thin : m `Thins` n) -> View thin
view IsId = Id m
view (IsThinner IsBase) = Drop (id _)
view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)

-- Eliminators

export
viewId :
  (0 n : Nat) ->
  (0 p : View (id n) -> Type) ->
  p (Id n) ->
  p (view $ id n)
viewId n p x = x

export
viewDrop :
  (thin : m `Thins` n) ->
  (0 p : View (drop thin) -> Type) ->
  p (Drop thin) ->
  p (view $ drop thin)
viewDrop IsId p x = x
viewDrop (IsThinner thin) p x = x

export
viewKeep :
  forall m, n.
  (thin : m `Thins` n) ->
  (0 p : View (keep thin) -> Type) ->
  ((eq1 : m = n) ->
   (eq2 : thin = (rewrite eq1 in id n)) ->
   p (rewrite eq2 in rewrite eq1 in Id (S n))) ->
  ({auto 0 prf : IsNotId thin} -> p (Keep thin)) ->
  p (view $ keep thin)
viewKeep IsId p id keep = id Refl Refl
viewKeep (IsThinner thin) p id keep = keep

-- Composition -----------------------------------------------------------------

comp : Thinner m n -> Thinner k m -> Thinner k n
comp IsBase thin2 = IsDrop thin2
comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) IsBase = IsDrop thin1
comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)

export
(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
IsId . thin2 = thin2
IsThinner thin1 . IsId = IsThinner thin1
IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)

-- Categorical

comp'Assoc :
  (thin3 : Thinner m n) ->
  (thin2 : Thinner k m) ->
  (thin1 : Thinner j k) ->
  comp thin3 (comp thin2 thin1) = comp (comp thin3 thin2) thin1
comp'Assoc IsBase thin2 thin1 = Refl
comp'Assoc (IsDrop thin3) thin2 thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) IsBase thin1 = Refl
comp'Assoc (IsKeep thin3) (IsDrop thin2) thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) (IsKeep thin2) IsBase = Refl
comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsDrop thin1) = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsKeep thin1) = cong IsKeep (comp'Assoc thin3 thin2 thin1)

export
compAssoc :
  (thin3 : m `Thins` n) ->
  (thin2 : k `Thins` m) ->
  (thin1 : j `Thins` k) ->
  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
compAssoc IsId thin2 thin1 = Refl
compAssoc (IsThinner thin3) IsId thin1 = Refl
compAssoc (IsThinner thin3) (IsThinner thin2) IsId = Refl
compAssoc (IsThinner thin3) (IsThinner thin2) (IsThinner thin1) =
  cong IsThinner (comp'Assoc thin3 thin2 thin1)

export
compLeftId : (thin : m `Thins` n) -> id n . thin = thin
compLeftId thin = Refl

export
compRightId : (thin : m `Thins` n) -> thin . id m = thin
compRightId IsId = Refl
compRightId (IsThinner thin) = Refl

-- Specific Cases

export
compLeftDrop :
  (thin2 : m `Thins` n) ->
  (thin1 : k `Thins` m) ->
  drop thin2 . thin1 = drop (thin2 . thin1)
compLeftDrop IsId IsId = Refl
compLeftDrop IsId (IsThinner thin1) = Refl
compLeftDrop (IsThinner thin2) IsId = Refl
compLeftDrop (IsThinner thin2) (IsThinner thin1) = Refl

export
compRightDrop :
  (thin2 : m `Thins` n) ->
  (thin1 : k `Thins` m) ->
  keep thin2 . drop thin1 = drop (thin2 . thin1)
compRightDrop IsId thin1 = Refl
compRightDrop (IsThinner thin2) IsId = Refl
compRightDrop (IsThinner thin2) (IsThinner thin1) = Refl

export
compKeep :
  (thin1 : m `Thins` n) ->
  (thin2 : k `Thins` m) ->
  keep thin1 . keep thin2 = keep (thin1 . thin2)
compKeep IsId thin2 = Refl
compKeep (IsThinner thin1) IsId = Refl
compKeep (IsThinner thin1) (IsThinner thin2) = Refl

export
compLeftWkn1 : (thin : m `Thins` n) -> wkn1 n . thin = drop thin
compLeftWkn1 thin = trans (compLeftDrop (id n) thin) (cong drop $ compLeftId thin)

export
compRightWkn1 : (thin : m `Thins` n) -> keep thin . wkn1 m = drop thin
compRightWkn1 thin = trans (compRightDrop thin (id m)) (cong drop $ compRightId thin)

export
wkn1Comm : (thin : m `Thins` n) -> keep thin . wkn1 m = wkn1 n . thin
wkn1Comm thin = trans (compRightWkn1 thin) (sym $ compLeftWkn1 thin)

-- Weakening -------------------------------------------------------------------

wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)

export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin

-- Categorical

export
wknId : (i : Fin n) -> wkn i (id n) = i
wknId i = Refl

wkn'Homo :
  (i : Fin k) ->
  (thin2 : Thinner m n) ->
  (thin1 : Thinner k m) ->
  wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
wkn'Homo i IsBase thin1 = Refl
wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo i (IsKeep thin2) IsBase = Refl
wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)

export
wknHomo :
  (i : Fin k) ->
  (thin1 : k `Thins` m) ->
  (thin2 : m `Thins` n) ->
  wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
wknHomo i (IsThinner thin1) IsId = Refl
wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1

-- Specific Cases

export
wknDrop : (i : Fin m) -> (thin : m `Thins` n) -> wkn i (drop thin) = FS (wkn i thin)
wknDrop i IsId = Refl
wknDrop i (IsThinner thin) = Refl

export
wknKeepFZ : (thin : m `Thins` n) -> wkn 0 (keep thin) = 0
wknKeepFZ IsId = Refl
wknKeepFZ (IsThinner thin) = Refl

export
wknKeepFS : (i : Fin m) -> (thin : m `Thins` n) -> wkn (FS i) (keep thin) = FS (wkn i thin)
wknKeepFS i IsId = Refl
wknKeepFS i (IsThinner thin) = Refl