Simple equality proofs on lists in idris (prooving xs ++ [x] = ys ++ [y] -> x = y -> xs = ys)

Question

I am learning idris and am very interested in proving properties about lists.

If you have a look at the standard library, theres a proof that "Two lists are equal, if their heads are equal and their tails are equal."

consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> x :: xs = y :: ys
consCong2 Refl Refl = Refl

We can also prove the other direction

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x::xs = y::ys -> x = y -> xs = ys
consCong2' Refl Refl = Refl

Or even more explicitly, we can drop the heads on both side of the equations to get to the proof.

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x::xs = y::ys -> x = y -> xs = ys
consCong2' prf_cons Refl = (cong {f = drop 1} prf_cons)

It would be interesting to see if these properties can be proven also for the last item in the rest and everything before that. Proving "Two lists are equal, if the first part and the very last item are equal" turned out to be very easy

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> xs ++ [x] = ys ++ [y]
consCong2' Refl Refl = Refl

But the other direction fails the typecheck:

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' Refl Refl = Refl

Because

Type mismatch between
                         ys ++ [x]
                 and
                         xs ++ [x]

Obviously, because if xs ++ [x] = ys ++ [y] comes first in the deduction, idris can't possible unify both sides.

So all we need to do is tell idris to apply init on both sides of the equation, like we did before with drop 1. That fails because init requires a proof that the list is non-empty, which somehow cannot be implicitly inferred here. So for that i wrote a helper function, that explicitly defines (a ++ [x]) = a.

dropOneRight :  (xs : List a) -> List a
dropOneRight xs with (snocList xs)
  dropOneRight [] | Empty = []
  dropOneRight (a ++ [x]) | Snoc rec = a

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' prf_cons Refl = cong {f = dropOneRight} prf_cons

But this yields

Type mismatch between
                 dropOneRight (ys ++ [x])
         and
                 ys

I spend some time on other approaches, case-splitting using snocList but can not get notable progress. I don't understand how i can show idris that dropOneRight (ys ++ [x]) = ys. How can i prove xs ++ [x] = ys ++ [y] -> x = y -> xs = ys?

Answer 1

I guess the snocList approach will be tricky; at least with the simple proof strategy to follow the definition. To prove ys = dropOneRight (ys ++ [x]) unifying snocList (ys ++ [x]) with the arguments will cause trouble, roughly:

prf' : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
prf' ys x with (snocList (ys ++ [x]))
    ...
    prf' ?? x | Snoc rec = ?hole

If you allow dropOneRight to be simpler, it's rather straight-forward:

dropOneRight : (xs : List a) -> List a
dropOneRight [] = []
dropOneRight [x] = []
dropOneRight (x :: y :: xs) = x :: dropOneRight (y :: xs)

dropPrf : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
dropPrf [] z = Refl
dropPrf [x] z = Refl
dropPrf (x :: y :: xs) z = cong $ dropPrf (y::xs) z

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
             xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' {xs} {ys} {x} prf_cons Refl = 
  rewrite dropPrf ys x in rewrite dropPrf xs x in
  cong prf_cons