Questions tagged [witness]

In mathematical logic, a witness is a specific value t to be substituted for variable x of an existential statement of the form ∃x φ(x) such that φ(t) is true. (from Wikipedia)

Filter by
Sorted by
Tagged with
14 votes
4 answers

How to extract the witness from exists in Coq in function notation/without destructing?

Assuming I have some definition with a forall and an exists like so: Definition fooable A B P := forall a : A, exists b : B, P a b. Then on an intuitive level, I ...
Sacchan's user avatar
  • 243