polynomial simplification?

Stream: new members

[Kevin Lacker]

Can I get Lean to simplify a polynomial for me without me doing a bunch of comm, distrib etc steps? For example, to prove (n^2 + 2 * m^2 - 2 * n * m) * (n^2 + 2 * m^2 + 2 * n * m) = n^4 + 4 * m ^ 4 which is just standard multiplying out the polynomials and canceling terms

[Alex J. Best]

tactic#ring is probably what you want

[Kevin Lacker]

oh cool - i had imported algebra.ring not tactic.ring

[Kevin Lacker]

similar question maybe - is there any library that corresponds integer arithmetic with natural number arithmetic? like if i know a+b=c with integers, and they're all positive, and i want to conclude a+b=c with natural numbers

[Alex J. Best]

For that we have tactic#lift now!

[Kevin Lacker]

nice. is there any example of that in code? the docs say... Usage: 'lift' expr 'to' expr ('using' expr)? ('with' id (id id?)?)?. which, i feel like that is using some sort of non-lean notation

[Alex J. Best]

I don't know of any examples, but you can check out the test file at https://github.com/leanprover-community/mathlib/blob/680f877108074901a88bcb5b7cf595f2c7951448/test/tactics.lean#L214
if you delete the lines that don't start with lift that should give you an example

[Kevin Lacker]

thanks

[Bryan Gin-ge Chen]

Adding examples to the tactic doc entry would make a great PR...

[Kevin Lacker]

i gave up on using this tactic, for what it's worth. maybe I don't really get how to use tactics in general - if I happen to write a large sequence of tactics that works, it's great, but i can't really figure out how to debug or to see the partial state of what's going on when i'm partway through writing some sequence

[Kevin Lacker]

whereas, if i'm not using tactics but just writing a bunch of have h, from blah blah, statements, at least then I can see if each one is valid

[Kevin Lacker]

i feel like if i use a tactic and it works immediately, great, and otherwise i am just stumped

[Paul van Wamelen]

Did you give up on the lift tactic?
Here is a simple example

lemma pos_le_mul_self (b : ℤ) (h2 : 0 ≤ b) : b ≤ b ^ 2 :=
begin
  rw pow_two,
  lift b to ℕ using h2,
  norm_cast, apply nat.le_mul_self
end

grepping mathlib should give you plenty more...

[Kevin Lacker]

i still don't get that example honeslty

[Kevin Lacker]

i have to look up norm_cast. but, i don't see any examples of that in the docs either

[Paul van Wamelen]

It changes the the type of b to ℕ (it can, because you tell it that 0 ≤ b) and changes all occurrences of b to ↑b (meaning the coercion of b from ℕ to ℤ) in your proof state.

[Alex J. Best]

Kevin Lacker said:

similar question maybe - is there any library that corresponds integer arithmetic with natural number arithmetic? like if i know a+b=c with integers, and they're all positive, and i want to conclude a+b=c with natural numbers

Can you give an (incomplete) lean statement you'd like to prove along these lines, like are you working on some actual proof where this sort of thing is an intermediate step? It might be useful to see this to recommend a course of action.

[Kevin Lacker]

sure. i have (n^2 + 2 * m^2 - 2 * n * m) * (n^2 + 2 * m^2 + 2 * n * m) = n^4 + 4 * m ^ 4 for integers

[Kevin Lacker]

and i want to prove it for natural numbers

[Paul van Wamelen]

In the example norm_cast gets rid of the ↑s.

[Kevin Buzzard]

Kevin Lacker said:

i gave up on using this tactic, for what it's worth. maybe I don't really get how to use tactics in general - if I happen to write a large sequence of tactics that works, it's great, but i can't really figure out how to debug or to see the partial state of what's going on when i'm partway through writing some sequence

You do have the info-view open, right? (thing on the right explaining what the goal and local context is)
infoview.png

[Kevin Lacker]

the part I don't get is how i can apply one norm cast to a statement and see what it outputs

[Kevin Lacker]

ah this seems key. no, I don't have an info-view, I am just writing code in emacs

[Paul van Wamelen]

OMG! You are missing out! :)

[Kevin Lacker]

is the info view basically just necessary to have this work sanely at all

[Kevin Lacker]

and not existent in the emacs lean mode?

[Kevin Buzzard]

sure it exists

[Kevin Buzzard]

if you've set up Lean in emacs properly; the problem is that barely anyone uses emacs so you'll wait longer for answers

[Kevin Lacker]

