[Agda] more unification using more complex with abstractions

[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


On 07/31/2018 02:00 PM, rick wrote:
> 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