Stream: Coq users

Topic: How to instantiate existential variable in the context


view this post on Zulip Daniel Hilst Selli (Oct 19 2022 at 20:33):

If I have a variable (x : a) in the context and a hypothesis H : exists (y : a), P how can I instantiate y with x? With forall I would do specialize (H x) but with exists this do not work, here is a minimal example

Section Foo.
  Parameter a : Set.
  Parameter P : Prop.
  Context (x : a).
  Context (H : exists (y : a), P).
  Goal P.
    specialize (H x).  (* want to do something like this *)
``

view this post on Zulip Li-yao (Oct 19 2022 at 23:02):

When exists is in an assumption, you don't get to choose the witness.

view this post on Zulip Paolo Giarrusso (Oct 20 2022 at 01:36):

Indeed; what you can do is destruct H to get the witness out and use it in a proof

view this post on Zulip Daniel Hilst Selli (Oct 20 2022 at 20:29):

Hmm, thanks I think I misunderstood the exists


Last updated: Feb 06 2023 at 13:03 UTC