Zulip Chat Archive

Stream: new members

Topic: MIL comments


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 06:29):

Thanks!

view this post on Zulip 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.

view this post on Zulip 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_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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 28 2020 at 09:52):

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

view this post on Zulip Kenny Lau (Jul 28 2020 at 09:57):

how does that work?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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