diff options
Diffstat (limited to 'src/Data/Fin/Occurs.idr')
| -rw-r--r-- | src/Data/Fin/Occurs.idr | 62 |
1 files changed, 32 insertions, 30 deletions
diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr index 899e2a1..58c8faa 100644 --- a/src/Data/Fin/Occurs.idr +++ b/src/Data/Fin/Occurs.idr @@ -45,23 +45,24 @@ export thinSkips : (x : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x) thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf) +%inline thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ -thinSucZero FZ = Refl -thinSucZero (FS x) = Refl +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 x) = Refl +thinSucSuc FZ (FS z) = Refl thinSucSuc (FS x) FZ = Refl -thinSucSuc (FS x) (FS y) = Refl +thinSucSuc (FS x) (FS z) = Refl export -thinInverse : (x, y : Fin n) -> Not (x = y) -> (z ** thin x z = y) +thinInverse : (x, y : Fin 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 (FS x) (FS y) neq = - let (z ** prf) = thinInverse x y (\eq => neq $ cong FS eq) in + let (z ** prf) = thinInverse x y (neq . cong FS) in (suc z ** trans (thinSucSuc x z) (cong FS prf)) -- Thickening ------------------------------------------------------------------ @@ -71,31 +72,32 @@ thick : Fin n -> Fin n -> Maybe (Fin (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) (FS y) = suc <$> thick x y export -thickIsNothing : (x, y : Fin n) -> (x = y) <=> (thick x y = Nothing) -thickIsNothing FZ FZ = MkEquivalence (const Refl) (const Refl) -thickIsNothing FZ (FS y) = MkEquivalence absurd absurd -thickIsNothing (FS x) FZ = MkEquivalence absurd absurd -thickIsNothing (FS x) (FS y) = - let rec = thickIsNothing x y in - MkEquivalence - (cong (Just suc <*>) . rec.leftToRight . injective) - (cong FS . rec.rightToLeft . appNothingRight suc (thick x y)) +thickRefl : (x : Fin n) -> IsNothing (thick x x) +thickRefl FZ = ItIsNothing +thickRefl (FS x) = mapNothing suc (thickRefl x) export -thickIsJust : (x, y : Fin n) -> Not (x = y) <=> (z ** (thick x y = Just z, thin x z = y)) -thickIsJust FZ FZ = MkEquivalence (\f => absurd $ f Refl) (\p => absurd $ fst $ snd p) -thickIsJust FZ (FS y) = MkEquivalence (const (y ** (Refl, Refl))) (const absurd) -thickIsJust (FS x) FZ = - MkEquivalence - (const (zero x ** (Refl, thinSucZero x))) - (const absurd) -thickIsJust (FS x) (FS y) = - let rec = thickIsJust x y in - MkEquivalence - (\neq => - let (z ** (prf1, prf2)) = rec.leftToRight (neq . cong FS) in - (suc z ** (rewrite prf1 in Refl, trans (thinSucSuc x z) (cong FS prf2)))) - (\(z ** (prf1, prf2)), prf => thinSkips (FS x) z $ trans prf2 (sym prf)) +thickNeq : (x, y : Fin 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)) + +export +thickNothing : (x, y : Fin 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 + +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 +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)) |