The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Dear Daniel

If your proofs revolve mostly around proving membership in sigma types
then the Program Package might be what you are looking for.

Regards 
Christian


Am Donnerstag, den 07.10.2010, 22:25 -0700 schrieb Daniel Schepler:
> 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.