int lemma changes between 3.12 and 3.13

Stream: new members

[Sam Estep]

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?

[Shing Tak Lam]

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.

[Kevin Buzzard]

Did they get moved into mathlib?

[Shing Tak Lam]

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

[Sam Estep]

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

[Shing Tak Lam]

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

[Shing Tak Lam]

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.

[Sam Estep]

@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'"

[Kevin Buzzard]

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

[Sam Estep]

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

[Sam Estep]

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

[Sam Estep]

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

[Patrick Massot]

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

[Patrick Massot]

You may have had conflicting lean and olean files.

[Sam Estep]

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

[Sam Estep]

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?

[Patrick Massot]

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

[Patrick Massot]

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

[Sam Estep]

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)

[Kevin Buzzard]

(deleted)