Beginner question, pattern matching

Stream: new members

[Jens Kristian Egsgaard]

Trying to figure out why the following fails, and what i should be doing instead.
I have a goal of n:N and n+nn-nn=n.
I try to use
rw <-nat.mul_sub_left_distrub
But get the error "rewrite tactic failed, did not find instance of the pattern in target expression ?m_1?m_2 - ?m_1?m_3.
I was expecting a match of nn-nn.
Thanks!

[Kevin Buzzard]

I'm not at lean right now. What does #check @nat.mul_sub_left_distrib say?

[Kevin Buzzard]

(outside of tactic mode)

[Kevin Buzzard]

If you use single quotes ` you can quote code. Some of what you wrote got mangled. Was that * symbols? I'm thinking you're applying the wrong lemma

[Kevin Buzzard]

Oh I understand now! n+n*n-n*n=n is your goal. Zulip was garbling stuff and I thought it was the LaTeX issue. Yeah, that's bracketed the wrong way for you.

[Kevin Buzzard]

That's (n + n * n) - n * n so the rewrite can't find it

[Kevin Buzzard]

I would be tempted to just try the simplifier

[Kevin Buzzard]

Import tactic.linarith and then try example (a b : nat) : (a + b) - b = a := by library_search and see if you get lucky

[Kevin Buzzard]

(if the simplifier doesn't do it)

[Mario Carneiro]

There is a lemma for this, use library_search to find it

[Patrick Massot]

One more detail: you need mathlib to get access to library_search, and import tactic at top of your file if you have no import from mathlib at all

[Patrick Massot]

(although the lemma you're looking for is almost certainly in core)

[Jens Kristian Egsgaard]

Thanks for all the suggestions! Sorry about the garbled code. Kevin was spot on with the implicit bracketing being the wrong way around.

[Patrick Massot]

Associativity is tricky for mathematicians because we never think about it. We turn this property into "I can write sums without caring about parentheses", which is not very formalization friendly. But we certainly want Lean to take care of this (and indeed you can prove your goal by simp).

[Jens Kristian Egsgaard]

My main goal was to figure out why it didn't match, as I couldn't find any information about how the matching is performed but i think this enlightened me. Now I'm trying to figure out how to get the right bracketing :)
I cant seem to prove my goal with simp (but I have a proof by exact nat.add_sub_cancel n (n*n))

[Patrick Massot]

It means you didn't import enough of mathlib. The simp attribute is set in https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/basic.lean#L21

[Patrick Massot]

I think almost any mathlib import would be enough to drag this in

[Patrick Massot]

and you really don't want to start using Lean without mathlib

[Kevin Buzzard]

at least not if you're doing maths. The computer scientists will wince when I say this but whenever I start on a new file, if I'm just goofing around, I import tactic.linarith because I know this gives me all the good stuff.

[Jens Kristian Egsgaard]

Thanks Patrick, that definitely explains why simp didn't work, I have yet to bite the bullet and figure out how to install mathlib. I postponed that while trying to figure out how things worked.

[Kevin Buzzard]

Good instructions in the mathlib README. Let us know if there's any problems. You should end up with a fully working Lean and mathlib with everything installed and compiled, if all goes well.

[Jens Kristian Egsgaard]

Thanks! I i think i had success this time, but is not really usable. The autocompletion in vsstudio works when i write (ie it shows all kind of linear algebra stuff that i assume is part of mathlib) import linear_algebra.finsupp but as soon as i finish typing it stalls at updating

[Kevin Buzzard]

It's supposed to say "updating" all the time. Are you sure it's doing something? it might just be ready.

[Kevin Buzzard]

I will be the first to admit that this is not particuarly clear.

[Patrick Massot]

Yes, we'll need to fix that at some point. Many people are confused by this

[Patrick Massot]

And Gabriel could change it very easily

[Kevin Buzzard]

It's the orange bars which indicate that there is a problem. This means your code is compiling (and compiling should be quick if lean and mathlib are all already compiled).

[Jens Kristian Egsgaard]

Ok, that was a bit confusing. For some time the cpu usage was 600%, then it calmed down. Now im left with a red swiggle under import and no output in lean messages. A new panel opened in the bottom telling me i have 1k+ problems. (Lean server errors)

[Patrick Massot]

Then the installation procedure didn't work.

[Kevin Buzzard]

Try restarting Lean -- ctrl-shift-P and then Lean : Restart

[Jens Kristian Egsgaard]

Restarting gave me orange bars, so i guess im compiling now?

[Patrick Massot]

This is not good.

[Patrick Massot]

What is your OS?

[Patrick Massot]

did you follow the instructions at https://github.com/leanprover-community/mathlib/blob/master/README.md?

[Kevin Buzzard]

Your copy of mathlib is pretty much unusable unless you've compiled it.

[Kevin Buzzard]

Did you follow the installation procedure up to and including the update-mathlib part?

[Kevin Buzzard]

orange bars indicate that the import worked but that you have an uncompiled mathlib -- compiling it might be the only step you have left. Alternatively if the bars disappear within around 10-20 seconds then you are OK.

[Kevin Buzzard]

Once you've compiled it, it's trouble-free.

[Jens Kristian Egsgaard]

I followed the instructions, including the update-mathlib. It went quite.fast though, so i suspect no compiling happened. Tried again and it prints 'reusing cached olean archive'

[Patrick Massot]

That's good

[Patrick Massot]

Can you list what is in your project folder?

[Patrick Massot]

The point of update-mathlib is exactly to ensure that no compiling happens on your machine, it fetches precompiled stuff

[Jens Kristian Egsgaard]

_target, leanpkg.[path, toml], src

[Patrick Massot]

Ok, and the Lean file you are editing is in src, right?

[Jens Kristian Egsgaard]

Yes

[Jens Kristian Egsgaard]

Ah okay, i wasnt clear on the role of update-mathlib

[Patrick Massot]

And you told VScode to open the folder whose content you just listed, right (not the src folder)?

[Jens Kristian Egsgaard]

Yes

[Patrick Massot]

Weird. Let's get VScode out of the game. Can you try to run leanpkg build in a terminal in this project folder?

[Patrick Massot]

And tell us if it starts mentioning mathlib files

[Jens Kristian Egsgaard]

It does a.git checkout, then prints lean --make src

[Patrick Massot]

And is it running for a long time here?

[Patrick Massot]

Can you paste the content of your leanpkg.toml?

[Jens Kristian Egsgaard]

No just a second

[Jens Kristian Egsgaard]

[package]
name = "my_project"
version = "0.1"
lean_version = "3.4.2"
path = "src"

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

[Patrick Massot]

Ok, so the VScode extension is misbehaving, but Lean is fine

[Patrick Massot]

Did you change any setting of the VScode extension?

[Jens Kristian Egsgaard]

Wait, i think it might be working now

[Jens Kristian Egsgaard]

Yes, the orange bars are just a second or two now, and now it seems to work as expected!

[Floris van Doorn]

I sometimes have to restart VScode to make it behave well (in certain cases even Lean: Restart Server doesn't work properly). Probably something similar is going on here.

[Patrick Massot]

Even when everything works as expected, it's painful...