The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Thanks for the quick suggestions.  Perhaps the purely brute force
method can be slightly improved like this:

repeat match goal with
| k: _ |- _ =>
progress change MyMap.key in k
end;
repeat match goal with
| k: MyMap.key, v: ?A, m: MyMap.t ?A, H: _ =>
    progress change (MyMay.MapsTo k v m) in H
end.

On Wed, Feb 9, 2011 at 3:11 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> 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.
>