From 60d5896ab7939ae42cf7744f93e8eaefa0675854 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 11 Jul 2023 13:54:54 +0100
Subject: Use new notion of Fin to reduce casts.

---
 src/Data/Fin/Strong.idr | 76 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100644 src/Data/Fin/Strong.idr

(limited to 'src/Data/Fin/Strong.idr')

diff --git a/src/Data/Fin/Strong.idr b/src/Data/Fin/Strong.idr
new file mode 100644
index 0000000..ebf3483
--- /dev/null
+++ b/src/Data/Fin/Strong.idr
@@ -0,0 +1,76 @@
+module Data.Fin.Strong
+
+import Data.Fin
+
+public export
+data SFin : Nat -> Type where
+  FZ : SFin (S n)
+  FS : SFin (S n) -> SFin (S (S n))
+
+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)
+
+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)
+
+%inline
+export
+FS' : SFin n -> SFin (S n)
+FS' = finToStrong . FS . strongToFin
+
+export
+Injective (FS {n}) where
+  injective Refl = Refl
+
+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
+Uninhabited (SFin 0) where uninhabited x impossible
+
+export
+Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
+
+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
-- 
cgit v1.2.3