[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]

Sorry, one correction on mu below.

Instead of what I listed, please use the following:

_>>_ : {X Y Z : Set} -> (X -> Y) -> (Y -> Z) -> (X -> Z)
(f >> g) x = g (f x)

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

I got lazy and thought I could remove the composition operator, but it's
just as east to list it.

--

rick

Post by 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 _++_ []
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
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.
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.

[Nils Anders Danielsson]

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

{-# BUILTIN EQUALITY _==_ #-}

mu : ∀ {X} (xss : List (List X)) →
listMap (unit >> mult) xss == xss
mu [] = refl []
mu (xs₁ ,- xs₂) rewrite lem xs₁ | mu xs₂ = refl _