idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #392 from buzden/append-properties

Browse Source 
Injectivity and similar properties were added for lists'a append
This commit is contained in:
Edwin Brady 2020-07-05 14:08:07 +01:00 committed by GitHub
commit a9478875b3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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