Prove weakening interacts well with extension.

1 files changed, 54 insertions, 0 deletions

diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr
index 1fe8e28..b9fbfd8 100644
--- a/src/Core/Environment.idr
+++ b/src/Core/Environment.idr
@@ -99,3 +99,57 @@ doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $
 export
 indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i
 indexEqIsEq prf i = doIndexEqIsEq prf $ view i
+
+-- Interaction with Extension
+
+doWknIndex :
+  {0 thin : sx `Thins` sy} ->
+  IsExtension thin env2 env1 ->
+  (v : View i) ->
+  wkn (expand $ doIndex env1 v) thin = expand (doIndex env2 $ view $ wkn i thin)
+doWknIndex IdWf v =
+  rewrite wknId i in
+  Calc $
+  |~ wkn (expand $ doIndex env2 v) (id sy)
+  ~~ expand (doIndex env2 v)               ...(wknId (expand $ doIndex env2 v))
+  ~~ expand (doIndex env2 $ view i)        ...(cong (expand . doIndex env2) $ viewUnique v (view i))
+doWknIndex {sy = sy :< n} (DropWf {env2, thin, n, t} ext) v =
+  rewrite wknDropIsThere i thin n in
+  rewrite viewUnique (view $ there {n} $ wkn i thin) (There $ wkn i thin) in
+  Calc $
+  |~ wkn (expand (doIndex env1 v)) (drop thin n)
+  ~~ wkn (expand (doIndex env1 v)) (wkn1 sy n . thin)            ...(sym $ cong (wkn _) $ compLeftWkn1 thin n)
+  ~~ wkn (wkn (expand $ doIndex env1 v) thin) (wkn1 sy n)        ...(sym $ wknHomo (expand $ doIndex env1 v) thin (wkn1 sy n))
+  ~~ wkn (expand $ doIndex env2 $ view $ wkn i thin) (wkn1 sy n) ...(cong (\t => wkn t (wkn1 sy n)) $ doWknIndex ext v)
+  ~~ expand (doIndex (Add env2 t) (There $ wkn i thin))          ...(sym $ expandShift (doIndex env2 $ view $ wkn i thin) (wkn1 sy n))
+doWknIndex {sx = sx :< n, sy = sy :< n} (KeepWf {thin, n, t} ext) Here =
+  rewrite wknKeepHereIsHere thin n in
+  rewrite viewUnique (view $ here {sx = sy, n}) Here in
+  Calc $
+  |~ wkn (expand $ shift t (wkn1 sx n)) (keep thin n)
+  ~~ wkn (wkn (expand t) (wkn1 sx n)) (keep thin n)   ...(cong (\t => wkn t (keep thin n)) $ expandShift t (wkn1 sx n))
+  ~~ wkn (expand t) (keep thin n . wkn1 sx n)         ...(wknHomo (expand t) (wkn1 sx n) (keep thin n))
+  ~~ wkn (expand t) (drop thin n)                     ...(cong (wkn $ expand t) $ compRightWkn1 thin n)
+  ~~ wkn (expand t) (wkn1 sy n . thin)                ...(sym $ cong (wkn $ expand t) $ compLeftWkn1 thin n)
+  ~~ wkn (wkn (expand t) thin) (wkn1 sy n)            ...(sym $ wknHomo (expand t) thin (wkn1 sy n))
+  ~~ wkn (expand $ shift t thin) (wkn1 sy n)          ...(sym $ cong (\t => wkn t (wkn1 sy n)) $ expandShift t thin)
+  ~~ expand (shift (shift t thin) (wkn1 sy n))        ...(sym $ expandShift (shift t thin) (wkn1 sy n))
+doWknIndex {sx = sx :< n, sy = sy :< n} (KeepWf {env1, env2, thin, n, t} ext) (There i) =
+  rewrite wknKeepThereIsThere i thin n in
+  rewrite viewUnique (view $ there {n} $ wkn i thin) (There $ wkn i thin) in
+  Calc $
+  |~ wkn (expand $ shift (doIndex env1 $ view i) (wkn1 sx n)) (keep thin n)
+  ~~ wkn (wkn (expand $ doIndex env1 $ view i) (wkn1 sx n)) (keep thin n)   ...(cong (\t => wkn t (keep thin n)) $ expandShift (doIndex env1 $ view i) (wkn1 sx n))
+  ~~ wkn (expand $ doIndex env1 $ view i) (keep thin n . wkn1 sx n)         ...(wknHomo _ (wkn1 sx n) (keep thin n))
+  ~~ wkn (expand $ doIndex env1 $ view i) (drop thin n)                     ...(cong (wkn (expand $ doIndex env1 $ view i)) $ compRightWkn1 thin n)
+  ~~ wkn (expand $ doIndex env1 $ view i) (wkn1 sy n . thin)                ...(sym $ cong (wkn _) $ compLeftWkn1 thin n)
+  ~~ wkn (wkn (expand $ doIndex env1 $ view i) thin) (wkn1 sy n)            ...(sym $ wknHomo _ thin (wkn1 sy n))
+  ~~ wkn (expand $ doIndex env2 $ view $ wkn i thin) (wkn1 sy n)            ...(cong (\t => wkn t (wkn1 sy n)) $ doWknIndex ext $ view i)
+  ~~ expand (doIndex (Add env2 (shift t thin)) (There $ wkn i thin))        ...(sym $ expandShift (doIndex env2 $ view $ wkn i thin) (wkn1 sy n))
+
+export
+wknIndex :
+  IsExtension thin env2 env1 ->
+  (i : Var sx) ->
+  wkn (index env1 i) thin = index env2 (wkn i thin)
+wknIndex ext i = doWknIndex ext (view i)