Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] apply without instantiating

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] apply without instantiating


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] apply without instantiating
  • Date: Thu, 24 Jan 2019 12:54:07 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f51.google.com
  • Ironport-phdr: 9a23:EKJGgROOkeQI9/UzOlAl6mtUPXoX/o7sNwtQ0KIMzox0Lfn/rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUclRWS5ODIOyYYUMEuQPI/pXopLnqFcStxazHxWgCP/txzJOm3T43bc60+MkEQzewgIgH8gJsHPMo9r2NacSVOW1w7fSzTXGdfxW3zH945XPfxA9ofGDQ7VwfdDQyEkuEgPFi1SQpJfqPzOQzOsNsmyb4/B8WuKojm4qsgd8qSWsyMc0koTFmJ4Zx1Te+Sh6wIs5P8O0RFBlbdK+EJZcqieXPJZsTMw4WWFnoiM6x6UGuZGleCgKz4wqxxvFZPyGd4iE+w/jW/yMLTthinJoeK+ziwy98Uinze38Wc2030hQoiVZldnMs2gB1x3V6seZVvtw5lmt1SqL2gzJ6exJIVo4mbTFJ5I/2LI9locfvVzGHiDsmUX2iKGWdl8j+uit8+nnfrXmqYGbN4NuiwD+M6Eumsm+AekjPQgOWnKU+eW41LH54UL5R7BKguUskqbFqJDaOdgbpqmhDgBJ1YYj8g+zACui0NQFhnYKN0lFeRKCj4jxIV7COvH4DfGlg1Stijhn3f7GPqeySqnKe1PEif/Keat3oxpXzxN2xtRC7bpVDKsAKbT9QBmimsbfC0oFM42z9NTmDdBwzIYXX2THVrOZPaSUo16N4+MHLOyFZYtTszH4fat2r8XyhGM0zAdONZKi2oEaPTXhRqw/chepJEH0i9JEKl8k+w83TejkklqHCGcBaHO7XqZ67TY+Wtv/UdXzA7u1ibnE5x+VW4VMbzkfWF+JGHbsMY6DXqVUMX/AEopaijUBEIOZZcoh2BWp7lKozrNmKq/J83Rdu8+6ktdy4OLXmFc58jkmV8k=

Indeed, none of the answers that were given to you so far work.
It would be quite useful to have a way to say "prevent this evar from being instantiated until I say so" in a proof script.
As a workaround, you could use the following:

Ltac has_no_evars := tryif match goal with |- ?G => has_evar G end then fail "Has evars" else idtac.

"has_no_evars; reflexivity" would then work.

Unfortunately this would be an over approximation given that for a goal like "?x = ?x", it would fail even if "reflexivity" wouldn't instantiate "?x".

Le jeu. 24 janv. 2019 à 05:42, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :
Hi Jason,

trivial seems to instantiate the evar in this example

Coq < Goal forall T (y : T), exists x, x=y.
1 subgoal

   ============================
   forall (T : Type) (y : T), exists x : T, x = y

Unnamed_thm < intros.
1 subgoal

   T : Type
   y : T
   ============================
   exists x : T, x = y

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

   T : Type
   y : T
   ============================
   ?x = y

Unnamed_thm < trivial.
No more subgoals.

Unnamed_thm < Qed.
Unnamed_thm is defined

Coq < Check Unnamed_thm.
Unnamed_thm
      : forall (T : Type) (y : T), exists x : T, x = y

Jeremy

On 22/1/19 5:32 pm, Jason -Zhong Sheng- Hu wrote:
> 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



Archive powered by MHonArc 2.6.18.

Top of Page