The Coq mailing list

[Andrew Kent <andmkent AT indiana.edu>]

After reading on the differences between compute and hnf and experimenting with hnf a little, I realized there were a few definitions that were opaque that needed to be transparent in order to be solved/simplified in the way I wanted. Now it's working fine! (it's now efficient enough for the examples I wish to run through the wringer)

Thank you all for the comments! You saved me quite a bit of time by having me think about those approaches.

Best,

Andrew

On Wed, Jul 9, 2014 at 7:55 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

You might try replacing "eval compute" with "eval hnf" so it only does
the computation needed to determine which constructor the result is,
and not computation of the internal details of proofs.  If that still
doesn't make things efficient enough, you might try writing an
intermediate function MyRel_dec_int : forall a b, Acc lt (weight_fn a
b) -> {MyRel a b} + {~MyRel a b} which is a fixed point on the Acc
predicate.  Then, use the trick of expanding the Acc proof 2^N times
and feeding that into MyRel_dec_int instead of your original Acc
proof, to define MyRel_dec.  (Sorry I don't recall the details of how
the expansion of Acc is written off the top of my head, but it's been
posted several times before in the mailing list.)
--
Daniel Schepler