The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Although this is solved, I also point an other alternative.
In your proof you have two kind of elements:
- the "constructive" elements
- the "pure proof" elements

I often use the following pattern:

Definition foo : bar.
refine (
  <computational skeleton part with '_' where proofs should be>
).
Proof.
  clear <not needed hypotheses>.
  abstract (<tactics solving the goal>).
Proof.
  clear <not needed hypotheses>.
  abstract (<tactics solving the goal>).
…
Defined.

The idea is similar to the proposed one with a decider returning a boolean value, and then proving the correctness of the decider.

Advantages:
- only one term (well 'abstract' generates others, but you can ignore them, and they do not appear in the .v file)
- avoid to do two times the same steps (one time to define the function, and one time to prove it)
- do in parallel both the decider and the proof (so you do not have to switch from the proof to the decider to correct it and then go back to the proof and readjust it every time)

Drawbacks:
- abstract is a "one shot" tactic, you do not have interactivity, thus I often start by not using abstract, and once the proof is complete, I change it in a "one shot" one (that is use '[', '|', ']', ';' …)
- you need to manually clean the not used hypothesis (unless you do not use "fix" and do not care having abstracted terms with way too many hypothesis)

Of course, if providing a skeleton in the "refine" tactic is too annoying, you can directly use tactics for that, and use "abstract" only for proofs which are not involved in deciding.

2014-07-10 2:37 GMT+02:00 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

--
.../Sedrikov\...