Define thinning and thickening.

3 files changed, 106 insertions, 1 deletions

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
new file mode 100644
index 0000000..74199d3
--- /dev/null
+++ b/src/Data/Fin/Occurs.idr
@@ -0,0 +1,100 @@
+module Data.Fin.Occurs
+
+import Data.DPair
+import Data.Fin
+import Data.Maybe.Properties
+
+-- Utilities -------------------------------------------------------------------
+
+predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
+predInjective {n = S n} prf = cong S prf
+
+indexIsSuc : Fin n -> Exists (\k => n = S k)
+indexIsSuc FZ = Evidence _ Refl
+indexIsSuc (FS x) = Evidence _ Refl
+
+%inline %tcinline
+zero : (0 _ : Fin n) -> Fin n
+zero x = rewrite snd (indexIsSuc x) in FZ
+
+%inline %tcinline
+suc : (_ : Fin (pred n)) -> Fin n
+suc x =
+  replace {p = Fin}
+    (sym $ predInjective $ snd $ indexIsSuc x)
+    (FS $ rewrite sym $ snd $ indexIsSuc x in x)
+
+-- Thinning --------------------------------------------------------------------
+
+export
+thin : Fin n -> Fin (pred n) -> Fin n
+thin FZ y = FS y
+thin (FS x) FZ = FZ
+thin (FS x) (FS y) = FS (thin x y)
+
+-- Properties
+
+export
+thinInjective : (x : Fin n) -> {y, z : Fin (pred n)} -> thin x y = thin x z -> y = z
+thinInjective FZ prf = injective prf
+thinInjective (FS x) {y = FZ, z = FZ} prf = Refl
+thinInjective (FS x) {y = FS y, z = FS z} prf = cong FS $ thinInjective x $ injective prf
+
+export
+thinSkips : (x : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x)
+thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
+
+thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
+thinSucZero FZ = Refl
+thinSucZero (FS x) = Refl
+
+thinSucSuc : (x : Fin n) -> (z : Fin (pred n)) -> thin (FS x) (suc z) = FS (thin x z)
+thinSucSuc FZ FZ = Refl
+thinSucSuc FZ (FS x) = Refl
+thinSucSuc (FS x) FZ = Refl
+thinSucSuc (FS x) (FS y) = Refl
+
+export
+thinInverse : (x, y : Fin n) -> Not (x = y) -> (z ** thin x z = y)
+thinInverse FZ FZ neq = void (neq Refl)
+thinInverse FZ (FS y) neq = (y ** Refl)
+thinInverse (FS x) FZ neq = (zero x ** thinSucZero x)
+thinInverse (FS x) (FS y) neq =
+  let (z ** prf) = thinInverse x y (\eq => neq $ cong FS eq) in
+  (suc z ** trans (thinSucSuc x z) (cong FS prf))
+
+-- Thickening ------------------------------------------------------------------
+
+export
+thick : Fin n -> Fin n -> Maybe (Fin (pred n))
+thick FZ FZ = Nothing
+thick FZ (FS y) = Just y
+thick (FS x) FZ = Just (zero x)
+thick (FS x) (FS y) = [| suc (thick x y) |]
+
+export
+thickIsNothing : (x, y : Fin n) -> (x = y) <=> (thick x y = Nothing)
+thickIsNothing FZ FZ = MkEquivalence (const Refl) (const Refl)
+thickIsNothing FZ (FS y) = MkEquivalence absurd absurd
+thickIsNothing (FS x) FZ = MkEquivalence absurd absurd
+thickIsNothing (FS x) (FS y) =
+  let rec = thickIsNothing x y in
+  MkEquivalence
+    (cong (Just suc <*>) . rec.leftToRight . injective)
+    (cong FS . rec.rightToLeft . appNothingRight suc (thick x y))
+
+export
+thickIsJust : (x, y : Fin n) -> Not (x = y) <=> (z ** (thick x y = Just z, thin x z = y))
+thickIsJust FZ FZ = MkEquivalence (\f => absurd $ f Refl) (\p => absurd $ fst $ snd p)
+thickIsJust FZ (FS y) = MkEquivalence (const (y ** (Refl, Refl))) (const absurd)
+thickIsJust (FS x) FZ =
+  MkEquivalence
+    (const (zero x ** (Refl, thinSucZero x)))
+    (const absurd)
+thickIsJust (FS x) (FS y) =
+  let rec = thickIsJust x y in
+  MkEquivalence
+    (\neq =>
+      let (z ** (prf1, prf2)) = rec.leftToRight (neq . cong FS) in
+      (suc z ** (rewrite prf1 in Refl, trans (thinSucSuc x z) (cong FS prf2))))
+    (\(z ** (prf1, prf2)), prf => thinSkips (FS x) z $ trans prf2 (sym prf))
diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
index f00b79f..495256e 100644
--- a/src/Data/Maybe/Properties.idr
+++ b/src/Data/Maybe/Properties.idr
@@ -4,3 +4,7 @@ export
 mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
 mapFusion Nothing = Refl
 mapFusion (Just x) = Refl
+
+export
+appNothingRight : (0 f : a -> b) -> (y : Maybe a) -> Just f <*> y = Nothing -> y = Nothing
+appNothingRight f Nothing prf = Refl
diff --git a/unify.ipkg b/unify.ipkg
index 06f2f78..7b0e0dd 100644
--- a/unify.ipkg
+++ b/unify.ipkg
@@ -7,5 +7,6 @@ options = "--total"
 depends = contrib
 
 modules
-  = Data.Maybe.Properties
+  = Data.Fin.Occurs
+  , Data.Maybe.Properties
   , Data.Term