2 files changed, 41 insertions, 182 deletions
diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index dead052..bbf6dd6 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -1,9 +1,8 @@
 module Data.Fin.Occurs
 
 import Data.DPair
-import Data.Fin.Strong
+import Data.Fin
 import Data.Maybe
-import Data.Maybe.Properties
 import Data.Nat
 
 import Syntax.PreorderReasoning
@@ -11,83 +10,67 @@ import Syntax.PreorderReasoning
 -- Thinning --------------------------------------------------------------------
 
 export
-thin : SFin n -> SFin (pred n) -> SFin n
-thin FZ y = FS' y
+thin : Fin (S n) -> Fin n -> Fin (S n)
+thin FZ y = FS y
 thin (FS x) FZ = FZ
 thin (FS x) (FS y) = FS (thin x y)
 
 -- Properties
 
 export
-thinInjective : (x : SFin n) -> {y, z : SFin (pred n)} -> thin x y = thin x z -> y = z
-thinInjective FZ prf = injective {f = FS'} prf
+thinInjective : (x : Fin (S n)) -> {y, z : Fin 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 : SFin n) -> (y : SFin (pred n)) -> Not (thin x y = x)
-thinSkips FZ y prf = sucNonZero y prf
+thinSkips : (x : Fin (S n)) -> (y : Fin n) -> Not (thin x y = x)
+thinSkips FZ y prf = absurd prf
 thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
 
-thinSuc : {n : Nat} -> (x : SFin (S n)) -> (y : SFin n) -> thin (FS x) (FS' y) = FS (thin x y)
-thinSuc {n = S n} x y = rewrite sucIsFS y in Refl
-
-export
-thinInverse : (x, y : SFin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
-thinInverse FZ FZ neq = void (neq Refl)
-thinInverse FZ (FS y) neq = (y ** sucIsFS y)
-thinInverse (FS x) FZ neq = (FZ ** Refl)
-thinInverse (FS x) (FS y) neq =
-  let (z ** prf) = thinInverse x y (\prf => neq $ cong FS prf) in
-  (FS' z ** trans (thinSuc x z) (cong FS $ prf))
-
 -- Thickening ------------------------------------------------------------------
 
 export
-thick : SFin n -> SFin n -> Maybe (SFin (pred n))
+thick : {n : Nat} -> Fin (S n) -> Fin (S n) -> Maybe (Fin n)
 thick FZ FZ = Nothing
 thick FZ (FS y) = Just y
-thick (FS x) FZ = Just FZ
-thick (FS x) (FS y) = FS' <$> thick x y
+thick {n = S n} (FS x) FZ = Just FZ
+thick {n = S n} (FS x) (FS y) = FS <$> thick x y
 
-export
-thickRefl : (x : SFin n) -> IsNothing (thick x x)
-thickRefl FZ = ItIsNothing
-thickRefl (FS x) = mapNothing FS' (thickRefl x)
+public export
+data ThickProof : Fin (S n) -> Fin (S n) -> Maybe (Fin n) -> Type where
+  Equal : res = Nothing -> ThickProof x x res
+  Thinned : (y : Fin n) -> res = Just y -> ThickProof x (thin x y) res
 
-export
-thickNeq : (x, y : SFin 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 FS' (thickNeq x y (\prf => neq $ cong FS prf))
+%name ThickProof prf
 
 export
-thickNothing : (x, y : SFin n) -> (0 _ : IsNothing (thick x y)) -> x = y
-thickNothing FZ FZ prf = Refl
-thickNothing (FS x) (FS y) prf =
-  cong FS (thickNothing x y (mapNothingInverse FS' (thick x y) prf))
+thickProof : {n : Nat} -> (x, y : Fin (S n)) -> ThickProof x y (thick x y)
+thickProof FZ FZ = Equal Refl
+thickProof FZ (FS y) = Thinned y Refl
+thickProof {n = S n} (FS x) FZ = Thinned FZ Refl
+thickProof {n = S n} (FS x) (FS y) with (thickProof x y)
+  thickProof (FS x) (FS x) | Equal prf = Equal (cong (map FS) prf)
+  thickProof (FS x) (FS _) | Thinned y prf = Thinned (FS y) (cong (map FS) prf)
+
+thickRefl' :
+  (x, y : Fin (S n)) ->
+  (0 _ : x = y) ->
+  ThickProof x y (thick x y) ->
+  thick x y = Nothing
+thickRefl' x x _ (Equal prf) = prf
+thickRefl' x (thin x z) prf (Thinned z _) = absurd $ thinSkips x z (sym prf)
 
-export thickJust : (x : SFin n) -> (y : SFin n) -> (0 _ : thick x y = Just z) -> thin x z = y
-thickJust FZ (FS y) Refl = sucIsFS y
-thickJust (FS x) FZ Refl = Refl
-thickJust (FS x) (FS y) prf =
-  let invertJust = mapJustInverse FS' (thick x y) prf in
-  Calc $
-    |~ thin (FS x) z
-    ~~ thin (FS x) (FS' invertJust.fst) ...(cong (thin (FS x)) $ snd invertJust.snd)
-    ~~ FS (thin x invertJust.fst)       ...(thinSuc x invertJust.fst)
-    ~~ FS y                             ...(cong FS $ thickJust x y (fst invertJust.snd))
+export
+thickRefl : {n : Nat} -> (x : Fin (S n)) -> thick x x = Nothing
+thickRefl x = thickRefl' x x Refl (thickProof x x)
 
 export
-thickThin : (x : SFin n) -> (y : SFin (pred n)) -> thick x (thin x y) = Just y
-thickThin x y =
-  let
-    fromJust =
-      extractIsJust $
-      thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf)
-  in
-  Calc $
-    |~ thick x (thin x y)
-    ~~ Just fromJust.fst  ...(fromJust.snd)
-    ~~ Just y             ...(cong Just $ thinInjective x $ thickJust x (thin x y) fromJust.snd)
+thickThin : {n : Nat} -> (x : Fin (S n)) -> (y : Fin n) -> thick x (thin x y) = Just y
+thickThin x y with (thin x y) proof prf
+  _ | z with (thickProof x z)
+    thickThin x y | x | Equal prf' = absurd $ thinSkips x y prf
+    thickThin x y | _ | Thinned z prf' = Calc $
+      |~ thick x (thin x z)
+      ~~ Just z             ...(prf')
+      ~~ Just y             ..<(cong Just $ thinInjective x prf)
diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
deleted file mode 100644
index 1fcd667..0000000
--- a/src/Data/Fin/Strong.idr
+++ /dev/null
@@ -1,124 +0,0 @@
-module Data.Fin.Strong
-
-import Data.Fin
-import Decidable.Equality.Core
-import Syntax.PreorderReasoning
-
--- Definition ------------------------------------------------------------------
-
-public export
-data SFin : Nat -> Type where
-  FZ : SFin (S n)
-  FS : SFin (S n) -> SFin (S (S n))
-
--- Properties
-
-export
-Injective (FS {n}) where
-  injective Refl = Refl
-
-export
-Uninhabited (SFin 0) where uninhabited x impossible
-
-export
-Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
-
--- Conversion ------------------------------------------------------------------
-
--- Utlities
-
-public export
-0 indexPred : (0 x : Fin n) -> Nat
-indexPred {n = S n} x = n
-
-public export
-0 indexPredPrf : (0 x : Fin n) -> n = S (indexPred x)
-indexPredPrf {n = S n} x = Refl
-
-public export
-0 indexPred' : (0 x : SFin n) -> Nat
-indexPred' {n = S n} x = n
-
-public export
-0 indexPred'Prf : (0 x : SFin n) -> n = S (indexPred' x)
-indexPred'Prf {n = S n} x = Refl
-
-public export
-finToStrong : Fin n -> SFin n
-finToStrong FZ = FZ
-finToStrong (FS x) =
-  rewrite indexPredPrf x in
-  FS (replace {p = SFin} (indexPredPrf x) (finToStrong x))
-
-public export
-strongToFin : SFin n -> Fin n
-strongToFin FZ = FZ
-strongToFin (FS x) = FS (strongToFin x)
-
--- Properties
-
-export
-finToStrongToFin : (x : Fin n) -> strongToFin (finToStrong x) = x
-finToStrongToFin FZ = Refl
-finToStrongToFin (FS FZ) = Refl
-finToStrongToFin (FS (FS x)) = cong FS $ finToStrongToFin (FS x)
-
-export
-strongToFinToStrong : (x : SFin n) -> finToStrong (strongToFin x) = x
-strongToFinToStrong FZ = Refl
-strongToFinToStrong (FS x) = cong FS (strongToFinToStrong x)
-
-export
-Injective (strongToFin {n}) where
-  injective {x, y} prf = Calc $
-    |~ x
-    ~~ finToStrong (strongToFin x) ..<(strongToFinToStrong x)
-    ~~ finToStrong (strongToFin y) ...(cong finToStrong prf)
-    ~~ y                           ...(strongToFinToStrong y)
-
--- Decidable Equality ----------------------------------------------------------
-
-export
-DecEq (SFin n) where
-  decEq x y = viaEquivalence
-    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
-    (decEq (strongToFin x) (strongToFin y))
-
--- Useful Constructor ----------------------------------------------------------
-
-%inline
-export
-FS' : SFin n -> SFin (S n)
-FS' = finToStrong . FS . strongToFin
-
-export
-Injective (FS' {n}) where
-  injective {x = FZ, y = FZ} prf = Refl
-  injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
-
-export
-sucNonZero : (x : SFin n) -> Not (FS' x = FZ)
-sucNonZero FZ prf = absurd prf
-sucNonZero (FS x) prf = absurd prf
-
-export
-sucIsFS : (x : SFin (S n)) -> FS' x = FS x
-sucIsFS x = rewrite strongToFinToStrong x in Refl
-
--- Num Interface ---------------------------------------------------------------
-
-public export
-{n : Nat} -> Num (SFin (S n)) where
-  x + y = finToStrong (strongToFin x + strongToFin y)
-  x * y = finToStrong (strongToFin x * strongToFin y)
-  fromInteger = finToStrong . restrict n
-
--- Weaken and Shift ------------------------------------------------------------
-
-export
-weakenN : (0 k : Nat) -> SFin n -> SFin (n + k)
-weakenN k = finToStrong . weakenN k . strongToFin
-
-export
-shift : (k : Nat) -> SFin n -> SFin (k + n)
-shift k = finToStrong . shift k . strongToFin