@Pierre-Marie Pédrot The behavior of:
Goal 1 + 1 = 2. cbv delta fix beta. cbv match.
has changed in 8.14. In 8.13, it created a beta-redex, but it doesn't in master. Is this change expected and is it related to https://github.com/coq/coq/pull/13563 (the changelog talks about new beta-redexes, not fewer)?
It is indeed probably related to the change of match representation.
Before, real iota-reduction was actually a step of match followed by a beta.
Because internally, the match nodes were represented using functions.
Now this beta step is automatically performed because there are no lambda-abstractions anymore in the match case.
(If you ask me the previous behaviour was a bug. I expect that performing iota would result in the substitution of the constructor arguments.)
A simpler minimal example:
Inductive box (A : Type) := Box : A -> box A. Goal match Box _ tt with Box _ x => x end = tt. Proof. cbv match.
The new behavior seems better,
match should get you the body of the branch, not a beta redex
OK thanks. cc @Jason Gross who I recall explained that behavior to Jim in one of the documentation PR (though I don't think it ended up being documented).
I'm moderately concerned if
iota doesn't leave behind beta-redexes, because this means that there's no longer a way to reduce a bare fixpoint by a single step. (Previously, I could do
cbv iota; cbv beta and this would reduce a bare fixpoint by a single step.) Can we get single-step reduction tactics (by which I mean, reduction strategies which do not trigger in subterms of their output)?
Doesn't it still work if you split
iota into its
That being said, I agree with the need for single-step reduction tactics. This is something that beginners would really benefit from to fully understand how computations operate.
I have not tested. If splitting
match works, then I have no objection
The example added by Jim in his PR on the conversion chapter (https://github.com/coq/coq/pull/13815) still works fine (https://coq.gitlab.io/-/coq/-/jobs/1188471474/artifacts/_install_ci/share/doc/coq/sphinx/html/language/core/conversion.html#examples). The only difference is that the call to
cbv match at the end does not create a beta redex.
Last updated: Oct 16 2021 at 03:02 UTC