Add occurs check for terms.

1 files changed, 32 insertions, 30 deletions

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index 899e2a1..58c8faa 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -45,23 +45,24 @@ 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)
 
+%inline
 thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
-thinSucZero FZ = Refl
-thinSucZero (FS x) = Refl
+thinSucZero x = rewrite snd (indexIsSuc x) in Refl
 
+%inline
 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 FZ (FS z) = Refl
 thinSucSuc (FS x) FZ = Refl
-thinSucSuc (FS x) (FS y) = Refl
+thinSucSuc (FS x) (FS z) = Refl
 
 export
-thinInverse : (x, y : Fin n) -> Not (x = y) -> (z ** thin x z = y)
+thinInverse : (x, y : Fin n) -> (0 _ : 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
+  let (z ** prf) = thinInverse x y (neq . cong FS) in
   (suc z ** trans (thinSucSuc x z) (cong FS prf))
 
 -- Thickening ------------------------------------------------------------------
@@ -71,31 +72,32 @@ 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) |]
+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))
+thickRefl : (x : Fin n) -> IsNothing (thick x x)
+thickRefl FZ = ItIsNothing
+thickRefl (FS x) = mapNothing suc (thickRefl x)
 
 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))
+thickNeq : (x, y : Fin n) -> (0 _ : Not (x = y)) -> IsJust (thick x y)
+thickNeq FZ FZ neq = void (neq Refl)
+thickNeq FZ (FS y) neq = ItIsJust
+thickNeq (FS x) FZ neq = ItIsJust
+thickNeq (FS x) (FS y) neq = mapIsJust suc (thickNeq x y (neq . cong FS))
+
+export
+thickNothing : (x, y : Fin n) -> (0 _ : IsNothing (thick x y)) -> x = y
+thickNothing FZ FZ prf = Refl
+thickNothing (FS x) (FS y) prf =
+  rewrite thickNothing x y (mapNothingInverse suc (thick x y) prf) in
+  Refl
+
+export
+thickJust : (x, y : Fin n) -> (0 _ : thick x y = Just z) -> thin x z = y
+thickJust FZ (FS y) Refl = Refl
+thickJust (FS x) FZ Refl = thinSucZero x
+thickJust (FS x) (FS y) prf =
+  let 0 z = mapJustInverse suc (thick x y) prf in
+  rewrite snd $ z.snd in
+  trans (thinSucSuc x z.fst) (cong FS $ thickJust x y (fst $ z.snd))