From 4f112495da9b05a83b56d572dbd188183901d8b4 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 2 Apr 2023 09:41:38 +0100
Subject: Prove thinning Views are unique.

---
 src/Core/Thinning.idr | 32 +++++++++++++++++++++++++++++---
 1 file changed, 29 insertions(+), 3 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3