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?

Can you show an example?

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.

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

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

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

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

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.

@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.

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).

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…

either way, an actual `Notation Layer’ args := (body).`

might be a way to control pretty-printing of the expanded terms.

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

`simpl`

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

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?

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

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

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!

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.

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.

Ramkumar Ramachandra has marked this topic as resolved.

Last updated: May 19 2024 at 16:02 UTC