Prove properties of thinning composition.

1 files changed, 103 insertions, 0 deletions

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index 1c8f41f..5c380df 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -2,6 +2,8 @@ module Core.Thinning
 
 import Core.Context
 
+import Syntax.PreorderReasoning
+
 -- Definition ------------------------------------------------------------------
 
 data Thinner : Context -> Context -> Type where
@@ -72,3 +74,104 @@ export
 IsId . thin1 = thin1
 (IsThinner thinner2) . IsId = IsThinner thinner2
 (IsThinner thinner2) . (IsThinner thinner1) = comp thinner2 thinner1
+
+-- Composition Properties ------------------------------------------------------
+
+-- Identities
+
+export
+compLeftIdentity : (thin : sx `Thins` sy) -> id sy . thin = thin
+compLeftIdentity thin = Refl
+
+export
+compRightIdentity : (thin : sx `Thins` sy) -> thin . id sx = thin
+compRightIdentity IsId = Refl
+compRightIdentity (IsThinner thinner) = Refl
+
+-- Drop
+
+export
+compLeftDrop :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  (0 n : Name) ->
+  drop thin2 n . thin1 = drop (thin2 . thin1) n
+compLeftDrop IsId IsId n = Refl
+compLeftDrop IsId (IsThinner thinner) n = Refl
+compLeftDrop (IsThinner thinner) IsId n = Refl
+compLeftDrop (IsThinner thinner) (IsThinner thinner1) n = Refl
+
+export
+compRightDrop :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  (0 n : Name) ->
+  keep thin2 n . drop thin1 n = drop (thin2 . thin1) n
+compRightDrop IsId thin1 n = Refl
+compRightDrop (IsThinner thinner) IsId n = Refl
+compRightDrop (IsThinner thinner) (IsThinner thinner1) n = Refl
+
+-- Keep
+
+export
+compKeep :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  (0 n : Name) ->
+  keep thin2 n . keep thin1 n = keep (thin2 . thin1) n
+compKeep IsId thin1 n = Refl
+compKeep (IsThinner thinner) IsId n = Refl
+compKeep (IsThinner thinner) (IsThinner thinner1) n = Refl
+
+-- Associative
+
+compAssoc' :
+  {thin3 : sz `Thins` sw} ->
+  {thin2 : sy `Thins` sz} ->
+  {thin1 : sx `Thins` sy} ->
+  View thin3 ->
+  View thin2 ->
+  View thin1 ->
+  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
+
+compAssoc' (Id sw) view2 view1 = Refl
+compAssoc' (Drop thin3 n) view2 view1 = Calc $
+  |~ drop thin3 n . (thin2 . thin1)
+  ~~ drop (thin3 . (thin2 . thin1)) n ...(compLeftDrop thin3 (thin2 . thin1) n)
+  ~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) view2 view1)
+  ~~ drop (thin3 . thin2) n . thin1   ..<(compLeftDrop (thin3 . thin2) thin1 n)
+  ~~ (drop thin3 n . thin2) . thin1   ..<(cong (. thin1) $ compLeftDrop thin3 thin2 n)
+compAssoc' (Keep thin3 n _) (Id _) view1 = cong (. thin1) $ sym $ compRightIdentity (keep thin3 n)
+compAssoc' (Keep thin3 n _) (Drop thin2 n) view1 = Calc $
+  |~ keep thin3 n . (drop thin2 n . thin1)
+  ~~ keep thin3 n . drop (thin2 . thin1) n ...(cong (keep thin3 n .) $ compLeftDrop thin2 thin1 n)
+  ~~ drop (thin3 . (thin2 . thin1)) n      ...(compRightDrop thin3 (thin2 . thin1) n)
+  ~~ drop ((thin3 . thin2) . thin1) n      ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) view1)
+  ~~ drop (thin3 . thin2) n . thin1        ..<(compLeftDrop (thin3 . thin2) thin1 n)
+  ~~ (keep thin3 n . drop thin2 n) . thin1 ..<(cong (. thin1) $ compRightDrop thin3 thin2 n)
+compAssoc' (Keep thin3 n _) (Keep thin2 n _) (Id _) = Calc $
+  |~ keep thin3 n . (keep thin2 n . id _)
+  ~~ keep thin3 n . keep thin2 n          ...(cong (keep thin3 n .) $ compRightIdentity (keep thin2 n))
+  ~~ (keep thin3 n . keep thin2 n) . id _ ..<(compRightIdentity (keep thin3 n . keep thin2 n))
+compAssoc' (Keep thin3 n _) (Keep thin2 n _) (Drop thin1 n) = Calc $
+  |~ keep thin3 n . (keep thin2 n . drop thin1 n)
+  ~~ keep thin3 n . drop (thin2 . thin1) n        ...(cong (keep thin3 n .) $ compRightDrop thin2 thin1 n)
+  ~~ drop (thin3 . (thin2 . thin1)) n             ...(compRightDrop thin3 (thin2 . thin1) n)
+  ~~ drop ((thin3 . thin2) . thin1) n             ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) (view thin1))
+  ~~ keep (thin3 . thin2) n . drop thin1 n        ..<(compRightDrop (thin3 . thin2) thin1 n)
+  ~~ (keep thin3 n . keep thin2 n) . drop thin1 n ..<(cong (. drop thin1 n) $ compKeep thin3 thin2 n)
+compAssoc' (Keep thin3 n _) (Keep thin2 n _) (Keep thin1 n _) = Calc $
+  |~ keep thin3 n . (keep thin2 n . keep thin1 n)
+  ~~ keep thin3 n . keep (thin2 . thin1) n        ...(cong (keep thin3 n .) $ compKeep thin2 thin1 n)
+  ~~ keep (thin3 . (thin2 . thin1)) n             ...(compKeep thin3 (thin2 . thin1) n)
+  ~~ keep ((thin3 . thin2) . thin1) n             ...(cong (\thin => keep thin n) $ compAssoc' (view thin3) (view thin2) (view thin1))
+  ~~ keep (thin3 . thin2) n . keep thin1 n        ..<(compKeep (thin3 . thin2) thin1 n)
+  ~~ (keep thin3 n . keep thin2 n) . keep thin1 n ..<(cong (. keep thin1 n) $ compKeep thin3 thin2 n)
+
+export
+compAssoc :
+  (thin3 : sz `Thins` sw) ->
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
+compAssoc thin3 thin2 thin1 = compAssoc' (view thin3) (view thin2) (view thin1)