Skip to content

Instantly share code, notes, and snippets.

@YBogomolov
Last active May 2, 2020 10:17
Show Gist options
  • Save YBogomolov/430e55c2ce85be963e85b66954a1d483 to your computer and use it in GitHub Desktop.
Save YBogomolov/430e55c2ce85be963e85b66954a1d483 to your computer and use it in GitHub Desktop.
Proof that a ++ b = a ++ c -> b = c and a ++ c = b ++ c -> a = b
module AppendInjective
import Data.List.Views
%access export
%default total
appendInjectiveRight : (a, b, c : List x) -> a ++ b = a ++ c -> b = c
appendInjectiveRight [] _ _ prf = prf
appendInjectiveRight (_ :: xs) b c prf = appendInjectiveRight xs b c (cong { f = drop 1 } prf)
appendEmptyInjective : {a, b : List x} -> a ++ [] = b ++ [] -> a = b
appendEmptyInjective {a} {b} prf =
rewrite sym $ appendNilRightNeutral a in
rewrite sym $ appendNilRightNeutral b in
prf
dropOneRight : (xs : List a) -> List a
dropOneRight [] = []
dropOneRight [x] = []
dropOneRight (x :: y :: xs) = x :: dropOneRight (y :: xs)
dropOneRightProof : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
dropOneRightProof [] z = Refl
dropOneRightProof [x] z = Refl
dropOneRightProof (x :: y :: xs) z = cong $ dropOneRightProof (y::xs) z
consCong : {A : Type} -> {x : A} -> {xs : List A} -> {ys : List A} ->
xs ++ [x] = ys ++ [x] -> xs = ys
consCong {xs} {ys} {x} prf_cons =
rewrite dropOneRightProof ys x in
rewrite dropOneRightProof xs x in
cong prf_cons
appendInjectiveLeft : (a, b, c : List x) -> a ++ c = b ++ c -> a = b
appendInjectiveLeft a b c prf with (snocList c)
appendInjectiveLeft a b [] prf | Empty = appendEmptyInjective prf
appendInjectiveLeft a b (cs ++ [c]) prf | (Snoc rec) = appendInjectiveLeft a b cs (consCong {x=c} (
rewrite sym $ appendAssociative a cs [c] in
rewrite sym $ appendAssociative b cs [c] in
prf
)) | rec
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment