The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I think there is no problem in hget_evar (from what I saw): it
reliably build a let abstraction of the nth evar.

The problem is that it cannot be used as a wrapper around vm_compute:
one needs to build the right proof term, in addition to the
"abstraction of evars", which cannot be done by piecing tactics
together...

Thomas


On Fri, Jan 25, 2013 at 12:45 AM, Chung-Kil Hur 
<gil.hur AT gmail.com>
 wrote:
> Right. It doesn't work.
> But in my case I got "Uncaught exception".
> I am using Coq 8.4 not 8.4pl1.
>
> Anyway, I don't know the reason.
>
> By the way, "hget_evar" is what I wrote and put it into Coq from 8.3.
> I am not 100% sure whether there is a bug with the code because I am not a
> real expert.
> The code itself is very short (10 lines or so).
> It would be nice if some coq expert looks at the code and check whether it
> is really correct or not because I find the tactic very useful.
>
> Best,
> Gil
>
>
>
> On Thu, Jan 24, 2013 at 7:44 PM, Thomas Braibant 
> <thomas.braibant AT gmail.com>
> wrote:
>>
>> I tried your tactics on my examples (the one in the github
>> repository), and I cannot do hide_evars; vm_compute. vm_compute
>> unfolds the definition that you just put in the hypotheses, using
>> set...  Could you try and see if I missed something.
>>
>> In any case, I feel like the repeat hide_evar tactic is sub optimal:
>> you iterate n times in the goal, with n being the number of
>> existential variables.
>>
>> Thomas.
>> By the way I did not knew this hget_evar tactic, which is
>> undocumented. It seems nice. For the audience, it folds the nth evar
>> that appears in the goal as a let.
>>
>>
>> On Thu, Jan 24, 2013 at 7:24 PM, Chung-Kil Hur 
>> <gil.hur AT gmail.com>
>>  wrote:
>> >
>> > Definition _Evar_Gil_ (A:Type) (x:A) := x.
>> >
>> > Tactic Notation "hide_evar" int_or_var(n) := let QQ := fresh "QQ" in
>> >   hget_evar n; intro;
>> >   lazymatch goal with [ H := ?X |- _] =>
>> >     set (QQ := X) in *; fold (@_Evar_Gil_ _ X) in QQ; clear H
>> >   end.
>> >
>> > Ltac hide_evars := repeat (hide_evar 1).
>> >
>> > Ltac show_evars :=
>> >   repeat (match goal with [ H := @_Evar_Gil_ _ _ |- _ ] =>
>> >     unfold _Evar_Gil_ in H; unfold H in *; clear H end).
>
>