When to use instances for terms

Stream: mathlib4

[Violeta Hernández]

The way I'm used to working with Mathlib is, you prove predicates and pass them as arguments to other predicates. Typeclasses exist a level above this in some sense. They're the implicit assumptions about whatever type you're working within, stuff you are rarely if ever going to need to specify explicitly.

There are a few places where this design philosphy doesn't apply. The two I'm aware of are docs#ONote.NF and docs#SetTheory.PGame.Impartial. These are typeclasses for specific values, rather than for the types of objects they describe.

The idea in both cases is, I believe, that the compiler should be able to do structural proofs automatically. For instance, if G is impartial, the compiler should be able to determine -G + 1 + * is impartial as well, without having to write down the proof yourself. The downside is that, whenever you don't know if a value satisfies your predicate a priori, you need to prove it first in a haveI block, or make all arguments explicit with @. This is made slightly more annoying by the level of indirection between the instance and the actual predicate.

I don't really think this is a huge problem that needs solving. We've managed just fine with e.g. docs#SetTheory.PGame.Numeric, even though it shares this structural property.

I'm generally not a fan of using instances like this, and I'd like both of these usages to be refactored out, but I'd like to hear what others think.

[Violeta Hernández]

Another issue with this design is how sensitive instances are to rewrites. And when one breaks, you don't have the name of the instance at hand to debug it. None of these problems exist if you just call the theorem name explicitly.

[Eric Wieser]

I think this is a common source of contention. One common argument for "P x should be a typeclass" is "I want to write instance [P X] : UndisputableTypeclass X, and Fact (P X) is too annoying".

I think probably everyone is happy that docs#Even is not a typeclass, but I think the status of docs#IsClosed (which is a typeclass, even though IsOpen is not) was more divisive

[Eric Wieser]

Another awkward one is docs#Invertible, which has good reason to be a typeclass because there would be no other way to provide the notation; but the API is difficult to use precisely because it is a data-carrying typeclass, and so it usually only plays a part while assembling a more user-friendly interface.

[Violeta Hernández]

I don't think either of the cases I mention would be good as Fact either. It's not like we're making extensive use of the impartiality of * or anything like that.

[Violeta Hernández]

The whole thing with ONote is honestly a bit of a mess, that file was made back in 2017 and hasn't been touched much since. But at least with Impartial that refactor would be pretty easy.

[Violeta Hernández]

I'd like to hear from other people within the game part of the library. @Junyan Xu or @Timo Carlin-Burns?

[Timo Carlin-Burns]

I haven't tried to work in either of these files, but after a quick look my first impression is that:

• ONote.NF should probably be a regular proposition but there should be a type for { o // o.NF} which is closed under addition, etc.
• Impartial shouldn't be a type class either

[Violeta Hernández]

{o // o.NF} does exist, it's docs#NONote

[Violeta Hernández]

I'll make the PR for Impartial sometime soon, I'll wait a bit on ONote since there's a lot more that needs to be cleaned up within that file first

[Violeta Hernández]

Huh, actually, it seems like we had discussed this exact thing before in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Well-founded.20recursion.20for.20pgames/near/286467225

[Mario Carneiro]

Violeta Hernández said:

{o // o.NF} does exist, it's docs#NONote

Note that this is supposed to be the main type that people use outside the file. ONote is only needed within the file itself

[Violeta Hernández]

I opened #16054 for removing the Impartial typeclass. A few proofs become slightly longer but not by much, dot notation means you can just write stuff like hG.add hH for the impartiality proofs.