The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 7 Oct 2010 22:25:13 -0700,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> 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.

I do not use Function, nor Program, but it seems a lot like what you
want. Have you really read these parts of the manual?
[{coq_documentation_directory}/html/refman/Reference-Manual004.html#toc15]
[{coq_documentation_directory}/html/refman/Reference-Manual028.html]
> 
> 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.

There is also the refine tactic, in which you could be interested.
>>>
Definition eq (m n: nat): {m = n}+{m <> n}.
refine ( fix eq m n : {m = n} + {m <> n} :=
          match m with
          | O => match n with
                 | O => left _ _
                 | S n => right _ _
                 end
          | S m => match n with
                   | O => right _ _
                   | S n => if eq m n
                            then left _ _
                            else right _ _
                   end
          end
).
(* 0=0 *)
split.
(* 0<>S n0 *)
intro; discriminate.
(* S m0<>0 *)
intro; discriminate.
(* _H : m0 = n0 |- S m0 = S n0 *)
destruct _H; split.
(* _H : m0 <> n0 |- S m0 <> S n0 *)
intro H; destruct _H.
inversion_clear H; split.
Defined.
<<<
But beware, I am not sure you can make parts of this program opaque and
other transparents; that means that your term will either be unfoldable
everywhere with its full proof (when terminating with "Defined")
or never unfoldable (when terminating with "Qed"),
but to produce an unfoldable skeleton with opaque proofs, I am pretty
sure that you need "Program".

> 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.

the "set" tactic does so, but you need to give the full term in the
instant you use the tactic.

> 
> 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.

Cannot you create you own type:
>>>
Record elt_of {X: Type} (T: Ensemble X): Type :=
{ elt: X;
  elt_is_in: In _ T inhabitant
}.

Definition inclusion_fun {X:Type} (S T:Ensemble X):
  Included _ S T -> {f : elt_of S -> elt_of T
                    | forall x : elt_of S, (f x).(elt _) = x.(elt _)}.
<<<
This will also have the advantage, that if you are lazy and do not
provide names to your hypothesis, then destructing an "elt_of" will
provide meaningfuller names than "x3" or "H2".

Such a trick can also be usefull when redefining some common operators:

Record and (A B: Prop): Prop :=
{ proj1: A;
  proj2: B
}.

Record exist (A: Type) (f: A -> Prop): Prop :=
{ witness: A;
  witness_spe: f witness
}.

(* you can even do the useless "Record True : Prop := {}." *)

You can also use "Notation".

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