Zulip Chat Archive

Stream: new members

Topic: int lemma changes between 3.12 and 3.13


view this post on Zulip Sam Estep (Aug 06 2020 at 05:27):

Continuing to work through TPiL, section 4.2 lists a bunch of int lemmas that all seem to be recognized just fine in 3.12.0, but these ones aren't recognized as of 3.13.0:

[add_zero, zero_add, mul_one, one_mul, neg_add_self, add_neg_self, sub_self, add_comm, add_assoc, mul_comm, mul_assoc, mul_add, left_distrib, add_mul, right_distrib, mul_sub, sub_mul]

From the changelog it seems like this is due to #229, but I can't find mention of some of those lemmas (such as neg_add_self) in the diff for that PR... in any case, prefacing all the lemma names with int. doesn't fix that example in 3.13.0; what other changes are needed for this example?

view this post on Zulip Shing Tak Lam (Aug 06 2020 at 05:36):

What I've found so far

variables a b c d : 

example : a + 0 = a := int.add_zero a
example : 0 + a = a := int.zero_add a
example : a * 1 = a := int.mul_one a
example : 1 * a = a := int.one_mul a
example : a - a = 0 := int.sub_self a
example : a + b = b + a := int.add_comm a b
example : a + b + c = a + (b + c) := int.add_assoc a b c
example : a * b = b * a := int.mul_comm a b
example : a * b * c = a * (b * c) := int.mul_assoc a b c
example : a * (b - c) = a * b - a * c := int.mul_sub a b c
example : (a - b) * c = a * c - b * c := int.sub_mul a b c

/- Errors -/

-- these would come from the `add_group ℤ` instance (which comes from the `comm_ring ℤ` instance)

example : -a + a = 0 := neg_add_self a
example : a + -a = 0 := add_neg_self a

example : -a + a = 0 := int.add_left_neg a -- the one used in the `comm_ring ℤ` instance

-- these would come from `distrib ℤ` (which comes from the `comm_ring ℤ` instance)
example : a * (b + c) = a * b + a * c := mul_add a b c
example : a * (b + c) = a * b + a * c := left_distrib a b c
example : (a + b) * c = a * c + b * c := add_mul a b c
example : (a + b) * c = a * c + b * c := right_distrib a b c

-- alternatives used in the instance `comm_ring ℤ`
example : a * (b + c) = a * b + a * c := int.distrib_left a b c
example : (a + b) * c = a * c + b * c := int.distrib_right a b c

So most of them are there in one way or another. What remains is

  • add_neg_self - Not a group axiom in mathlib, since it can be proven from the others. Which is probably why there isn't an int. version
  • mul_add,add_mul, left_distrib and right_distrib are names from distrib, but there are similar ones from int.

view this post on Zulip Kevin Buzzard (Aug 06 2020 at 06:04):

Did they get moved into mathlib?

view this post on Zulip Shing Tak Lam (Aug 06 2020 at 06:05):

Yeah. If you import data.int.basic you get all of them and the original example works.

view this post on Zulip Sam Estep (Aug 08 2020 at 20:25):

@Shing Tak Lam Cool, thanks! That seems to mostly work; but mul_add, add_mul, mul_sub, and sub_mul seem to still be absent (same for after importing data.nat.basic in the example at the beginning of TPiL section 6.2)

view this post on Zulip Shing Tak Lam (Aug 09 2020 at 04:58):

@Sam Estep

I think Jeremy switched TPIL's examples (and testing) to use the community web editor, which has mathlib available. Those lemmas are present if your import mathlib, so all the examples compile fine now.

view this post on Zulip Shing Tak Lam (Aug 09 2020 at 05:00):

Although TPiL probably now needs to have a paragraph talking about community lean, and the links for installation should probably go to leanprover-community and not leanprover.

view this post on Zulip Sam Estep (Aug 09 2020 at 18:24):

@Shing Tak Lam That would make sense... but I thought that I already have mathlib installed for my local project? For instance I have this in my leanpkg.toml file:

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "b5baf5559ec648925d987c932bde47ebc7df87c9"}

And when I hover over the import data.nat.basic in my file it says this:

imported file '/home/sam/sandbox/my_project/_target/deps/mathlib/src/data/nat/basic.lean' uses sorry

so it seems like it's already present, but I'm still getting "unknown identifier 'add_mul'"

view this post on Zulip Kevin Buzzard (Aug 09 2020 at 22:19):

Remove all oleans in project and use leanproject to get new ones? You shouldn't have any errors at all in mathlib files

view this post on Zulip Sam Estep (Aug 09 2020 at 22:58):

@Kevin Buzzard I think my local setup might have gotten messed up when I upgraded from Ubuntu 18.04 to 20.04 the other day... I'm trying what you mentioned by starting a new project:

$ leanproject new my_project
Traceback (most recent call last):
  File "/home/sam/.local/bin/leanproject", line 7, in <module>
    from mathlibtools.leanproject import safe_cli
ModuleNotFoundError: No module named 'mathlibtools'

The issue seems to persist even after following these instructions (including the pipx install mathlibtools at the bottom)

view this post on Zulip Sam Estep (Aug 09 2020 at 23:17):

Hmm weird, I was able to resolve the pipx issue by replacing it with python3 -m pip install mathlibtools

view this post on Zulip Sam Estep (Aug 09 2020 at 23:19):

That fixed it @Kevin Buzzard! I must have just had an outdated mathlib version (I guess commit b5baf5559ec648925d987c932bde47ebc7df87c9 used sorry in data.nat.basic?)

view this post on Zulip Patrick Massot (Aug 09 2020 at 23:20):

No, we don't have commits using sorry in mathlib.

view this post on Zulip Patrick Massot (Aug 09 2020 at 23:21):

You may have had conflicting lean and olean files.

view this post on Zulip Sam Estep (Aug 09 2020 at 23:25):

So regarding what Shing Tik Lam mentioned about TPiL using mathlib, is there a way I can import mathlib in such a way as to get make leantest to pass? It looks like it's not finding mathlib currently:

/home/sam/github/leanprover/theorem_proving_in_lean/_build/leantest/quantifiers_and_equality_51.lean:1:0: error: file 'data/real/basic' not found in the search path

view this post on Zulip Sam Estep (Aug 09 2020 at 23:36):

Ah apparently I can just do leanproject new in the theorem_proving_in_lean directory; is that how one is meant to do it? Or is there a way to install mathlib globally?

view this post on Zulip Patrick Massot (Aug 10 2020 at 01:13):

https://leanprover-community.github.io/leanproject.html#global-mathlib-install

view this post on Zulip Patrick Massot (Aug 10 2020 at 01:13):

But the real answer is that TPIL was not designed to use mathlib.

view this post on Zulip Sam Estep (Aug 10 2020 at 01:58):

Patrick Massot said:

But the real answer is that TPIL was not designed to use mathlib.

Sure, that makes sense; I was just intrigued once I figured out that there was a way to make all the tests pass with the recent update of TPiL to Lean 3.18.4, since it seemed exceedingly unlikely that Jeremy was able to achieve that without being able to run them all as a batch (so I assume he uses leanproject global-install since there is no leanproject in TPiL)

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:11):

(deleted)


Last updated: May 12 2021 at 23:13 UTC