diff options
Diffstat (limited to 'src/Total')
| -rw-r--r-- | src/Total/Encoded/Util.idr | 24 | ||||
| -rw-r--r-- | src/Total/LogRel.idr | 48 | ||||
| -rw-r--r-- | src/Total/NormalForm.idr | 4 | ||||
| -rw-r--r-- | src/Total/Reduction.idr | 29 | ||||
| -rw-r--r-- | src/Total/Syntax.idr | 31 | ||||
| -rw-r--r-- | src/Total/Term.idr | 138 |
6 files changed, 140 insertions, 134 deletions
diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr index 705d74b..1a848c0 100644 --- a/src/Total/Encoded/Util.idr +++ b/src/Total/Encoded/Util.idr @@ -22,8 +22,8 @@ namespace Bool False = Suc Zero export - If : Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty - If t u v = Rec t u (Abs $ wkn v (Drop Id)) + If : Len ctx => Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty + If t u v = Rec t u (Abs $ wkn v (Drop id)) namespace Arb export @@ -112,7 +112,7 @@ namespace Pair export mapProd : {ctx, tys, tys' : SnocList Ty} -> - {auto 0 prf : length tys = length tys'} -> + {auto 0 prf : SnocList.length tys = SnocList.length tys'} -> All (Term ctx) (zipWith (~>) tys tys') -> Term ctx (Product tys ~> Product tys') mapProd {tys = [<], tys' = [<]} [<] = Abs (Var Here) @@ -120,8 +120,8 @@ namespace Pair Abs' (S Z) (\p => App' (lift pair) - [<App (wkn (mapProd fs {prf = injective prf}) (Drop Id) . lift fst) p - , App (wkn f (Drop Id) . lift snd) p + [<App (wkn (mapProd fs {prf = injective prf}) (Drop id) . lift fst) p + , App (wkn f (Drop id) . lift snd) p ]) replicate : Nat -> a -> SnocList a @@ -292,9 +292,9 @@ namespace Nat Cond ((n, v) :: xs) = Abs' (S Z) (\t => - If (App' (lift LE) [<t, wkn n (Drop Id)]) - (App (wkn v (Drop Id)) t) - (App (wkn (Cond xs) (Drop Id)) (App' (lift Sub) [<t, wkn n (Drop Id)]))) + If (App' (lift LE) [<t, wkn n (Drop id)]) + (App (wkn v (Drop id)) t) + (App (wkn (Cond xs) (Drop id)) (App' (lift Sub) [<t, wkn n (Drop id)]))) namespace Data public export @@ -394,7 +394,7 @@ namespace Data (lift $ put {tys = map (flip fillShape N) c} $ rewrite forgetMap (flip fillShape N) c in elemMap (flip fillShape N) i) - (App' (lift mapSnd) [<Abs (lift $ enumerate n), wkn t (Drop Id)]))) + (App' (lift mapSnd) [<Abs (lift $ enumerate n), wkn t (Drop id)]))) :: calcData (App (lift snd) t) (Suc Zero) ) ]) @@ -409,8 +409,8 @@ namespace Data elim cases = Abs' (S Z) (\t => let tags = Suc (App (lift $ project $ There $ There Here) t) in - let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop Id)) in - let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop Id)) in + let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop id)) in + let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop id)) in App' (Rec tags (lift arb) @@ -420,7 +420,7 @@ namespace Data (rewrite forgetMap (flip fillShape N) c in gmap (\f => - wkn f (Drop $ Drop $ Drop Id) . + wkn f (Drop $ Drop $ Drop id) . App (lift mapShape) (rec . App (lift Add) (App offset n))) cases) . vals) diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr index 1ed7276..ebde8d5 100644 --- a/src/Total/LogRel.idr +++ b/src/Total/LogRel.idr @@ -178,44 +178,49 @@ allValid : allValid help (Var i) sub allRels = index help.var allRels i allValid help (Abs t) sub allRels = let valid = allValid help t in - ( let + (let rec = valid - (wknAll sub (Drop Id) :< Var Here) - (wknAllRel help allRels (Drop Id) :< help.var Here) + (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here) + (wknAllRel help allRels (Drop $ id @{termsLen sub}) :< help.var Here) in help.abs rec , \thin, u, rel => let eq : - (subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u) = + (subst + (wkn (subst t (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here)) (Keep thin)) + (Base (id @{length _}) :< u) = subst t (wknAll sub thin :< u)) - eq = Calc $ - |~ subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u) - ~~ subst (subst t (wknAll sub (Drop Id) :< Var Here)) (restrict (Base Id :< u) (keep thin)) - ...(substWkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin) (Base Id :< u)) - ~~ subst (subst t (wknAll sub (Drop Id) :< Var Here)) (Base thin :< u) - ...(cong (subst (subst t (wknAll sub (Drop Id) :< Var Here))) $ restrictKeep (Base Id) u thin) - ~~ subst t ((Base thin :< u) . wknAll sub (Drop Id) :< u) - ...(substHomo t (wknAll sub (Drop Id) :< Var Here) (Base thin :< u)) - ~~ subst t (Base (thin . Id) . sub :< u) - ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop Id)) - ~~ subst t (Base thin . sub :< u) - ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin) - ~~ subst t (wknAll sub thin :< u) - ...(cong (subst t . (:< u)) $ baseComp thin sub) + eq = + rewrite lenUnique (termsLen sub) (length ctx') in + Calc $ + |~ subst (wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)) (Base id :< u) + ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (restrict (Base id :< u) (Keep thin)) + ...(substWkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin) (Base id :< u)) + ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (Base thin :< u) + ...(cong (subst (subst t (wknAll sub (Drop id) :< Var Here)) . (:< u) . Base) $ identityLeft thin) + ~~ subst t ((Base thin :< u) . wknAll sub (Drop id) :< u) + ...(substHomo t (wknAll sub (Drop id) :< Var Here) (Base thin :< u)) + ~~ subst t (Base (thin . id) . sub :< u) + ...(cong (subst t . (:< u)) $ compWknAll sub (Base thin :< u) (Drop id)) + ~~ subst t (Base thin . sub :< u) + ...(cong (subst t . (:< u) . (. sub) . Base) $ identityRight thin) + ~~ subst t (wknAll sub thin :< u) + ...(cong (subst t . (:< u)) $ baseComp thin sub) in preserve (backStepHelper help.step) (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel)) (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)} eq - AppBeta) + (AppBeta (length _))) ) allValid help (App t u) sub allRels = let (pt, app) = allValid help t sub allRels in let rel = allValid help u sub allRels in - rewrite sym $ wknId (subst t sub) in app Id (subst u sub) rel + rewrite sym $ wknId @{termsLen sub} (subst t sub) in + app (id @{termsLen sub}) (subst u sub) rel allValid help Zero sub allRels = help.zero allValid help (Suc t) sub allRels = let pt = allValid help t sub allRels in @@ -234,4 +239,5 @@ allRel : ValidHelper P -> (t : Term ctx ty) -> P t -allRel help t = rewrite sym $ substId t in escape (allValid help t (Base Id) Base) +allRel help t = + rewrite sym $ substId @{length ctx} t in escape (allValid help t (Base $ id @{length ctx}) Base) diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr index b5580b5..266d00d 100644 --- a/src/Total/NormalForm.idr +++ b/src/Total/NormalForm.idr @@ -93,8 +93,8 @@ recNf' : recNf' Zero n relU relV = backStepsRel relU [<RecZero] recNf' (Suc t') n relU relV = let rec = recNf' t' (invSuc n) relU relV in - let step : Rec (Suc t') u v > App (wkn v Id) (Rec t' u v) = rewrite wknId v in RecSuc in - backStepsRel (snd relV Id _ rec) [<step] + let step : Rec (Suc t') u v > App (wkn v id) (Rec t' u v) = rewrite wknId v in RecSuc in + backStepsRel (snd relV id _ rec) [<step] recNf' t'@(Var _) n relU relV = let nfU = escape relU in let nfV = escape {ty = ty ~> ty} relV in diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr index cb13706..b11665b 100644 --- a/src/Total/Reduction.idr +++ b/src/Total/Reduction.idr @@ -8,7 +8,9 @@ data (>) : Term ctx ty -> Term ctx ty -> Type where AbsCong : t > u -> Abs t > Abs u AppCong1 : t > u -> App t v > App u v AppCong2 : u > v -> App t u > App t v - AppBeta : App (Abs t) u > subst t (Base Id :< u) + AppBeta : + (0 len : Len ctx) -> + App (Abs t) u > subst t (Base (id @{len}) :< u) SucCong : t > u -> Suc t > Suc u RecCong1 : t1 > t2 -> Rec t1 u v > Rec t2 u v RecCong2 : u1 > u2 -> Rec t u1 v > Rec t u2 v @@ -68,27 +70,28 @@ RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step -- Properties ------------------------------------------------------------------ lemma : + (0 len : Len ctx) -> (t : Term (ctx :< ty) ty') -> (thin : ctx `Thins` ctx') -> (u : Term ctx ty) -> - subst (wkn t (keep thin)) (Base Id :< wkn u thin) = wkn (subst t (Base Id :< u)) thin -lemma t thin u = Calc $ - |~ subst (wkn t (keep thin)) (Base Id :< wkn u thin) - ~~ subst t (restrict (Base Id :< wkn u thin) (keep thin)) - ...(substWkn t (keep thin) (Base Id :< wkn u thin)) - ~~ subst t (Base thin :< wkn u thin) - ...(cong (subst t) $ restrictKeep (Base Id) (wkn u thin) thin) - ~~ subst t (Base (thin . Id) :< wkn u thin) - ...(sym $ cong (subst t . (:< wkn u thin) . Base) $ identityRight thin) - ~~ wkn (subst t (Base Id :< u)) thin - ...(sym $ wknSubst t (Base Id :< u) thin) + subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = wkn (subst t (Base (id @{len}) :< u)) thin +lemma len t thin u = Calc $ + |~ subst (wkn t (Keep thin)) (Base id :< wkn u thin) + ~~ subst t (restrict (Base id :< wkn u thin) (Keep thin)) + ...(substWkn t (Keep thin) (Base id :< wkn u thin)) + ~~ subst t (Base (id . thin) :< wkn u thin) + ...(Refl) + ~~ subst t (Base (thin . id) :< wkn u thin) + ...(cong (subst t . (:< wkn u thin) . Base) $ trans (identityLeft thin) (sym $ identityRight thin)) + ~~ wkn (subst t (Base id :< u)) thin + ...(sym $ wknSubst t (Base id :< u) thin) export wknStep : t > u -> wkn t thin > wkn u thin wknStep (AbsCong step) = AbsCong (wknStep step) wknStep (AppCong1 step) = AppCong1 (wknStep step) wknStep (AppCong2 step) = AppCong2 (wknStep step) -wknStep (AppBeta {t, u}) {thin} = rewrite sym $ lemma t thin u in AppBeta +wknStep (AppBeta len {t, u}) {thin} = rewrite sym $ lemma len t thin u in AppBeta _ wknStep (SucCong step) = SucCong (wknStep step) wknStep (RecCong1 step) = RecCong1 (wknStep step) wknStep (RecCong2 step) = RecCong2 (wknStep step) diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr index 084ae3e..6c34250 100644 --- a/src/Total/Syntax.idr +++ b/src/Total/Syntax.idr @@ -14,29 +14,17 @@ public export tys ~>* ty = foldr (~>) ty tys public export -data Len : SnocList Ty -> Type where - Z : Len [<] - S : Len tys -> Len (tys :< ty) - -%name Len k, m, n - -public export -Cast (Len ctx) Nat where - cast Z = 0 - cast (S k) = S (cast k) - -public export -0 Fun : Len tys -> (Ty -> Type) -> Type -> Type +0 Fun : {sx : SnocList a} -> Len sx -> (a -> Type) -> Type -> Type Fun Z arg ret = ret -Fun (S {ty} k) arg ret = Fun k arg (arg ty -> ret) +Fun (S {x = ty} k) arg ret = Fun k arg (arg ty -> ret) -after : (k : Len tys) -> (a -> b) -> Fun k p a -> Fun k p b +after : (k : Len sx) -> (a -> b) -> Fun k p a -> Fun k p b after Z f x = f x after (S k) f x = after k (f .) x before : - (k : Len tys) -> - (forall ty. p ty -> q ty) -> + (k : Len sx) -> + (forall x. p x -> q x) -> Fun k q ret -> Fun k p ret before Z f x = x @@ -70,19 +58,20 @@ App' t [<] = t App' t (us :< u) = App (App' t us) u export -(.) : {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'') -t . u = Abs' (S Z) (\x => App (wkn t (Drop Id)) (App (wkn u (Drop Id)) x)) +(.) : Len ctx => {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'') +t . u = Abs' (S Z) (\x => App (wkn t (Drop id)) (App (wkn u (Drop id)) x)) export (.*) : + Len ctx => {ty : Ty} -> {tys : SnocList Ty} -> Term ctx (ty ~> ty') -> Term ctx (tys ~>* ty) -> Term ctx (tys ~>* ty') (.*) {tys = [<]} t u = App t u -(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop Id) . f) .* u +(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop id) . f) .* u export lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty -lift t = wkn t (empty ctx) +lift t = wkn t empty diff --git a/src/Total/Term.idr b/src/Total/Term.idr index d4da92a..d21ec73 100644 --- a/src/Total/Term.idr +++ b/src/Total/Term.idr @@ -29,7 +29,7 @@ data Term : SnocList Ty -> Ty -> Type where public export wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty wkn (Var i) thin = Var (index thin i) -wkn (Abs t) thin = Abs (wkn t $ keep thin) +wkn (Abs t) thin = Abs (wkn t $ Keep thin) wkn (App t u) thin = App (wkn t thin) (wkn u thin) wkn Zero thin = Zero wkn (Suc t) thin = Suc (wkn t thin) @@ -42,6 +42,12 @@ data Terms : SnocList Ty -> SnocList Ty -> Type where %name Terms sub +%hint +export +termsLen : Terms ctx' ctx -> Len ctx' +termsLen (Base thin) = lenTgt thin +termsLen (sub :< t) = termsLen sub + public export index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty index (Base thin) i = Var (index thin i) @@ -56,7 +62,7 @@ wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin public export subst : Term ctx ty -> Terms ctx' ctx -> Term ctx' ty subst (Var i) sub = index sub i -subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop Id) :< Var Here) +subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop id) :< Var Here) subst (App t u) sub = App (subst t sub) (subst u sub) subst Zero sub = Zero subst (Suc t) sub = Suc (subst t sub) @@ -65,7 +71,6 @@ subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub) public export restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms ctx'' ctx restrict (Base thin') thin = Base (thin' . thin) -restrict (sub :< t) Id = sub :< t restrict (sub :< t) (Drop thin) = restrict sub thin restrict (sub :< t) (Keep thin) = restrict sub thin :< t @@ -92,7 +97,7 @@ wknHomo : wknHomo (Var i) thin1 thin2 = cong Var (indexHomo thin2 thin1 i) wknHomo (Abs t) thin1 thin2 = - cong Abs $ trans (wknHomo t (keep thin1) (keep thin2)) (cong (wkn t) $ keepHomo thin2 thin1) + cong Abs (wknHomo t (Keep thin1) (Keep thin2)) wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) wknHomo Zero thin1 thin2 = @@ -103,8 +108,8 @@ wknHomo (Rec t u v) thin1 thin2 = cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2) export -wknId : (t : Term ctx ty) -> wkn t Id = t -wknId (Var i) = Refl +wknId : Len ctx => (t : Term ctx ty) -> wkn t Thinning.id = t +wknId (Var i) = cong Var (indexId i) wknId (Abs t) = cong Abs (wknId t) wknId (App t u) = cong2 App (wknId t) (wknId u) wknId Zero = Refl @@ -136,24 +141,13 @@ indexRestrict : (i : Elem ty ctx) -> index (restrict sub thin) i = index sub (index thin i) indexRestrict thin (Base thin') i = sym $ cong Var $ indexHomo thin' thin i -indexRestrict Id (sub :< t) i = Refl indexRestrict (Drop thin) (sub :< t) i = indexRestrict thin sub i indexRestrict (Keep thin) (sub :< t) Here = Refl indexRestrict (Keep thin) (sub :< t) (There i) = indexRestrict thin sub i -restrictId : (sub : Terms ctx' ctx) -> restrict sub Id = sub +restrictId : (len : Len ctx) => (sub : Terms ctx' ctx) -> restrict sub (id @{len}) = sub restrictId (Base thin) = cong Base (identityRight thin) -restrictId (sub :< t) = Refl - -export -restrictKeep : - (sub : Terms ctx'' ctx) -> - (t : Term ctx'' ty) -> - (thin : ctx' `Thins` ctx) -> - restrict (sub :< t) (keep thin) = restrict sub thin :< t -restrictKeep sub t Id = sym $ cong (:< t) $ restrictId sub -restrictKeep sub t (Drop thin) = Refl -restrictKeep sub t (Keep thin) = Refl +restrictId {len = S k} (sub :< t) = cong (:< t) (restrictId sub) restrictHomo : (sub : Terms ctx ctx''') -> @@ -161,9 +155,7 @@ restrictHomo : (thin2 : ctx' `Thins` ctx'') -> restrict sub (thin1 . thin2) = restrict (restrict sub thin1) thin2 restrictHomo (Base thin) thin1 thin2 = cong Base (assoc thin thin1 thin2) -restrictHomo (sub :< t) Id thin2 = Refl restrictHomo (sub :< t) (Drop thin1) thin2 = restrictHomo sub thin1 thin2 -restrictHomo (sub :< t) (Keep thin1) Id = Refl restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2 restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2 @@ -173,7 +165,6 @@ wknAllRestrict : (thin2 : ctx'' `Thins` ctx''') -> restrict (wknAll sub thin2) thin1 = wknAll (restrict sub thin1) thin2 wknAllRestrict thin1 (Base thin) thin2 = sym $ cong Base $ assoc thin2 thin thin1 -wknAllRestrict Id (sub :< t) thin2 = Refl wknAllRestrict (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2 wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2) @@ -188,16 +179,17 @@ wknSubst : wknSubst (Var i) sub thin = sym (indexWknAll sub thin i) wknSubst (Abs t) sub thin = + rewrite lenUnique (termsLen $ wknAll sub thin) (lenTgt thin) in cong Abs $ Calc $ - |~ wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin) - ~~ subst t (wknAll (wknAll sub (Drop Id)) (keep thin) :< Var (index (keep thin) Here)) - ...(wknSubst t (wknAll sub (Drop Id) :< Var Here) (keep thin)) - ~~ subst t (wknAll sub (keep thin . Drop Id) :< Var Here) - ...(cong2 (\sub, i => subst t (sub :< Var i)) (wknAllHomo sub (Drop Id) (keep thin)) (indexKeepHere thin)) - ~~ subst t (wknAll sub (Drop Id . thin) :< Var Here) - ...(cong (subst t . (:< Var Here) . wknAll sub) $ trans (keepDrop thin Id) (cong Drop $ identityRight thin)) - ~~ subst t (wknAll (wknAll sub thin) (Drop Id) :< Var Here) - ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop Id)) + |~ wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin) + ~~ subst t (wknAll (wknAll sub (Drop id)) (Keep thin) :< Var (index (Keep thin) Here)) + ...(wknSubst t (wknAll sub (Drop id) :< Var Here) (Keep thin)) + ~~ subst t (wknAll sub (Keep thin . Drop id) :< Var Here) + ...(cong (subst t . (:< Var Here)) (wknAllHomo sub (Drop id) (Keep thin))) + ~~ subst t (wknAll sub (Drop id . thin) :< Var Here) + ...(cong (subst t . (:< Var Here) . wknAll sub . Drop) $ trans (identityRight thin) (sym $ identityLeft thin)) + ~~ subst t (wknAll (wknAll sub thin) (Drop id) :< Var Here) + ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop id)) wknSubst (App t u) sub thin = cong2 App (wknSubst t sub thin) (wknSubst u sub thin) wknSubst Zero sub thin = @@ -216,14 +208,13 @@ substWkn : substWkn (Var i) thin sub = sym (indexRestrict thin sub i) substWkn (Abs t) thin sub = + rewrite lenUnique (termsLen $ restrict sub thin) (termsLen sub) in cong Abs $ Calc $ - |~ subst (wkn t $ keep thin) (wknAll sub (Drop Id) :< Var Here) - ~~ subst t (restrict (wknAll sub (Drop Id) :< Var Here) (keep thin)) - ...(substWkn t (keep thin) (wknAll sub (Drop Id) :< Var Here)) - ~~ subst t (restrict (wknAll sub (Drop Id)) thin :< Var Here) - ...(cong (subst t) $ restrictKeep (wknAll sub (Drop Id)) (Var Here) thin) - ~~ subst t (wknAll (restrict sub thin) (Drop Id) :< Var Here) - ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop Id)) + |~ subst (wkn t $ Keep thin) (wknAll sub (Drop id) :< Var Here) + ~~ subst t (restrict (wknAll sub (Drop id)) thin :< Var Here) + ...(substWkn t (Keep thin) (wknAll sub (Drop id) :< Var Here)) + ~~ subst t (wknAll (restrict sub thin) (Drop id) :< Var Here) + ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop id)) substWkn (App t u) thin sub = cong2 App (substWkn t thin sub) (substWkn u thin sub) substWkn Zero thin sub = @@ -236,26 +227,37 @@ substWkn (Rec t u v) thin sub = namespace Equiv public export data Equiv : Terms ctx' ctx -> Terms ctx' ctx -> Type where - Base : Equiv (Base (keep thin)) (Base (Drop thin) :< Var Here) + Base : Equiv (Base (Keep thin)) (Base (Drop thin) :< Var Here) WknAll : + (len : Len ctx) => Equiv sub sub' -> - Equiv (wknAll sub (Drop Id) :< Var Here) (wknAll sub' (Drop Id) :< Var Here) + Equiv + (wknAll sub (Drop $ id @{len}) :< Var Here) + (wknAll sub' (Drop $ id @{len}) :< Var Here) %name Equiv prf indexCong : Equiv sub sub' -> (i : Elem ty ctx) -> index sub i = index sub' i -indexCong Base Here = irrelevantEq $ cong Var (indexKeepHere _) -indexCong Base (There i) = irrelevantEq $ cong Var (indexKeepThere _ i) +indexCong Base Here = Refl +indexCong Base (There i) = Refl indexCong (WknAll prf) Here = Refl indexCong (WknAll {sub, sub'} prf) (There i) = Calc $ - |~ index (wknAll sub (Drop Id)) i - ~~ wkn (index sub i) (Drop Id) ...(indexWknAll sub (Drop Id) i) - ~~ wkn (index sub' i) (Drop Id) ...(cong (flip wkn (Drop Id)) $ indexCong prf i) - ~~ index (wknAll sub' (Drop Id)) i ...(sym $ indexWknAll sub' (Drop Id) i) + |~ index (wknAll sub (Drop id)) i + ~~ wkn (index sub i) (Drop id) ...(indexWknAll sub (Drop id) i) + ~~ wkn (index sub' i) (Drop id) ...(cong (flip wkn (Drop id)) $ indexCong prf i) + ~~ index (wknAll sub' (Drop id)) i ...(sym $ indexWknAll sub' (Drop id) i) -substCong : (t : Term ctx ty) -> Equiv sub sub' -> subst t sub = subst t sub' +substCong : + (len : Len ctx') => + (t : Term ctx ty) -> + {0 sub, sub' : Terms ctx' ctx} -> + Equiv sub sub' -> + subst t sub = subst t sub' substCong (Var i) prf = indexCong prf i -substCong (Abs t) prf = cong Abs (substCong t (WknAll prf)) +substCong (Abs t) prf = + rewrite lenUnique (termsLen sub) (termsLen sub') in + rewrite lenUnique (termsLen sub') len in + cong Abs (substCong t (WknAll prf)) substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf) substCong Zero prf = Refl substCong (Suc t) prf = cong Suc (substCong t prf) @@ -263,10 +265,12 @@ substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (subst substBase : (t : Term ctx ty) -> (thin : ctx `Thins` ctx') -> subst t (Base thin) = wkn t thin substBase (Var i) thin = Refl -substBase (Abs t) thin = cong Abs $ Calc $ - |~ subst t (Base (Drop thin) :< Var Here) - ~~ subst t (Base $ keep thin) ...(sym $ substCong t Base) - ~~ wkn t (keep thin) ...(substBase t (keep thin)) +substBase (Abs t) thin = + rewrite identityLeft thin in + cong Abs $ Calc $ + |~ subst t (Base (Drop thin) :< Var Here) + ~~ subst t (Base $ Keep thin) ...(sym $ substCong t Base) + ~~ wkn t (Keep thin) ...(substBase t (Keep thin)) substBase (App t u) thin = cong2 App (substBase t thin) (substBase u thin) substBase Zero thin = Refl substBase (Suc t) thin = cong Suc (substBase t thin) @@ -322,9 +326,12 @@ baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin) -- Substitution export -substId : (t : Term ctx ty) -> subst t (Base Id) = t -substId (Var i) = Refl -substId (Abs t) = cong Abs $ trans (sym $ substCong t Base) (substId t) +substId : (len : Len ctx) => (t : Term ctx ty) -> subst t (Base $ id @{len}) = t +substId (Var i) = cong Var (indexId i) +substId (Abs t) = + rewrite lenUnique (termsLen $ Base $ id @{len}) len in + rewrite identitySquared len in + cong Abs $ trans (sym $ substCong t Base) (substId t) substId (App t u) = cong2 App (substId t) (substId u) substId Zero = Refl substId (Suc t) = cong Suc (substId t) @@ -339,18 +346,19 @@ substHomo : substHomo (Var i) sub1 sub2 = sym $ indexComp sub1 sub2 i substHomo (Abs t) sub1 sub2 = + rewrite lenUnique (termsLen $ sub2 . sub1) (termsLen sub2) in cong Abs $ Calc $ - |~ subst (subst t (wknAll sub1 (Drop Id) :< Var Here)) (wknAll sub2 (Drop Id) :< Var Here) - ~~ subst t ((wknAll sub2 (Drop Id) :< Var Here) . (wknAll sub1 (Drop Id) :< Var Here)) - ...(substHomo t (wknAll sub1 (Drop Id) :< Var Here) (wknAll sub2 (Drop Id) :< Var Here)) - ~~ subst t ((wknAll sub2 (Drop Id) :< Var Here) . wknAll sub1 (Drop Id) :< Var Here) + |~ subst (subst t (wknAll sub1 (Drop id) :< Var Here)) (wknAll sub2 (Drop id) :< Var Here) + ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . (wknAll sub1 (Drop id) :< Var Here)) + ...(substHomo t (wknAll sub1 (Drop id) :< Var Here) (wknAll sub2 (Drop id) :< Var Here)) + ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . wknAll sub1 (Drop id) :< Var Here) ...(Refl) - ~~ subst t (restrict (wknAll sub2 (Drop Id)) Id . sub1 :< Var Here) - ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop Id) (wknAll sub2 (Drop Id) :< Var Here)) - ~~ subst t (wknAll sub2 (Drop Id) . sub1 :< Var Here) - ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop Id))) - ~~ subst t (wknAll (sub2 . sub1) (Drop Id) :< Var Here) - ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop Id)) + ~~ subst t (restrict (wknAll sub2 (Drop id)) id . sub1 :< Var Here) + ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop id) (wknAll sub2 (Drop id) :< Var Here)) + ~~ subst t (wknAll sub2 (Drop id) . sub1 :< Var Here) + ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop id))) + ~~ subst t (wknAll (sub2 . sub1) (Drop id) :< Var Here) + ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop id)) substHomo (App t u) sub1 sub2 = cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2) substHomo Zero sub1 sub2 = |