The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

Thanks a lot. I have one final question on this general topic.

Suppose I want to specify something using a mixture of logical and
computational existentials. For example, my aim is to construct a program
t : T1 -> T2 which realises a relation R : T1 -> T2 -> Prop (ie. the
graph of t should be contained in the relation). However, we do not start
with R but rather a specification of R, Defn : (T1 -> T2 -> Prop) ->
Prop, say.

I want to write something like

exists R . Defn (R) /\ {t: T1 -> T2 | (x:T1) R x (tx)}

but this won't work. For this example I can put the sig outside the
exists but, in general, I have a family of such definitions and it might
prove fiddly to reformulate like this.

I don't want to extract the R, but it must be provided somehow during the
prove.

Ewen