Proof that a ++ b = a ++ c -> b = c and a ++ c = b ++ c -> a = b

AppendInjective.idr

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