Stating properties as an instance vs. a theorem

Stream: general

[Patrick Lutz]

What are the conventions in mathlib about when to state a result as a theorem vs. an instance? And relatedly, what are the conventions about when to make an assumption to a theorem implicit vs. explicit (I don't know if this is the right way to phrase this, but what I mean is when should an assumption be written as [foo X] vs (h : foo X))?

The motivation for this question is the current PR on Galois field extensions (#4786). In that PR, several results about field extensions being Galois are stated as instances. Specifically, there is a theorem stating that if $F \subseteq K \subseteq E$ is a tower of field extensions and $E/F$ is Galois then $E/K$ is Galois. Is it better to state this as an instance of the Galois property or as a theorem? And likewise, should the assumption in the theorem that $E/F$ is Galois be explicit or implicit?

After looking at field_theory/normal.lean it looks like maybe the convention is to state things as instances rather than theorems and to make assumptions implicit. But sometimes this can be a little annoying: Lean cannot always infer an instance from the current context and it becomes necessary to insert haveIs in various places.

So: does mathlib have some conventions about this and, if so, what are they?

[Patrick Massot]

It's not about conventions, it's about using the type class inference mechanism as much as possible without pushing it to loop forever (or even search for a very long time).

[Patrick Lutz]

In this case, I don't think we've done enough with Galois theory yet to know if it will cause that sort of problem. What we have encountered once or twice is having to write haveI to establish that an implicit assumption of Galois-ness or normality holds

[Kevin Buzzard]

The main time you don't want to make a term of a typeclass into an instance is when you might be dealing with more than one term of that type

[Patrick Lutz]

Actually, some things in field_theory/galois.lean are very slow, but I think that might be for an unrelated reason

[Kevin Buzzard]

Eg you're considering several topologies on a type

[Simon Hudon]

@Kevin Buzzard I would amend your statement to add that if your definition has non-trivial assumptions (i.e. assumptions that can't be synthesized through type class resolution or unification), you also don't want it to be an instance

[Kevin Buzzard]

Another time is when the term contains some function and you'd for some reason like to have another (perhaps equal but not defeq) description of that function in your instance

[Kevin Buzzard]

Simon knows a lot more about this stuff than I do!

[Patrick Lutz]

Well, I guess with a property like normal or galois we don't care if there's multiple reasons that an extension is normal or galoisso the problem in the example with multiple topologies on the same space probably isn't an issue here?

[Patrick Lutz]

Simon Hudon said:

Kevin Buzzard I would amend your statement to add that if your definition has non-trivial assumptions (i.e. assumptions that can't be synthesized through type class resolution or unification), you also don't want it to be an instance

This was my interpretation of what Patrick Massot was saying

[Simon Hudon]

Patrick was highlighting a different issue. Sometimes, from instance A you can infer instance B and from B you can infer C and then back A. That's going to cause trouble with type class resolution

[Patrick Lutz]

Oh, I see

[Simon Hudon]

What I was talking about is that you have an assumption such as x ≤ y that does not have a canonical way to satisfy

[Patrick Lutz]

The two specific things I'm asking about here are these: https://github.com/leanprover-community/mathlib/blob/9305c59bc289c1284978d1f69a9ba6a085b8240f/src/field_theory/galois.lean#L46 and https://github.com/leanprover-community/mathlib/blob/9305c59bc289c1284978d1f69a9ba6a085b8240f/src/field_theory/galois.lean#L101

[Patrick Lutz]

I'm not sure whether the assumptions in those instances have canonical ways to satisfy

[Simon Hudon]

In the first case, I would say so. You're trying to create a term of type is_galois (mul_action.fixed_points G E) E, G and E are fixed.

[Simon Hudon]

With G and E fixed the rest are 0) type class resolution problems; 1) the problems are smaller than what you're currently handling. It should not loop and it should find a solution