The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Aaron Bohannon wrote:
> I am using FMaps in my development and want to write a tactic that
> matches hypotheses of the form (MyMap.MapsTo k v m).  The problem is
> that, when I destruct a proposition of the form (MyMap.In k m), I end
> up with a hypothesis of the form (MyMap.Raw.PX.MapsTo _ _ _).  A
> tactic that matches on (MyMap.MapsTo _ _ _) will not match hypotheses
> of the form (MyMap.Raw.PX.MapsTo _ _ _).  Of course, I can write a
> tactic that refers directly to MyMap.Raw.PX.MapsTo, but I feel like
> this is violating the intended abstraction of the FMap interface.
> Unforunately, the tactic "fold MyMap.MapsTo" does not help because
> MyMap.MapsTo seems to be defined as an eta-expansion of
> MyMap.Raw.PX.MapsTo.  Any other ideas?  Or do I have to write a tactic
> that breaks the abstraction?
>    

There's a potentially inefficient version that does:
match goal with
    | [ H : ?f ?a ?b ?c |- _ ] =>
    equate (f a b c) (MyMap.MapsTo a b c); (* use H as planned *)
end.

...for some implementation of an equality check [equate], for instance 
by [assert]ing that the two terms are equal, making sure [reflexivity] 
proves it, and then clearing the hypothesis that [assert] added.

(I haven't actually run the above code, so please excuse typos. :])

You may also find that you can ignore this altogether.  For instance, if 
you want to do forward reasoning with a theorem [thm] that takes a fact 
matching the hypothesis as its first assumption, you may be able to get 
away with running [apply thm in H] for every hypothesis [H], delegating 
the matching work to unification.