Prove weakening preserves typing judgements.

1 files changed, 215 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index d326c4e..94822e4 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -10,6 +10,8 @@ import Core.Var
 
 import Data.Nat
 
+import Syntax.PreorderReasoning
+
 public export
 data EnvWf : Env sx -> Type
 public export
@@ -287,3 +289,216 @@ wknPresTermConv :
   EnvWf env2 ->
   IsExtension thin env2 env1 ->
   TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)
+
+wknPresTypeWf (SetType envWf1) envWf ext = SetType envWf
+wknPresTypeWf (PiType {f, n} wf wf1) envWf ext =
+  let wf' = wknPresTypeWf wf envWf ext in
+  PiType wf' $
+  typeWfRespEnvEq
+    (wknPresTypeWf 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))
+wknPresTypeWf (LiftType wf) envWf ext = LiftType (wknPresTermWf wf envWf ext)
+
+wknPresTypeConv (ReflType wf) envWf ext = ReflType (wknPresTypeWf wf envWf ext)
+wknPresTypeConv (SymType conv) envWf ext = SymType (wknPresTypeConv conv envWf ext)
+wknPresTypeConv (TransType conv conv1) envWf ext =
+  TransType
+    (wknPresTypeConv conv envWf ext)
+    (wknPresTypeConv conv1 envWf ext)
+wknPresTypeConv (PiTypeConv {f, n} wf conv conv1) envWf ext =
+  let wf' = wknPresTypeWf wf envWf ext in
+  PiTypeConv wf' (wknPresTypeConv conv envWf ext) $
+  typeConvRespEnvEq
+    (wknPresTypeConv conv1 (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))
+wknPresTypeConv (LiftConv conv) envWf ext = LiftConv (wknPresTermConv conv envWf ext)
+
+wknPresTermWf (VarTerm {i} envWf1) envWf ext =
+  rewrite wknIndex ext i in
+  VarTerm envWf
+wknPresTermWf (PiTerm {f, n} wf wf1) envWf ext =
+  let wf' = wknPresTermWf wf envWf ext in
+  PiTerm wf' $
+  termWfRespEnvEq
+    (wknPresTermWf wf1 (envWf :< LiftType 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 (AbsTerm {f, n} wf wf1) envWf ext =
+  let wf' = wknPresTypeWf wf envWf ext in
+  AbsTerm 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 (AppTerm {g, u, n} wf wf1) envWf ext =
+  let
+    eq0 : (thin . id sx = id _ . thin)
+    eq0  = Calc $
+      |~ thin . id sx
+      ~~ thin          ...(compRightIdentity thin)
+      ~~ id _ . thin   ...(sym $ compLeftIdentity thin)
+
+    eq1 : (Base (thin . id sx) = restrict thin (Base (id _)))
+    eq1 = Calc $
+      |~ Base (thin . id sx)
+      ~~ Base (id _ . thin)          ...(cong Base eq0)
+      ~~ restrict thin (Base (id _)) ...(sym $ restrictBase thin (id _))
+
+    eq2 : wkn u (thin . id sx) = wkn (wkn u thin) (id _)
+    eq2 = Calc $
+      |~ wkn u (thin . id sx)
+      ~~ wkn u (id _ . thin)     ...(cong (wkn u) $ eq0)
+      ~~ wkn (wkn u thin) (id _) ...(sym $ wknHomo u thin (id _))
+
+    eq : (wkn (subst g (sub1 u)) thin = subst (wkn g (keep thin n)) (sub1 (wkn u thin)))
+    eq = Calc $
+      |~ wkn (subst g (sub1 u)) thin
+      ~~ subst g (Base (thin . id _) :< (u `Over` thin . id _))   ...(wknSubst g (sub1 u) thin)
+      ~~ subst g (Base (thin . id _) :< (wkn u thin `Over` id _)) ...(substCong g (Base :< eq2))
+      ~~ subst g (restrict thin _ :< (wkn u thin `Over` id _))    ...(cong (subst g . (:< (wkn u thin `Over` id _))) eq1)
+      ~~ subst g (restrict (keep thin n) (sub1 (wkn u thin)))     ...(sym $ cong (subst g) $ restrictKeep thin n (id _) (wkn u thin `Over` id _))
+      ~~ subst (wkn g (keep thin n)) (sub1 (wkn u thin))          ...(sym $ substWkn g (keep thin n) (sub1 (wkn u thin)))
+  in
+  rewrite eq in
+  AppTerm (wknPresTermWf wf envWf ext) (wknPresTermWf wf1 envWf ext)
+wknPresTermWf (ConvTerm wf conv) envWf ext =
+  ConvTerm (wknPresTermWf wf envWf ext) (wknPresTypeConv conv envWf ext)
+
+wknPresTermConv (ReflTerm wf) envWf ext = ReflTerm (wknPresTermWf wf envWf ext)
+wknPresTermConv (SymTerm conv) envWf ext = SymTerm (wknPresTermConv conv envWf ext)
+wknPresTermConv (TransTerm conv conv1) envWf ext =
+  TransTerm
+    (wknPresTermConv conv envWf ext)
+    (wknPresTermConv conv1 envWf ext)
+wknPresTermConv (ConvTermConv conv conv1) envWf ext =
+  ConvTermConv
+    (wknPresTermConv conv envWf ext)
+    (wknPresTypeConv conv1 envWf ext)
+wknPresTermConv (PiTermConv {f, n} wf conv conv1) envWf ext =
+  let wf' = wknPresTypeWf wf envWf ext in
+  PiTermConv wf' (wknPresTermConv conv envWf ext) $
+  termConvRespEnvEq
+    (wknPresTermConv conv1 (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))
+wknPresTermConv (PiBeta {f, g, t, u, n} wf wf1 wf2) envWf ext =
+  let
+    eq0 : (thin . id sx = id _ . thin)
+    eq0  = Calc $
+      |~ thin . id sx
+      ~~ thin          ...(compRightIdentity thin)
+      ~~ id _ . thin   ...(sym $ compLeftIdentity thin)
+
+    eq1 : (Base (thin . id sx) = restrict thin (Base (id _)))
+    eq1 = Calc $
+      |~ Base (thin . id sx)
+      ~~ Base (id _ . thin)          ...(cong Base eq0)
+      ~~ restrict thin (Base (id _)) ...(sym $ restrictBase thin (id _))
+
+    eq2 : wkn u (thin . id sx) = wkn (wkn u thin) (id _)
+    eq2 = Calc $
+      |~ wkn u (thin . id sx)
+      ~~ wkn u (id _ . thin)     ...(cong (wkn u) $ eq0)
+      ~~ wkn (wkn u thin) (id _) ...(sym $ wknHomo u thin (id _))
+
+    eq : (wkn (subst g (sub1 u)) thin = subst (wkn g (keep thin n)) (sub1 (wkn u thin)))
+    eq = Calc $
+      |~ wkn (subst g (sub1 u)) thin
+      ~~ subst g (Base (thin . id _) :< (u `Over` thin . id _))   ...(wknSubst g (sub1 u) thin)
+      ~~ subst g (Base (thin . id _) :< (wkn u thin `Over` id _)) ...(substCong g (Base :< eq2))
+      ~~ subst g (restrict thin _ :< (wkn u thin `Over` id _))    ...(cong (subst g . (:< (wkn u thin `Over` id _))) eq1)
+      ~~ subst g (restrict (keep thin n) (sub1 (wkn u thin)))     ...(sym $ cong (subst g) $ restrictKeep thin n (id _) (wkn u thin `Over` id _))
+      ~~ subst (wkn g (keep thin n)) (sub1 (wkn u thin))          ...(sym $ substWkn g (keep thin n) (sub1 (wkn u thin)))
+
+    eq' : (wkn (subst t (sub1 u)) thin = subst (wkn t (keep thin n)) (sub1 (wkn u thin)))
+    eq' = Calc $
+      |~ wkn (subst t (sub1 u)) thin
+      ~~ subst t (Base (thin . id _) :< (u `Over` thin . id _))   ...(wknSubst t (sub1 u) thin)
+      ~~ subst t (Base (thin . id _) :< (wkn u thin `Over` id _)) ...(substCong t (Base :< eq2))
+      ~~ subst t (restrict thin _ :< (wkn u thin `Over` id _))    ...(cong (subst t . (:< (wkn u thin `Over` id _))) eq1)
+      ~~ subst t (restrict (keep thin n) (sub1 (wkn u thin)))     ...(sym $ cong (subst t) $ restrictKeep thin n (id _) (wkn u thin `Over` id _))
+      ~~ subst (wkn t (keep thin n)) (sub1 (wkn u thin))          ...(sym $ substWkn t (keep thin n) (sub1 (wkn u thin)))
+  in
+  let wf' = wknPresTypeWf wf envWf ext in
+  rewrite eq in
+  rewrite eq' 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)
+wknPresTermConv (PiEta {f, n, t, u} wf wf1 wf2 conv) envWf ext =
+  let
+    eq : (0 t : Term sx) -> (wkn (wkn t thin) (wkn1 _ n) = wkn (wkn t (wkn1 sx n)) (keep thin n))
+    eq t = Calc $
+      |~ wkn (wkn t thin) (wkn1 _ n)
+      ~~ wkn t (wkn1 _ n . thin)               ...(wknHomo t thin (wkn1 _ n))
+      ~~ wkn t (drop thin n)                   ...(cong (wkn t) $ compLeftWkn1 thin n)
+      ~~ wkn t (keep thin n . wkn1 sx n)       ...(sym $ cong (wkn t) $ compRightWkn1 thin n)
+      ~~ wkn (wkn t (wkn1 sx n)) (keep thin n) ...(sym $ wknHomo t (wkn1 sx n) (keep thin n))
+
+    eq' :
+      (0 t : Term sx) ->
+      (App (wkn (wkn t thin) (wkn1 _ n)) (Var Var.here) = wkn (App (wkn t (wkn1 sx n)) (Var Var.here)) (keep thin n))
+    eq' t = cong2 App (eq t) (sym $ cong Var $ wknKeepHereIsHere thin n)
+  in
+  let wf' = wknPresTypeWf wf envWf ext in
+  PiEta wf'
+    (wknPresTermWf wf1 envWf ext)
+    (wknPresTermWf wf2 envWf ext)
+    (termConvRespEnvEq
+      (rewrite eq' t in
+       rewrite eq' u in
+       wknPresTermConv conv (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)))
+wknPresTermConv (AppConv {g, n, a} conv conv1) envWf ext =
+  let
+    eq0 : (thin . id sx = id _ . thin)
+    eq0  = Calc $
+      |~ thin . id sx
+      ~~ thin          ...(compRightIdentity thin)
+      ~~ id _ . thin   ...(sym $ compLeftIdentity thin)
+
+    eq1 : (Base (thin . id sx) = restrict thin (Base (id _)))
+    eq1 = Calc $
+      |~ Base (thin . id sx)
+      ~~ Base (id _ . thin)          ...(cong Base eq0)
+      ~~ restrict thin (Base (id _)) ...(sym $ restrictBase thin (id _))
+
+    eq2 : wkn a (thin . id sx) = wkn (wkn a thin) (id _)
+    eq2 = Calc $
+      |~ wkn a (thin . id sx)
+      ~~ wkn a (id _ . thin)     ...(cong (wkn a) $ eq0)
+      ~~ wkn (wkn a thin) (id _) ...(sym $ wknHomo a thin (id _))
+
+    eq : (wkn (subst g (sub1 a)) thin = subst (wkn g (keep thin n)) (sub1 (wkn a thin)))
+    eq = Calc $
+      |~ wkn (subst g (sub1 a)) thin
+      ~~ subst g (Base (thin . id _) :< (a `Over` thin . id _))   ...(wknSubst g (sub1 a) thin)
+      ~~ subst g (Base (thin . id _) :< (wkn a thin `Over` id _)) ...(substCong g (Base :< eq2))
+      ~~ subst g (restrict thin _ :< (wkn a thin `Over` id _))    ...(cong (subst g . (:< (wkn a thin `Over` id _))) eq1)
+      ~~ subst g (restrict (keep thin n) (sub1 (wkn a thin)))     ...(sym $ cong (subst g) $ restrictKeep thin n (id _) (wkn a thin `Over` id _))
+      ~~ subst (wkn g (keep thin n)) (sub1 (wkn a thin))          ...(sym $ substWkn g (keep thin n) (sub1 (wkn a thin)))
+  in
+  rewrite eq in
+  AppConv
+    (wknPresTermConv conv envWf ext)
+    (wknPresTermConv conv1 envWf ext)