Stream: Coq devs & plugin devs

Topic: simpl never and hnf

Hugo Herbelin (Sep 10 2021 at 14:10):

The reference manual says: "simpl never indicates that a constant should never be unfolded by cbn, simpl or hnf". However, we have the following:

Fixpoint f n := match n with 0 => nat | S n => nat -> f n end.
Arguments f : simpl never.
Goal f 2.
simpl. (* nop *)
cbn. (* nop *)
hnf. (* nop *)
Fail intros x.
Abort.

Arguments id : simpl never.
Goal id (nat -> nat).
simpl.
cbn. (* nop *)
hnf. (* reduce!? *) Undo.
intros x.
Abort.

Record t := {a:Prop}.
Arguments a : simpl never.
Goal {|a:=True->True|}.(a).
cbn. (* nop *)
hnf. (* reduce!? *) Undo.
intros x.
Abort.

Is there something that was more specifically intended originally? Should the doc or the code be changed?

Enrico Tassi (Sep 10 2021 at 14:12):

I think simpl never should not affect hnf (it affects cbn only because cbn tries to replace simpl)

Hugo Herbelin (Sep 10 2021 at 15:02):

Enrico Tassi said:

I think simpl never should not affect hnf (it affects cbn only because cbn tries to replace simpl)

So, the bugs are:

• in the doc, which should not mention hnf
• and in the no-op of hnf in the first example

Right? If agreement on that, I can amend the doc and the code (this is related to a resurgence of #5245 in #14640).

Jason Gross (Sep 11 2021 at 00:32):

I thought that it impacted hnf because hnf uses the simpl engine to do fixpoint refolding. Is there some reason to expect we can decouple unfolding from simpl without decoupling refolding (or vice versa)?

Last updated: Jun 04 2023 at 19:30 UTC