The Coq mailing list

["Larry D. Lee jr." <llee454 AT gmail.com>]

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.

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.

Unlike ex's definition this new definition gives a recursive property:

  ex2_rec : forall (A : Type) (P : A -> Prop) (P0 : ex2 P -> Set), 
(forall (x : A) (p : P x), P0 (ex2_intro P x p)) -> forall e : ex2 P, P0 e.

I was then able to define an existential instantiation operator as:

  Definition ei (H : ex2 P) : sig P :=
    ex2_rec (fun _ => sig P)
                 (fun (x : A) (H0 : P x) => exist P x H0) (* using a 
local existential instantiation to construct a set value. *)
                 H.

I could then use the existential operator to instantiate values that I 
can prove exist and satisfy certain constraints:

  Parameter A : Set.
  Parameter P : A -> Prop.
  Axiom existence_axiom : ex2 P.

  Definition a : sig P := ei existence_axiom.

I suspect that the ability to define values, by proving their existence 
rather than by "constructing" them, is essentially what distinguishes 
classical and constructive mathematics, but I'm not sure.

I have two questions. First, why is ex restricted to propositions? That 
is, Why doesn't ex have a recursive property? Second, is there an 
operation in the standard library that would allow me to instantiate 
existentially quantified variables at the global level without having to 
define my own constructs ex2 and ei?

Thanks for any insight, references, etc, that you all may be able to 
provide.
- Larry