Stream: Coq devs & plugin devs

Topic: simpl never and hnf


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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:

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

view this post on Zulip 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: Oct 21 2021 at 20:02 UTC