The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Sorry if this is a basic question, but I couldn't find any answer in the 
manual...  Say I want to make a definition of some function, but it involves 
passing in proofs into some of the subterms.  Is there a way I could leave 
those proofs to be filled in by the proof assistant, while making other parts 
of the definition explicit?  For a simple example of what I mean:

Definition inclusion_fun {X:Type} (S T:Ensemble X)
  (_:Included _ S T) (x:{x:X | In _ S x}) :
  {x:X | In _ T x} :=
  match x with
  | exist x0 _ => exist _ x0 ?
  end.

So I'd want the proof assistant to come up with a goal of "In X T x0" with 
appropriate variables and hypotheses in the upper section (including "H : 
Included X S T" and "H0 : In X S x0"), to fill in the "?".

Certainly, I could leave out the body and use the proof assistant to 
construct 
the whole thing; but then, on reading through the .v file, it would be 
unclear 
what the function is actually returning.  On the other hand, I could put in 
all those proofs by hand; in the case above, that would be easy enough, but 
in 
general that will tend to be cumbersome.  Or I could prove mini-lemmas 
beforehand that prove exactly the conditions I need to fill in the gaps; but 
that would also tend to distract attention from the important results in a .v 
file.

Such a feature would also be useful for leaving gaps in a "pose" definition, 
again generating the appropriate subgoals of the current goal.

On a related note, is there any way to generate a subgoal which will become a 
transparent definition once its proof is done?  It seems that "assert" always 
generates an opaque definition, and I don't see any alternative that 
generates 
a transparent definition.

Sometimes I've worked around this by having functions that return a sigma-
type.  Then the ability to e.g. "destruct inclusion_fun in ..." is immensely 
useful.  But sometimes that tends to be a little cumbersome, too...

Definition inclusion_fun {X:Type} (S T:Ensemble X):
  Included _ S T -> {f : {x:X | In _ S x} -> {x:X | In _ T x} |
  forall x:{x:X | In _ S x}, proj1_sig (f x) = proj1_sig x}.
...
Defined.

That's already a bit of a mouthful, and tends to get even more so if there 
are 
multiple cases for the definition.
-- 
Daniel Schepler