Stream: Coq users

Topic: ✔ Forcing reduction of record map


view this post on Zulip Meven Lennon-Bertrand (Jan 12 2023 at 20:00):

I tried the following code:

Set Primitive Projections.

Record foo := { foo_field : nat }.

Definition map_foo (f : nat -> nat) (u : foo) : foo := {| foo_field := f u.(foo_field) |}.

Arguments map_foo f !u.

Eval cbn in (map_foo S {| foo_field := 1 |}).

From what I gather, the Arguments command should let map_foo unfold in the last line reducing to {| foo_field := 2 |}, as its second argument is a constructor. This is also what About map_foo tells me when I call it after the Arguments line. Yet, the unfolding/reduction is not triggered. Have I misunderstood the purpose of ! in Arguments? Or am I doing something else wrong?

view this post on Zulip Meven Lennon-Bertrand (Jan 12 2023 at 20:01):

I seem to be observing the same issue if I replace foo by an inductive with a single field – in other words, this does not seem to be specific to records.

view this post on Zulip Gaëtan Gilbert (Jan 12 2023 at 20:29):

! adds an additional condition on unfolding, so it reduces if it would reduce without the ! AND the argument reduces to a constructor
it seems like you want it to reduce IFF the argument reduces to a constructor which would be Arguments map_foo f !u /.

view this post on Zulip Paolo Giarrusso (Jan 12 2023 at 20:50):

Arguments's output is indeed misleading, which comes up on the bug tracker when people try to reverse engineer simpl and cbn

view this post on Zulip Paolo Giarrusso (Jan 12 2023 at 20:51):

I recall that ! without / has different meanings between simpl and cbn, but I stopped trying it so I forgot the details

view this post on Zulip Meven Lennon-Bertrand (Jan 12 2023 at 21:10):

Ah, I see… The documentation and the error message are indeed not very clear

view this post on Zulip Notification Bot (Jan 12 2023 at 21:10):

Meven Lennon-Bertrand has marked this topic as resolved.


Last updated: Jun 24 2024 at 14:01 UTC