The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Pierre,

Well, in this example simple apply (which I assume is what you meant) 
instantiates the variable.  Is there something else you do to stop that?

Cheers,

Jeremy

Coq < Goal exists x, (x = a).
1 subgoal

   ============================
   exists x : nat, x = a

Unnamed_thm < eexists.
1 focused subgoal
(shelved: 1)

   ============================
   ?x = a

Unnamed_thm < simple_apply eq_refl.
Toplevel input, characters 0-12:
 > simple_apply eq_refl.
 > ^^^^^^^^^^^^
Error: The reference simple_apply was not found in the current environment.

Unnamed_thm < simple apply eq_refl.
No more subgoals.



On 01/22/2019 06:16 PM, Pierre Courtieu wrote:
> Did you try simple_apply? One of the differences with apply seems to be 
> more or less what you want. It is not the only difference though.
> Best regards
> Pierre
> 
> Pierre
> ------------------------------------------------------------------------
> *De :* 
> coq-club-request AT inria.fr
>  de la part de Jason -Zhong Sheng- Hu 
> <fdhzs2010 AT hotmail.com>
> *Envoyé :* mardi, janvier 22, 2019 7:33 AM
> *À :* 
> coq-club AT inria.fr
> *Objet :* Re: [Coq-Club] apply without instantiating
> I believe lots of tactics, e.g. trivial, will eliminate reflexive goals 
> but not instantiating evars.
> 
> Thanks,
> Jason Hu
> 
> On Jan 22, 2019 01:21, Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>
>  wrote:
> 
> Hi,
> 
> Is there a way of applying a theorem without instantiating existential
> variables in a goal?
> 
> For example, if you want to eliminate equality goals but not create
> phony ones, as with the goals
> 
> a ++ b ++ c = ?d ++ ?e
> and
> f ++ g = f ++ g
> 
> I want some variant of
> 
> all : try (apply eq_refl).
> 
> which would catch the second goal but not the first
> 
> thanks
> 
> Jeremy