avigad/mathematics_in_lean_source

Source code for the Mathematics in Lean tutorial.

mathematics_in_lean_source's Issues

Numbering scheme

As I wrote in an email, I think

On Zulip, you can helpfully specify that you are asking about the third exercise by referring to it as "the third problem in exercises/logic/propositional_logic.lean."

is not robust enough. We need an immutable tag system. In my tutorials I explicitly number exercises, and reordering or deleting exercises is not meant to change tags.

`@` symbol not explained

In some examples the @ symbol is used before names of theorems / functions, but it was not explained that it displays the implicit arguments. Maybe worth mentioning.

Explain structural eta reduction

#121 added a comment about structural eta reduction to Chapter 6, Section 1, without explaining it.

some theorems are no longer in mathlib

Some theorems used in the tutorial are no longer present in the current version of mathlib, e.g., factors_count_pow. But maybe it is not a serious problem -- I was just a bit confused why I couldn't use the theorem I learned in another project. Maybe this theorem got moved somewhere under a different name? But I couldn't easily find.

rintros ⟨⟩

Do we want to explain the rintros ⟨⟩ trick somewhere?

More automation in weightedaverage example

The exercise about

def weightedAverage {n : ℕ} (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardSimplex n) : StandardSimplex n

would benefit a lot from gcongr and linear_combination. Revising this should probably wait for inserting discussion of those tactics earlier in the book.

choose tactic

There is an example of the choose tactic commented out in the chapter Sets, Functions, and Relations. We should decide whether to discuss it there or wait until a later chapter.

obtain

Do we want to mention obtain in chapter 3 where we discuss rintros and rcases?

`by` could be used for easier solving

Is there any reason we skip by in this line?

mathematics_in_lean_source/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean

Line 382 in 02c54eb

theorem self_sub (a : R) : a - a = 0 :=

Took me a bit of time to figure out why I was getting lean errors while trying to prove the statement.

Git Pod set up failed

I can't open workspace of git pod. :(

New refine calc

This is also a somewhat global issue so I won't try to fix it right now. The behavior of calc in tactic mode changed recently, and I think we should mention it. We can now leave holes in the proof, and they become new goals at the end of the calculation, because calc in tactic mode now means refine calc ... instead of exact calc ....

I don't know where to point it out, but we should certainly keep it in mind while writing and proof-reading explanations involving calc.

lambda

We need to explicitly explain the lambda thing. Remember "lambda abstraction" means nothing to an average mathematician. Worse, we don't have any word to mean that. I think it shows up first in the Logic chapter, introduced by "remember that" without having been explained anywhere (classic teaching trick).

Then later we write "The intros command corresponds to a lambda". But again this is completely alien, and I think it deserves more explanation.

Type* in C3S1

Near the end of C3S1, there's a Type*, which is Lean 3 syntax, should be Type _.

Suffices

Introduce the suffices tactic somewhere

finite sets

We need to explain the finset vs fintype vs finite mess somewhere, probably in Chapter 4.

Update instructions

The introduction currently says

You can update to a newer version by tying ``git pull`` followed by ``lake exe cache get`` inside
the ``mathematics_in_lean`` folder.

but this won't work for people who have edited the exercises. We should describe a better workflow.

Missing import in C02_Basics/S01_Calculating

This file contains the text "The import line at the beginning of the example", but there is no such import.

Basic definitions in Sets

For some reason I forgot a bunch of margin notes from my printed copy of the book when I commented to Chapter 4 PR.

• Maybe warn that empty and univ often need a type ascription
• Mention the notation in and notin from the beginning, use it to actually spell out the definition of subset and intersection instead of alluding to them
• After commutativity of intersection, there is a mysterious explanation of $ without any $ in sight.

in lean4 07-15 nightly the package proof widget should use version >= v0.0.12

Examples should use `Type*` not `Type _`

Some context in this Zulip thread, cc @mattrobball.

Not we will need #105 to make this feature available.

Index

We got off to a good start with building an index, but then we fell off the wagon. We should go through systematically and add index entries.

factorial simp example

In Chapter 5, we have

example : fac 0 = 1 := by
  simp [fac]

