Zulip Chat Archive

Stream: new members

Topic: polynomial simplification?


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

view this post on Zulip Alex J. Best (Sep 25 2020 at 16:39):

tactic#ring is probably what you want

view this post on Zulip Kevin Lacker (Sep 25 2020 at 16:41):

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

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

view this post on Zulip Alex J. Best (Sep 25 2020 at 16:52):

For that we have tactic#lift now!

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 16:57):

thanks

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 17:59):

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

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

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

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:28):

i still don't get that example honeslty

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

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

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:36):

and i want to prove it for natural numbers

view this post on Zulip Paul van Wamelen (Sep 25 2020 at 18:36):

In the example norm_cast gets rid of the s.

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

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

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

view this post on Zulip Paul van Wamelen (Sep 25 2020 at 18:37):

OMG! You are missing out! :)

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:38):

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:38):

and not existent in the emacs lean mode?

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 18:38):

sure it exists

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:39):

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:39):

you guys all use vscode?

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

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 18:39):

It's called something else in emacs then, probably

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:40):

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

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

view this post on Zulip Alex J. Best (Sep 25 2020 at 18:41):

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:42):

the "goal window" = the "infoview" ?

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 18:57):

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 18:57):

where do you see that

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 18:57):

I had to search github a bit.

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:01):

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:01):

leanproject up still leaves me using 2.14

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:01):

3.14

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:05):

well, that seems to have worked

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:05):

Either format is fine.

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:09):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:09):

Did you restart Lean since you ran leanproject up?

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:10):

yep

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:11):

i guess i should try totally uninstalling and reinstalling

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:11):

What was the output when you ran leanproject up?

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:11):

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:12):

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

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

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

view this post on Zulip Yakov Pechersky (Sep 25 2020 at 19:14):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:14):

And you ran leanproject up in the hellolean directory?

view this post on Zulip Yakov Pechersky (Sep 25 2020 at 19:14):

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:14):

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:15):

sounds like i should just delete it all and reinstall

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:19):

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

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:25):

there isn't any directory named hellolean

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

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:26):

How did you create the hellolean project?

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:26):

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

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 19:26):

You should only be creating projects with leanproject.

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

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:29):

yeah because it's already in a larger git repo

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

view this post on Zulip Kevin Lacker (Sep 25 2020 at 19:31):

it seems like it's working now though

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

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

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

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