Théo Zimmermann (Apr 17 2021 at 11:48): Théo Zimmermann (Apr 17 2021 at 11:48):@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)?
Pierre-Marie Pédrot (Apr 17 2021 at 12:03):It is indeed probably related to the change of match representation.
Pierre-Marie Pédrot (Apr 17 2021 at 12:04):Before, real iota-reduction was actually a step of match followed by a beta.
Pierre-Marie Pédrot (Apr 17 2021 at 12:04):Because internally, the match nodes were represented using functions.
Pierre-Marie Pédrot (Apr 17 2021 at 12:05):Now this beta step is automatically performed because there are no lambda-abstractions anymore in the match case.
Pierre-Marie Pédrot (Apr 17 2021 at 12:06):(If you ask me the previous behaviour was a bug. I expect that performing iota would result in the substitution of the constructor arguments.)
Pierre-Marie Pédrot (Apr 17 2021 at 12:08):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
Théo Zimmermann (Apr 17 2021 at 15:12):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).
Jason Gross (Apr 17 2021 at 15:19):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)?
Théo Zimmermann (Apr 17 2021 at 15:30):Doesn't it still work if you split iota into its fix and match component?
Théo Zimmermann (Apr 17 2021 at 15:30):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.
Jason Gross (Apr 17 2021 at 15:32):I have not tested. If splitting iota into fix and match works, then I have no objection
Théo Zimmermann (Apr 17 2021 at 15:49):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 08 2024 at 16:02 UTC