Zulip Chat Archive

Stream: general

Topic: Stating properties as an instance vs. a theorem


view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:07):

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 FKEF \subseteq K \subseteq E is a tower of field extensions and E/FE/F is Galois then E/KE/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/FE/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?

view this post on Zulip Patrick Massot (Nov 04 2020 at 00:09):

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

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:10):

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

view this post on Zulip Kevin Buzzard (Nov 04 2020 at 00:12):

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

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:12):

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

view this post on Zulip Kevin Buzzard (Nov 04 2020 at 00:12):

Eg you're considering several topologies on a type

view this post on Zulip Simon Hudon (Nov 04 2020 at 00:14):

@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

view this post on Zulip Kevin Buzzard (Nov 04 2020 at 00:14):

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

view this post on Zulip Kevin Buzzard (Nov 04 2020 at 00:14):

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

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:15):

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?

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:15):

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

view this post on Zulip Simon Hudon (Nov 04 2020 at 00:17):

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

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:17):

Oh, I see

view this post on Zulip Simon Hudon (Nov 04 2020 at 00:17):

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

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:20):

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

view this post on Zulip Patrick Lutz (Nov 04 2020 at 00:20):

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

view this post on Zulip Simon Hudon (Nov 04 2020 at 00:23):

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.

view this post on Zulip Simon Hudon (Nov 04 2020 at 00:27):

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


Last updated: May 14 2021 at 12:18 UTC