The Coq mailing list

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

The problem is that eexists cannot use variables created later than eexists itself. This is not avoidable (at least in the current state of coq). So you have to create variables before applying eexists. Either by using destruct or some previously proven inversion lemmas (which is maybe easier to put in an automatic tactic).

P.

2016-11-14 11:00 GMT+01:00 Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>:

Hello Pierre,

thanks for the suggestion. Putting the "@ex" into the
ltac rule does seem to be a bit limiting, though. I'd need
different versions of the rule, one with and one without
the @ex. And maybe the goal looks different.

For instance, consider

Inductive foo : Set :=
  | bar : forall n, n = 7 -> foo.

Inductive baz : nat -> Prop :=
  | bam : forall n, n = 7 -> baz n.

Goal foo -> exists {n:nat}, baz n.

Usually I'd hope to be able to use

Hint Constructors baz.

to automate that proof, but again the goal that triggers
the proof becomes available only after "eexists".

Klaus

Am 14/11/16 um 10:46 schrieb Pierre Courtieu:

Hi,

I am not sure when exactly you want to trigger the destruct but you can match goal on ex like below.

Ltac destruct_foo := 

match goal with

| H:foo |- @ex _ (fun n => @eq nat n 7)  => destruct H

end.

Hint Extern 1 => destruct_foo:foo. (* you can add same pattern than above @ex... *)

Goal foo -> exists {n:nat}, n=7.

intros.

eauto with foo.

2016-11-14 10:22 GMT+01:00 Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>:

When proving a goal with an existential, it matters when
eexists is used. For instance, with

Inductive foo : Set :=
  | bar : forall n, n = 7 -> foo.

the following proof works

Goal foo -> exists {n:nat}, n=7.
intros. destruct H. eexists. exact(e). Defined.

but this one yields a "cannot instantiate ... not in scope" error

Goal foo -> exists {n:nat}, n=7.
intros.  eexists. destruct H. exact(e).

It's easy to correct this error in a manual proof, but it is not clear to
me how to deal with such goals in (goal-direct) proof automation.

In principle, I could automate proofs like that using something like

Hint Extern 1 (?n = 7) =>
      match goal with
        | [ H : foo |- ?n = 7 ] => destruct H
      end.

but the hint won't fire until I used "eexists" first - but I need to use
eexists _after_ the "destruct".

Is there a way to solve this conundrum?

Klaus