Created
November 23, 2020 04:53
-
-
Save SekiT/34344d81f6a24183f442d96689758bc8 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment