Using Agda "rewrite" to prove "composition of maps is map of compositions"

Question

I'm very new to Agda, and I'm trying to do a simple proof of "composition of maps is the map of compositions".

(An exercise taken from this course)

Relevant definition:

_=$=_ : {X Y : Set}{f f' : X -> Y}{x x' : X} ->
        f == f' -> x == x' -> f x == f' x'
refl f =$= refl x = refl (f x)

and

data Vec (X : Set) : Nat -> Set where
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_

I want to prove:

vMapCpFact : {X Y Z : Set}{f : Y -> Z}{g : X -> Y}{h : X -> Z} ->
             (heq : (x : X) -> f (g x) == h x) ->
             {n : Nat} (xs : Vec X n) ->
             vMap f (vMap g xs) == vMap h xs

I already figured out the proof using =$=

vMapCpFact heq [] = refl []
vMapCpFact heq (x ,- xs) = refl _,-_ =$= heq x =$= vMapCpFact heq xs

But when I tried to do the proof using rewrite, I stuck at this step:

vMapCpFact heq [] = refl []
vMapCpFact heq (x ,- xs) rewrite heq x | vMapCpFact heq xs = {!!}

Agda says the goal is still

(h x ,- vMap f (vMap g xs)) == (h x ,- vMap h xs)

I wonder why the rewrite of vMapCpFact heq xs failed?

Answer 1

Simply because vMapCpFact heq xs didn't fire at all. The type of this expression, as reported by Agda, is

vMap _f_73 (vMap _g_74 xs) == vMap (λ z → h z) xs

i.e. Agda can't infer f and g (those _f_73 and _g_74 are unresolved metavariables) and so it can't realize what exactly to rewrite.

You can fix this by explicitly specifying f:

vMapCpFact {f = f} heq (x ,- xs) rewrite heq x | vMapCpFact {f = f} heq xs = {!!}

Now the type of the goal is

(h x ,- vMap h xs) == (h x ,- vMap h xs)

as expected.

Or you can rewrite from right to left, since the rhs of the type of vMapCpFact heq xs is fully inferred:

vMap (λ z → h z) xs

For rewriting from right to left you only need to use sym. Then the whole thing type checks:

vMapCpFact heq (x ,- xs) rewrite heq x | sym (vMapCpFact heq xs) = refl _

because the _f_73 and _g_74 metavariables are forced to unify with the actual f and g variables by the refl.