diff options
Diffstat (limited to 'src/Data/Fin')
| -rw-r--r-- | src/Data/Fin/Occurs.idr | 111 | ||||
| -rw-r--r-- | src/Data/Fin/Strong.idr | 76 |
2 files changed, 121 insertions, 66 deletions
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 |