Stream: Coq users

Topic: How to instantiate existential variable in the context

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 *)
``

Li-yao (Oct 19 2022 at 23:02):

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

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

Daniel Hilst Selli (Oct 20 2022 at 20:29):

Hmm, thanks I think I misunderstood the exists

Last updated: Oct 13 2024 at 01:02 UTC