Stream: Coq users

Topic: undo exists tactics


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip walker (Feb 10 2022 at 09:40):

any ideas how to do that ?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip walker (Feb 10 2022 at 09:57):

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

view this post on Zulip 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).

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC