2
$\begingroup$

I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting) I then manually figure out which rewrite rules were applied and perform the steps manually or semi-automatically. Often applying transitivity or Proper by hand is quicker.

Is there some way to have Coq tell me which rules autorewrite applied? Possibly also how it instantiated the variables.

I found issue #9285, but it does not mention existing features.

Edit: Link to the relevant page of the reference manual on Programmable Proof Search where the autorewrite tactic is described.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

I don't know about autorewrite specifically, but in general one you have a proof term, you can Print it and figure out what automatic steps did in your back:

Lemma foo: forall n : nat, n = n.
Proof.
auto.
Qed.

Print foo. (* from this we know a proof is: intro n ; apply eq_refl *)
```
Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ I tried to use this approach, but I find it impractical in my situation. setoid_rewrite is involved, with multiple nested Proper functions. This leads to large proof terms which are difficult to understand. If only equality were used, it might be easier. $\endgroup$
    – 8bc3 457f
    Apr 30 at 21:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.