Support for primitive projections

[clarus]

Hello,

After some trials, it seems that coq-record-update does not support the Set Primitive Projections. flag. Here is an example were we did not get the expected result:

From RecordUpdate Require Import RecordSet.

(* Worked without this flag. *)
Set Primitive Projections.

Module TypeParameterExample.
  Record X T := mkX { a: nat; b: T; c: T * T; }.
  Arguments a {T}.
  Arguments b {T}.
  Arguments c {T}.

  Instance etaX T : Settable _ := settable! (@mkX T) <a;b;c>.

  Import RecordSetNotations.
  Unset Primitive Projections.
  Definition set_a (x:X unit) := x <| a := 3 |>.
  Definition set_b (x:X unit) := x <| b := tt |>.
  Definition set_b' {T} (x:X T) (v:T) := x <| b := v |>.
  Definition set_c {T} (x:X T) (v:T) := x <| c := (v,v) |>.

  Lemma foo x : (set_a x).(a) = 3.
    simpl.
    Show.
End TypeParameterExample.

Do you know if this is expected? Is there any plans to support the primitive projections?

[tchajed]

This is not expected, thanks for letting me know! I’ll try to take a look in the next week or so.

[tchajed]

I looked into this and it doesn't look like a simple fix. (The only thing I could do right away is trigger an error because the setter doesn't do anything.) The problem is that what's supposed to happen is we use eval pattern a in constr:(fun x => mkX (a x) (b x) (c x)) to get fun f => fun x => mkX (f x) (b x) (c x), abstracting over the projection a. With primitive projections the term a doesn't even show up, instead x.(a) is a primitive form.

I think the path in #19 might be a way to fix this, which doesn't use the eta expansion at all and just builds the right term from scratch. In some ways that's the most principled way for coq-record-update to work, it's just scarier because it uses Ltac2.Constr.Unsafe which is very low-level and possibly unstable.

[clarus]

OK, thanks for your answer! (I missed it before).

[clarus]

I do not know the status of this issue, but we had a solution made by @emarzion with https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/RecordUpdate.v that we use for our needs.