# Zulip Chat Archive

## Stream: new members

### Topic: MIL comments

#### Julian Külshammer (Jul 09 2020 at 06:08):

Since @Patrick Massot encouraged me to write comments about "Mathematics in Lean", here are some regarding Chapter 2 which I just finished (solving most of the exercises):

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.

#### Kevin Buzzard (Jul 09 2020 at 06:29):

Thanks!

#### Jeremy Avigad (Jul 09 2020 at 11:41):

Thanks, Julian! These are *extremely* helpful. We'll make these fixes to next version of MiL soon, and maybe come back with questions.

A quick response to the last comment: indeed, we certainly intend to write a chapter on how to define and work with algebraic structures. There's a wiki here, https://github.com/avigad/mathematics_in_lean_source/wiki, but the plans keep changing.

#### Jeremy Avigad (Jul 09 2020 at 22:37):

@Julian Külshammer, in my just-updated mathlib, I tried this:

```
import data.real.basic
import tactic
example (a : ℝ) : 0 ≤ a^2 :=
begin
library_search,
-- exact pow_two_nonneg a
end
```

I get the suggestion: "Try this: exact pow_two_nonneg a". That is what we want. Can you confirm that it fails when you try it?

In the next exercise, the idea was indeed to encourage you to use `library_search`

figure out how to show `exp a <= exp b`

. You can then say this:

```
example (h : a ≤ b) : c - exp b ≤ c - exp a :=
begin
have : exp a ≤ exp b,
from exp_le_exp.mpr h,
library_search
end
```

Once again `library_search`

gives you a one-liner that will finish it off, though `linarith`

also works. We were trying to encourage you to play around with `library_search`

, tab completion, and `linarith`

-- whatever it takes to get the job done. Can you think of better wording for that?

#### Jeremy Avigad (Jul 09 2020 at 22:45):

In answer to the fifth question, yes, you could give the previous example a name like `dvd_square`

or `dvd_pow_two`

and then apply it. Though in this case it is probably easier to repeat the two commands.

#### Julian Külshammer (Jul 28 2020 at 08:31):

@Jeremy Avigad Sorry for the late reply, I thought too much about your question how to reformulate and then forgot.

To answer your question: For the first example, I just quoted the wrong line, I wanted to refer to the exp example below, sorry ofr that. For me a wording like "Using the same tricks, confirm that linarith instead of library_search can also finish the job." instead of "Also, confirm that linarith can do it with a bit of help." would have been more clear, but this is maybe personal taste. It was more a question whether I had missed something.

#### Julian Külshammer (Jul 28 2020 at 08:55):

Some more comments, mostly typos:

3.2 Inside a existential quantifier (should be "an")

Overall, I was slightly overwhelmed with the amount of tactics in Section 3. Compared to that, I found Section 4 much more manageable (but I also did Section 4 after the workshop, so I definitely had more experience then).

4.1 and the the anonymous constructors (one "the" too much)

4.1 In the first exercise when trying rintros, I also needed the brackets to have `rintros x (h1 | h2)`

. This is only explained in a later paragraph.

4.1 Two prove that two sets are equal (should be "To")

4.1 I had some trouble in the set-theoretic identities one might enjoy proving: The direction `s\cup t\subseteq s\t\cup t`

didn't work for me. At some point I tried `by_cases h : x\in t`

but it didn't let me do it. Probably I took the wrong turn.

4.1 Here is are some examples (remove "is")

4.2 In the downloaded version in vscode of the second-to-last example of the chapter, somehow "open_locale classical" didn't work. I could fix it by importing tactic additionally. I didn't see the problem when doing the exercise in the web-browser.

4.2 In the last exercise I found it easier to not use h3 at all and finish the exercise after h2 with `apply h₁, rwa h`

#### Mario Carneiro (Jul 28 2020 at 09:37):

For `by_cases`

to work on arbitrary propositions, you have to have classical logic enabled (using `open_locale classical`

at the top of your file, or `classical,`

at the beginning of your proof)

#### Scott Morrison (Jul 28 2020 at 09:52):

This isn't true anymore:

```
import tactic.core
example (P : Prop) : true :=
begin
by_cases P,
trivial,
trivial,
end
```

#### Scott Morrison (Jul 28 2020 at 09:52):

(Without the `import`

it doesn't work, however...!)

#### Kenny Lau (Jul 28 2020 at 09:57):

how does that work?

#### Jalex Stark (Jul 28 2020 at 11:45):

I would guess it just runs `classical`

if it can't find an instance of decidability for P

#### Jalex Stark (Jul 28 2020 at 11:47):

I also imagine that's what `tauto!`

does, but I should probably do less imagining and more reading source code

#### Jeremy Avigad (Jul 28 2020 at 15:14):

Thanks again, Julian. We'll make all these corrections soon.

Regarding the proof, I just confirmed that this works with a recent version of Lean mathlib:

```
import tactic
open set
variable {α : Type*}
variables (s t u : set α)
example : (s \ t) ∪ t = s ∪ t :=
begin
ext x, split,
{ rintros (⟨xs, xnt⟩ | xt),
{ left, exact xs },
right, exact xt },
rintros (xs | xt),
{ by_cases xt : x ∈ t,
{ right, exact xt },
left, exact ⟨xs, xt⟩ },
right, exact xt
end
```

The `import tactic`

is hidden in the html display (we generally eliminate the repeated boilerplate to avoid cluttering the text), but it is there when you open the snippet.

I can't figure out why it works. If I hover over `by_cases`

, the tactic documentation says that the proposition has to be decidable, but printing the term shows that the generated proof uses `classical.prop_decidable`

. The `by_cases`

tactic ultimately calls an internal function, `mk_instance`

. I am guessing that that was recently changed to use classical logic if all else fails.

Last updated: May 13 2021 at 20:13 UTC