The Coq mailing list

[Ilia Zaichuk <zoickx AT ztld.org>]

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.