Begin big unification proof.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
index ebf3483..a0ed5df 100644
--- a/src/Data/Fin/Strong.idr
+++ b/src/Data/Fin/Strong.idr
@@ -1,6 +1,8 @@
 module Data.Fin.Strong
 
 import Data.Fin
+import Decidable.Equality.Core
+import Syntax.PreorderReasoning
 
 public export
 data SFin : Nat -> Type where
@@ -61,6 +63,14 @@ Injective (FS' {n}) where
   injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
 
 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)
+
+export
 Uninhabited (SFin 0) where uninhabited x impossible
 
 export
@@ -74,3 +84,9 @@ sucNonZero (FS x) prf = absurd prf
 export
 sucIsFS : (x : SFin (S n)) -> FS' x = FS x
 sucIsFS x = rewrite strongToFinToStrong x in Refl
+
+export
+DecEq (SFin n) where
+  decEq x y = viaEquivalence
+    (MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
+    (decEq (strongToFin x) (strongToFin y))