NamelessLambda.idr

module NamelessLambda

%default total
%access public export

data Term: Type where
  Var    : Nat -> Term
  Lambda : Term -> Term
  Apply  : Term -> Term -> Term

Eq Term where
  (Var m)       == (Var n)         = m == n
  (Lambda t1)   == (Lambda t1')    = t1 == t1'
  (Apply t1 t2) == (Apply t1' t2') = t1 == t1' && t2 == t2'
  _             == _               = False

doShiftUp : Nat -> Nat -> Term -> Term
doShiftUp n cutoff (Var m)       = if m < cutoff then Var m else Var (m + n)
doShiftUp n cutoff (Lambda t1)   = Lambda $ doShiftUp n (S cutoff) t1
doShiftUp n cutoff (Apply t1 t2) = Apply (doShiftUp n cutoff t1) (doShiftUp n cutoff t2)

shiftUp : Nat -> Term -> Term
shiftUp n t = doShiftUp n Z t

doShiftDown : Nat -> Nat -> Term -> Term
doShiftDown n cutoff (Var m)       = if m < cutoff then Var m else Var (minus m n)
doShiftDown n cutoff (Lambda t1)   = Lambda $ doShiftDown n (S cutoff) t1
doShiftDown n cutoff (Apply t1 t2) = Apply (doShiftDown n cutoff t1) (doShiftDown n cutoff t2)

shiftDown : Nat -> Term -> Term
shiftDown n t = doShiftDown n Z t

substitute : Nat -> Term -> Term -> Term
substitute k s (Var m)       = if k == m then s else Var m
substitute k s (Lambda t1)   = Lambda $ substitute (S k) (shiftUp 1 s) t1
substitute k s (Apply t1 t2) = Apply (substitute k s t1) (substitute k s t2)

rank : Term -> Nat
rank (Var m)       = S m
rank (Lambda t1)   = pred $ rank t1
rank (Apply t1 t2) = maximum (rank t1) (rank t2)

eval1 : Term -> Term
eval1 (Var m)                = Var m
eval1 (Lambda t1)            = Lambda t1
eval1 (Apply (Var m) t2)     = Apply (Var m) (eval1 t2)
eval1 (Apply (Lambda t1) t2) = shiftDown 1 $ substitute 0 (shiftUp 1 t2) t1
eval1 (Apply t1 t2)          = Apply (eval1 t1) t2

partial eval : Term -> Term
eval t = case eval1 t of
  (Apply (Lambda t1) t2) => eval $ substitute 0 t2 t1
  t'                     => t'

-- Properties

Closed : Term -> Type
Closed t = (rank t = Z)

varIsNotClosed : (n : Nat) -> Not $ Closed (Var n)
varIsNotClosed n = absurd

doShiftUpZeroNeutral : (t : Term) -> (cutoff : Nat) -> doShiftUp Z cutoff t = t
doShiftUpZeroNeutral (Lambda t1)   cutoff = rewrite doShiftUpZeroNeutral t1 (S cutoff) in Refl
doShiftUpZeroNeutral (Apply t1 t2) cutoff = rewrite doShiftUpZeroNeutral t1 cutoff in rewrite doShiftUpZeroNeutral t2 cutoff in Refl
doShiftUpZeroNeutral (Var m)       cutoff with (m < cutoff)
  doShiftUpZeroNeutral (Var m) cutoff | True  = Refl
  doShiftUpZeroNeutral (Var m) cutoff | False = rewrite plusZeroRightNeutral m in Refl

shiftUpZeroNeutral : (t : Term) -> shiftUp Z t = t
shiftUpZeroNeutral t = doShiftUpZeroNeutral t Z

Uninhabited (EQ = LT) where
  uninhabited Refl impossible
Uninhabited (EQ = GT) where
  uninhabited Refl impossible
Uninhabited (LT = EQ) where
  uninhabited Refl impossible
Uninhabited (Prelude.Interfaces.LT = GT) where
  uninhabited Refl impossible
Uninhabited (GT = EQ) where
  uninhabited Refl impossible
Uninhabited (Prelude.Interfaces.GT = LT) where
  uninhabited Refl impossible

compareRecoversLT : (m, n : Nat) -> compare m n = LT -> LT m n
compareRecoversLT Z     Z     eq = absurd $ uninhabited eq
compareRecoversLT Z     (S n) eq = LTESucc LTEZero
compareRecoversLT (S m) Z     eq = absurd $ uninhabited eq
compareRecoversLT (S m) (S n) eq = LTESucc $ compareRecoversLT m n eq

compareRecoversEQ : (m, n : Nat) -> compare m n = EQ -> m = n
compareRecoversEQ Z     Z     eq = Refl
compareRecoversEQ Z     (S n) eq = absurd $ uninhabited eq
compareRecoversEQ (S m) Z     eq = absurd $ uninhabited eq
compareRecoversEQ (S m) (S n) eq = rewrite compareRecoversEQ m n eq in Refl

compareRecoversGT : (m, n : Nat) -> compare m n = GT -> GT m n
compareRecoversGT Z     Z     eq = absurd $ uninhabited eq
compareRecoversGT Z     (S n) eq = absurd $ uninhabited eq
compareRecoversGT (S m) Z     eq = LTESucc LTEZero
compareRecoversGT (S m) (S n) eq = LTESucc $ compareRecoversGT m n eq

succNotLTE : (n : Nat) -> Not $ LTE (S n) n
succNotLTE Z     lte = succNotLTEzero lte
succNotLTE (S n) lte = succNotLTE n (fromLteSucc lte)

lteSuccPred : (n : Nat) -> LTE n (S (pred n))
lteSuccPred Z     = LTEZero
lteSuccPred (S n) = lteRefl

lteMaxLeft : (m, n : Nat) -> LTE m (maximum m n)
lteMaxLeft Z     n     = LTEZero
lteMaxLeft (S m) Z     = lteRefl
lteMaxLeft (S m) (S n) = LTESucc (lteMaxLeft m n)

lteMaxRight : (m, n : Nat) -> LTE n (maximum m n)
lteMaxRight m n = rewrite maximumCommutative m n in lteMaxLeft n m

shiftUpWithCutoffGTERankNeutral : (t : Term) -> (cutoff : Nat) -> GTE cutoff (rank t) -> (n : Nat) -> doShiftUp n cutoff t = t
shiftUpWithCutoffGTERankNeutral (Var m)       c p n with (compare m c) proof p'
  shiftUpWithCutoffGTERankNeutral (Var m) c p n | LT = Refl
  shiftUpWithCutoffGTERankNeutral (Var m) c p n | EQ = absurd $ succNotLTE c $ replace {P = \m => LTE (S m) c} (compareRecoversEQ m c (sym p')) p
  shiftUpWithCutoffGTERankNeutral (Var m) c p n | GT = absurd $ succNotLTE m $ lteTransitive (lteSuccRight p) (compareRecoversGT m c (sym p'))
shiftUpWithCutoffGTERankNeutral (Lambda t1)   c p n = rewrite shiftUpWithCutoffGTERankNeutral t1 (S c) (lteTransitive (lteSuccPred (rank t1)) (LTESucc p)) n in Refl
shiftUpWithCutoffGTERankNeutral (Apply t1 t2) c p n =
  let r1 = rank t1 in
  let r2 = rank t2 in
  let r1LTEc = lteTransitive (lteMaxLeft  r1 r2) p in
  let r2LTEc = lteTransitive (lteMaxRight r1 r2) p in
  rewrite shiftUpWithCutoffGTERankNeutral t1 c r1LTEc n in
  rewrite shiftUpWithCutoffGTERankNeutral t2 c r2LTEc n in Refl

shiftUpClosedNeutral : (t : Term) -> Closed t -> (n : Nat) -> shiftUp n t = t
shiftUpClosedNeutral t cl n = shiftUpWithCutoffGTERankNeutral t Z (replace cl lteRefl) n

plusNDistributesOverMaximumRight : (n : Nat) -> (a : Nat) -> (b : Nat) -> n + maximum a b = maximum (a + n) (b + n)
plusNDistributesOverMaximumRight Z     a b = rewrite plusZeroRightNeutral a in rewrite plusZeroRightNeutral b in Refl
plusNDistributesOverMaximumRight (S n) a b =
  rewrite sym $ plusSuccRightSucc a n in
  rewrite sym $ plusSuccRightSucc b n in
  rewrite plusNDistributesOverMaximumRight n a b in Refl

nonZeroPredLT : (n : Nat) -> LT Z (pred n) -> LT (pred n) n
nonZeroPredLT Z     lt = absurd $ succNotLTEzero lt
nonZeroPredLT (S n) lt = lteRefl

plusPredLeftPred : (m, n : Nat) -> LT Z m -> pred (m + n) = pred m + n
plusPredLeftPred Z     n lt = absurd $ succNotLTEzero lt
plusPredLeftPred (S m) n lt = Refl

maximumToEither : (m, n : Nat) -> Either (maximum m n = m) (maximum m n = n)
maximumToEither Z     Z     = Left Refl
maximumToEither Z     (S n) = Right Refl
maximumToEither (S m) Z     = Left Refl
maximumToEither (S m) (S n) = case maximumToEither m n of
  Left  eq => rewrite eq in Left  Refl
  Right eq => rewrite eq in Right Refl

ltOrGte : (m, n : Nat) -> Either (LT m n) (GTE m n)
ltOrGte m n with (compare m n) proof cmp
  ltOrGte m n | LT = Left $ compareRecoversLT m n (sym cmp)
  ltOrGte m n | EQ = rewrite compareRecoversEQ m n (sym cmp) in Right lteRefl
  ltOrGte m n | GT = Right $ lteTransitive (lteSuccRight lteRefl) (compareRecoversGT m n (sym cmp))

maximumOfGte : (m, n : Nat) -> GTE m n -> maximum m n = m
maximumOfGte Z     Z     gte = Refl
maximumOfGte Z     (S n) gte = absurd $ succNotLTEzero gte
maximumOfGte (S m) Z     gte = Refl
maximumOfGte (S m) (S n) gte = rewrite maximumOfGte m n (fromLteSucc gte) in Refl

shiftUpWithCutoffLTRankAddsRank : (t : Term) -> (cutoff : Nat) -> LT cutoff (rank t) -> (n : Nat) -> rank (doShiftUp n cutoff t) = rank t + n
shiftUpWithCutoffLTRankAddsRank (Var m)       c lt n with (compare m c) proof cmp
  shiftUpWithCutoffLTRankAddsRank (Var m) c lt n | LT = absurd $ succNotLTE c $ lteTransitive lt (compareRecoversLT m c (sym cmp))
  shiftUpWithCutoffLTRankAddsRank (Var m) c lt n | EQ = Refl
  shiftUpWithCutoffLTRankAddsRank (Var m) c lt n | GT = Refl
shiftUpWithCutoffLTRankAddsRank (Lambda t1)   c lt n =
  let rankt1GTpred = nonZeroPredLT (rank t1) (lteTransitive (LTESucc LTEZero) lt) in
  let cPlus1LTrankt1 = lteTransitive (LTESucc lt) rankt1GTpred in
  rewrite shiftUpWithCutoffLTRankAddsRank t1 (S c) cPlus1LTrankt1 n in
  rewrite plusPredLeftPred (rank t1) n (lteTransitive (LTESucc LTEZero) cPlus1LTrankt1) in Refl
shiftUpWithCutoffLTRankAddsRank (Apply t1 t2) c lt n = case maximumToEither (rank t1) (rank t2) of
  Left  eq =>
    rewrite shiftUpWithCutoffLTRankAddsRank t1 c (replace eq lt) n in
    case ltOrGte c (rank t2) of
      Left  lt'  =>
        rewrite shiftUpWithCutoffLTRankAddsRank t2 c lt' n in
        rewrite sym $ plusNDistributesOverMaximumRight n (rank t1) (rank t2) in
        plusCommutative n (maximum (rank t1) (rank t2))
      Right gte' =>
        rewrite shiftUpWithCutoffGTERankNeutral t2 c gte' n in
        let rankt2LTErankt1 = replace eq (lteTransitive (lteTransitive gte' (lteSuccRight lteRefl)) lt) in
        rewrite maximumOfGte (rank t1 + n) (rank t2) (lteTransitive rankt2LTErankt1 (lteAddRight (rank t1))) in
        rewrite eq in Refl
  Right eq =>
    rewrite shiftUpWithCutoffLTRankAddsRank t2 c (replace eq lt) n in
    case ltOrGte c (rank t1) of
      Left  lt'  =>
        rewrite shiftUpWithCutoffLTRankAddsRank t1 c lt' n in
        rewrite sym $ plusNDistributesOverMaximumRight n (rank t1) (rank t2) in
        plusCommutative n (maximum (rank t1) (rank t2))
      Right gte' =>
        rewrite shiftUpWithCutoffGTERankNeutral t1 c gte' n in
        let rankt1LTErankt2 = replace eq (lteTransitive (lteTransitive gte' (lteSuccRight lteRefl)) lt) in
        rewrite maximumCommutative (rank t1) (rank t2 + n) in
        rewrite maximumOfGte (rank t2 + n) (rank t1) (lteTransitive rankt1LTErankt2 (lteAddRight (rank t2))) in
        rewrite eq in Refl

shiftUpNonClosedAddsRank : (t : Term) -> Not (Closed t) -> (n : Nat) -> rank (shiftUp n t) = rank t + n
shiftUpNonClosedAddsRank t ncl n with (rank t) proof rt
  shiftUpNonClosedAddsRank t ncl n | Z     = absurd $ ncl Refl
  shiftUpNonClosedAddsRank t ncl n | (S r) =
    rewrite shiftUpWithCutoffLTRankAddsRank t Z (replace rt (LTESucc LTEZero)) n in
    rewrite sym rt in Refl