Prove variable weakening is homomorphic.

1 files changed, 82 insertions, 3 deletions

diff --git a/src/Core/Var.idr b/src/Core/Var.idr
index e1f45a0..791151d 100644
--- a/src/Core/Var.idr
+++ b/src/Core/Var.idr
@@ -71,14 +71,93 @@ viewUnique view1 view2 =
   rewrite viewInversePrf1 view2 in
   Refl
 
--- Operations ------------------------------------------------------------------
+-- Weakening -------------------------------------------------------------------
 
 doWkn : Var sx -> {0 thin : sx `Thins` sy} -> View thin -> Var sy
+doWkn' : {0 i : Var (sx :< n)} -> View i -> sx `Thins` sy -> Var (sy :< n)
+
 doWkn i (Id sy) = i
 doWkn i (Drop thin n) = there $ doWkn i (view thin)
-doWkn (MakeVar 0 Here) (Keep thin n) = here
-doWkn (MakeVar (S k) (There prf)) (Keep thin n) = there $ doWkn (MakeVar k prf) (view thin)
+doWkn i (Keep thin n) = doWkn' (view i) thin
+
+doWkn' Here thin = here
+doWkn' (There i) thin = there $ doWkn i (view thin)
 
 export
 wkn : Var sx -> sx `Thins` sy -> Var sy
 wkn i thin = doWkn i (view thin)
+
+-- Is Homomorphic
+
+export
+doWknHomo :
+  (i : Var sx) ->
+  {thin1 : sx `Thins` sy} ->
+  {thin2 : sy `Thins` sz} ->
+  (view1 : View thin1) ->
+  (view2 : View thin2) ->
+  doWkn (doWkn i view1) view2 = wkn i (thin2 . thin1)
+doWknHomo' :
+  {0 i : Var (sx :< n)} ->
+  (v : View i) ->
+  (thin1 : sx `Thins` sy) ->
+  (thin2 : sy `Thins` sz) ->
+  doWkn' (view $ doWkn' v thin1) thin2 = doWkn' v (thin2 . thin1)
+
+doWknHomo i view1 (Id sz) =
+  rewrite compLeftIdentity thin1 in
+  cong (doWkn i) $ viewUnique view1 (view thin1)
+doWknHomo i view1 (Drop thin2 n) =
+  rewrite compLeftDrop thin2 thin1 n in
+  rewrite
+    viewUnique
+      (view $ drop (thin2 . thin1) n)
+      (Drop (thin2 . thin1) n)
+  in
+  cong there $ doWknHomo i view1 (view thin2)
+doWknHomo i (Id _) (Keep thin2 n) =
+  rewrite compRightIdentity $ keep thin2 n in
+  rewrite
+    viewUnique
+      (view $ keep thin2 n)
+      (Keep thin2 n)
+  in
+  Refl
+doWknHomo i (Drop thin1 n) (Keep thin2 n) =
+  rewrite compRightDrop thin2 thin1 n in
+  rewrite
+    viewUnique
+      (view $ drop (thin2 . thin1) n)
+      (Drop (thin2 . thin1) n)
+  in
+  rewrite
+    Var.viewUnique
+      (view $ there {n} $ doWkn i $ view thin1)
+      (There $ doWkn i $ view thin1)
+  in
+  cong there $ doWknHomo i (view thin1) (view thin2)
+doWknHomo i (Keep {prf = prf1} thin1 n) (Keep {prf = prf2} thin2 n) =
+  rewrite compKeep thin2 thin1 n in
+  rewrite
+    viewUnique
+      (view $ keep (thin2 . thin1) n)
+      (Keep {prf = compPresNotId prf2 prf1} (thin2 . thin1) n)
+  in
+  doWknHomo' (view i) thin1 thin2
+
+doWknHomo' Here thin1 thin2 = Refl
+doWknHomo' (There i) thin1 thin2 =
+  rewrite
+    viewUnique
+      (view $ there {n} $ doWkn i $ view thin1)
+      (There $ doWkn i $ view thin1)
+  in
+  cong there $ doWknHomo i (view thin1) (view thin2)
+
+export
+wknHomo :
+  (i : Var sx) ->
+  (thin1 : sx `Thins` sy) ->
+  (thin2 : sy `Thins` sz) ->
+  wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
+wknHomo i thin1 thin2 = doWknHomo i (view thin1) (view thin2)