## Stream: new members

### Topic: polynomial simplification?

#### Kevin Lacker (Sep 25 2020 at 16:34):

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 (Sep 25 2020 at 16:39):

tactic#ring is probably what you want

#### Kevin Lacker (Sep 25 2020 at 16:41):

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

#### Kevin Lacker (Sep 25 2020 at 16:48):

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 (Sep 25 2020 at 16:52):

For that we have tactic#lift now!

#### Kevin Lacker (Sep 25 2020 at 16:54):

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 (Sep 25 2020 at 16:57):

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

thanks

#### Bryan Gin-ge Chen (Sep 25 2020 at 17:59):

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

#### Kevin Lacker (Sep 25 2020 at 18:19):

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 (Sep 25 2020 at 18:19):

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 (Sep 25 2020 at 18:20):

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

#### Paul van Wamelen (Sep 25 2020 at 18:24):

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 (Sep 25 2020 at 18:28):

i still don't get that example honeslty

#### Kevin Lacker (Sep 25 2020 at 18:30):

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

#### Paul van Wamelen (Sep 25 2020 at 18:34):

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 (Sep 25 2020 at 18:35):

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 (Sep 25 2020 at 18:35):

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 (Sep 25 2020 at 18:36):

and i want to prove it for natural numbers

#### Paul van Wamelen (Sep 25 2020 at 18:36):

In the example norm_cast gets rid of the ↑s.

#### Kevin Buzzard (Sep 25 2020 at 18:36):

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 (Sep 25 2020 at 18:36):

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

#### Kevin Lacker (Sep 25 2020 at 18:36):

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

#### Paul van Wamelen (Sep 25 2020 at 18:37):

OMG! You are missing out! :)

#### Kevin Lacker (Sep 25 2020 at 18:38):

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

#### Kevin Lacker (Sep 25 2020 at 18:38):

and not existent in the emacs lean mode?

sure it exists

#### Kevin Buzzard (Sep 25 2020 at 18:38):

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 (Sep 25 2020 at 18:39):

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

#### Kevin Lacker (Sep 25 2020 at 18:39):

you guys all use vscode?

#### Paul van Wamelen (Sep 25 2020 at 18:39):

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

#### Kevin Buzzard (Sep 25 2020 at 18:39):

It's called something else in emacs then, probably

#### Kevin Lacker (Sep 25 2020 at 18:40):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 18:40):

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

#### Alex J. Best (Sep 25 2020 at 18:41):

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

#### Jesse Selover (Sep 25 2020 at 18:42):

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

#### Kevin Lacker (Sep 25 2020 at 18:42):

the "goal window" = the "infoview" ?

#### Jesse Selover (Sep 25 2020 at 18:43):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 18:44):

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 (Sep 25 2020 at 18:45):

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 (Sep 25 2020 at 18:48):

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 (Sep 25 2020 at 18:50):

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 (Sep 25 2020 at 18:50):

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 (Sep 25 2020 at 18:50):

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

#### Alex J. Best (Sep 25 2020 at 18:53):

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 (Sep 25 2020 at 18:55):

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 (Sep 25 2020 at 18:55):

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 (Sep 25 2020 at 18:57):

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

#### Kevin Lacker (Sep 25 2020 at 18:57):

where do you see that

#### Bryan Gin-ge Chen (Sep 25 2020 at 18:57):

I had to search github a bit.

#### Bryan Gin-ge Chen (Sep 25 2020 at 18:58):

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 (Sep 25 2020 at 19:00):

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 (Sep 25 2020 at 19:01):

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

#### Kevin Lacker (Sep 25 2020 at 19:01):

leanproject up still leaves me using 2.14

3.14

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:03):

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 (Sep 25 2020 at 19:04):

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 (Sep 25 2020 at 19:05):

well, that seems to have worked

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:05):

Either format is fine.

#### Kevin Lacker (Sep 25 2020 at 19:09):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:09):

Did you restart Lean since you ran leanproject up?

yep

#### Kevin Lacker (Sep 25 2020 at 19:11):

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 (Sep 25 2020 at 19:11):

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 (Sep 25 2020 at 19:11):

i guess i should try totally uninstalling and reinstalling

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:11):

What was the output when you ran leanproject up?

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:11):

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

#### Kevin Lacker (Sep 25 2020 at 19:11):

\$ 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 (Sep 25 2020 at 19:12):

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

#### Kevin Lacker (Sep 25 2020 at 19:12):

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

#### Kevin Lacker (Sep 25 2020 at 19:13):

[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 (Sep 25 2020 at 19:14):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:14):

And you ran leanproject up in the hellolean directory?

#### Yakov Pechersky (Sep 25 2020 at 19:14):

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

#### Kevin Lacker (Sep 25 2020 at 19:14):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:14):

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

#### Kevin Lacker (Sep 25 2020 at 19:15):

sounds like i should just delete it all and reinstall

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:16):

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 (Sep 25 2020 at 19:19):

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

#### Kevin Lacker (Sep 25 2020 at 19:20):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:24):

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 (Sep 25 2020 at 19:25):

there isn't any directory named hellolean

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:25):

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

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:26):

How did you create the hellolean project?

#### Kevin Lacker (Sep 25 2020 at 19:26):

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 (Sep 25 2020 at 19:26):

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

#### Kevin Buzzard (Sep 25 2020 at 19:26):

You should only be creating projects with leanproject.

#### Kevin Lacker (Sep 25 2020 at 19:27):

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 (Sep 25 2020 at 19:29):

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 (Sep 25 2020 at 19:29):

yeah because it's already in a larger git repo

#### Kevin Lacker (Sep 25 2020 at 19:30):

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 (Sep 25 2020 at 19:31):

it seems like it's working now though

#### Bryan Gin-ge Chen (Sep 25 2020 at 19:31):

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 (Sep 25 2020 at 19:35):

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 (Sep 25 2020 at 19:36):

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

#### Scott Morrison (Sep 26 2020 at 01:49):

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.

Last updated: May 13 2021 at 18:26 UTC