diff options
Diffstat (limited to 'src/Total/Term.idr')
| -rw-r--r-- | src/Total/Term.idr | 485 |
1 files changed, 197 insertions, 288 deletions
diff --git a/src/Total/Term.idr b/src/Total/Term.idr index 129662a..7d6fba0 100644 --- a/src/Total/Term.idr +++ b/src/Total/Term.idr @@ -1,13 +1,19 @@ module Total.Term +import Control.Relation import public Data.SnocList.Elem +import public Subst import public Thinning + import Syntax.PreorderReasoning +import Syntax.PreorderReasoning.Generic %prefix_record_projections off infixr 10 ~> +-- Types ----------------------------------------------------------------------- + public export data Ty : Type where N : Ty @@ -15,64 +21,48 @@ data Ty : Type where %name Ty ty +-- Definition ------------------------------------------------------------------ + public export -data Term : SnocList Ty -> Ty -> Type where - Var : (i : Elem ty ctx) -> Term ctx ty - Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty') - App : {ty : Ty} -> Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty' - Zero : Term ctx N - Suc : Term ctx N -> Term ctx N - Rec : Term ctx N -> Term ctx ty -> Term ctx (ty ~> ty) -> Term ctx ty +data Term : Ty -> SnocList Ty -> Type where + Var : (i : Elem ty ctx) -> Term ty ctx + Abs : Term ty' (ctx :< ty) -> Term (ty ~> ty') ctx + App : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx + Zero : Term N ctx + Suc : Term N ctx -> Term N ctx + Rec : Term N ctx -> Term ty ctx -> Term (ty ~> ty) ctx -> Term ty ctx %name Term t, u, v -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 (App t u) thin = App (wkn t thin) (wkn u thin) -wkn Zero thin = Zero -wkn (Suc t) thin = Suc (wkn t thin) -wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin) +-- Raw Interfaces -------------------------------------------------------------- -public export -data Terms : SnocList Ty -> SnocList Ty -> Type where - Base : ctx `Thins` ctx' -> Terms ctx' ctx - (:<) : Terms ctx' ctx -> Term ctx' ty -> Terms ctx' (ctx :< ty) +export +Point Ty Term where + point = Var -%name Terms sub +export +Weaken Ty Term where + wkn (Var i) thin = Var (index thin i) + 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) + wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin) -public export -index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty -index (Base thin) i = Var (index thin i) -index (sub :< t) Here = t -index (sub :< t) (There i) = index sub i +export +PointWeaken Ty Term where -public export -wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx -wknAll (Base thin') thin = Base (thin . thin') -wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin +-- Substitution ---------------------------------------------------------------- public export -subst : Len ctx' => Term ctx ty -> Terms ctx' ctx -> Term ctx' ty +subst : Term ty ctx -> Subst Term ctx ctx' -> Term ty ctx' 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 $ lift sub) subst (App t u) sub = App (subst t sub) (subst u sub) subst Zero sub = Zero subst (Suc t) sub = Suc (subst t sub) 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) (Drop thin) = restrict sub thin -restrict (sub :< t) (Keep thin) = restrict sub thin :< t - -public export -(.) : Len ctx'' => Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx -sub2 . (Base thin) = restrict sub2 thin -sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2 - -- Properties ------------------------------------------------------------------ -- Utilities @@ -84,106 +74,63 @@ cong3 f Refl Refl Refl = Refl -- Weakening export -wknHomo : - (t : Term ctx ty) -> - (thin1 : ctx `Thins` ctx') -> - (thin2 : ctx' `Thins` ctx'') -> - wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1) -wknHomo (Var i) thin1 thin2 = - cong Var (indexHomo thin2 thin1 i) -wknHomo (Abs t) thin1 thin2 = - 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 = - Refl -wknHomo (Suc t) thin1 thin2 = - cong Suc (wknHomo t thin1 thin2) -wknHomo (Rec t u v) thin1 thin2 = - cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2) +FullWeaken Ty Term where + shiftIsWkn t = Refl + + wknId (Var i) = cong Var $ indexId i + wknId (Abs t) = cong Abs $ trans (cong (wkn t) (keepId _ _)) (wknId t) + wknId (App t u) = cong2 App (wknId t) (wknId u) + wknId Zero = Refl + wknId (Suc t) = cong Suc (wknId t) + wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v) + + wknHomo (Var i) thin1 thin2 = cong Var $ indexHomo thin1 thin2 i + wknHomo (Abs t) thin1 thin2 = + cong Abs $ + trans + (wknHomo t (keep thin1 _) (keep thin2 _)) + (cong (wkn t) $ keepHomo thin2 thin1 _) + wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) + wknHomo Zero thin1 thin2 = Refl + wknHomo (Suc t) thin1 thin2 = cong Suc (wknHomo t thin1 thin2) + wknHomo (Rec t u v) thin1 thin2 = + cong3 Rec + (wknHomo t thin1 thin2) + (wknHomo u thin1 thin2) + (wknHomo v thin1 thin2) export -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 -wknId (Suc t) = cong Suc (wknId t) -wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v) - -indexWknAll : - (sub : Terms ctx' ctx) -> - (thin : ctx' `Thins` ctx'') -> - (i : Elem ty ctx) -> - index (wknAll sub thin) i = wkn (index sub i) thin -indexWknAll (Base thin') thin i = sym $ cong Var $ indexHomo thin thin' i -indexWknAll (sub :< t) thin Here = Refl -indexWknAll (sub :< t) thin (There i) = indexWknAll sub thin i - -wknAllHomo : - (sub : Terms ctx ctx''') -> - (thin1 : ctx `Thins` ctx') -> - (thin2 : ctx' `Thins` ctx'') -> - wknAll (wknAll sub thin1) thin2 = wknAll sub (thin2 . thin1) -wknAllHomo (Base thin) thin1 thin2 = cong Base (assoc thin2 thin1 thin) -wknAllHomo (sub :< t) thin1 thin2 = cong2 (:<) (wknAllHomo sub thin1 thin2) (wknHomo t thin1 thin2) - --- Restrict - -indexRestrict : - (thin : ctx `Thins` ctx') -> - (sub : Terms ctx'' ctx') -> - (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 (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 : (len : Len ctx) => (sub : Terms ctx' ctx) -> restrict sub (id @{len}) = sub -restrictId (Base thin) = cong Base (identityRight thin) -restrictId {len = S k} (sub :< t) = cong (:< t) (restrictId sub) - -restrictHomo : - (sub : Terms ctx ctx''') -> - (thin1 : ctx'' `Thins` ctx''') -> - (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) (Drop thin1) thin2 = restrictHomo sub thin1 thin2 -restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2 -restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2 - -wknAllRestrict : - (thin1 : ctx `Thins` ctx') -> - (sub : Terms ctx'' ctx') -> - (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 (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2 -wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2) +FullPointWeaken Ty Term where + wknPoint i thin = Refl -- Substitution & Weakening export +substCong : + (t : Term ty ctx) -> + {0 sub1, sub2 : Subst Term ctx ctx'} -> + Equiv sub1 sub2 -> + subst t sub1 = subst t sub2 +substCong (Var i) e = e.equiv i +substCong (Abs t) e = cong Abs $ substCong t (liftCong e) +substCong (App t u) e = cong2 App (substCong t e) (substCong u e) +substCong Zero e = Refl +substCong (Suc t) e = cong Suc (substCong t e) +substCong (Rec t u v) e = cong3 Rec (substCong t e) (substCong u e) (substCong v e) + +export wknSubst : - (t : Term ctx ty) -> - (sub : Terms ctx' ctx) -> + (t : Term ty ctx) -> + (sub : Subst Term ctx ctx') -> (thin : ctx' `Thins` ctx'') -> - wkn (subst t sub) thin = subst t (wknAll sub thin) + wkn (subst t sub) thin = subst t (wkn sub thin) wknSubst (Var i) sub thin = - sym (indexWknAll sub thin i) -wknSubst (Abs t) sub thin = + indexWkn sub thin i +wknSubst (Abs {ty} t) sub thin = 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) - ...(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)) + |~ wkn (subst t (lift sub)) (keep thin ty) + ~~ subst t (wkn (lift sub) (keep thin ty)) ...(wknSubst t (lift sub) (keep thin _)) + ~~ subst t (lift (wkn sub thin)) ...(substCong t (wknLift sub thin)) wknSubst (App t u) sub thin = cong2 App (wknSubst t sub thin) (wknSubst u sub thin) wknSubst Zero sub thin = @@ -195,163 +142,125 @@ wknSubst (Rec t u v) sub thin = export substWkn : - (t : Term ctx ty) -> + (t : Term ty ctx) -> + (sub : Subst Term ctx' ctx'') -> (thin : ctx `Thins` ctx') -> - (sub : Terms ctx'' ctx') -> subst (wkn t thin) sub = subst t (restrict sub thin) -substWkn (Var i) thin sub = - sym (indexRestrict thin sub i) -substWkn (Abs t) thin sub = - cong Abs $ Calc $ - |~ 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 = - Refl -substWkn (Suc t) thin sub = - cong Suc (substWkn t thin sub) -substWkn (Rec t u v) thin sub = - cong3 Rec (substWkn t thin sub) (substWkn u thin sub) (substWkn 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) - WknAll : - (len : Len ctx) => - Equiv sub sub' -> - 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 = 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) - -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 (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) -substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (substCong v prf) - -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 = - 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) -substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin) - --- Substitution Composition - -indexComp : - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx'' ctx') -> - (i : Elem ty ctx) -> - index (sub2 . sub1) i = subst (index sub1 i) sub2 -indexComp (Base thin) sub2 i = indexRestrict thin sub2 i -indexComp (sub1 :< t) sub2 Here = Refl -indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i - -wknAllComp : - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx'' ctx') -> - (thin : ctx'' `Thins` ctx''') -> - wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin -wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin -wknAllComp (sub1 :< t) sub2 thin = - cong2 (:<) - (wknAllComp sub1 sub2 thin) - (sym $ wknSubst t sub2 thin) - -compDrop : - (sub1 : Terms ctx' ctx) -> - (thin : ctx' `Thins` ctx'') -> - (sub2 : Terms ctx''' ctx'') -> - sub2 . wknAll sub1 thin = restrict sub2 thin . sub1 -compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin' -compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2) - -export -compWknAll : - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx''' ctx'') -> - (thin : ctx' `Thins` ctx'') -> - sub2 . wknAll sub1 thin = restrict sub2 thin . sub1 -compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin' -compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2) - -export -baseComp : - (thin : ctx' `Thins` ctx'') -> - (sub : Terms ctx' ctx) -> - Base thin . sub = wknAll sub thin -baseComp thin (Base thin') = Refl -baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin) - --- Substitution - -export -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 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) -substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v) - -export -substHomo : - (t : Term ctx ty) -> - (sub1 : Terms ctx' ctx) -> - (sub2 : Terms ctx'' ctx') -> - subst (subst t sub1) sub2 = subst t (sub2 . sub1) -substHomo (Var i) sub1 sub2 = - sym $ indexComp sub1 sub2 i -substHomo (Abs t) sub1 sub2 = +substWkn (Var i) sub thin = + indexRestrict sub thin i +substWkn (Abs t) sub thin = 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) - ...(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)) -substHomo (App t u) sub1 sub2 = - cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2) -substHomo Zero sub1 sub2 = + |~ subst (wkn t (keep thin _)) (lift sub) + ~~ subst t (restrict (lift sub) (keep thin _)) ...(substWkn t (lift sub) (keep thin _)) + ~~ subst t (lift (restrict sub thin)) ...(substCong t (restrictLift sub thin)) +substWkn (App t u) sub thin = + cong2 App (substWkn t sub thin) (substWkn u sub thin) +substWkn Zero sub thin = Refl -substHomo (Suc t) sub1 sub2 = - cong Suc (substHomo t sub1 sub2) -substHomo (Rec t u v) sub1 sub2 = - cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2) +substWkn (Suc t) sub thin = + cong Suc (substWkn t sub thin) +substWkn (Rec t u v) sub thin = + cong3 Rec (substWkn t sub thin) (substWkn u sub thin) (substWkn v sub thin) + +-- -- 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 = +-- -- 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) +-- -- substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin) + +-- -- -- Substitution Composition + +-- -- indexComp : +-- -- (sub1 : Terms ctx' ctx) -> +-- -- (sub2 : Terms ctx'' ctx') -> +-- -- (i : Elem ty ctx) -> +-- -- index (sub2 . sub1) i = subst (index sub1 i) sub2 +-- -- indexComp (Base thin) sub2 i = indexRestrict thin sub2 i +-- -- indexComp (sub1 :< t) sub2 Here = Refl +-- -- indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i + +-- -- wknAllComp : +-- -- (sub1 : Terms ctx' ctx) -> +-- -- (sub2 : Terms ctx'' ctx') -> +-- -- (thin : ctx'' `Thins` ctx''') -> +-- -- wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin +-- -- wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin +-- -- wknAllComp (sub1 :< t) sub2 thin = +-- -- cong2 (:<) +-- -- (wknAllComp sub1 sub2 thin) +-- -- (sym $ wknSubst t sub2 thin) + +-- -- compDrop : +-- -- (sub1 : Terms ctx' ctx) -> +-- -- (thin : ctx' `Thins` ctx'') -> +-- -- (sub2 : Terms ctx''' ctx'') -> +-- -- sub2 . wknAll sub1 thin = restrict sub2 thin . sub1 +-- -- compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin' +-- -- compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2) + +-- -- export +-- -- compWknAll : +-- -- (sub1 : Terms ctx' ctx) -> +-- -- (sub2 : Terms ctx''' ctx'') -> +-- -- (thin : ctx' `Thins` ctx'') -> +-- -- sub2 . wknAll sub1 thin = restrict sub2 thin . sub1 +-- -- compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin' +-- -- compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2) + +-- -- export +-- -- baseComp : +-- -- (thin : ctx' `Thins` ctx'') -> +-- -- (sub : Terms ctx' ctx) -> +-- -- Base thin . sub = wknAll sub thin +-- -- baseComp thin (Base thin') = Refl +-- -- baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin) + +-- -- -- Substitution + +-- -- export +-- -- 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 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) +-- -- substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v) + +-- -- export +-- -- substHomo : +-- -- (t : Term ctx ty) -> +-- -- (sub1 : Terms ctx' ctx) -> +-- -- (sub2 : Terms ctx'' ctx') -> +-- -- subst (subst t sub1) sub2 = subst t (sub2 . sub1) +-- -- substHomo (Var i) sub1 sub2 = +-- -- sym $ indexComp sub1 sub2 i +-- -- substHomo (Abs t) sub1 sub2 = +-- -- 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) +-- -- ...(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)) +-- -- substHomo (App t u) sub1 sub2 = +-- -- cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2) +-- -- substHomo Zero sub1 sub2 = +-- -- Refl +-- -- substHomo (Suc t) sub1 sub2 = +-- -- cong Suc (substHomo t sub1 sub2) +-- -- substHomo (Rec t u v) sub1 sub2 = +-- -- cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2) |