The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

For what it's worth, there's an approach that gives you the best of both 
worlds.
You can define your function normally, specify it implicitly using an
inductive definition similar to Cedric's (or any weaker specification
which "sufficiently" specifies the behaviour of the function for the
use you have in mind), and declare it as globally opaque afterwards.

Fixpoint numeric (t : term) :=
 match t with
 | Term_Zero    => true
 | Term_Succ t0 => numeric t0
 | Term_Pred t0 => numeric t0
 | _            => false
end.

(* here specifies your function as you wish *)
...
(* suppose you have defined [numeric_spe] as in Cédric's proposition,
now prove the following reflection lemma,
   where [reflects] is defined as:

Inductive reflects (P : Prop) : bool -> Prop :=
| reflects_true : forall (Htrue : P), reflects P true
| reflects_false : forall (Hfalse : ~P), reflects P false.

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

On Mon, Aug 1, 2011 at 6:37 PM, frank maltman
<frank.maltman AT googlemail.com>
 wrote:
> On Mon, 1 Aug 2011 17:17:16 +0200
> AUGER Cedric 
>Â <Cedric.Auger AT lri.fr>
>  wrote:
>>
>> By the way, just some informal stuff, there are several ways to
>> simplify a term in coq, here I used an "unfold" followed by a "fold";
>> it has the great advantage that you make the simplification you
>> precisely want (simpl, tends to reduce all that can be reduced,
>> without recursion unrolling, often leading to better terms, but in
>> your case, it was an awful one), but the disadvantage that you have
>> to find the good way to use it (provide the term in which you want it
>> to be rewritten).
>>
>> A good workaround is to build opaque, but specified functions.
>
> Thanks, I was wondering what the general approach was in that case
> actually (after having seen terms reaching to hundreds of lines after
> a simpl on a fixpoint definition)!
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06