Prove environment equality preserves typing.

1 files changed, 72 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index b90bf20..9f60d34 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -160,11 +160,83 @@ data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
 
 -- Environment Equality --------------------------------------------------------
 
+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
 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
 
+envWfRespEnvEq [<] [<] = [<]
+envWfRespEnvEq (envWf :< wf) (prf :< eq) =
+  envWfRespEnvEq envWf prf :<
+  rewrite sym eq in typeWfRespEnvEq wf prf
+
+typeWfRespEnvEq (SetType envWf) prf = SetType (envWfRespEnvEq envWf prf)
+typeWfRespEnvEq (PiType wf wf1) prf =
+  PiType
+    (typeWfRespEnvEq wf prf)
+    (typeWfRespEnvEq wf1 $ prf :< Refl)
+typeWfRespEnvEq (LiftType wf) prf = LiftType (termWfRespEnvEq wf prf)
+
+typeConvRespEnvEq (ReflType wf) prf = ReflType (typeWfRespEnvEq wf prf)
+typeConvRespEnvEq (SymType conv) prf = SymType (typeConvRespEnvEq conv prf)
+typeConvRespEnvEq (TransType conv conv1) prf =
+  TransType
+    (typeConvRespEnvEq conv prf)
+    (typeConvRespEnvEq conv1 prf)
+typeConvRespEnvEq (PiTypeConv wf conv conv1) prf =
+  PiTypeConv
+    (typeWfRespEnvEq wf prf)
+    (typeConvRespEnvEq conv prf)
+    (typeConvRespEnvEq conv1 $ prf :< Refl)
+typeConvRespEnvEq (LiftConv conv) prf = LiftConv (termConvRespEnvEq conv prf)
+
+termWfRespEnvEq (VarTerm {i} envWf) prf =
+  rewrite indexEqIsEq prf i in
+  VarTerm (envWfRespEnvEq envWf prf)
+termWfRespEnvEq (PiTerm wf wf1) prf =
+  PiTerm
+    (termWfRespEnvEq wf prf)
+    (termWfRespEnvEq wf1 $ prf :< Refl)
+termWfRespEnvEq (AbsTerm wf wf1) prf =
+  AbsTerm
+    (typeWfRespEnvEq wf prf)
+    (termWfRespEnvEq wf1 $ prf :< Refl)
+termWfRespEnvEq (AppTerm wf wf1) prf = AppTerm (termWfRespEnvEq wf prf) (termWfRespEnvEq wf1 prf)
+termWfRespEnvEq (ConvTerm wf conv) prf =
+  ConvTerm
+    (termWfRespEnvEq wf prf)
+    (typeConvRespEnvEq conv prf)
+
+termConvRespEnvEq (ReflTerm wf) prf = ReflTerm (termWfRespEnvEq wf prf)
+termConvRespEnvEq (SymTerm conv) prf = SymTerm (termConvRespEnvEq conv prf)
+termConvRespEnvEq (TransTerm conv conv1) prf =
+  TransTerm
+    (termConvRespEnvEq conv prf)
+    (termConvRespEnvEq conv1 prf)
+termConvRespEnvEq (ConvTermConv conv conv1) prf =
+  ConvTermConv (termConvRespEnvEq conv prf) (typeConvRespEnvEq conv1 prf)
+termConvRespEnvEq (PiTermConv wf conv conv1) prf =
+  PiTermConv
+    (typeWfRespEnvEq wf prf)
+    (termConvRespEnvEq conv prf)
+    (termConvRespEnvEq conv1 $ prf :< Refl)
+termConvRespEnvEq (PiBeta wf wf1 wf2) prf =
+  PiBeta
+    (typeWfRespEnvEq wf prf)
+    (termWfRespEnvEq wf1 $ prf :< Refl)
+    (termWfRespEnvEq wf2 prf)
+termConvRespEnvEq (PiEta wf wf1 wf2 conv) prf =
+  PiEta
+    (typeWfRespEnvEq wf prf)
+    (termWfRespEnvEq wf1 prf)
+    (termWfRespEnvEq wf2 prf)
+    (termConvRespEnvEq conv $ prf :< Refl)
+termConvRespEnvEq (AppConv conv conv1) prf =
+  AppConv
+    (termConvRespEnvEq conv prf)
+    (termConvRespEnvEq conv1 prf)
+
 -- Well Formed Environment -----------------------------------------------------
 
 typeWfImpliesEnvWf : TypeWf env a -> EnvWf env