The Coq mailing list

[Benjamin Werner <werner>]

Yes. One tedious thing with having the computational/logical
distinction carried by the typing is that it leads to numerous
versions of each connector/quantifier.

For instance one might want an "or" between two sets, which is
extracted to booleans: one keeps the left/right information but
discards the respective proof that we are in the corresponding branch.

There are a few of this connectors and quantifiers which are provided
in the library (together with some syntactic sugar) but in some cases
you will have to define your ad hoc quantifier yourself.

In the present case this seems the best solution:
> 
> I want to write something like
> 
> exists R . Defn (R) /\ {t: T1 -> T2 | (x:T1) R x (tx)}

An existential is an inductive definition with one constructor. Here
it would be something like:

Inductive myEx [Defn : (T1 -> T2 -> Prop)->Prop ] : Set :=
 myExi : (t:T1->T2)(R:T1->T2->Prop)(Defn R)->
              ((x:T1)(R x (t x)))->
                  (nyEx Defn).

You then get myEX :  ((T1 -> T2 -> Prop)->Prop) -> Set

and (myEx Defn) is the set/proposition you want. And it gets extracted
to T1->T2 (that is only the t remains of a proof of (myEx Defn) after
extraction).

You use the Elim the usual way. Exists has to be replaced by 
"Apply myExi with t:= ... R:= ... .".



The situation might change if we finaly use another way to mark
computational content. This way of handling things still seems
bearable to me, though.



Cheers,



Benjamin