Stream: Coq users

Topic: undo exists tactics

walker (Feb 10 2022 at 07:23):

Is there an easy way to reverse an exists foo tactic. something that works like generalize dependent but for exists

Christian Doczkal (Feb 10 2022 at 09:32):

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).

walker (Feb 10 2022 at 09:40):

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.

walker (Feb 10 2022 at 09:40):

any ideas how to do that ?

Guillaume Melquiond (Feb 10 2022 at 09:43):

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).

walker (Feb 10 2022 at 09:45):

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.

Guillaume Melquiond (Feb 10 2022 at 09:52):

If your hypothesis H was {x | P x} instead of (exists x, P x), you could do apply (proj2_sig H).

walker (Feb 10 2022 at 09:57):

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

Pierre Courtieu (Feb 10 2022 at 09:57):

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).

Guillaume Melquiond (Feb 10 2022 at 10:00):

{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.)

walker (Feb 10 2022 at 10:02):

@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.

Guillaume Melquiond (Feb 10 2022 at 10:05):

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.

Guillaume Melquiond (Feb 10 2022 at 10:06):

(No, scrap that, it is a filter only if P is constrained, but the monadic style can nevertheless be used.)

Last updated: Apr 16 2024 at 13:01 UTC