Is there an easy way to reverse an `exists foo`

tactic. something that works like generalize dependent but for `exists`

Unless I misunderstand what you mean, I don't think there can be such a thing. If you choose the wrong witness, you can easily turn a provable goal into an unprovable one. Say your goal is `exists n, n = 0`

and you execute `exists 1`

then your goal becomes `1 = 0`

, and there clearly cannot be any sound way of going back to the provable goal `exists n, n = 0`

. If you don't want to commit to a (possibly) wrong instance, you can use `eexists`

to introduce an evar that can then be instantiated at a later point (using variables that were available at the point where `eexists`

was invoked).

```
Theorem test_foo: forall (X: Type) (P Q: X -> Prop) , (exists x, P x) -> (exists x, P x \/ Q x).
Proof.
intros X P Q H.
eexists.
left.
Fail apply H.
```

I know I can distruct H but I hoped I can apply it as it is.

any ideas how to do that ?

What is wrong with destructing `H`

? This is the sensible way forward. If you fear you will still need `H`

afterward, just do `destruct (H)`

.

In this particular example there was no problem, but in other example the environment might grow to be huge and I would like to avoid destructing stuff and try to use it as it is if possible.

If your hypothesis `H`

was `{x | P x}`

instead of `(exists x, P x)`

, you could do `apply (proj2_sig H)`

.

I am not fully sure I understand what does `{x | P x}`

mean

I don't really understand why you consider destructing a problem, and you probably can't avoid destruct here (except switching to sig as @Guillaume Melquiond said), but this theorem allows precisely to avoid destructing existentials in some further proofs. You might want to prove a stronger one like this.

```
Theorem test_foo: forall (X: Type) (P Q: X -> Prop) , (exists x, P x) -> (forall x, P x -> Q X)-> (exists x, Q x).
```

`{x | P x}`

is the same as `(exists x, P x)`

, except that it lives in `Set`

rather than in the non-informative `Prop`

. In other words, you can recover `x`

from the earlier, but not from the latter. (And you need to recover `x`

in order to fill `P ?x`

without destructing `H`

.)

@Pierre Courtieu that wasn't something I was trying to prove, I just had a similar pattern that emerged somewhere in some much longer proof.

@Guillaume Melquiond thanks for the clarifications.

That said, @Pierre Courtieu 's solution is a good one. `fun P => exists x, P x`

is a filter, so you can work in a monadic style (e.g., `test_foo`

) and never ever destruct existentials.

(No, scrap that, it is a filter only if `P`

is constrained, but the monadic style can nevertheless be used.)

Last updated: Jun 16 2024 at 03:41 UTC