The Coq mailing list

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

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