Unfold anonymous function in Coq proof

Question

I am stuck trying to prove something in Coq that involves the use of a type class.

The specific type class is almost identical to this Functor type class: https://gist.github.com/aztek/2911378

My instance looks like this:

Instance ListFunctor : Functor list := { fmap := map }.
  (* Proof stuff here *)
Defined.

map is the map over lists from the standard library.

The "proof" I am doing is basically just a unit test:

Example list_map_test : fmap (fun x => x + 1) (1::2::3::nil) = (2::3::4::nil).

My goal looks like this and I am stuck:

(let (fmap0, _, _) := ListFunctor in fmap0) nat nat
 (fun x : nat => x + 1) (1 :: 2 :: 3 :: nil) = 2 :: 3 :: 4 :: nil

Coq destructured the instance to get fmap0 and then applied the resulting anonymous function with the args nat nat (fun x : nat => x + 1) (1 :: 2 :: 3 :: nil).

As the next step in my proof, I would like to unfold fmap0 or the anonymous function.

How can I do this? I cannot do unfold fmap0.

My expectation was that fmap0 is the standard lib map because that is what I gave to the instance.

I was able to destruct the instance myself, but this shows the abstract version of fmap0 and not the implementation that was given when instantiating the type class.

What am I doing wrong?

Answer 1

If f is an anonymous function (that is, something of the form fun x => expr), then simpl should be enough. If it is an identifier and you cannot unfold it, then either (1) it is a local variable bound in your context, or (2) it is a global definition defined via Qed. In the latter case, just remove the Qed from your definition, replacing it by Defined. In the former case, I would guess that you should have tried to unfold or simplify expr1 so that Coq can have access to the actual definition of f (this, in turn, might require removing Qeds from other global definitions).

Answer 2

I don't know exactly why, but if you simplify directly the goal

1 subgoal
______________________________________(1/1)
fmap (λ x : nat, (x + 1)%nat) (1 :: 2 :: 3 :: [ ]) = 2 :: 3 :: 4 :: [ ]

using simpl or cbv for example, you get your instance of map (in fact you get the result of map S applied to 1 :: 2 :: 3 :: [] hence the goal becomes trivial). I don't know why unfolding fmap or destructing the ListFunctor yields a generic fmap0.