idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Injectivity and similar properties were added for lists'a append.

Browse Source
This commit is contained in:
Denis Buzdalov 2020-06-30 14:13:19 +03:00
parent df60e07962
commit 77f1d69acb
1 changed files with 35 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
libs/contrib/Data/List/Equalities.idr
View File

@ -10,6 +10,12 @@ snocNonEmpty : {x : a} -> {xs : List a} -> xs ++ [x] = [] -> Void
snocNonEmpty {xs = []} prf = uninhabited prf
snocNonEmpty {xs = y :: ys} prf = uninhabited prf
||| Proof that snoc'ed list is not empty in terms of `NonEmpty`.
export %hint
SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (xs `snoc` x)
SnocNonEmpty [] _ = IsNonEmpty
SnocNonEmpty (_::_) _ = IsNonEmpty
||| (::) is injective
export
consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
@ -75,3 +81,32 @@ export
lengthSnoc : (x : _) -> (xs : List a) -> length (snoc xs x) = S (length xs)
lengthSnoc x [] = Refl
lengthSnoc x (_ :: xs) = cong S (lengthSnoc x xs)
||| Appending the same list at left is injective.
export
appendSameLeftInjective : (xs, ys, zs : List a) -> zs ++ xs = zs ++ ys -> xs = ys
appendSameLeftInjective xs ys [] = id
appendSameLeftInjective xs ys (_::zs) = appendSameLeftInjective xs ys zs . snd . consInjective
||| Appending the same list at right is injective.
export
appendSameRightInjective : (xs, ys, zs : List a) -> xs ++ zs = ys ++ zs -> xs = ys
appendSameRightInjective xs ys [] = rewrite appendNilRightNeutral xs in
rewrite appendNilRightNeutral ys in
id
appendSameRightInjective xs ys (z::zs) = rewrite appendAssociative xs [z] zs in
rewrite appendAssociative ys [z] zs in
fst . snocInjective . appendSameRightInjective (xs ++ [z]) (ys ++ [z]) zs
||| List cannot be equal to itself prepended with some non-empty list.
export
appendNonEmptyLeftNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = xs ++ zs)
appendNonEmptyLeftNotEq [] (_::_) Refl impossible
appendNonEmptyLeftNotEq (z::zs) (_::xs) prf = appendNonEmptyLeftNotEq zs (xs ++ [z]) @{SnocNonEmpty xs z}
rewrite sym $ appendAssociative xs [z] zs in snd $ consInjective prf
||| List cannot be equal to itself appended with some non-empty list.
export
appendNonEmptyRightNotEq : (zs, xs : List a) -> NonEmpty xs => Not (zs = zs ++ xs)
appendNonEmptyRightNotEq [] (_::_) Refl impossible
appendNonEmptyRightNotEq (_::zs) (x::xs) prf = appendNonEmptyRightNotEq zs (x::xs) $ snd $ consInjective prf