Stream: new members

Topic: Beginner question, pattern matching

Jens Kristian Egsgaard (Sep 20 2019 at 10:59):

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 (Sep 20 2019 at 11:03):

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

Kevin Buzzard (Sep 20 2019 at 11:03):

(outside of tactic mode)

Kevin Buzzard (Sep 20 2019 at 11:05):

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 (Sep 20 2019 at 11:08):

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 (Sep 20 2019 at 11:08):

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

Kevin Buzzard (Sep 20 2019 at 11:09):

I would be tempted to just try the simplifier

Kevin Buzzard (Sep 20 2019 at 11:12):

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 (Sep 20 2019 at 11:12):

(if the simplifier doesn't do it)

Mario Carneiro (Sep 20 2019 at 11:20):

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

Patrick Massot (Sep 20 2019 at 11:23):

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 (Sep 20 2019 at 11:23):

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

Jens Kristian Egsgaard (Sep 20 2019 at 11:33):

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 (Sep 20 2019 at 11:40):

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 (Sep 20 2019 at 11:48):

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 (Sep 20 2019 at 11:58):

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 (Sep 20 2019 at 11:59):

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

Patrick Massot (Sep 20 2019 at 11:59):

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

Kevin Buzzard (Sep 20 2019 at 13:30):

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 (Sep 20 2019 at 13:58):

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 (Sep 20 2019 at 13:59):

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 (Sep 20 2019 at 14:25):

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 (Sep 20 2019 at 14:26):

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

Kevin Buzzard (Sep 20 2019 at 14:26):

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

Patrick Massot (Sep 20 2019 at 14:26):

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

Patrick Massot (Sep 20 2019 at 14:27):

And Gabriel could change it very easily

Kevin Buzzard (Sep 20 2019 at 14:27):

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 (Sep 20 2019 at 14:34):

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 (Sep 20 2019 at 14:34):

Then the installation procedure didn't work.

Kevin Buzzard (Sep 20 2019 at 14:34):

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

Jens Kristian Egsgaard (Sep 20 2019 at 14:36):

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

Patrick Massot (Sep 20 2019 at 14:37):

This is not good.

Kevin Buzzard (Sep 20 2019 at 14:39):

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

Kevin Buzzard (Sep 20 2019 at 14:39):

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

Kevin Buzzard (Sep 20 2019 at 14:39):

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 (Sep 20 2019 at 14:39):

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

Jens Kristian Egsgaard (Sep 20 2019 at 14:45):

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'

That's good

Patrick Massot (Sep 20 2019 at 14:46):

Can you list what is in your project folder?

Patrick Massot (Sep 20 2019 at 14:46):

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

Jens Kristian Egsgaard (Sep 20 2019 at 14:47):

_target, leanpkg.[path, toml], src

Patrick Massot (Sep 20 2019 at 14:48):

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

Yes

Jens Kristian Egsgaard (Sep 20 2019 at 14:48):

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

Patrick Massot (Sep 20 2019 at 14:48):

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

Yes

Patrick Massot (Sep 20 2019 at 14:49):

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 (Sep 20 2019 at 14:49):

And tell us if it starts mentioning mathlib files

Jens Kristian Egsgaard (Sep 20 2019 at 14:52):

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

Patrick Massot (Sep 20 2019 at 14:52):

And is it running for a long time here?

Patrick Massot (Sep 20 2019 at 14:52):

Can you paste the content of your leanpkg.toml?

No just a second

Jens Kristian Egsgaard (Sep 20 2019 at 14:56):

[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 (Sep 20 2019 at 14:57):

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

Patrick Massot (Sep 20 2019 at 14:57):

Did you change any setting of the VScode extension?

Jens Kristian Egsgaard (Sep 20 2019 at 15:00):

Wait, i think it might be working now

Jens Kristian Egsgaard (Sep 20 2019 at 15:03):

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

Floris van Doorn (Sep 20 2019 at 15:05):

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 (Sep 20 2019 at 15:11):

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

Last updated: May 09 2021 at 19:11 UTC