i don't see "info view" referenced in https://github.com/leanprover/lean-mode

[Kevin Lacker]

you guys all use vscode?

[Paul van Wamelen]

Not really, but it would be a miracle if you could make progress without the infoview!

[Kevin Buzzard]

It's called something else in emacs then, probably

[Kevin Lacker]

well, it makes sense why tactics seemed pretty hard to use, to me

[Bryan Gin-ge Chen]

There's a goal buffer and a lean info buffer I think. (I'm not actually an emacs user myself either).

[Alex J. Best]

Probably 80%-90% of us use vscode? But there are definitely users of emacs too.

[Jesse Selover]

I think if you use lean-mode in emacs the key to bring up the goal window is C-c C-g

[Kevin Lacker]

the "goal window" = the "infoview" ?

[Jesse Selover]

It shows the tactic state at least, not sure about the other parts of the infoview (i'm new myself)

[Bryan Gin-ge Chen]

Yeah, I think the vscode infoview combines the info in the goal buffer and the Lean info buffer.

Yury and Anne's videos in the LFTCM2020 playlist show them using Lean in emacs.

[Kevin Lacker]

is there anywhere in the lean docs that describes the "infoview" or "goal buffer" and what you use it for? like i don't see anythign on https://leanprover.github.io/reference/tactics.html

[Alex J. Best]

Going back to your question, here is a proof using a bunch of tactics:

lemma int_version (n m : ℤ) : (n^2 + 2 * m^2 - 2 * n * m) * (n^2 + 2 * m^2 + 2 * n * m) = n^4 + 4 * m ^ 4 := by ring
example (n m : ℕ) : (n^2 + 2 * m^2 - 2 * n * m) * (n^2 + 2 * m^2 + 2 * n * m) = n^4 + 4 * m ^ 4 := begin
  zify, -- change to a statement about integers as much as possible
  rw ← int_version, -- use the integer version
  congr, -- focus the part of the two expressions that actually differs
  norm_cast, -- normalizes the casts, but you could delete this line in fact
  refine int.of_nat_sub _, -- typing "suggest" told me this was a good lemma to use
  nlinarith, -- we have  a problem with non-linear inequalitites
end

[Kevin Lacker]

ok. and so if you'll bear with even more noobish questions, zify, norm_cast, and nlinarith are things you use enough to just know what they are off the top of your head? or did some system suggest those

[Bryan Gin-ge Chen]

The tactics chapter of Theorem proving in Lean has some info: https://leanprover.github.io/theorem_proving_in_lean/tactics.html#tactics

[Alex J. Best]

They are things I use enough to remember, but these are a good portion of the really common ones.

[Alex J. Best]

Have you seen the tactic cheat sheet? https://leanprover-community.github.io//img/lean-tactics.pdf it doesn't have all of the ones I mentioned, but it has a lot less than the tactic page I linked to before.

[Alex J. Best]

But just asking questions like you're doing is really the best way to learn which tactics are useful for the goals you are proving (like zify was really designed for exactly the sort of problems you're dealing with here), so don't worry about asking questions!

[Kevin Lacker]

great. more questions then. "import tactic.zify" doesn't work for me, in lean 3.14. am i importing it wrong or might something else be going on?

[Bryan Gin-ge Chen]

It looks like zify was added when mathlib was using 3.16.2.

[Kevin Lacker]

where do you see that

[Bryan Gin-ge Chen]

I had to search github a bit.

[Bryan Gin-ge Chen]

Is there a reason you're using 3.14 instead of a newer version of Lean? leanproject up should update your Lean and mathlib to the latest.

[Bryan Gin-ge Chen]

You do bring up a good point which is that the docs are only valid for mathlib master. Maybe at some point we should save versions of the docs for the commits of mathlib that correspond to older versions of Lean.

[Kevin Lacker]

i did an elan update, but that apparently does not update the lean version

[Kevin Lacker]

leanproject up still leaves me using 2.14

[Kevin Lacker]

3.14

[Bryan Gin-ge Chen]

That's weird. I thought leanproject up changed the version of Lean by default, since there's a --no-lean-upgrade option. I'd try editing the lean_version field in leanpkg.toml to 3.20.0 and then trying leanproject up.

[Kevin Lacker]

right now it's set to lean_version = "leanprover-community/lean:3.14.0", should i just change that last bit to a 3.20.0 ?

[Kevin Lacker]

well, that seems to have worked

[Bryan Gin-ge Chen]

Either format is fine.

[Kevin Lacker]

