Bugs in the book "Mathematics in Lean"

Stream: new members

[Sven Manthe]

Two "bugs" in the book (sorry for not opening a pull request, I didn't look at how to do this yet):

1. In the 4th line of the calc of the proof of cauchySeq_of_le_geometric_two' in the file S02_Metric_Spaces.lean, the (1 / 2) ^ i seems to evaluate to 0 due to the use of integer division; I propose specifying the type as ℝ.
2. In the example starting at line 392 of the file S03_Topological_Spaces.lean, I propose replacing the assumption RegularSpace by T3Space, as otherwise you cannot use the results on Hausdorff spaces proposed in the book.
   PS: If there are some rules about how to post in the Lean Zulip etc., please tell me.

[Yaël Dillies]

1. is due to the elaboration issue for ^.

[Sven Manthe]

I don't think I follow. I was also quite confused about the following example, obtained by minimizing the above:

import Mathlib
open BigOperators
#check ((∑ i in Finset.range 7, (1 / 7) ^ i) : ℝ )
#check ((∑ i in Finset.range 7, (1 / 7) ^ 2) : ℝ )
#check ((∑ i in Finset.range 7, (1 / 7) ^ i) = (3: ℝ) )
#check ((∑ i in Finset.range 7, (1 / 7) ^ (2:ℕ)) = (3: ℝ) )
#check ((∑ i in Finset.range 7, (1 / 7) ^ 2) = (3: ℝ) )

In lines 3,4 the 1/7 is interpreted as a natural, in 1,2,5 as a real.

[Kyle Miller]

(@Yaël Dillies This seems to be a mistake in the exercise, not the ^ issue)

@Sven Manthe I think you're right, there appear to be missing ℝ ascriptions. (I'm sitting near @Jeremy Avigad right now, but here's a ping :smile:)

[Sven Manthe]

Yes, I'm quite sure that there is an error in the proof skeleton of the exercise (after all, my elaborator interprets 1/2 as natural). However, I'm also a bit confused about how the typing/coercing works in this situation (more precisely, I'd have expected a different behavior then in my example above) and would like to understand it if there is an easy explanation

[Kevin Buzzard]

The Lean 4 algorithm for figuring out whether you're a natural or a real is far more arcane than the Lean 3 version and I'm still not sure I understand it. But my understanding of it is that now, in contrast to Lean 3, Lean 4 attempts to assign a type to both sides of an = indepedently, so forcing the RHS to be a real as you do in the last three examples may not have the effect you expect on the LHS. In the third and 4th example, Lean guesses it's a nat because the exponent is a nat. In the 5th example the conclusion is "I don't know yet, let's look at the RHS".

[Kyle Miller]

@Sven Manthe Here are some observations:

1. In an equality, the sides don't communicate about what types they are until the very end. This means that if one side can be interpreted as a Nat, it will be interpreted as a nat. At the end, if it needs to have been a real, then the whole value is coerced.
2. All the basic arithmetic operations are able to work together to figure out what type each of the constituent terms are supposed to be. There's an algorithm that tries to compute one type everything has to be coerced to, and each term is individually coerced.
3. Not every operation is able to participate in this algorithm. For example, ∑ doesn't and isn't able to, but it should still be able to pick up on the expected type when elaborating the inside.

[Kyle Miller]

I didn't test it, but this might (almost) give you what you want:

#check (∑ i in Finset.range 7, (1 / 7) ^ 2 : ℝ) = (3 : ℝ)

[Kyle Miller]

You'll run into the thing Yaël mentioned earlier though, where ^ makes sure the exponent has the same type too if possible. This ideally would fix that, though I'm not sure it does:

#check (∑ i in Finset.range 7, (1 / 7) ^ (2 : ℕ) : ℝ) = (3 : ℝ)

[Kevin Buzzard]

Re 1. @Kyle Miller isn't the 5th example a counterexample to your claim? The LHS could be a nat but ends up being a real.

[Kyle Miller]

@Kevin Buzzard You're right, I'm not able to count and I didn't test things, so these last two messages aren't illustrative of anything.

[Kyle Miller]

I guess this was supposed to be an example of it inferring as Real without the LHS ascription. This makes sense because Lean doesn't commit to the numerals (1 / 7) ^ 2 being in any particular type until the very end, and by that point the type from the RHS propagates to the LHS, and then they become Real with a Real ^.

[Kyle Miller]

In (1 / 7) ^ (2:ℕ) and (1 / 7) ^ i, it's able to see that 2 and i are nats, and the arithmetic operation elaborator propagates this type to each of the parts of the expression, which makes 1 and 7 be nats, with / and ^ being the nat operations.

[Sven Manthe]

Okay, it seems to be more complicated than I expected (I guess, naively I expected that type checking would proceed only "from the outside to the inside" or only "from the inside to the outside", realized soon that the second one isn't the case, but the above examples show that the first one also isn't). So probably my "if there is an easy explanation" fails, and I won't try to understand the details of the typing algorithm now (and fixing these problems by specifying types seems to be almost always easy). Thank you all for your help

[Jeremy Avigad]

Thanks for the heads up. @Patrick Massot and I will fix it!

[Patrick Massot]

Thanks Sven. I'm sorry about those issues. Very weirdly they were fixed in the solutions but not in the exercises. They should now be fixed everywhere.

[Patrick Massot]

Be careful if you update the repository to not overwrite your files (you were told in https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html#getting-started to make a copy of the MIL folder in order to avoid that risk).