[Agda] more unification using more complex with abstractions

[rick]

Given

data List (X : Set) : Set where
  [] : List X
  _,-_ : (x : X)(xs : List X) -> List X

data _==_ {X : Set} : X -> X -> Set where
  refl : (x : X) -> x == x

_++_ : {A : Set} -> List A -> List A -> List A
[] ++ ys = ys
(x ,- xs) ++ ys = x ,- (xs ++ ys)

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr c n [] = n
foldr c n (x ,- xs) = c x (foldr c n xs)

unit : ∀{A} -> A -> List A
unit x = x ,- []

mult : {X : Set} -> List (List X) -> List X
mult = foldr _++_ []

Agda unifies the following:

um : ∀ {X} -> (xs : List X) -> mult (unit xs)  == xs
um [] = refl []
um (x ,- xs) with mult (unit xs) | um xs
um (x ,- []) | [] | s = refl (x ,- [])
um (x ,- (x₁ ,- xs)) | [] | ()
um (x ,- .(x₁ ,- [])) | x₁ ,- []
   | refl .(x₁ ,- []) = refl (x ,- (x₁ ,- []))
um (x ,- .(x₁ ,- (x₂ ,- r))) | x₁ ,- (x₂ ,- r)
   | refl .(x₁ ,- (x₂ ,- r))
   = refl (x ,- (x₁ ,- (x₂ ,- r)))

which proves propositional equality if you add a layer to the outside of 
the list then flatten it.

The initial goal before pattern matching on with abstractions was (x ,- 
r) == (x ,- xs).

However, given


listMap : {A B : Set} -> (A -> B) -> List A -> List B
listMap f xs = foldr (\ x r -> f x ,- r) [] xs

Agda does not unify the following :

mu : ∀ {X} -> (xss : List (List X))
   -> listMap (mult (unit xss))  == xss
mu [] = refl []
mu (xs ,- xs₁) with listMap (mult (unit xs₁)) | mu xs₁
... | r | s = {! ((xs ++ []) ,- r) == (xs ,- xs₁) !}

which adds a layer to each list inside the list of lists, then flattens it.

I should qualify my statement and say does not unify within a few 
pattern matching attempts before I stop to assess whether I can simplify.

I can prove the following lemma :

lem : ∀{X} -> (xs : List X)
   -> (xs ++ []) == xs
lem [] = refl []
lem (x ,- xs) with (xs ++ []) | lem xs
lem (x ,- []) | [] | s = refl (x ,- [])
lem (x ,- (x₁ ,- xs)) | [] | ()
lem (x ,- []) | x₁ ,- [] | ()
lem (x ,- []) | x₁ ,- (x₂ ,- r) | ()
lem (x ,- (x₁ ,- xs)) | .x₁ ,- .xs | refl .(x₁ ,- xs) = refl (x ,- (x₁ 
,- xs))

which seems to allow for proving the concatenation on the first 
component of the pair on the left hand side.

Can I use the lemma and if so how can I use it to cause Agda to unify mu?

Thanks in advance for your help! And for all the great work on Agda.

-- 
rick