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
    Commented Apr 30, 2023 at 21:07

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