Stream: Coq devs & plugin devs

Topic: Changed behavior of reduction tactics.


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

view this post on Zulip Pierre-Marie Pédrot (Apr 17 2021 at 12:03):

It is indeed probably related to the change of match representation.

view this post on Zulip Pierre-Marie Pédrot (Apr 17 2021 at 12:04):

Before, real iota-reduction was actually a step of match followed by a beta.

view this post on Zulip Pierre-Marie Pédrot (Apr 17 2021 at 12:04):

Because internally, the match nodes were represented using functions.

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

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

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

view this post on Zulip Enrico Tassi (Apr 17 2021 at 13:12):

The new behavior seems better, match should get you the body of the branch, not a beta redex

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

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

view this post on Zulip Théo Zimmermann (Apr 17 2021 at 15:30):

Doesn't it still work if you split iota into its fix and match component?

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

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

view this post on Zulip 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 16 2021 at 03:02 UTC