Yannick Zakowski (May 25 2020 at 18:33): Yannick Zakowski (May 25 2020 at 18:33):The documentation for cbn correctly states:
They unfold a constant if and only if it leads to a ι-reduction, i.e. reducing a match or unfolding a fixpoint.
Is there any good reason for it to not unfold constants that would lead to unfolding a cofixpoint?
We are working with a definition wrapper around our primitive projection in the Interaction Trees project and it seems to prevent cbn from reducing, forcing us to unfold this definition wrapper in a slightly annoying fashion
Kenji Maillard (May 25 2020 at 19:05):I had the impression that both fixpoints and cofixpoints are only unfolded when the thing on which they are guarded is enough evaluated. For instance cbn won;t unfold twice in the following definition because its argument is not a constructor:
Fixpoint twice (n:nat) {struct n} : nat :=
match n with
| 0 => 0
| S n => S (S (twice n))
end.
Section Test.
Context (n:nat).
Eval cbn in twice n. (* twice n *)
End Test.
Dually, if I provide enough observations to a cofixpoint, cbn seems to unfold it correctly:
Set Implicit Arguments.
CoInductive Stream (A : Type) : Type := { hd : A ; tl : @Stream A }.
CoFixpoint from (n:nat) : Stream nat := {| hd := n ; tl := from (S n) |}.
Eval cbn in tl (from 0). (* from 1*)
Hmm consider the following example:
Set Primitive Projections.
Variant streamF (stream : Type) :=
| NilF
| ConsF (n : nat) (k : stream)
.
Arguments NilF {_}.
Arguments ConsF {_} n k.
CoInductive stream : Type :=
go { _observe : streamF stream }.
Definition observe (s : stream) : streamF stream := _observe s.
Section App.
Variable k : stream.
Definition _app
(app : stream -> stream)
(os : streamF stream) : stream :=
match os with
| NilF => k
| ConsF n s => go (ConsF n (app s))
end.
CoFixpoint app (s: stream) : stream :=
_app app (observe s).
End App.
Variable k s: stream.
Eval cbn in observe (app k s).
Eval cbn in _observe (app k s).
Goal observe (app k s) = _observe (app k s).
cbn.
(* Here the version to the right does a step of reduction by unfolding the cofix app to its body.
However it does not do the same on the left because it has to unfold a constant in order to find the primitive projection and hence be allowed to reduce the cofix.
If I am not mistaken, if unfolding this constant had exposed the possibility to unfold a fixpoint, cbn would have performed it
*)
Sorry the example is a bit long, but it should make my concern clearer.
Kenji Maillard (May 25 2020 at 19:50):But in this case unfolding the constant observe will lead you to the term (fun s => _observe s) (app k s) where no cofixpoint unfolding is directly available, no ? (so that behaviour is annoying in this case but to fire the cofixpoint you also need to do a step of beta reduction)
[Edit: my argument does not stand, it works perfectly for a fixpoint
Context (n:nat).
Definition bidule (f : nat -> nat) := f (S n).
Eval cbn in bidule twice. (* S (S (twice n)) *)
]
Li-yao (May 25 2020 at 19:52):One other solution is to avoid the observe wrapper and be careful to always apply primitive projections, and have warnings or errors when that's not the case.
Yannick Zakowski (May 25 2020 at 19:54):Hmm I am not completely sure I understand.
When I perform unfold observe, I end up with the same term as the one to the right.
Is your point that that the tactic unfold actually both unfold and beta reduces, and that cbn definitely does not want to unfold a constant for a beta reduction, so that it does not get to access the unfolding of a cofix special case?
Li-yao (May 25 2020 at 19:56):Although, one more reason we use the observe wrapper, IIRC, is that primitive projections force their arguments to head-normal form even if the head is stuck (so we'd rather not reduce anything, or have a more conservative reduction strategy).
Kenji Maillard (May 25 2020 at 20:08):Li-yao said:
Although, one more reason we use the
observewrapper, IIRC, is that primitive projections force their arguments to head-normal form even if the head is stuck (so we'd rather not reduce anything, or have a more conservative reduction strategy).
wdym by "the head is stuck" exactly ? Something like the examples below ?
Set Primitive Projections.
Set Implicit Arguments.
Record Wrap (A : Type) := wrap { unwrap : A }.
Definition foo (b : bool) := if b then wrap 3 else wrap 6.
Definition bar (b : bool) := wrap (if b then 3 else 6).
Variable b : bool.
Eval cbn in unwrap (foo b). (* does not reduce *)
Eval cbn in unwrap (bar b). (* does reduce *)
Yeah something like that. I'll have to look for a concrete example because I don't have one off the top of my head now.
Kenji Maillard (May 25 2020 at 20:43):@Yannick Zakowski I don't really understand if the behavior of cbn is expected in your example, but couldn't you deal with it by issuing a Arguments observe s /. command ?
Yannick Zakowski (May 25 2020 at 20:44):Oh I never think of using this, that's actually a good idea indeed!
Yannick Zakowski (May 25 2020 at 21:13):By the way with respect to this trick, isn't the documentation inaccurate? It states:
A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the / symbol in the argument list of the Arguments vernacular command.
But it's not just only, it's also if, and even if it would not be unfolded normally
Enrico Tassi (May 26 2020 at 07:23):IIRC / can be mixed with !, and in that case it is an and, not an or. Anyway, any improvement to the doc is very welcome. The file in question is here: https://github.com/coq/coq/blob/master/doc/sphinx/language/extensions/arguments-command.rst#effects-of-cmdarguments-on-unfolding
Enrico Tassi (May 26 2020 at 07:25):If you submit a PR, CI builds the doc for you and posts a link to it in the PR, you don't even need to install sphinx to make small adjustments
Paolo Giarrusso (May 26 2020 at 08:21):@Yannick Zakowski one general concern with observe s / is that you can’t use observe anymore in lemmas for rewriting — if foo : observe (bar ...) = baz then rewrite /= foo and cbn; rewrite foo are likely to stop working (because the LHS of foo is not a “cbn normal form”) — except maybe for the limited unfolding done by rewrite (which I don’t understand enough to rely on)
Paolo Giarrusso (May 26 2020 at 08:24):I wonder if the right Arguments _observe would help? I think many of the heuristics by cbn and simpl can be selected by tuning reduction settings for Arguments...
Paolo Giarrusso (May 26 2020 at 08:25):I have _lots_ of those Arguments command in my code (and of Notations), so I almost never unfold by hand, but sometimes I can’t use simpl or cbn because they unfold too much (and then use rewrite lemmas whose proofs are just eq_refl _ to control reduction)
Last updated: Oct 03 2023 at 04:02 UTC