which is misleading since giving [fac] plays no role.

'iSup_delab' has already been declared

I am getting the following error when building MIL.Common

error: stdout:
./././MIL/Common.lean:81:4: error: 'iSup_delab' has already been declared
error: external command `/Users/username/.elan/toolchains/leanprover--lean4---v4.2.0-rc3/bin/lean` exited with code 1

It seems that iSup_delab has been actually added to mathlib4 (5 days ago according to git blame).

Set autoimplicit flag to false

We should set the autoImplicit flag to false, to match mathlib. See Eric Wieser's comments at #110.

Git clone via HTTPS instead of SSH

We tried following the installation instructions on a new computer (macOS 12 Monterey) and got an error on the second install step:

In a terminal, navigate to the folder where you want to put a copy of the repository, and type git clone [email protected]:leanprover-community/mathematics_in_lean.git to fetch it from github.

The error was: permission denied (publickey). It looks like this computer has no public keys at all in the ~/.ssh folder. (Don't you also need to connect your key to a GitHub account?)

Should the instructions instead suggest the HTTPS clone url https://github.com/leanprover-community/mathematics_in_lean.git, since it does not require any setup?

Function application

If I'm not mistaken, we never point out that f x means f(x) and, more importantly how functions with several inputs are handled through curryfication. I think we use it first in Chapter 2 when talking about exp and log. And the two variables cases first arises with min and max.

Issue with `^` in `SO3_Using_Theorems_and_Lemmas`

In Basics/SO3, there is

variable (a b c d e : ℝ)
-- ....
example : 0 ≤ a ^ 2 := by
  -- apply?
    exact sq_nonneg a

presented as an example that should just work. However, I get the error

type mismatch
  sq_nonneg a
has type
  0 ≤ a ^ @OfNat.ofNat ℕ 2 (instOfNatNat 2) : Prop
but is expected to have type
  0 ≤ a ^ @OfNat.ofNat ℝ 2 instOfNat : Prop

If I try to "make the 2 a Nat", it still doesn't work with error

type mismatch
  sq_nonneg a
has type
  0 ≤ a ^ 2 : Prop
but is expected to have type
  0 ≤ a ^ ↑2 : Prop

Alex J. Best said:

There is an issue where lean 4 wants to interpret powers as coming from the same type (i.e, a real to a real rather than a real to a nat), if you add the line

local macro_rules | ($x ^ $y) => (HPow.hPow $x $y)

above the lemma it should hopefully fix it, but we should also fix this example in the book somehow

Tactic state explains comes late

In the basics chapter there is a paragraph starting with "In the Lean editor mode, when a cursor is in the middle of a tactic proof, Lean reports on the current proof state". (because GitHub renders rst and md files, I don't know how to link to specific lines). I think this explanations comes too late, it feels weird that we suddenly explain this after so many proofs. I guess this was created through copy-paste and reorganization.

Also I'm note sure "Lean editor mode" is clear. Is it meant to include the web editor and emacs? If yes then do we explain this anywhere?

When do we introduce simp?

From Zulip:

Another general remark about my tutorials: I never tell my students about simp. That would be too powerful, and it would encourage them to try simp every other line instead of thinking.

Note that I do introduce ring and linarith very early. There are much better than simp because students are not too tempted to try them on each and every goal (although linarith is a bit too powerful here, especially when it comes to find contradiction, so I delay its introduction some more).

Anyway, we need to decide when we introduce simp.

Link to project instructions

The project instructions https://leanprover-community.github.io/install/project.html#working-on-an-existing-project have more steps than the instructions in section 1.1 (like the extra step for MacOS users before running code .)

The best solution is probably just to link to the aforementioned page.

Repeated text in 2.4 (page 23-24)

Text is repeated. Once in bold and once in normal font

Thread panic when running `lake exe cache get`

Lean version: Lean (version 4.0.0-nightly-2023-08-23, commit 216d2460e0ad, Release)
Windows 11 Pro

This occurred when setting up the leanprover-community fork of this project.

Error:

info: downloading component 'lean'
179.9 MiB / 179.9 MiB (100 %)   5.0 MiB/s ETA:   0 s
info: installing component 'lean'
info: cloning https://github.com/leanprover-community/mathlib4 to .\lake-packages\mathlib
info: cloning https://github.com/leanprover/std4 to .\lake-packages\std
info: cloning https://github.com/gebner/quote4 to .\lake-packages\Qq
info: cloning https://github.com/JLimperg/aesop to .\lake-packages\aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to .\lake-packages\Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to .\lake-packages\proofwidgets
info: Downloading proofwidgets/v0.0.13/windows-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/windows-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [4/9] Compiling Cache.Requests
info: [4/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
Attempting to download 3678 file(s)
Downloaded: 3678 file(s) [attempted 3678/3678 = 100%] (100% success)
Decompressing 3678 file(s)
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Os { code: 32, kind: Uncategorized, message: "The process cannot access the file because it is being used by another process." }', D:\a\leangz\leangz\src\ltar.rs:68:53
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Os { code: 32, kind: Uncategorized, message: "The process cannot access the file because it is being used by another process." }', D:\a\leangz\leangz\src\ltar.rs:68:53
uncaught exception: leantar failed with error code 101

Unused variables

The linter currently complains about unused variables e.g. in fun a b aleb ↦ mf (mg aleb). We should probably explain this somewhere and then replace unused variables by underscores.

Keep up with translations.json

The VSCode translations files actually has a pretty active life and I'm a bit worried that MIL contains many references to its current behavior. I'm not even sure it's currently up to date. It would be nice to have a way to flag those references and setup some CI, or at least have a command generating a list for manual inspection. The dream would be to have some rst command like:

..translation:: real, ℝ

that would register the fact we claimed \real is leading to ℝ, and those claims would be extracted as part of the build process.

Külshammer's list

Copy-pasting from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/MIL.20comments to make sure we don't forget

2.2: In the example at the end if one "feels cocky": Normally I would prove mul_right_inv before proving mul_one. Maybe this is just me and maybe it is a good lesson for "cocky" people.
2.3 As a beginner in Lean I was very confused over le_trans that addition and multiplication are by default left associated while implication is right associated. I feel like, this could be pointed out at this point (it is at least stated in Chapter 3.
2.3 "however we will use that fact that" should be "however we will use the fact that", small typo I think.
2.3 In the exercise to prove 0\le a^2, if I follow the advice and use library_search, then it replies "failed" for me. If I tell it that it has e^a\le e^b, then library_search does work, but also linarith works (with the same "amount of help"), so I didn't quite get the sentence below the exercise.
2.4 In the example where one should prove x | y * (x * z) + x^2 + w^2 could one put the lemma x | x^2 in the code that was proved before, so that one can use that instead of duplicating this part of the goal?
2.5 Small typo: "algebraic structures likes" should be "algebraic structures like"
2.5 You write that "It is a good exercise to prove that not every lattice is distributive by constructing one", unfortunately, what this tutorial seems to be missing is an explanation how to set up such a structure, i.e. how does one give an example of a group, a vector space, etc. Maybe this is worth another section/chapter to explain how to define a mathematical object and how to give an instance of a mathematical object.

Ideas from LFTCM

These are notes I wrote to myself during the meeting:

• Describe the tactics suggest and hint
• Talk about ctrl+space for better tab completion
• show_term
• specialize

missing import statement

See this block of text in Basics/Calculating:

Let’s try out rw.

example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
begin
  rw mul_comm a b,
  rw mul_assoc b a c
end

The import line at the beginning of the example imports the theory of the real numbers from mathlib.

The import data.real.basic line doesn't actually appear in the page.

Term mode is now nicer

This is a global issue hence I'm not doing anything about it in the PR I'm currently preparing. A lot of things were written back in the old days when proof terms were completely opaque. With a recent Lean+VSCode, the tactic state get updated when you move the cursor through a proof term. So we need to explain that and rehabilitate term mode somehow. Unfortunately this needs going through the whole thing, and I didn't have that in mind yesterday while reading.

Automation chapter (RFC)

Initially, we made the decision to introduce automation piecemeal. Tactics like ring, abel, and linarith are introduced in Chapter 2. There are a few references to simp in Chapter 3, but it is only discussed in any detail in Chapter 4. And there is a lot of useful automation that we do not yet discuss at all:

• congr
• linear_combination
• polyrith
• positivity
• gcongr
• tauto
• aesop

The list is likely to grow quickly in Lean 4. Since the point of Chapters 2, 3, and 4 are to introduce rw, apply, and logical manipulations, it makes sense to favor manual calculation there. But beyond that point, we'd do well to show students/readers how to use automation like this wherever it is appropriate.

I suggest we add a new chapter, Automation, in between the current Chapters 4 and 5, and then systematically use automation after that wherever it is appropriate. We can discuss all the items listed above, and show how they can be used to simplify a lot of the examples and exercises from the previous chapters. I suggest using simp in restricted ways in Chapters 3 and 4, but deferring a full discussion to the new chapter.

I am curious to hear whether others think this is a good idea, and, if so, what else should be included in this chapter.

unicode in pdf doesn't show

The pdf https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf doesn't show all unicode characters, like the blackboard 1 in chapter 7.

Remove extra parentheses

The crazy parentheses in the following snippet from Chapter 5 are probably either a mathport issue of working around a precedence bug that no longer exists.

example (f : ℕ → ℕ) : (∑ x in range 0, f x) = 0 :=
  Finset.sum_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : (∑ x in range n.succ, f x) = (∑ x in range n, f x) + f n :=
  Finset.sum_range_succ f n

Small typo in 4. Sets and Functions

I guess Classical.some is changed to Classical.choose now?

mathematics_in_lean_source/MIL/C04_Sets_and_Functions/Source_S02_Functions.lean

Lines 534 to 535 in 1c83219

	one convenient method is to use the classical ``some``
	operator, illustrated below.

mathematics_in_lean_source/MIL/C04_Sets_and_Functions/Source_S02_Functions.lean

Lines 547 to 557 in 1c83219

	#check Classical.choose h
	example : P (Classical.choose h) :=
	Classical.choose_spec h
	-- QUOTE.
	/- TEXT:
	Given ``h : ∃ x, P x``, the value of ``Classical.some h``
	is some ``x`` satisfying ``P x``.
	The theorem ``Classical.some_spec h`` says that ``Classical.some h``
	meets this specification.

Field one_mul if the group definition seems wrong

At

mathematics_in_lean_source/lean_source/06_Abstract_Algebra/source_02_Algebraic_Structures.lean

Line 143 in 5a6c20b

(one_mul: ∀ x : α, mul x one = x)

it seems that the definition of one_mul is wrong. Namely, it is (one_mul: ∀ x : α, mul x one = x), while I guess the intention was to have x and one swapped.

The same also appears later in the file, at the definition of group₂.

namespace and open

I think we haven't really decided where we explain namespace, open and the dot notation (here I'm not even thinking of the magical one, simply using fully specified names). This kind of question is much easier in TPIL that takes a more systematic approach (or even more in the reference manual). So we need extra thinking here.

Outdated reference to the `from` tactic in chapter 3

This text in the section on negation no longer matches the preceding example.

`Prime` norm num extension

The extension now lives in the Mathlib.Tactic.NormNum.Prime module, and you don't get it automatically by importing the definitions like you did in Lean 3 (we're trying to keep theory and meta code separate in mathlib4).

This tripped up a number of students during the first week of the MSRI workshop, and there was another question about it on Zulip which reminded me to make an issue.

apply and exact in Section 2.2

In Section 2.2, after "We have used a new trick!" I think there is a slight inconsistency issue. The paragraph mentions apply and exact as things that will be discussed later. But exact has already been discussed, and apply is used anyway in the next big code block.

Present tactic unfold

As a beginner, I am finding tactic unfold very handy while I'm not able to "see through definitions" yet. Maybe it could be mentioned at some point, together with its at * variant.

Lattice notation vs set notation

Not an actual issue up to now, but let's record that we should carefully monitor leanprover-community/mathlib#3083

Topology chapter should teach/warn about products of metric spaces

The metric space on α × β uses the max-distance, not the Euclidean distance, and maybe give a forward-reference to the Euclidean distance.