Branch autorewrite on rewrite_strat

[mattam82]

Version

8.8 ?

Description of the problem

Autorewrite's implementation is relatively slow and could be replaced by calling the rewrite_strat tactic instead. rewrite_strat subsumes autorewrite and this should only be a matter of plumbing, maybe involving compatibility issues. See #6101 for a potential test-case.

Edit added by @JasonGross:

Related Compatibility Issues

• rewrite_strat does not support "in *" #6107 (in *)
• rewrite_strat makes poor use of using #6114 (unshelve solve and beta-reduction in using tactics)

[JasonGross]

I was under the impression that rewrite_strat uses setoid_rewrite which is modulo δ (unless Keyed Unification is set?) while autorewrite uses rewrite which is only modulo δ on the relation, not the constants. Is there a way to tell rewrite_strat hints ... to not rewrite under binders and to not be modulo δ?

Also I believe autorewrite with foo never fails, while I've seen rewrite_strat try topdown hints foo fail with an unsatisfiable constraints error.

[mattam82]

setoid_rewrite uses rewrite_strat, with a specific selection strategy, you’re right. It can be made accessible. About delta, it’s configurable by hints on the “rewrite” database I think. Indeed for failure I guess it should somehow follow the autorewrite semantics, I’ll have to see how this can work.

[ppedrot]

While we're at it, it might be nice to merge the implementation of discrimination nets for auto hints and for rewrite hints. Currently they are completely distinct (Dn vs. Dnet), which leads to quite a lot of code duplication, not to mention the layers that are built atop of that and are only used once (Term_dnet and Btermdn). This would make the behaviour of hint selection more uniform.

[andres-erbsen]

@mattam82

setoid_rewrite uses rewrite_strat, with a specific selection strategy, you’re right. It can be made accessible. About delta, it’s configurable by hints on the “rewrite” database I think.

If it is, I would like to make use of this feature. In particular, I would like to have the behavior of setoid_rewrite except without acting modulo delta on any identifiers. Is there documentation / living knowledge on how to achieve that?

[mattam82]

@andres-erbsen actually you can. Configure the "rewrite" hint database transparency information to parameterize setoid_rewrite's unification flags.

[cryslith]

@mattam82 Is there any way to do that from within a Coq file? I couldn't find any documentation about it.

[andres-erbsen]

@mattam82 I would also like to know how to use setoid_rewrite (or really anything that can rewrite under binders) without allowing it to unfold definitions.

[mattam82]

I think something like Hint Constants Opaque : rewrite. will do it in Coq 8.9. In the meantime you need to selectively add Hint Opaque hints in the rewrite database.

[mattam82]

For example:

Definition f : nat -> nat := @id nat.
Axiom fax : forall x, f x = x.
Axiom idax : forall x : nat, id x = x.

Hint Opaque f : rewrite.

Goal (forall (x : nat), f x = x).
  Fail setoid_rewrite idax.
  setoid_rewrite fax.