Stream: Coq users

Topic: ✔ Primitive Projections


view this post on Zulip Ramkumar Ramachandra (Feb 25 2022 at 11:02):

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?

view this post on Zulip Paolo Giarrusso (Feb 25 2022 at 20:28):

Can you show an example?

view this post on Zulip 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.

view this post on Zulip Ramkumar Ramachandra (Feb 26 2022 at 10:45):

I couldn't find any open or closed issues for the second, so I've filed a bug here: https://github.com/coq/coq/issues/15739

view this post on Zulip Ramkumar Ramachandra (Feb 26 2022 at 10:46):

I'm going to try to work on a reduced-case example for the first.

view this post on Zulip Kenji Maillard (Feb 26 2022 at 10:56):

Here's a minimised version:

(* 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...

view this post on Zulip 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.

view this post on Zulip Ramkumar Ramachandra (Feb 26 2022 at 11:29):

Here's an real-world goal-diff of the first: https://github.com/coq/coq/issues/15740 -- It'll take me some time to cook up a reduced case.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ramkumar Ramachandra (Feb 26 2022 at 16:21):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Mar 02 2022 at 18:15):

Ramkumar Ramachandra has marked this topic as resolved.


Last updated: Jan 29 2023 at 05:03 UTC