✔ Primitive Projections · Coq users

I've noticed a couple of things with Primitive Projections: first, it seems doesn't seem to use the abbreviations I've defined for certain terms; it seems to expand out all the terms, and the goal becomes quite ugly. Second, without Primitive Projections, I can't write out a list of possible Arguments; I can only have one. Are these two known limitations?

Paolo Giarrusso (Feb 25 2022 at 20:28):

Ramkumar Ramachandra (Feb 26 2022 at 10:39):

Here's a reduced-case example of the second: https://termbin.com/s3r8 -- the error I get is "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.", and it works with Set Primitive Projections.

Ramkumar Ramachandra (Feb 26 2022 at 10:45):

Ramkumar Ramachandra (Feb 26 2022 at 10:46):

Kenji Maillard (Feb 26 2022 at 10:56):

(* Set Primitive Projections. *)
Record foo := { A : Type ; a : A }.
Arguments a {_}, _.

If I understand correctly the error message, Coq is telling you that without primitive projections it cannot determine which version of the implicit arguments should apply (because the first projection A in my example can be an arrow type so a can be applied to an arbitrary number of arguments depending on the choice of A). I'm not sure how primitive projections make a difference in the implementation though...

Ramkumar Ramachandra (Feb 26 2022 at 11:28):

Nice. @Gaëtan Gilbert has additionally pointed out the lines in the source that error out in the issue.

Ramkumar Ramachandra (Feb 26 2022 at 11:29):

Paolo Giarrusso (Feb 26 2022 at 15:50):

@Ramkumar Ramachandra looking at the issue, why would you expect it to use that definition? notations/abbreviations are supposed to be used when pretty-printing the body, but there’s no such expectation for definitions.

Paolo Giarrusso (Feb 26 2022 at 15:55):

so, a priori, it just means the definition has been delta-reduced. Yes, Gaëtan’s example seems to reduce it very eagerly, maybe more than it should (hard to tell).

Paolo Giarrusso (Feb 26 2022 at 15:57):

well, if that example were less eager, then the next risk would be that simpl might reduce the definition, but simpl gives users more control…

Paolo Giarrusso (Feb 26 2022 at 15:58):

either way, an actual Notation Layer’ args := (body). might be a way to control pretty-printing of the expanded terms.

Ramkumar Ramachandra (Feb 26 2022 at 16:18):

It's not a notation, @Paolo Giarrusso -- it's a definition we use until the very end, proving everything else in terms of that.

Ramkumar Ramachandra (Feb 26 2022 at 16:21):

simpl leads to unusable blowups almost everywhere in our proof script, except for a few corners.

Ramkumar Ramachandra (Feb 26 2022 at 16:23):

Without Primitive Projections, Coq uses all the Class projections uniformly, irrespective of whether they're a Definition, or just given a Type. With Primitive Projections, Definitions seem to be forgotten completely. Isn't this contrary to expectation?

Ramkumar Ramachandra (Feb 26 2022 at 16:26):

The reason it's not a notation, is because we want to type-check the definition too. It lives within a big Class.

Paolo Giarrusso (Feb 26 2022 at 17:47):

@Ramkumar Ramachandra I see the confusion: you said “abbreviation” early on, but that’s a technical term for these kind of notations.

Paolo Giarrusso (Feb 26 2022 at 17:49):

re expectations, I can see your point but I don’t know what to expect of these definitions-in-records. It’s certainly a good question!

Ramkumar Ramachandra (Feb 26 2022 at 18:19):

Yeah, I don’t know what the term for this is. When Hugo and I were chatting informally, he used the term “abbreviation” and it stuck :) We’re calling it “definition-projection” in the issue.

Paolo Giarrusso (Feb 26 2022 at 18:24):

Side note on simpl: if you'd like it to be usable, you can tell it to stop unfolding a definition foo via Arguments foo : simpl never.

Stream: Coq users

Topic: ✔ Primitive Projections

Ramkumar Ramachandra (Feb 25 2022 at 11:02):