Stream: Coq users

Topic: Opaque, simpl never, Coq 8.18


view this post on Zulip Andrew Appel (Mar 08 2024 at 21:21):

In Coq 8.18 (different from Coq 8.17) it seems as if simpl does not respect Opaque, and I must do Arguments foo: simpl never to get the same effect. Is that true, or is something else going on?

view this post on Zulip Janno (Mar 08 2024 at 22:53):

I know some things changed regarding simpl and aliases (https://github.com/coq/coq/pull/13448) but I don't know that that is related to what you are seeing. An example would help. A quick experiment shows that it is not generally true that simpl ignores Opaque:

Definition zero : nat := 0.
Eval simpl in match zero with 0 => true | _ => false end.        (* [true] *)
Opaque zero.
Eval simpl in match zero with 0 => true | _ => false end.        (* [match ..] *)
Transparent zero.
Arguments zero : simpl never.
Eval simpl in match zero with 0 => true | _ => false end.        (* [true] *)

view this post on Zulip Janno (Mar 08 2024 at 22:56):

https://github.com/coq/coq/pull/18602 has some clarification about simpl never that is probably helpful. The fact that simpl ignores it in certain positions is by design but hadn't been documented. (Well, it still isn't documented until that PR goes in.)

view this post on Zulip Andrew Appel (Mar 11 2024 at 13:18):

I withdraw the question. Upon further investigation, I find that there is no change in the behavior of Coq 8.18, in this particular case. My bug was caused by something else. Janno, thank you for your answer.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 12 2024 at 15:14):

Indeed @Andrew Appel recent work in this area introduced some potential compatibility problems, but TTBOOK, the implementation should have moved towards being _more_ respectful of opacity, not less.


Last updated: Jun 13 2024 at 19:02 UTC