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.

$\endgroup$

1 Answer 1

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 *)
```
$\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
    Commented Apr 30, 2023 at 21:07

Your Answer

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

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