The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

You are right, simple apply do performs evar instantiation. It only
stops unification modulo conversion in presence of evars.
P.

Le lun. 28 janv. 2019 à 11:15, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> 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