Write an encoding for data types.

6 files changed, 683 insertions, 12 deletions

diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr
new file mode 100644
index 0000000..705d74b
--- /dev/null
+++ b/src/Total/Encoded/Util.idr
@@ -0,0 +1,437 @@
+module Total.Encoded.Util
+
+import public Data.Fin
+import public Data.List1
+import public Data.List.Elem
+import public Data.List.Quantifiers
+import public Total.Syntax
+
+%prefix_record_projections off
+
+namespace Bool
+  export
+  B : Ty
+  B = N
+
+  export
+  True : Term ctx B
+  True = Zero
+
+  export
+  False : Term ctx B
+  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))
+
+namespace Arb
+  export
+  arb : {ty : Ty} -> Term [<] ty
+  arb {ty = N} = Zero
+  arb {ty = ty ~> ty'} = Abs (lift arb)
+
+namespace Union
+  export
+  (<+>) : Ty -> Ty -> Ty
+  N <+> N = N
+  N <+> (u ~> u') = u ~> u'
+  (t ~> t') <+> N = t ~> t'
+  (t ~> t') <+> (u ~> u') = (t <+> u) ~> (t' <+> u')
+
+  export
+  injL : {t, u : Ty} -> Term [<] (t ~> (t <+> u))
+  export
+  injR : {t, u : Ty} -> Term [<] (u ~> (t <+> u))
+  export
+  prjL : {t, u : Ty} -> Term [<] ((t <+> u) ~> t)
+  export
+  prjR : {t, u : Ty} -> Term [<] ((t <+> u) ~> u)
+
+  injL {t = N, u = N} = Abs' (S Z) id
+  injL {t = N, u = u ~> u'} = Abs' (S $ S Z) (\n, _ => App (lift (prjR . injL)) n)
+  injL {t = t ~> t', u = N} = Abs' (S Z) id
+  injL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injL . f . lift prjL)
+
+  injR {t = N, u = N} = Abs' (S Z) id
+  injR {t = N, u = u ~> u'} = Abs' (S Z) id
+  injR {t = t ~> t', u = N} = Abs' (S $ S Z) (\n, _ => App (lift (prjL . injR)) n)
+  injR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injR . f . lift prjR)
+
+  prjL {t = N, u = N} = Abs' (S Z) id
+  prjL {t = N, u = u ~> u'} = Abs' (S Z) (\f => App (lift (prjL . injR) . f) (lift $ arb))
+  prjL {t = t ~> t', u = N} = Abs' (S Z) id
+  prjL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjL . f . lift injL)
+
+  prjR {t = N, u = N} = Abs' (S Z) id
+  prjR {t = N, u = u ~> u'} = Abs' (S Z) id
+  prjR {t = t ~> t', u = N} = Abs' (S Z) (\f => App (lift (prjR . injL) . f) (lift $ arb))
+  prjR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjR . f . lift injR)
+
+namespace Unit
+  export
+  Unit : Ty
+  Unit = N
+
+namespace Pair
+  export
+  (*) : Ty -> Ty -> Ty
+  t * u = B ~> (t <+> u)
+
+  export
+  pair : {t, u : Ty} -> Term [<] (t ~> u ~> (t * u))
+  pair = Abs' (S $ S $ S Z)
+    (\fst, snd, b => If b (App (lift injL) fst) (App (lift injR) snd))
+
+  export
+  fst : {t, u : Ty} -> Term [<] ((t * u) ~> t)
+  fst = Abs' (S Z) (\p => App (lift prjL . p) True)
+
+  export
+  snd : {t, u : Ty} -> Term [<] ((t * u) ~> u)
+  snd = Abs' (S Z) (\p => App (lift prjR . p) False)
+
+  export
+  mapSnd : {t, u, v : Ty} -> Term [<] ((u ~> v) ~> (t * u) ~> (t * v))
+  mapSnd = Abs' (S $ S Z) (\f, p => App' (lift pair) [<App (lift fst) p , App (f . lift snd) p])
+
+  export
+  Product : SnocList Ty -> Ty
+  Product = foldl (*) Unit
+
+  export
+  pair' : {tys : SnocList Ty} -> Term [<] (tys ~>* Product tys)
+  pair' {tys = [<]} = arb
+  pair' {tys = tys :< ty} = Abs' (S $ S Z) (\p, t => App' (lift pair) [<p, t]) .* pair' {tys}
+
+  export
+  project : {tys : SnocList Ty} -> Elem ty tys -> Term [<] (Product tys ~> ty)
+  project {tys = tys :< ty} Here = snd
+  project {tys = tys :< ty} (There i) = project i . fst
+
+  export
+  mapProd :
+    {ctx, tys, tys' : SnocList Ty} ->
+    {auto 0 prf : length tys = length tys'} ->
+    All (Term ctx) (zipWith (~>) tys tys') ->
+    Term ctx (Product tys ~> Product tys')
+  mapProd {tys = [<], tys' = [<]} [<] = Abs (Var Here)
+  mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) =
+    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
+          ])
+
+  replicate : Nat -> a -> SnocList a
+  replicate 0 x = [<]
+  replicate (S n) x = replicate n x :< x
+
+  replicateLen : (n : Nat) -> SnocList.length (replicate n x) = n
+  replicateLen 0 = Refl
+  replicateLen (S k) = cong S (replicateLen k)
+
+  export
+  Vect : Nat -> Ty -> Ty
+  Vect n ty = Product (replicate n ty)
+
+  zipReplicate :
+    {0 f : a -> b -> c} ->
+    {0 p : c -> Type} ->
+    {n : Nat} ->
+    p (f x y) ->
+    SnocList.Quantifiers.All.All p (zipWith f (replicate n x) (replicate n y))
+  zipReplicate {n = 0} z = [<]
+  zipReplicate {n = S k} z = zipReplicate z :< z
+
+  export
+  mapVect :
+    {n : Nat} ->
+    {ty, ty' : Ty} ->
+    Term [<] ((ty ~> ty') ~> Vect n ty ~> Vect n ty')
+  mapVect =
+    Abs' (S Z)
+      (\f => mapProd {prf = trans (replicateLen n) (sym $ replicateLen n)} $ zipReplicate f)
+
+  export
+  Nil : {ty : Ty} -> Term [<] (Vect 0 ty)
+  Nil = arb
+
+  export
+  Cons : {n : Nat} -> {ty : Ty} -> Term [<] (ty ~> Vect n ty ~> Vect (S n) ty)
+  Cons = Abs' (S $ S Z) (\t, ts => App' (lift pair) [<ts, t])
+
+  export
+  head : {n : Nat} -> {ty : Ty} -> Term [<] (Vect (S n) ty ~> ty)
+  head = snd
+
+  export
+  tail : {n : Nat} -> {ty : Ty} -> Term [<] (Vect (S n) ty ~> Vect n ty)
+  tail = fst
+
+  export
+  index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> Term [<] (Vect n ty ~> ty)
+  index FZ = head
+  index (FS i) = index i . tail
+
+  export
+  enumerate : (n : Nat) -> Term [<] (Vect n N)
+  enumerate 0 = arb
+  enumerate (S k) = App' pair [<App' mapVect [<Abs' (S Z) Suc, enumerate k], Zero]
+
+namespace Sum
+  export
+  (+) : Ty -> Ty -> Ty
+  t + u = B * (t <+> u)
+
+  export
+  left : {t, u : Ty} -> Term [<] (t ~> (t + u))
+  left = Abs' (S Z) (\e => App' (lift pair) [<True, App (lift injL) e])
+
+  export
+  right : {t, u : Ty} -> Term [<] (u ~> (t + u))
+  right = Abs' (S Z) (\e => App' (lift pair) [<False, App (lift injR) e])
+
+  export
+  case' : {t, u, ty : Ty} -> Term [<] ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty)
+  case' = Abs' (S $ S $ S Z)
+    (\f, g, s =>
+      If (App (lift fst) s)
+        (App (f . lift (prjL . snd)) s)
+        (App (g . lift (prjR . snd)) s))
+
+  Sum' : Ty -> List Ty -> Ty
+  Sum' ty [] = ty
+  Sum' ty (ty' :: tys) = ty + Sum' ty' tys
+
+  export
+  Sum : List1 Ty -> Ty
+  Sum (ty ::: tys) = Sum' ty tys
+
+  put' :
+    {ty, ty' : Ty} ->
+    {tys : List Ty} ->
+    (i : Elem ty (ty' :: tys)) ->
+    Term [<] (ty ~> Sum' ty' tys)
+  put' {tys = []} Here = Abs' (S Z) id
+  put' {tys = _ :: _} Here = left
+  put' {tys = _ :: _} (There i) = right . put' i
+
+  export
+  put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> Term [<] (ty ~> Sum tys)
+  put {tys = _ ::: _} i = put' i
+
+  caseAll' :
+    {ctx : SnocList Ty} ->
+    {ty, ty' : Ty} ->
+    {tys : List Ty} ->
+    All (Term ctx . (~> ty)) (ty' :: tys) ->
+    Term ctx (Sum' ty' tys ~> ty)
+  caseAll' (t :: []) = t
+  caseAll' (t :: u :: ts) = App' (lift case') [<t, caseAll' (u :: ts)]
+
+  export
+  caseAll :
+    {ctx : SnocList Ty} ->
+    {tys : List1 Ty} ->
+    {ty : Ty} ->
+    All (Term ctx . (~> ty)) (forget tys) ->
+    Term ctx (Sum tys ~> ty)
+  caseAll {tys = _ ::: _} = caseAll'
+
+namespace Nat
+  export
+  IsZero : Term [<] (N ~> B)
+  IsZero = Abs' (S Z) (\m => Rec m (lift True) (Abs (lift False)))
+
+  export
+  Add : Term [<] (N ~> N ~> N)
+  Add = Abs' (S $ S Z) (\m, n => Rec m n (Abs' (S Z) Suc))
+
+  export
+  sum : {n : Nat} -> Term [<] (Vect n N ~> N)
+  sum {n = 0} = Abs Zero
+  sum {n = S k} = Abs' (S Z)
+    (\ns => App' (lift Add) [<App (lift head) ns, App (lift (sum . tail)) ns])
+
+  export
+  Pred : Term [<] (N ~> N)
+  Pred = Abs' (S Z)
+    (\m =>
+      App' (lift case')
+        [<Abs Zero
+        , Abs' (S Z) id
+        , Rec m
+            (lift $ App left (arb {ty = Unit}))
+            (App' (lift case')
+              [<Abs (lift $ App right Zero)
+              , Abs' (S Z) (\n => App (lift right) (Suc n))
+              ])
+        ])
+
+  export
+  Sub : Term [<] (N ~> N ~> N)
+  Sub = Abs' (S $ S Z) (\m, n => Rec n m (lift Pred))
+
+  export
+  LE : Term [<] (N ~> N ~> B)
+  LE = Abs' (S Z) (\m => lift IsZero . App (lift Sub) m)
+
+  export
+  LT : Term [<] (N ~> N ~> B)
+  LT = Abs' (S Z) (\m => App (lift LE) (Suc m))
+
+  export
+  Cond :
+    {ctx : SnocList Ty} ->
+    {ty : Ty} ->
+    List (Term ctx N, Term ctx (N ~> ty)) ->
+    Term ctx (N ~> ty)
+  Cond [] = lift arb
+  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)])))
+
+namespace Data
+  public export
+  Shape : Type
+  Shape = (Ty, Nat)
+
+  public export
+  Container : Type
+  Container = List1 Shape
+
+  public export
+  fillShape : Shape -> Ty -> Ty
+  fillShape (shape,  n) ty = shape * Vect n ty
+
+  public export
+  fill : Container -> Ty -> Ty
+  fill c ty = Sum (map (flip fillShape ty) c)
+
+  export
+  fix : Container -> Ty
+  fix c = Product [<N, N ~> N, N ~> fill c N]
+  --                ^  ^       ^- tags and next positions
+  --                |  |- offset
+  --                |- pred (number of tags in structure)
+
+  mapShape :
+    {shape : Shape} ->
+    {ty, ty' : Ty} ->
+    Term [<] ((ty ~> ty') ~> fillShape shape ty ~> fillShape shape ty')
+  mapShape {shape = (shape, n)} = mapSnd . mapVect
+
+  gmap :
+    {0 f : a -> b} ->
+    {0 P : a -> Type} ->
+    {0 Q : b -> Type} ->
+    ({x : a} -> P x -> Q (f x)) ->
+    {xs : List a} ->
+    All P xs ->
+    All Q (map f xs)
+  gmap f [] = []
+  gmap f (px :: pxs) = f px :: gmap f pxs
+
+  forgetMap :
+    (0 f : a -> b) ->
+    (0 xs : List1 a) ->
+    forget (map f xs) = map f (forget xs)
+  forgetMap f (head ::: tail) = Refl
+
+  calcOffsets :
+    {ctx : SnocList Ty} ->
+    {c : Container} ->
+    {n : Nat} ->
+    (ts : Term ctx (Vect n (fix c))) ->
+    (acc : Term ctx N) ->
+    List (Term ctx N, Term ctx (N ~> N))
+  calcOffsets {n = 0} ts acc = []
+  calcOffsets {n = S k} ts acc =
+    let hd = App (lift head) ts in
+    let n = App (lift $ project $ There $ There Here) hd in
+    let offset = App (lift $ project $ There Here) hd in
+    (n, App (lift Add) acc . offset) ::
+    calcOffsets
+      (App (lift tail) ts)
+      (App' (lift Add) [<Suc n, acc])
+
+  calcData :
+    {ctx : SnocList Ty} ->
+    {c : Container} ->
+    {n : Nat} ->
+    (ts : Term ctx (Vect n (fix c))) ->
+    (acc : Term ctx N) ->
+    List (Term ctx N, Term ctx (N ~> fill c N))
+  calcData {n = 0} ts acc = []
+  calcData {n = S k} ts acc =
+    let hd = App (lift head) ts in
+    let n = App (lift $ project $ There $ There Here) hd in
+    (n, App (lift $ project Here) hd) ::
+    calcData
+      (App (lift tail) ts)
+      (App' (lift Add) [<Suc n, acc])
+
+  export
+  intro :
+    {c : Container} ->
+    {shape : Shape} ->
+    Elem shape (forget c) ->
+    Term [<] (fillShape shape (fix c) ~> fix c)
+  intro {shape = (shape, n)} i = Abs' (S Z)
+    (\t =>
+      App' (lift $ pair' {tys = [<N, N ~> N, N ~> fill c N]})
+        [<App (lift (sum . App mapVect (Abs' (S Z) Suc . project (There $ There Here)) . snd)) t
+        , Cond ((Zero, Abs' (S Z) Suc) :: calcOffsets (App (lift snd) t) (Suc Zero))
+        , Cond
+          (  (Zero,
+              Abs
+                (App
+                  (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)])))
+          :: calcData (App (lift snd) t) (Suc Zero)
+          )
+        ])
+
+  export
+  elim :
+    {c : Container} ->
+    {ctx : SnocList Ty} ->
+    {ty : Ty} ->
+    All (Term ctx . (~> ty) . flip Data.fillShape ty) (forget c) ->
+    Term ctx (fix c ~> ty)
+  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
+      App'
+        (Rec tags
+          (lift arb)
+          (Abs' (S $ S Z) (\rec, n =>
+            App
+              (caseAll {tys = map (flip fillShape N) c}
+                (rewrite forgetMap (flip fillShape N) c in
+                 gmap
+                   (\f =>
+                     wkn f (Drop $ Drop $ Drop Id) .
+                     App (lift mapShape) (rec . App (lift Add) (App offset n)))
+                   cases) .
+               vals)
+              n)))
+        [<Zero])
+
+  -- elim cases (#tags-1,offset,data) =
+  --   let
+  --       step : (N -> ty) -> (N -> ty)
+  --       step rec n =
+  --         case rec n of
+  --           i => cases(i) . mapShape (rec . (+ offset n))
+  --   in
+  --       rec #tags arb step 0
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
index b0d60ea..1ed7276 100644
--- a/src/Total/LogRel.idr
+++ b/src/Total/LogRel.idr
@@ -6,6 +6,7 @@ import Total.Term
 
 %prefix_record_projections off
 
+public export
 LogRel :
   {ctx : SnocList Ty} ->
   (P : {ctx, ty : _} -> Term ctx ty -> Type) ->
@@ -21,6 +22,7 @@ LogRel p {ty = ty ~> ty'} t =
    LogRel p u ->
    LogRel p (App (wkn t thin) u))
 
+export
 escape :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
   {ty : Ty} ->
@@ -30,6 +32,7 @@ escape :
 escape {ty = N} pt = pt
 escape {ty = ty ~> ty'} (pt, app) = pt
 
+public export
 record PreserveHelper
   (P : {ctx, ty : _} -> Term ctx ty -> Type)
   (R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type) where
@@ -48,11 +51,22 @@ record PreserveHelper
     {ty : Ty} ->
     {0 t, u : Term ctx ty} ->
     P t ->
-    R t u ->
+    (0 _ : R t u) ->
     P u
 
 %name PreserveHelper help
 
+export
+backStepHelper :
+  {0 P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  (forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u) ->
+  PreserveHelper P (flip (>))
+backStepHelper pres =
+  MkPresHelper
+    (\thin, v, step => AppCong1 (wknStep step))
+    pres
+
+export
 preserve :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
   {R : {ctx, ty : _} -> Term ctx ty -> Term ctx ty -> Type} ->
@@ -60,7 +74,7 @@ preserve :
   {0 t, u : Term ctx ty} ->
   PreserveHelper P R ->
   LogRel P t ->
-  R t u ->
+  (0 _ : R t u) ->
   LogRel P u
 preserve help {ty = N} pt prf = help.pres pt prf
 preserve help {ty = ty ~> ty'} (pt, app) prf =
@@ -81,7 +95,7 @@ data AllLogRel : (P : {ctx, ty : _} -> Term ctx ty -> Type) -> Terms ctx' ctx ->
 
 index :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
-  (forall ty. (i : Elem ty ctx') -> LogRel P (Var i)) ->
+  ((i : Elem ty ctx') -> LogRel P (Var i)) ->
   {sub : Terms ctx' ctx} ->
   AllLogRel P sub ->
   (i : Elem ty ctx) ->
@@ -102,21 +116,24 @@ Valid p t =
   (allRel : AllLogRel p sub) ->
   LogRel p (subst t sub)
 
+public export
 record ValidHelper (P : {ctx, ty : _} -> Term ctx ty -> Type) where
   constructor MkValidHelper
-  var : forall ctx, ty. (i : Elem ty ctx) -> LogRel P (Var i)
-  abs : forall ctx, ty, ty'. {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t)
+  var : forall ctx. {ty : Ty} -> (i : Elem ty ctx) -> LogRel P (Var i)
+  abs : forall ctx, ty. {ty' : Ty} -> {0 t : Term (ctx :< ty) ty'} -> LogRel P t -> P (Abs t)
   zero : forall ctx. P {ctx} Zero
   suc : forall ctx. {0 t : Term ctx N} -> P t -> P (Suc t)
-  rec : forall ctx, ty.
+  rec :
+    {ctx : SnocList Ty} ->
+    {ty : Ty} ->
     {0 t : Term ctx N} ->
-    {0 u : Term ctx ty} ->
-    {0 v : Term ctx (ty ~> ty)} ->
+    {u : Term ctx ty} ->
+    {v : Term ctx (ty ~> ty)} ->
     LogRel P t ->
     LogRel P u ->
     LogRel P v ->
     LogRel P (Rec t u v)
-  step : forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> u > t -> P u
+  step : forall ctx, ty. {0 t, u : Term ctx ty} -> P t -> (0 _ : u > t) -> P u
   wkn : forall ctx, ctx', ty.
     {0 t : Term ctx ty} ->
     P t ->
@@ -150,6 +167,7 @@ wknAllRel :
 wknAllRel help Base thin = Base
 wknAllRel help (allRels :< rel) thin = wknAllRel help allRels thin :< wknRel help rel thin
 
+export
 allValid :
   {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
   {ctx : SnocList Ty} ->
@@ -169,8 +187,6 @@ allValid help (Abs t) sub allRels =
       help.abs rec
   , \thin, u, rel =>
     let
-      helper : PreserveHelper P (flip (>))
-      helper = MkPresHelper (\thin, v, step => AppCong1 (wknStep step)) help.step
       eq :
         (subst (wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)) (Base Id :< u) =
          subst t (wknAll sub thin :< u))
@@ -190,7 +206,7 @@ allValid help (Abs t) sub allRels =
           ...(cong (subst t . (:< u)) $ baseComp thin sub)
     in
       preserve
-        helper
+        (backStepHelper help.step)
         (valid (wknAll sub thin :< u) (wknAllRel help allRels thin :< rel))
         (replace {p = (App (wkn (subst (Abs t) sub) thin) u >)}
           eq
@@ -209,3 +225,13 @@ allValid help (Rec t u v) sub allRels =
   let relu = allValid help u sub allRels in
   let relv = allValid help v sub allRels in
   help.rec relt relu relv
+
+export
+allRel :
+  {P : {ctx, ty : _} -> Term ctx ty -> Type} ->
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  ValidHelper P ->
+  (t : Term ctx ty) ->
+  P t
+allRel help t = rewrite sym $ substId t in escape (allValid help t (Base Id) Base)
diff --git a/src/Total/NormalForm.idr b/src/Total/NormalForm.idr
index 93a1da7..b5580b5 100644
--- a/src/Total/NormalForm.idr
+++ b/src/Total/NormalForm.idr
@@ -1,5 +1,6 @@
 module Total.NormalForm
 
+import Total.LogRel
 import Total.Reduction
 import Total.Term
 
@@ -32,3 +33,113 @@ record NormalForm (0 t : Term ctx ty) where
   0 normal : Normal term
 
 %name NormalForm nf
+
+-- Strong Normalization Proof --------------------------------------------------
+
+invApp : Normal (App t u) -> Neutral (App t u)
+invApp (Ntrl n) = n
+
+invRec : Normal (Rec t u v) -> Neutral (Rec t u v)
+invRec (Ntrl n) = n
+
+invSuc : Normal (Suc t) -> Normal t
+invSuc (Suc n) = n
+
+wknNe : Neutral t -> Neutral (wkn t thin)
+wknNf : Normal t -> Normal (wkn t thin)
+
+wknNe Var = Var
+wknNe (App n m) = App (wknNe n) (wknNf m)
+wknNe (Rec n m k) = Rec (wknNe n) (wknNf m) (wknNf k)
+
+wknNf (Ntrl n) = Ntrl (wknNe n)
+wknNf (Abs n) = Abs (wknNf n)
+wknNf Zero = Zero
+wknNf (Suc n) = Suc (wknNf n)
+
+backStepsNf : NormalForm t -> (0 _ : u >= t) -> NormalForm u
+backStepsNf nf steps = MkNf nf.term (steps ++ nf.steps) nf.normal
+
+backStepsRel :
+  {ty : Ty} ->
+  {0 t, u : Term ctx ty} ->
+  LogRel (\t => NormalForm t) t ->
+  (0 _ : u >= t) ->
+  LogRel (\t => NormalForm t) u
+backStepsRel =
+  preserve {R = flip (>=)}
+    (MkPresHelper (\thin, v, steps => AppCong1' (wknSteps steps)) backStepsNf)
+
+ntrlRel : {ty : Ty} -> {t : Term ctx ty} -> (0 _ : Neutral t) -> LogRel (\t => NormalForm t) t
+ntrlRel {ty = N} n = MkNf t [<] (Ntrl n)
+ntrlRel {ty = ty ~> ty'} n =
+  ( MkNf t [<] (Ntrl n)
+  , \thin, u, rel =>
+    backStepsRel
+      (ntrlRel (App (wknNe n) (escape rel).normal))
+      (AppCong2' (escape rel).steps)
+  )
+
+recNf' :
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  {u : Term ctx ty} ->
+  {v : Term ctx (ty ~> ty)} ->
+  (t' : Term ctx N) ->
+  (0 n : Normal t') ->
+  LogRel (\t => NormalForm t) u ->
+  LogRel (\t => NormalForm t) v ->
+  LogRel (\t => NormalForm t) (Rec t' u v)
+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]
+recNf' t'@(Var _) n relU relV =
+  let nfU = escape relU in
+  let nfV = escape {ty = ty ~> ty} relV in
+  backStepsRel
+    (ntrlRel (Rec Var nfU.normal nfV.normal))
+    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+recNf' t'@(App _ _) n relU relV =
+  let nfU = escape relU in
+  let nfV = escape {ty = ty ~> ty} relV in
+  backStepsRel
+    (ntrlRel (Rec (invApp n) nfU.normal nfV.normal))
+    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+recNf' t'@(Rec _ _ _) n relU relV =
+  let nfU = escape relU in
+  let nfV = escape {ty = ty ~> ty} relV in
+  backStepsRel
+    (ntrlRel (Rec (invRec n) nfU.normal nfV.normal))
+    (RecCong2' nfU.steps ++ RecCong3' nfV.steps)
+
+recNf :
+  {ctx : SnocList Ty} ->
+  {ty : Ty} ->
+  {0 t : Term ctx N} ->
+  {u : Term ctx ty} ->
+  {v : Term ctx (ty ~> ty)} ->
+  NormalForm t ->
+  LogRel (\t => NormalForm t) u ->
+  LogRel (\t => NormalForm t) v ->
+  LogRel (\t => NormalForm t) (Rec t u v)
+recNf nf relU relV =
+  backStepsRel
+    (recNf' nf.term nf.normal relU relV)
+    (RecCong1' nf.steps)
+
+helper : ValidHelper (\t => NormalForm t)
+helper = MkValidHelper
+  { var = \i => ntrlRel Var
+  , abs = \rel => let nf = escape rel in MkNf (Abs nf.term) (AbsCong' nf.steps) (Abs nf.normal)
+  , zero = MkNf Zero [<] Zero
+  , suc = \nf => MkNf (Suc nf.term) (SucCong' nf.steps) (Suc nf.normal)
+  , rec = recNf
+  , step = \nf, step => backStepsNf nf [<step]
+  , wkn = \nf, thin => MkNf (wkn nf.term thin) (wknSteps nf.steps) (wknNf nf.normal)
+  }
+
+export
+normalize : {ctx : SnocList Ty} -> {ty : Ty} -> (t : Term ctx ty) -> NormalForm t
+normalize = allRel helper
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index 4870f30..cb13706 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -95,3 +95,8 @@ wknStep (RecCong2 step) = RecCong2 (wknStep step)
 wknStep (RecCong3 step) = RecCong3 (wknStep step)
 wknStep RecZero = RecZero
 wknStep RecSuc = RecSuc
+
+export
+wknSteps : t >= u -> wkn t thin >= wkn u thin
+wknSteps [<] = [<]
+wknSteps (steps :< step) = wknSteps steps :< wknStep step
diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
new file mode 100644
index 0000000..6a61cf5
--- /dev/null
+++ b/src/Total/Syntax.idr
@@ -0,0 +1,83 @@
+module Total.Syntax
+
+import public Data.List
+import public Data.List.Quantifiers
+import public Data.SnocList
+import public Data.SnocList.Quantifiers
+import public Total.Term
+
+infixr 20 ~>*
+infix 9 .*
+
+public export
+(~>*) : SnocList Ty -> Ty -> Ty
+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
+0 Fun : Len tys -> (Ty -> Type) -> Type -> Type
+Fun Z arg ret = ret
+Fun (S {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 Z f x = f x
+after (S k) f x = after k (f .) x
+
+before :
+  (k : Len tys) ->
+  (forall ty. p ty -> q ty) ->
+  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)
+
+export
+Lit : Nat -> Term ctx N
+Lit 0 = Zero
+Lit (S n) = Suc (Lit n)
+
+AbsHelper :
+  (k : Len tys) ->
+  Fun k (flip Elem (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
+  Term ctx (tys ~>* ty)
+AbsHelper Z x = x
+AbsHelper (S k) x =
+  AbsHelper k $
+  after k (\f => Term.Abs (f SnocList.Elem.Here)) $
+  before k SnocList.Elem.There x
+
+export
+Abs' :
+  (k : Len tys) ->
+  Fun k (Term (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
+  Term ctx (tys ~>* ty)
+Abs' k = AbsHelper k . before k Var
+
+export
+App' : {tys : SnocList Ty} -> Term ctx (tys ~>* ty) -> All (Term ctx) tys -> Term ctx ty
+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))
+
+export
+(.*) :
+  {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
+
+export
+lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty
+lift t = wkn t (empty ctx)
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 1530981..d4da92a 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -322,6 +322,15 @@ 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 (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) ->