That's a bit annoying. I think that Coq should be lifting from the smaller universe, e.g. TA : tele@{u}
such that u < Quant
. Perhaps I removed the Cumulative
annotation on tele
and that should be re-added?
It is worth noting that the succeeding case is strictly more powerful than the failing case.
As an alternative, what about dropping the quantifiers entirely? We think of this as ghost code so we could also make them look a bit more like lambdas.
Concretely one option could use ;
(,
might be another option)
AU << x y z ; ... >> @ .. , ..
<< a b c ; ... >>
Lambda is also an option, but I would personally prefer to not to add Unicode unless it is really helpful.
If this notation exists, then I think this is the most natural interpretation of it.
That said, I think it should be a parsing only
notation because IMO the |-
is an important part of the system (note that |-
notation also has the |-@{}
notation which is preferable to explicit casts.
On a practical level, using both sides of the entailment is generally more useful (e.g. for Coq rewrite
). To me, this suggests that lemmas should be written when an explicit |-
.
Gregory Malecha (171768c4) at 06 May 12:15
I don't think short names here are too problematic because named universes are extremely rare and have a different namespace than terms.
I don't know about other places that this would be beneficial to, but they could exist. This is probably the biggest gain in iris because bi
is so pervasive. This will reduce the number of universe constraints on any definition that mentions both universal and existential quantifiers. Adding annotations to bi_tforall
and bi_texist
would probably benefit the definitions that build on them.
The names L
and LQ
are still under the bi
module, so I would suggest using bi.L
and bi.LQ
when referring to them but I'm ok if you want to propose other names. L
was meant to be "logic" and LQ
was meant to be "quantifier".
If you guys are game for the universe reduction, then I can remove the extra stuff from the MR and we can merge it.
I guess if the test case passes it isn't crucial. I do like both naming the universes and reducing the number of universes. The later reduces the number of constraints and often the size of universe instances.
Gregory Malecha (2635a5e5) at 11 Apr 13:46
I've added the CHANGELOG entry.
Gregory Malecha (0feaf1f0) at 11 Apr 13:17
Update the CHANGELOG.
Gregory Malecha (ac310b6a) at 07 Apr 06:02
This is just duplicating information from the Reserved Notation
.
I force pushed with a revision to the commit and it seems like gitlab is picking up the fix now.
Gregory Malecha (298e7fcf) at 07 Apr 02:44
Use unicode and fix comment.
It's odd, the last commit diff has these fixed, but gitlab seems to be rendering the final diff incorrectly. See !368 (9c37da7e)
Hmmm..that's odd. Thanks.
Gregory Malecha (ac310b6a) at 07 Apr 02:27
Minor notation cleanup to avoid casts.
... and 1735 more commits