From 60df32ffd5b88498e4634649509bbd0810421004 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 11 Jul 2023 16:25:24 +0100
Subject: Begin big unification proof.

---
 src/Data/Fin/Strong.idr | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'src/Data/Fin')

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
@@ -60,6 +62,14 @@ 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
+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
 
@@ -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))
-- 
cgit v1.2.3