Prove thinning Views are unique.

1 files changed, 29 insertions, 3 deletions

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index 7ef2562..0b1de68 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -60,7 +60,35 @@ view (IsThinner (IsBase n)) = Drop IsId n
 view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n
 view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n
 
--- Operations ------------------------------------------------------------------
+-- Unique
+
+viewInverse : {0 thin : sx `Thins` sy} -> View thin -> sx `Thins` sy
+viewInverse (Id sy) = id sy
+viewInverse (Drop thin n) = drop thin n
+viewInverse (Keep thin n) = keep thin n
+
+viewInversePrf1 : (view : View thin) -> viewInverse view = thin
+viewInversePrf1 (Id _) = Refl
+viewInversePrf1 (Drop _ _) = Refl
+viewInversePrf1 (Keep _ _) = Refl
+
+viewInversePrf2 : (v : View thin) -> view (viewInverse v) = (rewrite viewInversePrf1 v in v)
+viewInversePrf2 (Id sy) = Refl
+viewInversePrf2 (Drop IsId n) = Refl
+viewInversePrf2 (Drop (IsThinner thinner) n) = Refl
+viewInversePrf2 (Keep {prf} IsId n) impossible
+viewInversePrf2 (Keep {prf = ItIsThinner} (IsThinner thinner) n) = Refl
+
+export
+viewUnique : (view1, view2 : View thin) -> view1 = view2
+viewUnique view1 view2 =
+  rewrite sym $ viewInversePrf2 view1 in
+  rewrite sym $ viewInversePrf2 view2 in
+  rewrite viewInversePrf1 view1 in
+  rewrite viewInversePrf1 view2 in
+  Refl
+
+-- Composition -----------------------------------------------------------------
 
 comp : Thinner sy sz -> Thinner sx sy -> Thinner sx sz
 comp (IsBase n) thinner1 = IsDrop thinner1 n
@@ -75,8 +103,6 @@ IsId . thin1 = thin1
 (IsThinner thinner2) . IsId = IsThinner thinner2
 (IsThinner thinner2) . (IsThinner thinner1) = IsThinner (comp thinner2 thinner1)
 
--- Composition Properties ------------------------------------------------------
-
 -- Identities
 
 export