unfortunately, after upgrading, lean appears to be constantly failing with too-much-memory-consumption errors

[Bryan Gin-ge Chen]

Did you restart Lean since you ran leanproject up?

[Kevin Lacker]

yep

[Kevin Lacker]

something seems wrong with this lean installation, it is dying by running out of memory on a file that simply contains "import tactic"

[Bryan Gin-ge Chen]

The memory issue usually happens because Lean is trying to recompile all of mathlib. However, leanproject up is supposed to download a precompiled set of olean files.

[Kevin Lacker]

i guess i should try totally uninstalling and reinstalling

[Bryan Gin-ge Chen]

What was the output when you ran leanproject up?

[Bryan Gin-ge Chen]

I don't think you need to completely uninstall and reinstall yet.

[Kevin Lacker]

$ leanproject up
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying path = "src" are deprecated.
This project does not depend on mathlib

[Bryan Gin-ge Chen]

Hmm... that's very weird. What does your leanpkg.toml look like? And how did you create the Lean project you're working in?

[Bryan Gin-ge Chen]

I'm assuming you read this page in its entirety? https://leanprover-community.github.io/install/project.html

[Kevin Lacker]

yeah, i mean it was all working fine til I upgraded lean to 3.20 just now

[Kevin Lacker]

[package]
name = "hellolean"
version = "0.1"
lean_version = "leanprover-community/lean:3.20.0"
path = "src"

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

[Yakov Pechersky]

After running leanproject up, make sure you restart your Lean interpreter that your editor is using.

[Bryan Gin-ge Chen]

And you ran leanproject up in the hellolean directory?

[Yakov Pechersky]

In VSCode, I do this via a Ctrl-Shift-P command

[Kevin Lacker]

yep, i restarted the editor entirely and killed all processes with "lean" in the name

[Bryan Gin-ge Chen]

I think something went wrong with leanproject since the output that Kevin linked above doesn't make sense.

[Kevin Lacker]

sounds like i should just delete it all and reinstall

[Bryan Gin-ge Chen]

Either you ran leanproject in the wrong directory, or leanproject is having trouble determining what directory it's in. Otherwise why would it think that the package is called _user_local_packages 1?

[Kevin Lacker]

well, clearly it did something, because it turned a functional system into a crashing one

[Kevin Lacker]

reinstalling lean hasn't fixed anything, i'll try creating a new project and seeing if that works

[Bryan Gin-ge Chen]

If you were using the same terminal window that you ran leanproject new hellolean in, did you cd hellolean before running leanproject up? Just making sure...

[Kevin Lacker]

there isn't any directory named hellolean

[Bryan Gin-ge Chen]

Oh, I thought you created hellolean by running leanproject new hellolean or something like that.

[Bryan Gin-ge Chen]

How did you create the hellolean project?

[Kevin Lacker]

I don't remember how I created it. it's possible there's some setup thing that I didn't place how a normal leanproject would, and 3.20 relied on that in some way that 3.14 didn't

[Kevin Lacker]

i'll recreate the project structure and see if that fixes things

[Kevin Buzzard]

You should only be creating projects with leanproject.

[Kevin Lacker]

i notice that it creates a new git repo - i at least had to mess around with the files to make that not happen

[Bryan Gin-ge Chen]

For now, leanproject requires that Lean projects are in git repos. Is there a strong reason you prefer not to initialize a git repo?

[Kevin Lacker]

yeah because it's already in a larger git repo

[Kevin Lacker]

you can't really have a multi-programming-language project if each programming language's tool insists on setting itself up in a new repo

[Kevin Lacker]

it seems like it's working now though

[Bryan Gin-ge Chen]

Ah, right. This is a use case that's been brought up before, but we don't have a satisfactory solution yet, mainly because most of us are just working with pure Lean projects.

[Bryan Gin-ge Chen]

If you can put leanpkg.toml in the root of the larger git repository then things work reasonably well. For instance, this is what we do with doc-gen which is mainly a python project. However, there are some projects where this makes less sense, like Lean itself which has both the core library and leanpkg as separate sub Lean projects.

[Kevin Lacker]

seems easy enough to work around. at any rate, i'm happily on 3.20, thank you for assisting!

[Scott Morrison]

Regarding using leanproject inside a larger git repository: I do this all the time, using git submodule. Assuming the project already exists somewhere (or if it doesn't first create it in a scratch directory using leanproject, then push to github), I just use git submodule add [URL], and then enter that directory and use leanproject like ususal.