Prove weakening of type judgements.

This is a huge commit that has many more changes. I should split
this up later.

1 files changed, 134 insertions, 6 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 1292fc9..2afceaa 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -1,6 +1,7 @@
 module Core.Declarative
 
 import Core.Environment
+import Core.Environment.Extension
 import Core.Term
 import Core.Term.Substitution
 import Core.Term.Thinned
@@ -82,7 +83,7 @@ data TermWf where
     TermWf env t (Pi a b) ->
     TermWf env u a ->
     ---
-    TermWf env (App t u) (subst b $ Wkn (id _) :< pure u)
+    TermWf env (App t u) (subst1 b u)
   ConvWf :
     TermWf env t a ->
     TypeConv env a b ->
@@ -107,7 +108,7 @@ data TermConv where
     TermConv env f g (Pi a b) ->
     TermConv env t u a ->
     ---
-    TermConv env (App f t) (App g u) (subst b $ Wkn (id _) :< pure t)
+    TermConv env (App f t) (App g u) (subst1 b t)
   PiTmConv :
     TypeWf env a ->
     TermConv env a c Set ->
@@ -129,10 +130,7 @@ data TermConv where
     TermWf (env :< pure a) t b ->
     TermWf env u a ->
     ---
-    TermConv env
-      (App (Abs t) u)
-      (subst t $ Wkn (id _) :< pure u)
-      (subst g $ Wkn (id _) :< pure u)
+    TermConv env (App (Abs t) u) (subst1 t u) (subst1 b u)
   ConvConv :
     TermConv env t u a ->
     TypeConv env a b ->
@@ -269,3 +267,133 @@ termConvImpliesEnvWf (PiTmConv tyWf tmConv tmConv1) = termConvImpliesEnvWf tmCon
 termConvImpliesEnvWf (PiEta tyWf tmWf tmWf1 tmConv) = termWfImpliesEnvWf tmWf
 termConvImpliesEnvWf (PiBeta tyWf tmWf tmWf1) = typeWfImpliesEnvWf tyWf
 termConvImpliesEnvWf (ConvConv tmConv tyConv) = termConvImpliesEnvWf tmConv
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+record ExtendsWf (0 thin : m `Thins` n) (0 env2 : Env n) (0 env1 : Env m) where
+  constructor MkExtWf
+  ext : Extends thin env2 env1
+  wf : EnvWf env2
+
+%name ExtendsWf extWf
+
+wknPiEta :
+  (t : Term m) ->
+  (thin : m `Thins` n) ->
+  wkn (App (wkn t (wkn1 m)) (Var 0)) (keep thin) =
+  App (wkn (wkn t thin) (wkn1 n)) (Var 0)
+wknPiEta t thin = cong2 App (sym $ wkn1Comm t thin) (cong Var $ wknKeepFZ thin)
+
+export
+weakenTypeWf :
+  TypeWf env1 a ->
+  ExtendsWf thin env2 env1 ->
+  TypeWf env2 (wkn a thin)
+export
+weakenTypeConv :
+  TypeConv env1 a b ->
+  ExtendsWf thin env2 env1 ->
+  TypeConv env2 (wkn a thin) (wkn b thin)
+export
+weakenTermWf :
+  TermWf env1 t a ->
+  ExtendsWf thin env2 env1 ->
+  TermWf env2 (wkn t thin) (wkn a thin)
+export
+weakenTermConv :
+  TermConv env1 t u a ->
+  ExtendsWf thin env2 env1 ->
+  TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)
+
+weakenTypeWf (SetTyWf envWf) extWf = SetTyWf extWf.wf
+weakenTypeWf (PiTyWf {a} tyWf tyWf1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiTyWf tyWf
+    (typeWfRespEq
+      (weakenTypeWf tyWf1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTypeWf (LiftWf tmWf) extWf = LiftWf (weakenTermWf tmWf extWf)
+
+weakenTypeConv (ReflTy tyWf) extWf = ReflTy (weakenTypeWf tyWf extWf)
+weakenTypeConv (SymTy tyConv) extWf = SymTy (weakenTypeConv tyConv extWf)
+weakenTypeConv (TransTy tyConv tyConv1) extWf =
+  TransTy
+    (weakenTypeConv tyConv extWf)
+    (weakenTypeConv tyConv1 extWf)
+weakenTypeConv (PiConv {a} tyWf tyConv tyConv1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiConv tyWf
+    (weakenTypeConv tyConv extWf)
+    (typeConvRespEq
+      (weakenTypeConv tyConv1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTypeConv (LiftConv tmConv) extWf = LiftConv (weakenTermConv tmConv extWf)
+
+weakenTermWf (PiTmWf {a} tmWf tmWf1) extWf =
+  let tmWf = weakenTermWf tmWf extWf in
+  PiTmWf tmWf
+    (termWfRespEq
+      (weakenTermWf tmWf1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< LiftWf tmWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermWf (VarWf {i} envWf) extWf =
+  rewrite sym $ expandHomo (index env1 i) thin in
+  rewrite sym $ indexHomo extWf.ext i in
+  VarWf extWf.wf
+weakenTermWf (AbsWf {a} tyWf tmWf) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  AbsWf tyWf
+    (termWfRespEq
+      (weakenTermWf tmWf $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermWf (AppWf {b, u} tmWf tmWf1) extWf =
+  rewrite wknSubst1 b u thin in
+  AppWf
+    (weakenTermWf tmWf extWf)
+    (weakenTermWf tmWf1 extWf)
+weakenTermWf (ConvWf tmWf tyConv) extWf =
+  ConvWf
+    (weakenTermWf tmWf extWf)
+    (weakenTypeConv tyConv extWf)
+
+weakenTermConv (ReflTm tmWf) extWf = ReflTm (weakenTermWf tmWf extWf)
+weakenTermConv (SymTm tmConv) extWf = SymTm (weakenTermConv tmConv extWf)
+weakenTermConv (TransTm tmConv tmConv1) extWf =
+  TransTm
+    (weakenTermConv tmConv extWf)
+    (weakenTermConv tmConv1 extWf)
+weakenTermConv (AppConv {b, t} tmConv tmConv1) extWf =
+  rewrite wknSubst1 b t thin in
+  AppConv
+    (weakenTermConv tmConv extWf)
+    (weakenTermConv tmConv1 extWf)
+weakenTermConv (PiTmConv {a} tyWf tmConv tmConv1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiTmConv tyWf
+    (weakenTermConv tmConv extWf)
+    (termConvRespEq
+      (weakenTermConv tmConv1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermConv (PiEta {a, t, u} tyWf tmWf tmWf1 tmConv) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiEta tyWf
+    (weakenTermWf tmWf extWf)
+    (weakenTermWf tmWf1 extWf)
+    (termConvRespEq
+      (rewrite sym $ wknPiEta t thin in
+       rewrite sym $ wknPiEta u thin in
+       weakenTermConv tmConv $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermConv (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)
+weakenTermConv (ConvConv tmConv tyConv) extWf =
+  ConvConv
+    (weakenTermConv tmConv extWf)
+    (weakenTypeConv tyConv extWf)