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/Occurs.idr | 111 ++++++++++++++++++++----------------------------
 src/Data/Fin/Strong.idr |  76 +++++++++++++++++++++++++++++++++
 2 files changed, 121 insertions(+), 66 deletions(-)
 create mode 100644 src/Data/Fin/Strong.idr

(limited to 'src/Data/Fin')

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index d70c8f3..dead052 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -1,114 +1,93 @@
 module Data.Fin.Occurs
 
 import Data.DPair
-import Data.Fin
+import Data.Fin.Strong
+import Data.Maybe
 import Data.Maybe.Properties
+import Data.Nat
 
--- Utilities -------------------------------------------------------------------
-
-predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
-predInjective {n = S n} prf = cong S prf
-
-public export
-indexIsSuc : Fin n -> Exists (\k => n = S k)
-indexIsSuc FZ = Evidence _ Refl
-indexIsSuc (FS x) = Evidence _ Refl
-
-%inline %tcinline
-zero : (0 _ : Fin n) -> Fin n
-zero x = rewrite snd (indexIsSuc x) in FZ
-
-%inline %tcinline
-suc : (_ : Fin (pred n)) -> Fin n
-suc x =
-  replace {p = Fin}
-    (sym $ predInjective $ snd $ indexIsSuc x)
-    (FS $ rewrite sym $ snd $ indexIsSuc x in x)
+import Syntax.PreorderReasoning
 
 -- Thinning --------------------------------------------------------------------
 
 export
-thin : Fin n -> Fin (pred n) -> Fin n
-thin FZ y = FS y
+thin : SFin n -> SFin (pred n) -> SFin n
+thin FZ y = FS' y
 thin (FS x) FZ = FZ
 thin (FS x) (FS y) = FS (thin x y)
 
 -- Properties
 
 export
-thinInjective : (x : Fin n) -> {y, z : Fin (pred n)} -> thin x y = thin x z -> y = z
-thinInjective FZ prf = injective prf
+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 (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 : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x)
+thinSkips : (x : SFin n) -> (y : SFin (pred n)) -> Not (thin x y = x)
+thinSkips FZ y prf = sucNonZero y prf
 thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
 
-%inline
-thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
-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 z) = Refl
-thinSucSuc (FS x) FZ = Refl
-thinSucSuc (FS x) (FS z) = Refl
+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 : Fin n) -> (0 _ : Not (x = y)) -> (z ** thin x z = y)
+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 ** Refl)
-thinInverse (FS x) FZ neq = (zero x ** thinSucZero x)
+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 (neq . cong FS) in
-  (suc z ** trans (thinSucSuc x z) (cong FS prf))
+  let (z ** prf) = thinInverse x y (\prf => neq $ cong FS prf) in
+  (FS' z ** trans (thinSuc x z) (cong FS $ prf))
 
 -- Thickening ------------------------------------------------------------------
 
 export
-thick : Fin n -> Fin n -> Maybe (Fin (pred n))
+thick : SFin n -> SFin n -> Maybe (SFin (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) FZ = Just FZ
+thick (FS x) (FS y) = FS' <$> thick x y
 
 export
-thickRefl : (x : Fin n) -> IsNothing (thick x x)
+thickRefl : (x : SFin n) -> IsNothing (thick x x)
 thickRefl FZ = ItIsNothing
-thickRefl (FS x) = mapNothing suc (thickRefl x)
+thickRefl (FS x) = mapNothing FS' (thickRefl x)
 
 export
-thickNeq : (x, y : Fin n) -> (0 _ : Not (x = y)) -> IsJust (thick x y)
+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 suc (thickNeq x y (neq . cong FS))
+thickNeq (FS x) (FS y) neq = mapIsJust FS' (thickNeq x y (\prf => neq $ cong FS prf))
 
 export
-thickNothing : (x, y : Fin n) -> (0 _ : IsNothing (thick x y)) -> x = y
+thickNothing : (x, y : SFin 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
+  cong FS (thickNothing x y (mapNothingInverse FS' (thick x y) prf))
 
-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
+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 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))
+  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
-thickThin : (x : Fin n) -> (y : Fin (pred n)) -> thick x (thin x y) = Just y
+thickThin : (x : SFin n) -> (y : SFin (pred n)) -> thick x (thin x y) = Just y
 thickThin x y =
-  let neq = thinSkips x y in
-  let isJust = thickNeq x (thin x y) (\prf => neq $ sym prf) in
-  let zPrf = extractIsJust isJust in
-  let z = zPrf.fst in
-  let 0 prf1 = zPrf.snd in
-  let 0 prf2 = thickJust x (thin x y) prf1 in
-  trans prf1 (cong Just $ thinInjective x prf2)
+  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)
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