Hey! Does anyone know of a way to make a definition opaque to
autorewrite so that unification doesn't unfold it while trying to rewrite with a lemma? (while not making the definition fully opaque -- I still want unification in other places to see through it)
As a very simple example, imagine
Require Import ssreflect. Require Import ZArith. Definition please_dont_unfold : Z := 10 - 1. Arguments please_dont_unfold : simpl never. Global Typeclasses Opaque please_dont_unfold. Lemma test : Z.to_nat please_dont_unfold = Z.to_nat 9. Proof. (* succeeds and unfolds the definition :( *) rewrite Z2Nat.inj_sub. Abort.
In my actual use case,
please_dont_unfold is a pretty large number, and the rewrite is done by an
autorewritedatabase. Since the
rewrite unfolds the definition,
simpl will then also subsequently try to compute it, even though my definition originally was
Edit: Sorry, I should have mentioned that I'm importing ssreflect.
What would you like the output of
rewrite Z2Nat.inj_sub. to be? In order for it to be applicable, it has to unfold
please_don't_unfold to find the subtraction, otherwise the expression is not rewritable. Or is the idea that this
rewrite should fail?
If so, it seems the vanilla rewrite fails, which you can test in the presence of ssr with
rewrite-> Z2Nat.inj_sub.. Not sure how to make ssr rewrite behave the same.
Maybe you want
rewrite [please_dont_unfold] lock ?Z2Nat.inj_sub -lock.? See also the documentation on ssr locking
Or is the idea that this rewrite should fail?
Indeed, the idea is that I'd like the rewrite to fail.
Thanks! The locking mechanism is helpful and successfully prevents the rewrite from happening.
For my original
autorewrite problem, it turns out that it was caused by one of my dependencies setting
Keyed Unification. I'm now using
Unset Keyed Unification, with which at least the non-ssreflect
autorewrite will not unfold the definition in this case.
Last updated: Oct 04 2023 at 23:01 UTC