Stream: Coq users

Topic: Make a definition opaque for rewrite?

view this post on Zulip Lennard Gäher (Feb 28 2023 at 17:42):

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.
  (* succeeds and unfolds the definition :( *)
  rewrite Z2Nat.inj_sub.

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 simpl never.

Edit: Sorry, I should have mentioned that I'm importing ssreflect.

view this post on Zulip Ana de Almeida Borges (Feb 28 2023 at 23:16):

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?

view this post on Zulip Ana de Almeida Borges (Feb 28 2023 at 23:17):

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.

view this post on Zulip Jason Gross (Mar 01 2023 at 04:08):

Maybe you want rewrite [please_dont_unfold] lock ?Z2Nat.inj_sub -lock.? See also the documentation on ssr locking

view this post on Zulip Lennard Gäher (Mar 02 2023 at 20:14):

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 04 2023 at 23:01 UTC