The Coq mailing list

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

Le Mon, 1 Aug 2011 20:08:22 +0200,
Stéphane Lescuyer 
<stephane.lescuyer AT polytechnique.org>
 a écrit :

…
> Lemma numeric_dec : forall t, reflects (numeric_spe t) (numeric t).
> Proof.
> ...
> Qed.
> 
> (* Now 'hide' numeric's true definition, you don't need it since you
> have [numeric_dec] instead. *)
> Global Opaque numeric.
> 
> You can now eliminate a term of the form [numeric t] by using the
> tactic [destruct (numeric_dec t)], instead of evaluation tactics.
> The nice thing is, you can still reduce your terms because they are
> defined as actual functions, so vm_compute or reflexivity will work
> fine.

I wasn't aware of that, that may be handy sometimes.
Even better would be to have some more control on the computation,
since "compute" or "vm_compute" should only be used for very simple
terms (when normalized), since it tends to be even clumsier than
"simpl".

I guess it is not the good idea, but having opacity levels or scopes
could be interesting also.

> Only tactics like simpl or unfold are actually blocked by the
> [Global Opaque] command, which is exactly what one wants in most
> cases. Also, if you extract [numeric] you'll get exaclty the function
> you wrote (whereas writing a function as a proof is always a bit less
> predictable as soon as you use a lot of automation).

For the last point, I like to use the "refine" tactic,
following this scheme:

Definition [name] [parameters]: [type].
refine (
  [term reflecting the overall structure,
   letting '_' for non-informative (Prop) parts
   and followed by a comment label]
).
Proof. (*[first comment label]*)
 clear - [all necessary hypothesis].
 abstract([proof]).
Proof. (*[second comment label]*)
…
Defined.

A littel like with "Program" and "Next Obligations",
but maybe with more control.
I think I have examples on this on the extraction page I did on
Cocorico!; with a good set of notations, it can be very pleasant.

Of course, the "clear - …. abstract …." part is quite annoying,
and I omit it if it is a simple as just an application
(which will any matters will be the case using "abstract").

> The specification
> of the function does not have to be a functional relation, it can be
> any relation which contains the function (in other words it can be
> weaker) and in that sense [numeric_dec] acts as an interface between
> the actual implementation of [numeric] and the development that depend
> on numeric specification.
> 
> HTH,
> 
> Stéphane L.
>