Setoid rewriting

[tperami]

The default rewriting tactic (rewrite/autorewrite) will refuse to rewrite under binders/arrows. See the manual. Unfortunately, that means that sauto will also not do those rewriting if they are in the rew:db: hint set.

Example:

Parameter A B : Prop. 
Parameter ab : A <-> B.
Hint Rewrite ab : ab.

Lemma test : (forall x : nat, A) -> B.
  sauto db:ab. (* fails *)

  setoid_rewrite ab.
  sauto (* succeeds *)
Qed.

The workaround is to define a custom autorewrite with ab with

Ltac ab_simp :=
  progress (repeat (rewrite_strat topdown hints ab); 
  repeat match goal with 
  | H : _ |- _ => rewrite_strat topdown hints ab in H
  end).

Then sauto simp+:ab_simp proves the test lemma.

This is kind of exactly what was done for boolean reflection, but it would be nice if the default sauto rewriting was already as powerful as this. It is possible that this change may break existing proofs with some not-well designed rewriting systems. Therefore, adding it as an extra option like setoid_rew:on might be worthwhile.

[lukaszcz]

Yes, it would make sense to have this as a separate option. There would be a performance penalty, however, so this should be an option. I think it shouldn't be too hard; I'll take a look sometime in the future, several months perhaps (you can try doing it yourself and submitting a pull request if you don't want to wait).

[tperami]

I may do it myself, but I've never written a Coq plugin, so I have no idea how to call something like setoid_rewrite from OCaml or how to access the hint database. That will require some learning

[lukaszcz]

If you have the desire to do it, read a Coq plugin tutorial (https://github.com/coq/coq/tree/master/doc/plugin_tutorial), and then look at the "sauto" tactic implementation in: https://github.com/lukaszcz/coqhammer/blob/coq8.14/src/tactics/sauto.ml The implementation already does things like calling external tactics and accessing hint databases.