The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Aaron,

This is unfortunate that destructing an hypothesis of the form In k m
unveils the underlying implementation of MapsTo, but maybe you should
prove your own inversion lemma for In k m, in terms of MapsTo:

Lemma In_inv : forall k m, In k m -> exists v, MapsTo k v m

and destruct instances of this lemma instead of directly destructing
the hypothesis. This would be tedious in manual proof but since you
are developing some Ltac tactic it is the easiest solution I can think
of.

HTH,

Stéphane

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



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06