From cedc6109895a53ce6ed667e0391b232bf5463387 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 15 Jun 2023 16:09:42 +0100 Subject: WIP : use smarter weakenings. --- src/Total/Encoded/Test.idr | 63 ++++++ src/Total/LogRel.idr | 258 +++++++++++----------- src/Total/NormalForm.idr | 5 +- src/Total/Pretty.idr | 4 +- src/Total/Reduction.idr | 46 ++-- src/Total/Syntax.idr | 65 +++--- src/Total/Term.idr | 485 +++++++++++++++++------------------------- src/Total/Term/CoDebruijn.idr | 451 ++++++++++++++++++--------------------- 8 files changed, 662 insertions(+), 715 deletions(-) create mode 100644 src/Total/Encoded/Test.idr (limited to 'src/Total') diff --git a/src/Total/Encoded/Test.idr b/src/Total/Encoded/Test.idr new file mode 100644 index 0000000..cf5aa8e --- /dev/null +++ b/src/Total/Encoded/Test.idr @@ -0,0 +1,63 @@ +module Total.Encoded.Test + +import Total.NormalForm +import Total.Pretty +import Total.Encoded.Util + +namespace List + ListC : Container + ListC = (Unit, 0) ::: [(N, 1)] + + export + List : Ty + List = fix ListC + + export + nil : FullTerm List [<] + nil = app (intro {c = ListC} Here) (app' pair [ List ~> List) [<] + cons = abs' (S $ S Z) + (\t, ts => + app (lift $ intro {c = ListC} $ There Here) + (app' (lift pair) + [ FullTerm ((N ~> ty ~> ty) ~> ty ~> List ~> ty) [<] + fold = abs' (S $ S Z) + (\f, z => elim + [ abs (drop z) + , abs' (S Z) (\p => + app' (drop f) + [ FullTerm List [<] +MkList = foldr (\n, ts => app' cons [ N) [<] +sum = app' fold [ app' (lift add) [ app (lift pred) n))] + let t : FullTerm (N ~> N) [<] = cond cases + -- let t : FullTerm N [<] = app sum (MkList [1,2,3,4]) + putDoc (group $ Doc.pretty "Input:" <+> line <+> pretty (toTerm t)) + putDoc (group $ Doc.pretty "Normal Form:" <+> line <+> pretty (toTerm (normalize t).term)) diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr index b088e6f..0b73706 100644 --- a/src/Total/LogRel.idr +++ b/src/Total/LogRel.idr @@ -11,24 +11,24 @@ import Total.Term.CoDebruijn public export LogRel : {ctx : SnocList Ty} -> - (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> + (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) -> {ty : Ty} -> - (t : FullTerm ty ctx) -> + (t : CoTerm ty ctx) -> Type LogRel p {ty = N} t = p t LogRel p {ty = ty ~> ty'} t = (p t, {ctx' : SnocList Ty} -> (thin : ctx `Thins` ctx') -> - (u : FullTerm ty ctx') -> + (u : CoTerm ty ctx') -> LogRel p u -> LogRel p (app (wkn t thin) u)) export escape : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> {ty : Ty} -> - {0 t : FullTerm ty ctx} -> + {0 t : CoTerm ty ctx} -> LogRel P t -> P t escape {ty = N} pt = pt @@ -36,22 +36,22 @@ escape {ty = ty ~> ty'} (pt, app) = pt public export record PreserveHelper - (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) - (R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type) where + (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) + (R : {ctx, ty : _} -> CoTerm ty ctx -> CoTerm ty ctx -> Type) where constructor MkPresHelper 0 app : {ctx : SnocList Ty} -> {ty, ty' : Ty} -> - (t, u : FullTerm (ty ~> ty') ctx) -> + (t, u : CoTerm (ty ~> ty') ctx) -> {ctx' : SnocList Ty} -> (thin : ctx `Thins` ctx') -> - (v : FullTerm ty ctx') -> + (v : CoTerm ty ctx') -> R t u -> R (app (wkn t thin) v) (app (wkn u thin) v) pres : {0 ctx : SnocList Ty} -> {ty : Ty} -> - {0 t, u : FullTerm ty ctx} -> + {0 t, u : CoTerm ty ctx} -> P t -> (0 _ : R t u) -> P u @@ -60,25 +60,26 @@ record PreserveHelper export backStepHelper : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - (forall ctx, ty. {0 t, u : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u) -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> + (forall ctx, ty. {0 t, u : CoTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u) -> PreserveHelper P (flip (>) `on` CoDebruijn.toTerm) backStepHelper pres = MkPresHelper - (\t, u, thin, v, step => - rewrite toTermApp (wkn u thin) v in + (\t, u, thin, v, step => ?appStep + {- rewrite toTermApp (wkn u thin) v in rewrite toTermApp (wkn t thin) v in rewrite sym $ wknToTerm t thin in rewrite sym $ wknToTerm u thin in - AppCong1 (wknStep step)) + AppCong1 (wknStep step)-} + ) pres export preserve : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {0 R : {ctx, ty : _} -> FullTerm ty ctx -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> + {0 R : {ctx, ty : _} -> CoTerm ty ctx -> CoTerm ty ctx -> Type} -> {ty : Ty} -> - {0 t, u : FullTerm ty ctx} -> + {0 t, u : CoTerm ty ctx} -> PreserveHelper P R -> LogRel P t -> (0 _ : R t u) -> @@ -87,12 +88,12 @@ preserve help {ty = N} pt prf = help.pres pt prf preserve help {ty = ty ~> ty'} (pt, app) prf = (help.pres pt prf, \thin, v, rel => preserve help (app thin v rel) (help.app _ _ thin v prf)) -data AllLogRel : (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> CoTerms ctx ctx' -> Type where - Lin : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - AllLogRel P [<] +data AllLogRel : (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) -> Subst CoTerm ctx ctx' -> Type where + Base : + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> + AllLogRel P (Base thin) (:<) : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> AllLogRel P sub -> LogRel P t -> AllLogRel P (sub :< t) @@ -100,57 +101,55 @@ data AllLogRel : (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> CoTerms ctx c %name AllLogRel allRels index : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ((i : Elem ty ctx') -> LogRel P (var i)) -> - {sub : CoTerms ctx ctx'} -> + {sub : Subst CoTerm ctx ctx'} -> AllLogRel P sub -> (i : Elem ty ctx) -> LogRel P (index sub i) +index f Base i = f (index _ i) index f (allRels :< rel) Here = rel index f (allRels :< rel) (There i) = index f allRels i restrict : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {0 sub : CoTerms ctx' ctx''} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> + {0 sub : Subst CoTerm ctx' ctx''} -> AllLogRel P sub -> (thin : ctx `Thins` ctx') -> AllLogRel P (restrict sub thin) -restrict [<] Empty = [<] -restrict (allRels :< rel) (Drop thin) = restrict allRels thin -restrict (allRels :< rel) (Keep thin) = restrict allRels thin :< rel Valid : - (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) -> + (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) -> {ctx : SnocList Ty} -> {ty : Ty} -> - (t : FullTerm ty ctx) -> + (t : CoTerm ty ctx) -> Type Valid p t = {ctx' : SnocList Ty} -> - (sub : CoTerms ctx ctx') -> + (sub : Subst CoTerm ctx ctx') -> (allRel : AllLogRel p sub) -> LogRel p (subst t sub) public export -record ValidHelper (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) where +record ValidHelper (P : {ctx, ty : _} -> CoTerm ty ctx -> Type) where constructor MkValidHelper - var : forall ctx. Len ctx => {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (var i) - abs : forall ctx, ty. {ty' : Ty} -> {0 t : FullTerm ty' (ctx :< ty)} -> LogRel P t -> P (abs t) - zero : forall ctx. Len ctx => P {ctx} zero - suc : forall ctx. {0 t : FullTerm N ctx} -> P t -> P (suc t) + var : forall ctx. {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (var i) + abs : forall ctx, ty. {ty' : Ty} -> {0 t : CoTerm ty' (ctx :< ty)} -> LogRel P t -> P (abs t) + zero : forall ctx. P {ctx} zero + suc : forall ctx. {0 t : CoTerm N ctx} -> P t -> P (suc t) rec : {ctx : SnocList Ty} -> {ty : Ty} -> - {0 t : FullTerm N ctx} -> - {u : FullTerm ty ctx} -> - {v : FullTerm (ty ~> ty) ctx} -> + {0 t : CoTerm N ctx} -> + {u : CoTerm ty ctx} -> + {v : CoTerm (ty ~> ty) ctx} -> LogRel P t -> LogRel P u -> LogRel P v -> LogRel P (rec t u v) - step : forall ctx, ty. {0 t, u : FullTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u + step : forall ctx, ty. {0 t, u : CoTerm ty ctx} -> P t -> (0 _ : toTerm u > toTerm t) -> P u wkn : forall ctx, ctx', ty. - {0 t : FullTerm ty ctx} -> + {0 t : CoTerm ty ctx} -> P t -> (thin : ctx `Thins` ctx') -> P (wkn t thin) @@ -158,101 +157,109 @@ record ValidHelper (P : {ctx, ty : _} -> FullTerm ty ctx -> Type) where %name ValidHelper help wknRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ValidHelper P -> {ty : Ty} -> - {0 t : FullTerm ty ctx} -> + {0 t : CoTerm ty ctx} -> LogRel P t -> (thin : ctx `Thins` ctx') -> LogRel P (wkn t thin) wknRel help {ty = N} pt thin = help.wkn pt thin wknRel help {ty = ty ~> ty'} (pt, app) thin = ( help.wkn pt thin - , \thin', u, rel => - rewrite wknHomo t thin' thin in - app (thin' . thin) u rel + , \thin', u, rel => ?appURel + -- rewrite wknHomo t thin' thin in + -- app (thin' . thin) u rel ) wknAllRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ValidHelper P -> {ctx : SnocList Ty} -> - {sub : CoTerms ctx ctx'} -> + {sub : Subst CoTerm ctx ctx'} -> AllLogRel P sub -> (thin : ctx' `Thins` ctx'') -> - AllLogRel P (wknAll sub thin) -wknAllRel help [<] thin = [<] + AllLogRel P (wkn sub thin) +wknAllRel help Base thin = Base wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin shiftRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ValidHelper P -> {ctx, ctx' : SnocList Ty} -> - {sub : CoTerms ctx ctx'} -> + {sub : Subst CoTerm ctx ctx'} -> AllLogRel P sub -> - AllLogRel P (shift {ty} sub) -shiftRel help [<] = [<] + AllLogRel P (shift sub) +shiftRel help Base = Base shiftRel help (allRels :< rel) = shiftRel help allRels :< - replace {p = LogRel P} (sym $ dropIsWkn _) (wknRel help rel (Drop id)) + ?shift1 + -- replace {p = LogRel P} (sym $ dropIsWkn _) (wknRel help rel (Drop id)) liftRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ValidHelper P -> {ctx, ctx' : SnocList Ty} -> {ty : Ty} -> - {sub : CoTerms ctx ctx'} -> + {sub : Subst CoTerm ctx ctx'} -> AllLogRel P sub -> - AllLogRel P (lift {ty} sub) + AllLogRel P (lift {z = ty} sub) liftRel help allRels = shiftRel help allRels :< help.var Here -absValid : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - ValidHelper P -> - {ctx : SnocList Ty} -> - {ty, ty' : Ty} -> - (t : CoTerm ty' (ctx ++ used)) -> - (thin : used `Thins` [ - (valid : {ctx' : SnocList Ty} -> - (sub : CoTerms (ctx ++ used) ctx') -> - AllLogRel P sub -> - LogRel P (subst' t sub)) -> - {ctx' : SnocList Ty} -> - (sub : CoTerms ctx ctx') -> - AllLogRel P sub -> - LogRel P (subst' (Abs (MakeBound t thin)) sub) -absValid help t (Drop Empty) valid sub allRels = - ( help.abs (valid (shift sub) (shiftRel help allRels)) - , \thin, u, rel => - preserve - (backStepHelper help.step) - (valid (wknAll sub thin) (wknAllRel help allRels thin)) - ?betaStep - ) -absValid help t (Keep Empty) valid sub allRels = - ( help.abs (valid (lift sub) (liftRel help allRels)) - , \thin, u, rel => - preserve (backStepHelper help.step) - (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel)) - ?betaStep' - ) +-- absValid : +-- {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> +-- ValidHelper P -> +-- {ctx : SnocList Ty} -> +-- {ty, ty' : Ty} -> +-- (t : FullTerm ty' (ctx ++ used)) -> +-- (thin : used `Thins` [ +-- (valid : {ctx' : SnocList Ty} -> +-- (sub : Subst CoTerm (ctx ++ used) ctx') -> +-- AllLogRel P sub -> +-- LogRel P (subst' t sub)) -> +-- {ctx' : SnocList Ty} -> +-- (sub : Subst CoTerm ctx ctx') -> +-- AllLogRel P sub -> +-- LogRel P (subst' (Abs (MakeBound t thin)) sub) +-- absValid help t (Drop Empty) valid sub allRels = +-- ( help.abs (valid (shift sub) (shiftRel help allRels)) +-- , \thin, u, rel => +-- preserve +-- (backStepHelper help.step) +-- (valid (wkn sub thin) (wknRel help allRels thin)) +-- ?betaStep +-- ) +-- absValid help t (Keep Empty) valid sub allRels = +-- ( help.abs (valid (lift sub) (liftRel help allRels)) +-- , \thin, u, rel => +-- preserve (backStepHelper help.step) +-- (valid (wkn sub thin :< u) (wknRel help allRels thin :< rel)) +-- ?betaStep' +-- ) + +%hint +retractSingleton : Singleton ctx' -> ctx `Thins` ctx' -> Singleton ctx +retractSingleton v Id = v +retractSingleton v Empty = Val [<] +retractSingleton (Val (ctx' :< ty)) (Drop thin) = retractSingleton (Val ctx') thin +retractSingleton (Val (ctx' :< ty)) (Keep thin) = pure (:< ty) <*> retractSingleton (Val ctx') thin export allValid : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ValidHelper P -> (s : Singleton ctx) => {ty : Ty} -> - (t : FullTerm ty ctx) -> + (t : CoTerm ty ctx) -> Valid P t allValid' : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> ValidHelper P -> (s : Singleton ctx) => {ty : Ty} -> - (t : CoTerm ty ctx) -> + (t : FullTerm ty ctx) -> {ctx' : SnocList Ty} -> - (sub : CoTerms ctx ctx') -> + (sub : Subst CoTerm ctx ctx') -> AllLogRel P sub -> LogRel P (subst' t sub) @@ -260,14 +267,17 @@ allValid help (t `Over` thin) sub allRels = allValid' help t (restrict sub thin) (restrict allRels thin) allValid' help Var sub allRels = index help.var allRels Here -allValid' help {s = Val ctx} (Abs {ty, ty'} (MakeBound t thin)) sub allRels = - let s' = [| Val ctx ++ retractSingleton (Val [)} -- -- eq -- -- (AppBeta (length _))) @@ -333,23 +343,25 @@ allValid' help (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub allRels = -- -- let relv = allValid help v sub allRels in -- -- help.rec relt relu relv -idRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> - {ctx : SnocList Ty} -> - ValidHelper P -> - AllLogRel P {ctx} (Base Thinning.id) -idRel help {ctx = [<]} = [<] -idRel help {ctx = ctx :< ty} = liftRel help (idRel help) +-- idRel : +-- {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> +-- {ctx : SnocList Ty} -> +-- ValidHelper P -> +-- AllLogRel P {ctx} (Base Thinning.id) +-- idRel help {ctx = [<]} = [<] +-- idRel help {ctx = ctx :< ty} = liftRel help (idRel help) export allRel : - {0 P : {ctx, ty : _} -> FullTerm ty ctx -> Type} -> + {0 P : {ctx, ty : _} -> CoTerm ty ctx -> Type} -> {ctx : SnocList Ty} -> {ty : Ty} -> ValidHelper P -> - (t : FullTerm ty ctx) -> + (t : CoTerm ty ctx) -> P t allRel help t = - rewrite sym $ substId t in - escape {P} $ - allValid help @{Val ctx} t (Base id) (idRel help) + let rel = allValid help t (Base Id) Base in + ?allRel_rhs + -- rewrite sym $ substId t in + -- escape {P} $ + -- allValid help @{Val ctx} t Base (idRel help) diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr index a7aba57..c3f16cf 100644 --- a/src/Total/NormalForm.idr +++ b/src/Total/NormalForm.idr @@ -29,7 +29,8 @@ data Neutral' where data Normal' where Ntrl : Neutral' t -> Normal' t - Abs : Normal' t -> Normal' (Abs (MakeBound t thin)) + Const : Normal' t -> Normal' (Const t) + Abs : Normal' t -> Normal' (Abs t) Zero : Normal' Zero Suc : Normal' t -> Normal' (Suc t) @@ -119,7 +120,7 @@ recNf'' Zero thin n relU relV = backStepsRel relU [ Prec -> Term ctx ty -> Doc Syntax - prettyTerm len d (Var i) = bound (pretty $ index (minus (cast len) (S $ elemToNat i)) names) + prettyTerm len d (Var i) = bound (pretty $ index (minus (lenToNat len) (S $ elemToNat i)) names) prettyTerm len d (Abs t) = let Evidence _ (len, t') = getLamNames (S len) t in parenthesise (d > startPrec) $ group $ align $ hang 2 $ @@ -73,7 +73,7 @@ parameters (names : Stream String) bound (pretty $ index offset names) <+> comma <++> prettyBindings' (S offset) (S k) prettyBindings : Len ctx' -> Doc Syntax - prettyBindings k = prettyBindings' (cast len) (minus (cast k) (cast len)) + prettyBindings k = prettyBindings' (lenToNat len) (minus (lenToNat k) (lenToNat len)) prettyTerm len d app@(App t u) = let (f, ts) = getSpline t [prettyArg u] in parenthesise (d >= appPrec) $ group $ align $ hang 2 $ diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr index a424515..4566724 100644 --- a/src/Total/Reduction.idr +++ b/src/Total/Reduction.idr @@ -4,13 +4,11 @@ import Syntax.PreorderReasoning import Total.Term public export -data (>) : Term ctx ty -> Term ctx ty -> Type where +data (>) : Term ty ctx -> Term ty ctx -> 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 : - (0 len : Len ctx) -> - App (Abs t) u > subst t (Base (id @{len}) :< u) + AppBeta : App (Abs t) u > subst t (Base Id :< 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 @@ -21,7 +19,7 @@ data (>) : Term ctx ty -> Term ctx ty -> Type where %name Reduction.(>) step public export -data (>=) : Term ctx ty -> Term ctx ty -> Type where +data (>=) : Term ty ctx -> Term ty ctx -> Type where Lin : t >= t (:<) : t >= u -> u > v -> t >= v @@ -70,37 +68,27 @@ RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step -- Properties ------------------------------------------------------------------ lemma : - (t : Term (ctx :< ty) ty') -> + (t : Term ty' (ctx :< ty)) -> (thin : ctx `Thins` ctx') -> - (u : Term ctx ty) -> - subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = - wkn (subst t (Base Thinning.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 (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 @{length ctx}) :< u) thin) + (u : Term ty ctx) -> + wkn (subst t (Base Id :< u)) thin = + subst (wkn t (Keep thin)) (Base Id :< wkn u thin) +lemma t thin u = Calc $ + |~ wkn (subst t (Base Id :< u)) thin + ~~ subst t (wkn (Base Id :< u) thin) ...(wknSubst t (Base Id :< u) thin) + ~~ subst t (Base (thin . Id) :< wkn u thin) ...(Refl) + ~~ subst t (Base thin :< wkn u thin) ...(substCong t (Base (identityRight thin) :< Refl)) + ~~ subst t (Base (Id . thin) :< wkn u thin) ...(Refl) + ~~ subst t (restrict (Base Id) thin :< wkn u thin) ...(substCong t (restrictBase Id thin :< Refl)) + ~~ subst t (restrict (Base Id :< wkn u thin) (Keep thin)) ...(Refl) + ~~ subst (wkn t (Keep thin)) (Base Id :< wkn u thin) ..<(substWkn t (Base Id :< wkn u thin) (Keep 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 len {ctx, t, u}) {thin} = - let - 0 eq : - (subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = - wkn (subst t (Base (id @{len}) :< u)) thin) - eq = rewrite lenUnique len (length ctx) in lemma t thin u - in - rewrite sym eq in - AppBeta _ +wknStep (AppBeta {t, u}) {thin} = rewrite lemma 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 fead586..2710ad3 100644 --- a/src/Total/Syntax.idr +++ b/src/Total/Syntax.idr @@ -10,35 +10,43 @@ import public Total.Term.CoDebruijn infixr 20 ~>* infixl 9 .~, .* +public export +data Len : SnocList a -> Type where + Z : Len [<] + S : Len sx -> Len (sx :< x) + +%name Len k + +export +lenToNat : Len sx -> Nat +lenToNat Z = 0 +lenToNat (S k) = S (lenToNat k) + public export (~>*) : SnocList Ty -> Ty -> Ty tys ~>* ty = foldr (~>) ty tys public export -0 Fun : {sx : SnocList a} -> Len sx -> (a -> Type) -> Type -> Type -Fun Z arg ret = ret -Fun (S {x = ty} k) arg ret = Fun k arg (arg ty -> ret) - -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 sx) -> - (forall x. p x -> q x) -> - Fun k q ret -> - Fun k p ret -before Z f x = x -before (S k) f x = before k f (after k (. f) x) +0 Fun : (sx : SnocList a) -> (a -> Type) -> Type -> Type +Fun [<] p ret = ret +Fun (sx :< x) p ret = Fun sx p (p x -> ret) + +after : Len sx -> (r -> s) -> Fun sx p r -> Fun sx p s +after Z f = f +after (S k) f = after k (f .) + +before : Len sx -> (forall x. p x -> q x) -> Fun sx q ret -> Fun sx p ret +before Z f = id +before (S k) f = before k f . after k (. f) export -lit : Len ctx => Nat -> FullTerm N ctx -lit 0 = Zero `Over` empty +lit : Nat -> FullTerm N ctx +lit 0 = Zero `Over` Empty lit (S n) = suc (lit n) absHelper : - (k : Len tys) -> - Fun k (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) -> + Len tys -> + Fun tys (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) -> FullTerm (tys ~>* ty) ctx absHelper Z x = x absHelper (S k) x = @@ -48,11 +56,10 @@ absHelper (S k) x = export abs' : - (len : Len ctx) => - (k : Len tys) -> - Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) -> + Len tys -> + Fun tys (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) -> FullTerm (tys ~>* ty) ctx -abs' k = absHelper k . before k (var @{lenAppend len k}) +abs' k = absHelper k . before k var export app' : @@ -97,7 +104,6 @@ app' t (us :< u) = app (app' t us) u export (.) : - Len ctx => {ty, ty' : Ty} -> FullTerm (ty' ~> ty'') ctx -> FullTerm (ty ~> ty') ctx -> @@ -106,7 +112,6 @@ t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x)) export (.*) : - Len ctx => {ty : Ty} -> {tys : SnocList Ty} -> FullTerm (ty ~> ty') ctx -> @@ -116,13 +121,9 @@ export (.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .* u export -lift : Len ctx => FullTerm ty [<] -> FullTerm ty ctx -lift t = wkn t empty - -export -id' : CoTerm (ty ~> ty) [<] -id' = Abs (MakeBound Var (Keep Empty)) +lift : FullTerm ty [<] -> FullTerm ty ctx +lift t = wkn t Empty export id : FullTerm (ty ~> ty) [<] -id = id' `Over` empty +id = Abs Var `Over` Empty 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) diff --git a/src/Total/Term/CoDebruijn.idr b/src/Total/Term/CoDebruijn.idr index 0efcdbb..8c8ba13 100644 --- a/src/Total/Term/CoDebruijn.idr +++ b/src/Total/Term/CoDebruijn.idr @@ -10,98 +10,75 @@ import Total.Term -- Definition ------------------------------------------------------------------ public export -data CoTerm : Ty -> SnocList Ty -> Type where - Var : CoTerm ty [ CoTerm (ty ~> ty') ctx - App : {ty : Ty} -> Pair (CoTerm (ty ~> ty')) (CoTerm ty) ctx -> CoTerm ty' ctx - Zero : CoTerm N [<] - Suc : CoTerm N ctx -> CoTerm N ctx - Rec : Pair (CoTerm N) (Pair (CoTerm ty) (CoTerm (ty ~> ty))) ctx -> CoTerm ty ctx +data FullTerm : Ty -> SnocList Ty -> Type where + Var : FullTerm ty [ FullTerm (ty ~> ty') ctx + Abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx + App : {ty : Ty} -> Pair (FullTerm (ty ~> ty')) (FullTerm ty) ctx -> FullTerm ty' ctx + Zero : FullTerm N [<] + Suc : FullTerm N ctx -> FullTerm N ctx + Rec : Pair (FullTerm N) (Pair (FullTerm ty) (FullTerm (ty ~> ty))) ctx -> FullTerm ty ctx -%name CoTerm t, u, v +%name FullTerm t, u, v public export -FullTerm : Ty -> SnocList Ty -> Type -FullTerm ty ctx = Thinned (CoTerm ty) ctx +CoTerm : Ty -> SnocList Ty -> Type +CoTerm ty ctx = Thinned (FullTerm ty) ctx -- Smart Constructors ---------------------------------------------------------- public export -var : Len ctx => Elem ty ctx -> FullTerm ty ctx -var i = Var `Over` point i +var : Elem ty ctx -> CoTerm ty ctx +var i = Var `Over` Point i public export -abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx -abs = map Abs . MkBound (S Z) +abs : CoTerm ty' (ctx :< ty) -> CoTerm (ty ~> ty') ctx +abs (t `Over` Id) = Abs t `Over` Id +abs (t `Over` Empty) = Const t `Over` Empty +abs (t `Over` Drop thin) = Const t `Over` thin +abs (t `Over` Keep thin) = Abs t `Over` thin public export -app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx +app : {ty : Ty} -> CoTerm (ty ~> ty') ctx -> CoTerm ty ctx -> CoTerm ty' ctx app t u = map App (MkPair t u) public export -zero : Len ctx => FullTerm N ctx -zero = Zero `Over` empty +zero : CoTerm N ctx +zero = Zero `Over` Empty public export -suc : FullTerm N ctx -> FullTerm N ctx +suc : CoTerm N ctx -> CoTerm N ctx suc = map Suc public export -rec : FullTerm N ctx -> FullTerm ty ctx -> FullTerm (ty ~> ty) ctx -> FullTerm ty ctx +rec : CoTerm N ctx -> CoTerm ty ctx -> CoTerm (ty ~> ty) ctx -> CoTerm ty ctx rec t u v = map Rec $ MkPair t (MkPair u v) --- Substitutions --------------------------------------------------------------- +-- Raw Interfaces -------------------------------------------------------------- -public export -data CoTerms : SnocList Ty -> SnocList Ty -> Type where - Lin : CoTerms [<] ctx' - (:<) : CoTerms ctx ctx' -> FullTerm ty ctx' -> CoTerms (ctx :< ty) ctx' - -%name CoTerms sub - -public export -index : CoTerms ctx ctx' -> Elem ty ctx -> FullTerm ty ctx' -index (sub :< t) Here = t -index (sub :< t) (There i) = index sub i - -public export -wknAll : CoTerms ctx ctx' -> ctx' `Thins` ctx'' -> CoTerms ctx ctx'' -wknAll [<] thin = [<] -wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin - -public export -shift : CoTerms ctx ctx' -> CoTerms ctx (ctx' :< ty) -shift [<] = [<] -shift (sub :< t) = shift sub :< drop t - -public export -lift : Len ctx' => CoTerms ctx ctx' -> CoTerms (ctx :< ty) (ctx' :< ty) -lift sub = shift sub :< var Here +export +Point Ty CoTerm where + point = var -public export -restrict : CoTerms ctx' ctx'' -> ctx `Thins` ctx' -> CoTerms ctx ctx'' -restrict [<] Empty = [<] -restrict (sub :< t) (Drop thin) = restrict sub thin -restrict (sub :< t) (Keep thin) = restrict sub thin :< t +export +Weaken Ty CoTerm where + wkn = Thinning.wkn + drop = Thinning.drop -public export -Base : (len : Len ctx') => ctx `Thins` ctx' -> CoTerms ctx ctx' -Base Empty = [<] -Base {len = S k} (Drop thin) = shift (Base thin) -Base {len = S k} (Keep thin) = lift (Base thin) +export PointWeaken Ty CoTerm where -- Substitution Operation ------------------------------------------------------ public export -subst : Len ctx' => FullTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx' +subst : CoTerm ty ctx -> Subst CoTerm ctx ctx' -> CoTerm ty ctx' public export -subst' : Len ctx' => CoTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx' +subst' : FullTerm ty ctx -> Subst CoTerm ctx ctx' -> CoTerm ty ctx' subst (t `Over` thin) sub = subst' t (restrict sub thin) subst' Var sub = index sub Here -subst' (Abs (MakeBound t (Drop Empty))) sub = abs (subst' t $ shift sub) -subst' (Abs (MakeBound t (Keep Empty))) sub = abs (subst' t $ lift sub) +subst' (Const t) sub = abs (drop $ subst' t sub) +subst' (Abs t) sub = abs (subst' t $ lift sub) subst' (App (MakePair t u _)) sub = app (subst t sub) (subst u sub) subst' Zero sub = zero subst' (Suc t) sub = suc (subst' t sub) @@ -110,10 +87,10 @@ subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub = -- Initiality ------------------------------------------------------------------ -toTerm' : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty +toTerm' : FullTerm ty ctx -> ctx `Thins` ctx' -> Term ty ctx' toTerm' Var thin = Var (index thin Here) -toTerm' (Abs (MakeBound t (Drop Empty))) thin = Abs (toTerm' t (Drop thin)) -toTerm' (Abs (MakeBound t (Keep Empty))) thin = Abs (toTerm' t (Keep thin)) +toTerm' (Const t) thin = Abs (toTerm' t (Drop thin)) +toTerm' (Abs t) thin = Abs (toTerm' t (Keep thin)) toTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin = App (toTerm' t (thin . thin1)) (toTerm' u (thin . thin2)) toTerm' Zero thin = Zero @@ -130,188 +107,184 @@ toTerm' (toTerm' v ((thin . thin') . thin3)) export -toTerm : FullTerm ty ctx -> Term ctx ty +toTerm : CoTerm ty ctx -> Term ty ctx toTerm (t `Over` thin) = toTerm' t thin -public export -toTerms : Len ctx' => CoTerms ctx ctx' -> Terms ctx' ctx -toTerms [<] = Base empty -toTerms (sub :< t) = toTerms sub :< toTerm t - export -Cast (FullTerm ty ctx) (Term ctx ty) where - cast = toTerm - -export -Len ctx' => Cast (CoTerms ctx ctx') (Terms ctx' ctx) where - cast = toTerms - -export -Len ctx => Cast (Term ctx ty) (FullTerm ty ctx) where - cast (Var i) = Var `Over` point i - cast (Abs t) = abs (cast t) - cast (App {ty} t u) = app {ty} (cast t) (cast u) - cast Zero = zero - cast (Suc t) = suc (cast t) - cast (Rec t u v) = rec (cast t) (cast u) (cast v) +fromTerm : Term ty ctx -> CoTerm ty ctx +fromTerm (Var i) = var i +fromTerm (Abs t) = abs (fromTerm t) +fromTerm (App t u) = app (fromTerm t) (fromTerm u) +fromTerm Zero = zero +fromTerm (Suc t) = suc (fromTerm t) +fromTerm (Rec t u v) = rec (fromTerm t) (fromTerm u) (fromTerm v) -- Properties ------------------------------------------------------------------ -wknToTerm' : - (t : CoTerm ty ctx) -> - (thin : ctx `Thins` ctx') -> - (thin' : ctx' `Thins` ctx''') -> - wkn (toTerm' t thin) thin' = toTerm' t (thin' . thin) -wknToTerm' Var thin thin' = cong Var (indexHomo thin' thin Here) -wknToTerm' (Abs (MakeBound t (Drop Empty))) thin thin' = - cong Abs (wknToTerm' t (Drop thin) (Keep thin')) -wknToTerm' (Abs (MakeBound t (Keep Empty))) thin thin' = - cong Abs (wknToTerm' t (Keep thin) (Keep thin')) -wknToTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin thin' = - rewrite sym $ assoc thin' thin thin1 in - rewrite sym $ assoc thin' thin thin2 in - cong2 App (wknToTerm' t (thin . thin1) thin') (wknToTerm' u (thin . thin2) thin') -wknToTerm' Zero thin thin' = Refl -wknToTerm' (Suc t) thin thin' = cong Suc (wknToTerm' t thin thin') -wknToTerm' - (Rec - (MakePair - (t `Over` thin1) - (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin'') _)) - thin - thin' = - rewrite sym $ assoc thin' thin thin1 in - rewrite sym $ assoc (thin' . thin) thin'' thin2 in - rewrite sym $ assoc thin' thin (thin'' . thin2) in - rewrite sym $ assoc thin thin'' thin2 in - rewrite sym $ assoc (thin' . thin) thin'' thin3 in - rewrite sym $ assoc thin' thin (thin'' . thin3) in - rewrite sym $ assoc thin thin'' thin3 in - cong3 Rec - (wknToTerm' t (thin . thin1) thin') - (wknToTerm' u (thin . (thin'' . thin2)) thin') - (wknToTerm' v (thin . (thin'' . thin3)) thin') - -export -wknToTerm : - (t : FullTerm ty ctx) -> - (thin : ctx `Thins` ctx') -> - wkn (toTerm t) thin = toTerm (wkn t thin) -wknToTerm (t `Over` thin') thin = wknToTerm' t thin' thin - -export -toTermVar : Len ctx => (i : Elem ty ctx) -> toTerm (var i) = Var i -toTermVar i = cong Var $ indexPoint i - -export -toTermApp : - (t : FullTerm (ty ~> ty') ctx) -> - (u : FullTerm ty ctx) -> - toTerm (app t u) = App (toTerm t) (toTerm u) -toTermApp (t `Over` thin1) (u `Over` thin2) = - cong2 App - (cong (toTerm' t) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).left) - (cong (toTerm' u) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).right) - -indexShift : - (sub : CoTerms ctx ctx') -> - (i : Elem ty ctx) -> - index (shift sub) i = drop (index sub i) -indexShift (sub :< t) Here = Refl -indexShift (sub :< t) (There i) = indexShift sub i - -indexBase : (thin : [ index (Base thin) Here = Var `Over` thin -indexBase (Drop thin) = trans (indexShift (Base thin) Here) (cong drop (indexBase thin)) -indexBase (Keep thin) = irrelevantEq $ cong ((Var `Over`) . Keep) $ emptyUnique empty thin - -restrictShift : - (sub : CoTerms ctx' ctx'') -> - (thin : ctx `Thins` ctx') -> - restrict (shift sub) thin = shift (restrict sub thin) -restrictShift [<] Empty = Refl -restrictShift (sub :< t) (Drop thin) = restrictShift sub thin -restrictShift (sub :< t) (Keep thin) = cong (:< drop t) (restrictShift sub thin) - -restrictBase : - (thin2 : ctx' `Thins` ctx'') -> - (thin1 : ctx `Thins` ctx') -> - CoDebruijn.restrict (Base thin2) thin1 = Base (thin2 . thin1) -restrictBase Empty Empty = Refl -restrictBase (Drop thin2) thin1 = - trans - (restrictShift (Base thin2) thin1) - (cong shift $ restrictBase thin2 thin1) -restrictBase (Keep thin2) (Drop thin1) = - trans - (restrictShift (Base thin2) thin1) - (cong shift $ restrictBase thin2 thin1) -restrictBase (Keep thin2) (Keep thin1) = - cong (:< (Var `Over` point Here)) $ - trans - (restrictShift (Base thin2) thin1) - (cong shift $ restrictBase thin2 thin1) - -substBase : - (t : CoTerm ty ctx) -> - (thin : ctx `Thins` ctx') -> - subst' t (Base thin) = t `Over` thin -substBase Var thin = indexBase thin -substBase (Abs (MakeBound t (Drop Empty))) thin = - Calc $ - |~ map Abs (MkBound (S Z) (subst' t (shift $ Base thin))) - ~~ map Abs (MkBound (S Z) (t `Over` Drop thin)) - ...(cong (map Abs . MkBound (S Z)) $ substBase t (Drop thin)) - ~~ map Abs (MakeBound t (Drop Empty) `Over` thin) - ...(Refl) - ~~ (Abs (MakeBound t (Drop Empty)) `Over` thin) - ...(Refl) -substBase (Abs (MakeBound t (Keep Empty))) thin = - Calc $ - |~ map Abs (MkBound (S Z) (subst' t (lift $ Base thin))) - ~~ map Abs (MkBound (S Z) (t `Over` Keep thin)) - ...(cong (map Abs . MkBound (S Z)) $ substBase t (Keep thin)) - ~~ map Abs (MakeBound t (Keep Empty) `Over` thin) - ...(Refl) - ~~ (Abs (MakeBound t (Keep Empty)) `Over` thin) - ...(Refl) -substBase (App (MakePair (t `Over` thin1) (u `Over` thin2) cover)) thin = - rewrite restrictBase thin thin1 in - rewrite restrictBase thin thin2 in - rewrite substBase t (thin . thin1) in - rewrite substBase u (thin . thin2) in - rewrite coprodEta thin cover in - Refl -substBase Zero thin = cong (Zero `Over`) $ irrelevantEq $ emptyUnique empty thin -substBase (Suc t) thin = cong (map Suc) $ substBase t thin -substBase - (Rec (MakePair - (t `Over` thin1) - (MakePair - (u `Over` thin2) - (v `Over` thin3) - cover' - `Over` thin') - cover)) - thin = - rewrite restrictBase thin thin1 in - rewrite restrictBase thin thin' in - rewrite restrictBase (thin . thin') thin2 in - rewrite restrictBase (thin . thin') thin3 in - rewrite substBase t (thin . thin1) in - rewrite substBase u ((thin . thin') . thin2) in - rewrite substBase v ((thin . thin') . thin3) in - rewrite coprodEta (thin . thin') cover' in - rewrite coprodEta thin cover in - Refl +-- Weakening export -substId : (t : FullTerm ty ctx) -> subst t (Base Thinning.id) = t -substId (t `Over` thin) = - Calc $ - |~ subst' t (restrict (Base id) thin) - ~~ subst' t (Base $ id . thin) - ...(cong (subst' t) $ restrictBase id thin) - ~~ subst' t (Base thin) - ...(cong (subst' t . Base) $ identityLeft thin) - ~~ (t `Over` thin) - ...(substBase t thin) +FullWeaken Ty CoTerm where + dropIsWkn (t `Over` thin) = ?dropIsWkn_rhs + + wknCong = ?wknCong_rhs + + wknId = ?wknId_rhs + + wknHomo = ?wknHomo_rhs + +-- -- wknToTerm' : +-- -- (t : FullTerm ty ctx) -> +-- -- (thin : ctx `Thins` ctx') -> +-- -- (thin' : ctx' `Thins` ctx''') -> +-- -- wkn (toTerm' t thin) thin' = toTerm' t (thin' . thin) +-- -- wknToTerm' Var thin thin' = cong Var (indexHomo thin' thin Here) +-- -- wknToTerm' (Abs (MakeBound t (Drop Empty))) thin thin' = +-- -- cong Abs (wknToTerm' t (Drop thin) (Keep thin')) +-- -- wknToTerm' (Abs (MakeBound t (Keep Empty))) thin thin' = +-- -- cong Abs (wknToTerm' t (Keep thin) (Keep thin')) +-- -- wknToTerm' (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin thin' = +-- -- rewrite sym $ assoc thin' thin thin1 in +-- -- rewrite sym $ assoc thin' thin thin2 in +-- -- cong2 App (wknToTerm' t (thin . thin1) thin') (wknToTerm' u (thin . thin2) thin') +-- -- wknToTerm' Zero thin thin' = Refl +-- -- wknToTerm' (Suc t) thin thin' = cong Suc (wknToTerm' t thin thin') +-- -- wknToTerm' +-- -- (Rec +-- -- (MakePair +-- -- (t `Over` thin1) +-- -- (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin'') _)) +-- -- thin +-- -- thin' = +-- -- rewrite sym $ assoc thin' thin thin1 in +-- -- rewrite sym $ assoc (thin' . thin) thin'' thin2 in +-- -- rewrite sym $ assoc thin' thin (thin'' . thin2) in +-- -- rewrite sym $ assoc thin thin'' thin2 in +-- -- rewrite sym $ assoc (thin' . thin) thin'' thin3 in +-- -- rewrite sym $ assoc thin' thin (thin'' . thin3) in +-- -- rewrite sym $ assoc thin thin'' thin3 in +-- -- cong3 Rec +-- -- (wknToTerm' t (thin . thin1) thin') +-- -- (wknToTerm' u (thin . (thin'' . thin2)) thin') +-- -- (wknToTerm' v (thin . (thin'' . thin3)) thin') + +-- -- export +-- -- wknToTerm : +-- -- (t : CoTerm ty ctx) -> +-- -- (thin : ctx `Thins` ctx') -> +-- -- wkn (toTerm t) thin = toTerm (wkn t thin) +-- -- wknToTerm (t `Over` thin') thin = wknToTerm' t thin' thin + +-- -- export +-- -- toTermVar : Len ctx => (i : Elem ty ctx) -> toTerm (var i) = Var i +-- -- toTermVar i = cong Var $ indexPoint i + +-- -- export +-- -- toTermApp : +-- -- (t : CoTerm (ty ~> ty') ctx) -> +-- -- (u : CoTerm ty ctx) -> +-- -- toTerm (app t u) = App (toTerm t) (toTerm u) +-- -- toTermApp (t `Over` thin1) (u `Over` thin2) = +-- -- cong2 App +-- -- (cong (toTerm' t) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).left) +-- -- (cong (toTerm' u) $ irrelevantEq $ triangleCorrect (coprod thin1 thin2).right) + +-- -- indexShift : +-- -- (sub : Subst CoTerm ctx ctx') -> +-- -- (i : Elem ty ctx) -> +-- -- index (shift sub) i = drop (index sub i) +-- -- indexShift (sub :< t) Here = Refl +-- -- indexShift (sub :< t) (There i) = indexShift sub i + +-- -- indexBase : (thin : [ index (Base thin) Here = Var `Over` thin +-- -- indexBase (Drop thin) = trans (indexShift (Base thin) Here) (cong drop (indexBase thin)) +-- -- indexBase (Keep thin) = irrelevantEq $ cong ((Var `Over`) . Keep) $ emptyUnique empty thin + +-- -- restrictShift : +-- -- (sub : Subst CoTerm ctx' ctx'') -> +-- -- (thin : ctx `Thins` ctx') -> +-- -- restrict (shift sub) thin = shift (restrict sub thin) +-- -- restrictShift [<] Empty = Refl +-- -- restrictShift (sub :< t) (Drop thin) = restrictShift sub thin +-- -- restrictShift (sub :< t) (Keep thin) = cong (:< drop t) (restrictShift sub thin) + +-- -- restrictBase : +-- -- (thin2 : ctx' `Thins` ctx'') -> +-- -- (thin1 : ctx `Thins` ctx') -> +-- -- CoDebruijn.restrict (Base thin2) thin1 = Base (thin2 . thin1) +-- -- restrictBase Empty Empty = Refl +-- -- restrictBase (Drop thin2) thin1 = +-- -- trans +-- -- (restrictShift (Base thin2) thin1) +-- -- (cong shift $ restrictBase thin2 thin1) +-- -- restrictBase (Keep thin2) (Drop thin1) = +-- -- trans +-- -- (restrictShift (Base thin2) thin1) +-- -- (cong shift $ restrictBase thin2 thin1) +-- -- restrictBase (Keep thin2) (Keep thin1) = +-- -- cong (:< (Var `Over` point Here)) $ +-- -- trans +-- -- (restrictShift (Base thin2) thin1) +-- -- (cong shift $ restrictBase thin2 thin1) + +-- substBase : +-- (t : FullTerm ty ctx) -> +-- (thin : ctx `Thins` ctx') -> +-- subst' t (Base thin) = t `Over` thin +-- -- substBase Var thin = indexBase thin +-- -- substBase (Abs (MakeBound t (Drop Empty))) thin = +-- -- Calc $ +-- -- |~ map Abs (MkBound (S Z) (subst' t (shift $ Base thin))) +-- -- ~~ map Abs (MkBound (S Z) (t `Over` Drop thin)) +-- -- ...(cong (map Abs . MkBound (S Z)) $ substBase t (Drop thin)) +-- -- ~~ map Abs (MakeBound t (Drop Empty) `Over` thin) +-- -- ...(Refl) +-- -- ~~ (Abs (MakeBound t (Drop Empty)) `Over` thin) +-- -- ...(Refl) +-- -- substBase (Abs (MakeBound t (Keep Empty))) thin = +-- -- Calc $ +-- -- |~ map Abs (MkBound (S Z) (subst' t (lift $ Base thin))) +-- -- ~~ map Abs (MkBound (S Z) (t `Over` Keep thin)) +-- -- ...(cong (map Abs . MkBound (S Z)) $ substBase t (Keep thin)) +-- -- ~~ map Abs (MakeBound t (Keep Empty) `Over` thin) +-- -- ...(Refl) +-- -- ~~ (Abs (MakeBound t (Keep Empty)) `Over` thin) +-- -- ...(Refl) +-- -- substBase (App (MakePair (t `Over` thin1) (u `Over` thin2) cover)) thin = +-- -- rewrite restrictBase thin thin1 in +-- -- rewrite restrictBase thin thin2 in +-- -- rewrite substBase t (thin . thin1) in +-- -- rewrite substBase u (thin . thin2) in +-- -- rewrite coprodEta thin cover in +-- -- Refl +-- -- substBase Zero thin = cong (Zero `Over`) $ irrelevantEq $ emptyUnique empty thin +-- -- substBase (Suc t) thin = cong (map Suc) $ substBase t thin +-- -- substBase +-- -- (Rec (MakePair +-- -- (t `Over` thin1) +-- -- (MakePair +-- -- (u `Over` thin2) +-- -- (v `Over` thin3) +-- -- cover' +-- -- `Over` thin') +-- -- cover)) +-- -- thin = +-- -- rewrite restrictBase thin thin1 in +-- -- rewrite restrictBase thin thin' in +-- -- rewrite restrictBase (thin . thin') thin2 in +-- -- rewrite restrictBase (thin . thin') thin3 in +-- -- rewrite substBase t (thin . thin1) in +-- -- rewrite substBase u ((thin . thin') . thin2) in +-- -- rewrite substBase v ((thin . thin') . thin3) in +-- -- rewrite coprodEta (thin . thin') cover' in +-- -- rewrite coprodEta thin cover in +-- -- Refl + +-- export +-- substId : (t : CoTerm ty ctx) -> subst t (Base Id) = t +-- substId (t `Over` thin) = +-- Calc $ +-- |~ subst' t (restrict (Base Id) thin) +-- ~~ subst' t (Base (Id . thin)) ...(cong (subst' t) $ restrictBase Id thin) +-- ~~ subst' t (Base thin) ...(Refl) +-- ~~ (t `Over` thin) ...(substBase t thin) -- cgit v1.2.3