Stream: Coq users

Topic: cbn in primitive projections


view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 19:24):

The refman says that a folded primitive projection delta reduces to an unfolded primitive projection. And I guess unfolded primitive projections are like matches, so they reduce by iota. Thus if I run
cbn delta iota I observe that it simplifies my record projections. However if I run cbn delta; cbn iota nothing happens. Am i to infer from this that the primitive projection being 'unfolded' does not persist if there are no further reductions?

view this post on Zulip Gaëtan Gilbert (Apr 23 2023 at 19:32):

looks like the refolding gets in the way
so I guess your interpretation is correct?
I don't really understand how refolding works though

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 22:07):

I experimented and the same thing happens with cbv.

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 22:07):

so you have to write cbv delta [proj] iota to unfold a constructor.

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 22:45):

Alright i'm lost now. I have no idea how this works.
I have a hypothesis

 j := @constructor (Build_Record A B C )

I try the following:

progress(cbv delta [constructor] iota) in j
>>> Failed to progress.
progress(cbv beta) in j
>>> Failed to progress.
progress(cbv delta [constructor] beta) in j
(* Success! *)
progress(cbv delta [constructor] iota) in j
(* Success! *)

What's strange to me about this is that there is no visible change to the term given by cbv delta [constructor] beta. It is apparently progressing but I diff'ed the two terms before and after and there's nothing. Somehow the presence of bothdelta and beta is making some permanent change to the fold status of the constructor?
I just don't understand what the beta is doing exactly.

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 22:47):

I did "Show Proof Diffs" and there was no change to the proof either

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 22:48):

Well, maybe there was , there were a lot of (...)'s from the full proof which I don't know how to unfold.

view this post on Zulip Gaëtan Gilbert (Apr 23 2023 at 22:55):

see https://github.com/coq/coq/commit/978ae7d9323558099efb0c4e4e39549221378d5d I guess
the handling of primitive projection is not very coherent across Coq

view this post on Zulip Gaëtan Gilbert (Apr 23 2023 at 22:57):

you can Set Printing Unfolded Projection As Match. to see when projections get unfolded

Set Primitive Projections.

Record R := mk { p : nat }.

Set Printing Unfolded Projection As Match.

Goal p (mk 0) = 0.
  cbv delta beta.
  (* now goal is "(let '{| p := p |} := {| p := 0 |} in p) = 0" *)
  cbv iota.

view this post on Zulip Gaëtan Gilbert (Apr 23 2023 at 22:59):

also compare with how it works with non primitive projections

Record R := mk { p : nat }.

Goal p (mk 0) = 0.
  cbv delta.
  cbv beta.
  cbv iota.

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 23:12):

I can't find this flag in the documentation and it doesn't work for me, it just says this flag is unknown.
Is it the same as "Set Printing Primitive Projection Parameters"

view this post on Zulip Patrick Nicodemus (Apr 23 2023 at 23:15):

Gaëtan Gilbert said:

see https://github.com/coq/coq/commit/978ae7d9323558099efb0c4e4e39549221378d5d I guess
the handling of primitive projection is not very coherent across Coq

Thank you, lol, very straightforward answer to my question I guess

view this post on Zulip Gaëtan Gilbert (Apr 24 2023 at 09:33):

Patrick Nicodemus said:

I can't find this flag in the documentation and it doesn't work for me, it just says this flag is unknown.
Is it the same as "Set Printing Primitive Projection Parameters"

It's not in a released Coq version yet

view this post on Zulip Patrick Nicodemus (Apr 27 2023 at 13:52):

Sweet, look forward to it in 8.1x


Last updated: Jun 17 2024 at 22:01 UTC