Prove variable Views are unique.

1 files changed, 26 insertions, 0 deletions

diff --git a/src/Core/Var.idr b/src/Core/Var.idr
index 4e357aa..e1f45a0 100644
--- a/src/Core/Var.idr
+++ b/src/Core/Var.idr
@@ -45,6 +45,32 @@ view : (i : Var sx) -> View i
 view (MakeVar 0 Here) = Here
 view (MakeVar (S k) (There prf)) = There (MakeVar k prf)
 
+-- Views are Unique
+
+viewInverse : {0 i : Var sx} -> View i -> Var sx
+viewInverse Here = here
+viewInverse (There i) = there i
+
+viewInversePrf1 : (view : View i) -> viewInverse view = i
+viewInversePrf1 Here = Refl
+viewInversePrf1 (There i) = Refl
+
+viewInversePrf2 :
+  {0 i : Var sx} ->
+  (v : View i) ->
+  view (viewInverse v) = (rewrite viewInversePrf1 v in v)
+viewInversePrf2 Here = Refl
+viewInversePrf2 (There (MakeVar index prf)) = Refl
+
+export
+viewUnique : {0 i : Var sx} -> (view1, view2 : View i) -> view1 = view2
+viewUnique view1 view2 =
+  rewrite sym $ viewInversePrf2 view1 in
+  rewrite sym $ viewInversePrf2 view2 in
+  rewrite viewInversePrf1 view1 in
+  rewrite viewInversePrf1 view2 in
+  Refl
+
 -- Operations ------------------------------------------------------------------
 
 doWkn : Var sx -> {0 thin : sx `Thins` sy} -> View thin -> Var sy