The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 20 Aug 2007, Benjamin Gregoire wrote:

> roconnor AT theorem.ca
>  wrote:
> Computing the head normal form of proof can be very costly.
> Personally I prefer to use the following scheme:
>     Definition semi_dec : A -> bool:= .... .
>     Lemma semi_dec_correct :forall a, semi_dec a -> complex_proposition.
>     Proof. .... Qed.
> Now you can trivially define your function. For proof by reflexion you can 
> use the lemma
> semi_dec_correct, and what you have to compute is "semi_dec a" which does 
> not contain proof terms.
>    Benjamin

I would have expected hnf to do the minimum amount of computation 
necessary to expose a constructor.  This is effectively what my semi_dec 
function does.  But hnf seems to actually run simpl until a constructor is 
exposed.

Anyhow, it's nice to know what I'm doing what you do.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''