Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Setoid rewriting #119

Open
tperami opened this issue Jan 10, 2022 · 3 comments
Open

Setoid rewriting #119

tperami opened this issue Jan 10, 2022 · 3 comments
Labels
enhancement New feature or request

Comments

@tperami
Copy link

tperami commented Jan 10, 2022

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 lukaszcz added the enhancement New feature or request label Jan 10, 2022
@lukaszcz
Copy link
Owner

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
Copy link
Author

tperami commented Jan 10, 2022

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
Copy link
Owner

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants