The Coq mailing list

[Joshua Gancher <jrg358 AT cornell.edu>]

Hi,

I am not sure if this is exactly what you want, but you might be interested in the Procrastination library: https://github.com/fakusb/coq-procrastination

Using this library, I can indeed do (something equivalent to) eexists where you want it:

Require Import Procrastination.

Inductive sum : nat -> nat -> nat -> Prop :=
| Sum0 : forall a, sum 0 a a
| SumS : forall a b c, sum a (S b) c -> sum (S a) b c.

Theorem sum_exists : forall a b, exists c, sum a b c.
  induction a; intro.
  - exists b; constructor.
  - begin defer assuming c.
    + exists c.
      constructor.
      defer.  
    + end defer.
      apply (IHa (S b)).
Qed.

Josh

On Fri, Aug 2, 2019 at 10:40 AM Ilia Zaichuk <zoickx AT ztld.org> wrote:

Hello everyone,

Consider the following example:

Inductive sum : nat -> nat -> nat -> Prop :=

| SumO : forall a, sum 0 a a

| SumS : forall a b c, sum a (S b) c -> sum (S a) b c.

Theorem sum_exists :

  forall a b, exists c, sum a b c.

Proof.

  induction a; intro.

  - exists b. constructor.

  - eexists.

    constructor.

    specialize (IHa (S b)).

    destruct IHa as [c IHa].

    Fail apply IHa.

Abort.

The problem here (as suggested by [apply]) is that the shelved [?c] does not

have [c] in its scope. Fair enough. This problem has been coming up in a few of

my proofs lately, and I have learned to deal with it by moving the [destruct] -

the instantiation of [c] - above the [eexists].

However, this comes with a problem - it breaks the "flow of thought" in a proof.

You either have to know in advance what variables you need instantiated, or go

down to the point where you need them and move the instantiation above [eexists].

That would be fine for this small example, but in more complex proofs, it quickly

becomes unwieldy.

Without [eexists], I cannot apply the [SumS] constructor.

It is possible to add a lemma:

Lemma SumS_existential (a b : nat) :

  (exists c, sum a (S b) c) -> exists c, sum (S a) b c.

Proof.

  intros.

  destruct H as [c H].

  exists c. constructor.

  assumption.

Qed.

, with which the proof goes smoothly. But this, once again, is unsustainable

for more complex problems. I have tried writing a generic lemma for

"existential implication", but was unsuccessful.

Can such a lemma exist? (Or is it a tactic I am looking for?)

I have also tried manipulating the contexts of the main goal and the existential

variables separately (via [Unshelve]), and failed at proving the lemma this way at all.

Is it at all possible to cleanly do that in this case?

Overall, how can I prove this lemma without getting the reasoning tangled?

Thanks and regards,

Ilia.