Hey! Does anyone know of a way to make a definition opaque to rewrite
/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 autorewrite
database. Since the rewrite
unfolds the definition, simpl
will then also subsequently try to compute it, even though my definition originally was simpl never
.
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 rewrite
and autorewrite
will not unfold the definition in this case.
Last updated: Oct 13 2024 at 01:02 UTC