Stream: Coq users

Topic: cbn in primitive projections

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?

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

Patrick Nicodemus (Apr 23 2023 at 22:07):

I experimented and the same thing happens with cbv.

Patrick Nicodemus (Apr 23 2023 at 22:07):

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

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.

Patrick Nicodemus (Apr 23 2023 at 22:47):

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

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.

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

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.

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.

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"

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

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

Patrick Nicodemus (Apr 27 2023 at 13:52):

Sweet, look forward to it in 8.1x

Last updated: Oct 04 2023 at 22:01 UTC