From 60d5896ab7939ae42cf7744f93e8eaefa0675854 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 11 Jul 2023 13:54:54 +0100 Subject: Use new notion of Fin to reduce casts. --- src/Data/Fin/Occurs.idr | 111 ++++++++++++++++++++---------------------------- 1 file changed, 45 insertions(+), 66 deletions(-) (limited to 'src/Data/Fin/Occurs.idr') 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) -- cgit v1.2.3