The Coq mailing list

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

(Oops...I hit send too early.)

I was just going to add that I'm not sure if my "optimization" is
measurably faster, though.

 - Aaron

On Wed, Feb 9, 2011 at 3:20 PM, Aaron Bohannon 
<bohannon AT cis.upenn.edu>
 wrote:
> 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.
>>
>