The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/25/2014 02:17 PM, Larry D. Lee jr. wrote:
> I've been working on a problem in which, given some predicate, P : A 
> -> Prop, I can prove that there exists some value, x : A, that 
> satisfies P (I.E. P x).
>
> This development occurred within the context of a module and I wanted 
> to say something like: "There exists a value x : A, such that P x. ... 
> Let K represent a value that satisfies P (we know that K exists 
> because...). ...". The second part of this statement is an instance of 
> existential instantiation.
>
> In Gallina, it is possible to represent existential instantiation, it 
> corresponds to ex's inductive property (ex_ind : forall (A : Type) (P 
> : A -> Prop) (P0 : Prop), (forall x : A, P x -> P0) -> ex P -> P0). 
> Specifically, the existentially quantified variable x is instantiated 
> in P0's context ("forall x : A, P x -> P0"). My problem was that I 
> wanted to instantiate an existentially quantified variable at the 
> global level and use the variable in subsequent calculations.

I am not sure I understand your requirements here.  Do you want to 
assert both K as a witness to A and "There exists a value x:A such that 
P x" where K is one such value as global hypotheses?  That can be done 
in Gallina using a Variable and a Hypothesis:

  Variable K : A.
  Hypothesis PK : P K.

> Ex's definition seemed to prohibit me from doing this. So I changed 
> the return type in ex's definition from Prop to Type producing:
>
>   Inductive ex2 (A : Type) (P : A -> Prop) : Type :=
>     ex2_intro : forall x : A, P x -> ex2 P.

That type already exists in Coq - it is called sig.  There is a whole 
family of these exist-like quantifier/inductives in Coq.Init.Specif.

-- Jonathan