Prove weakening of reduction.

1 files changed, 56 insertions, 5 deletions

diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index 9e1d318..50926bc 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -1,6 +1,7 @@
 module Core.Reduction
 
 import Core.Environment
+import Core.Environment.Extension
 import Core.Declarative
 import Core.Term
 import Core.Term.NormalForm
@@ -18,16 +19,13 @@ data TermStep : Env n -> Term n -> Term n -> Term n -> Type where
     TermStep env t u (Pi a b) ->
     TermWf env v a ->
     ---
-    TermStep env (App t v) (App u v) (subst b $ Wkn (id _) :< pure v)
+    TermStep env (App t v) (App u v) (subst1 b v)
   PiBeta :
     TypeWf env a ->
     TermWf (env :< pure a) t b ->
     TermWf env u a ->
     ---
-    TermStep env
-      (App (Abs t) u)
-      (subst t $ Wkn (id _) :< pure u)
-      (subst b $ Wkn (id _) :< pure u)
+    TermStep env (App (Abs t) u) (subst1 t u) (subst1 b u)
   ConvStep :
     TermStep env t u a ->
     TypeConv env a b ->
@@ -187,3 +185,56 @@ termRedDeterministic (Refl _) steps2 n m = whnfTermRedStays n steps2
 termRedDeterministic steps1 (Refl _) n m = sym $ whnfTermRedStays m steps1
 termRedDeterministic (Step step1 steps1) (Step step2 steps2) n m =
   termRedDeterministic steps1 (rewrite termStepDeterministic step1 step2 in steps2) n m
+
+-- Weakening -------------------------------------------------------------------
+
+export
+weakenTermStep :
+  TermStep env1 t u a ->
+  ExtendsWf thin env2 env1 ->
+  TermStep env2 (wkn t thin) (wkn u thin) (wkn a thin)
+weakenTermStep (AppStep {b, v} step tmWf) extWf =
+  rewrite wknSubst1 b v thin in
+  AppStep
+    (weakenTermStep step extWf)
+    (weakenTermWf tmWf extWf)
+weakenTermStep (PiBeta {a, b, t, u} tyWf tmWf tmWf1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  rewrite wknSubst1 t u thin in
+  rewrite wknSubst1 b u thin in
+  PiBeta tyWf
+    (termWfRespEq
+      (weakenTermWf tmWf $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+    (weakenTermWf tmWf1 extWf)
+weakenTermStep (ConvStep step tyConv) extWf =
+  ConvStep (weakenTermStep step extWf) (weakenTypeConv tyConv extWf)
+
+export
+weakenTypeStep :
+  TypeStep env1 a b ->
+  ExtendsWf thin env2 env1 ->
+  TypeStep env2 (wkn a thin) (wkn b thin)
+weakenTypeStep = weakenTermStep
+
+export
+weakenTypeRed :
+  TypeReduce env1 a b ->
+  ExtendsWf thin env2 env1 ->
+  TypeReduce env2 (wkn a thin) (wkn b thin)
+weakenTypeRed (Refl tyWf) extWf = Refl (weakenTypeWf tyWf extWf)
+weakenTypeRed (Step step steps) extWf =
+  Step
+    (weakenTypeStep step extWf)
+    (weakenTypeRed steps extWf)
+
+export
+weakenTermRed :
+  TermReduce env1 t u a ->
+  ExtendsWf thin env2 env1 ->
+  TermReduce env2 (wkn t thin) (wkn u thin) (wkn a thin)
+weakenTermRed (Refl tmWf) extWf = Refl (weakenTermWf tmWf extWf)
+weakenTermRed (Step step steps) extWf =
+  Step
+    (weakenTermStep step extWf)
+    (weakenTermRed steps extWf)