Define terms and thinnings.

1 files changed, 60 insertions, 0 deletions

diff --git a/src/Thinning.idr b/src/Thinning.idr
new file mode 100644
index 0000000..9de57fb
--- /dev/null
+++ b/src/Thinning.idr
@@ -0,0 +1,60 @@
+module Thinning
+
+import Data.SnocList.Elem
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Thins : SnocList a -> SnocList a -> Type
+public export
+data NotId : Thins sx sy -> Type
+
+data Thins where
+  Id : sx `Thins` sx
+  Drop : sx `Thins` sy -> sx `Thins` sy :< z
+  Keep :
+    (thin : sx `Thins` sy) ->
+    {auto 0 prf : NotId thin} ->
+    sx :< z `Thins` sy :< z
+
+data NotId where
+  DropNotId : NotId (Drop thin)
+  KeepNotId : (0 prf : NotId thin) -> NotId (Keep thin)
+
+%name Thins thin
+
+-- Smart Constructors ----------------------------------------------------------
+
+export
+keep : sx `Thins` sy -> sx :< z `Thins` sy :< z
+keep Id = Id
+keep (Drop thin) = Keep (Drop thin)
+keep (Keep thin) = Keep (Keep thin)
+
+-- Operations ------------------------------------------------------------------
+
+export
+index : sx `Thins` sy -> Elem z sx -> Elem z sy
+index Id i = i
+index (Drop thin) i = There (index thin i)
+index (Keep thin) Here = Here
+index (Keep thin) (There i) = There (index thin i)
+
+export
+(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
+compNotId :
+  (thin2 : sy `Thins` sz) ->
+  (thin1 : sx `Thins` sy) ->
+  {auto 0 _ : NotId thin2} ->
+  {auto 0 _ : NotId thin1} ->
+  NotId (thin2 . thin1)
+
+Id . thin1 = thin1
+(Drop thin2) . thin1 = Drop (thin2 . thin1)
+(Keep thin2) . Id = Keep thin2
+(Keep thin2) . (Drop thin1) = Drop (thin2 . thin1)
+(Keep thin2) . (Keep thin1) = Keep {prf = compNotId thin2 thin1} (thin2 . thin1)
+
+compNotId (Drop thin2) thin1 = DropNotId
+compNotId (Keep thin2) (Drop thin1) = DropNotId
+compNotId (Keep thin2) (Keep thin1) = KeepNotId (compNotId thin2 thin1)