Prove environment indexing preserves equality.

1 files changed, 39 insertions, 11 deletions

diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
index 4f167f9..d292a96 100644
--- a/src/Core/Term/Environment.idr
+++ b/src/Core/Term/Environment.idr
@@ -5,6 +5,8 @@ import Core.Term
 import Core.Thinning
 import Core.Var
 
+import Syntax.PreorderReasoning
+
 %prefix_record_projections off
 
 -- Definition ------------------------------------------------------------------
@@ -30,17 +32,19 @@ record IndexResult (sx : Context) where
   val : Term sy
   thin : sy `Thins` sx
 
+shift : IndexResult sx -> IndexResult (sx :< n)
+shift (MkRes val thin) = MkRes val (drop thin n)
+
+expand : IndexResult sx -> Term sx
+expand (MkRes val thin) = wkn val thin
+
 doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
-doIndex (Add env thin t) Here = MkRes t (drop thin _)
-doIndex (Add env thin t) (There i) =
-  let MkRes val thin = doIndex env $ view i in
-  MkRes val (drop thin _)
+doIndex (Add env thin t) Here = shift $ MkRes t thin
+doIndex (Add env thin t) (There i) = shift $ doIndex env $ view i
 
 export
 index : Env sx -> Var sx -> Term sx
-index env i =
-  let MkRes val thin = doIndex env $ view i in
-  wkn val thin
+index env i = expand $ doIndex env $ view i
 
 -- Equality --------------------------------------------------------------------
 
@@ -48,13 +52,37 @@ namespace Eq
   public export
   data EnvEq : Env sx -> Env sx -> Type where
     Lin : EnvEq [<] [<]
-    Add :
+    (:<) :
       EnvEq env1 env2 ->
       Term.wkn t thin1 = wkn u thin2 ->
       EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
 
   %name EnvEq prf
 
-  public export
-  (:<) : EnvEq env1 env2 -> (0 t : Term sx) -> EnvEq (env1 :< t) (env2 :< t)
-  prf :< t = Add prf Refl
+expandShift : (val : IndexResult sx) -> expand (shift val) = wkn (expand val) (drop (id sx) n)
+expandShift (MkRes val thin) = sym $ Calc $
+  |~ wkn (wkn val thin) (drop (id sx) n)
+  ~~ wkn val (drop (id sx) n . thin)     ...(wknHomo val thin $ drop (id sx) n)
+  ~~ wkn val (drop (id sx . thin) n)     ...(cong (wkn val) $ compLeftDrop (id sx) thin n)
+  ~~ wkn val (drop thin n)               ...(cong (\thin => wkn val (drop thin n)) $ compLeftIdentity thin)
+
+doIndexEqIsEq :
+  -- {env1, env2 : _} ->
+  EnvEq env1 env2 ->
+  {0 i : Var sx} ->
+  (view : View i) ->
+  expand (doIndex env1 view) = expand (doIndex env2 view)
+doIndexEqIsEq {sx = sx :< n} ((:<) {t, u, thin1, thin2} prf eq) Here = Calc $
+  |~ wkn t (drop thin1 n)
+  ~~ wkn (wkn t thin1) (drop (id sx) n) ...(expandShift (MkRes t thin1))
+  ~~ wkn (wkn u thin2) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ eq)
+  ~~ wkn u (drop thin2 n)               ...(sym $ expandShift (MkRes u thin2))
+doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $
+  |~ expand (shift $ doIndex env1 $ view i)
+  ~~ wkn (expand $ doIndex env1 $ view i) (drop (id sx) n) ...(expandShift $ doIndex env1 $ view i)
+  ~~ wkn (expand $ doIndex env2 $ view i) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ doIndexEqIsEq prf (view i))
+  ~~ expand (shift $ doIndex env2 $ view i)                ...(sym $ expandShift $ doIndex env2 $ view i)
+
+export
+indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i
+indexEqIsEq prf i = doIndexEqIsEq prf $ view i