The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

This solution does not quite work.  This does indeed apply vm_compute to the 
?X term.  However, this code will substitute the result or the existential 
variable.  The “reflexivity” tactic will then apply “simpl" to the original 
“3+4” term.  The “3+4” term needs to be evaluated exclusively by vm_compute 
and nothing else.

                       - Ken

> On Apr 22, 2017, at 9:13 AM, Laurent Thery 
> <Laurent.Thery AT inria.fr>
>  wrote:
> 
> 
> Oops, if you really want to only use vm_compute it should be
> 
> Theorem refl: exists x, x=3+4.
> Proof.
> match goal with |- exists _, _ = ?X =>
> let y := eval vm_compute in X in
> exists y; vm_cast_no_check (refl_equal y)
> end.
> Qed.
> 
> 
> On 04/22/2017 03:07 PM, Laurent Thery wrote:
>> On 04/22/2017 02:55 PM, Kenneth Roe wrote:
>>> Theorem refl: exists x, x=3+4.
>>> Proof.
>>>    apply ex_intro.
>>>    (* vm_compute. *)
>>>    compute.
>>>    reflexivity.
>>> Qed.
>> One way to go is to match the goal
>> Theorem refl: exists x, x=3+4.
>> Proof.
>> match goal with |- exists _, _ = ?X =>
>>  let y := eval vm_compute in X in
>>  exists y; reflexivity
>> end.
>> Qed.