MIL comments

Stream: new members

[Julian Külshammer]

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]

Thanks!

[Jeremy Avigad]

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]

@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_searchfigure 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]

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]

@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]

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]

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]

This isn't true anymore:

import tactic.core

example (P : Prop) : true :=
begin
  by_cases P,
  trivial,
  trivial,
end

[Scott Morrison]

(Without the import it doesn't work, however...!)

[Kenny Lau]

how does that work?

[Jalex Stark]

I would guess it just runs classical if it can't find an instance of decidability for P

[Jalex Stark]

I also imagine that's what tauto! does, but I should probably do less imagining and more reading source code

[Jeremy Avigad]

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.