Prove weakening preserves reduction.

2 files changed, 59 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 2dd7933..8704e07 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -157,6 +157,7 @@ data TermConv where
 envWfRespEnvEq : EnvWf env1 -> EnvEq env1 env2 -> EnvWf env2
 typeWfRespEnvEq : TypeWf env1 a -> EnvEq env1 env2 -> TypeWf env2 a
 typeConvRespEnvEq : TypeConv env1 a b -> EnvEq env1 env2 -> TypeConv env2 a b
+export
 termWfRespEnvEq : TermWf env1 t a -> EnvEq env1 env2 -> TermWf env2 t a
 termConvRespEnvEq : TermConv env1 t u b -> EnvEq env1 env2 -> TermConv env2 t u b
 
@@ -265,18 +266,21 @@ termConvImpliesEnvWf (AppConv conv conv1) = termConvImpliesEnvWf conv
 
 -- Weakening Preservation ------------------------------------------------------
 
+export
 wknPresTypeWf :
   {0 env1 : Env sx} ->
   TypeWf env1 a ->
   EnvWf env2 ->
   IsExtension thin env2 env1 ->
   TypeWf env2 (wkn a thin)
+export
 wknPresTypeConv :
   {0 env1 : Env sx} ->
   TypeConv env1 a b ->
   EnvWf env2 ->
   IsExtension thin env2 env1 ->
   TypeConv env2 (wkn a thin) (wkn b thin)
+export
 wknPresTermWf :
   {0 env1 : Env sx} ->
   TermWf env1 t a ->
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index 0c89abe..eb59446 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -6,6 +6,7 @@ import Core.Environment
 import Core.Term
 import Core.Term.NormalForm
 import Core.Term.Substitution
+import Core.Thinning
 
 public export
 data TermStep : Env sx -> Term sx -> Term sx -> Term sx -> Type where
@@ -131,3 +132,57 @@ termRedDeterministic red (Stay _) n m = sym $ termRedWhnfStays m red
 termRedDeterministic (step :: steps) (step1 :: steps1) n m =
   let steps1' : TermRed env _ v b = rewrite termStepDeterministic step step1 in steps1 in
   termRedDeterministic steps steps1' n m
+
+-- Weakening Preservation ------------------------------------------------------
+
+wknPresTermStep :
+  {0 env1 : Env sx} ->
+  TermStep env1 t u a ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
+  TermStep env2 (wkn t thin) (wkn u thin) (wkn a thin)
+wknPresTermStep (PiBeta {f, g, n, t, u} wf wf1 wf2) envWf ext =
+  rewrite wknSub1 g u thin in
+  rewrite wknSub1 t u thin in
+  let wf' = wknPresTypeWf wf envWf ext in
+  PiBeta wf'
+    (termWfRespEnvEq
+      (wknPresTermWf wf1 (envWf :< wf') $
+       replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
+         (compRightIdentity thin)
+         (KeepWf ext))
+      ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)))
+    (wknPresTermWf wf2 envWf ext)
+wknPresTermStep (AppStep {g, a} step wf) envWf ext =
+  rewrite wknSub1 g a thin in
+  AppStep (wknPresTermStep step envWf ext) (wknPresTermWf wf envWf ext)
+wknPresTermStep (StepConv step conv) envWf ext =
+  StepConv (wknPresTermStep step envWf ext) (wknPresTypeConv conv envWf ext)
+
+wknPresTypeStep :
+  {0 env1 : Env sx} ->
+  TypeStep env1 a b ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
+  TypeStep env2 (wkn a thin) (wkn b thin)
+wknPresTypeStep = wknPresTermStep
+
+wknPresTypeRed :
+  {0 env1 : Env sx} ->
+  TypeRed env1 a b ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
+  TypeRed env2 (wkn a thin) (wkn b thin)
+wknPresTypeRed (Stay wf) envWf ext = Stay (wknPresTypeWf wf envWf ext)
+wknPresTypeRed (step :: steps) envWf ext =
+  wknPresTypeStep step envWf ext :: wknPresTypeRed steps envWf ext
+
+wknPresTermRed :
+  {0 env1 : Env sx} ->
+  TermRed env1 t u a ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
+  TermRed env2 (wkn t thin) (wkn u thin) (wkn a thin)
+wknPresTermRed (Stay wf) envWf ext = Stay (wknPresTermWf wf envWf ext)
+wknPresTermRed (step :: steps) envWf ext =
+  wknPresTermStep step envWf ext :: wknPresTermRed steps envWf ext