To Is or not to Is (convention on Props)

Stream: general

[Fabrizio Montesi]

Sometimes Prop definitions stating that a value 'is' or 'has' something start with the respective prefix (e.g., IsTop), sometimes they do not (e.g., Even). Is there an established convention for this?

The rule of thumb I'm currently following in CSlib so far is that if I have both a bundled and unbundled version of something, then I distinguish the latter by using the Is prefix or similar. But sometimes, when I don't have such two versions, I just drop the prefix for the Prop definition, like Bisimulation (https://cs-lean.github.io/Cslib/Foundations/Semantics/Lts/Bisimulation.html#Bisimulation).

[Aaron Liu]

my rule of thumb is if it's obviously a Prop then don't use an Is but if it seems like it could be confused for data then make it Is

[Aaron Liu]

of course, we also have stuff like docs#IsAdjoinRoot and docs#CategoryTheory.Limits.IsLimit which are data

[Fabrizio Montesi]

Right, but 'obviously' is not always obvious. Couldn't one think that Even is an even number (instead of the property of being even)?

[Aaron Liu]

good point

[Luigi Massacci]

If I remember correctly the mathlib naming guide had a paragraph about Is, though I have forgotten what it says entirely

[Aaron Liu]

maybe replace "obviously" with some synonym which has a weaker connotation

[Etienne Marion]

Here is what the naming convention says: https://leanprover-community.github.io/contribute/naming.html#prop-valued-classes

[Fabrizio Montesi]

Mmh that'd suggest IsBisimulation, right?
And then I could have a bundled version Bisimulation that contains the relation and the proof of IsBisimulation (although I see no use for it right now).

[Tanner Duve]

this is what i did for “Fact” and “isFact” in my LL phase semantics PR fwiw

[Robert Maxton]

Aaron Liu said:

of course, we also have stuff like docs#IsAdjoinRoot and docs#CategoryTheory.Limits.IsLimit which are data

For IsLimit, the argument is that it's "morally a subsingleton", in that for category theoretic purposes it's unique up to isomorphism which is all we ever care about, so you can usually throw away the data/save it to an opaque variable and get away with it