Zulip Chat Archive

Stream: new members

Topic: Beginner question, pattern matching


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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 11:03):

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 11:03):

(outside of tactic mode)

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

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 11:08):

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 11:09):

I would be tempted to just try the simplifier

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 11:12):

(if the simplifier doesn't do it)

view this post on Zulip Mario Carneiro (Sep 20 2019 at 11:20):

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

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:23):

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

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

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

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

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:59):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:59):

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 14:26):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:26):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:27):

And Gabriel could change it very easily

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

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:34):

Then the installation procedure didn't work.

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 14:34):

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

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:36):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:37):

This is not good.

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:37):

What is your OS?

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:38):

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 14:39):

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 14:39):

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

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

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 14:39):

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

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:45):

That's good

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:46):

Can you list what is in your project folder?

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

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:47):

_target, leanpkg.[path, toml], src

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:48):

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

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:48):

Yes

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:48):

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

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

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:48):

Yes

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:49):

And tell us if it starts mentioning mathlib files

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:52):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:52):

And is it running for a long time here?

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:52):

Can you paste the content of your leanpkg.toml?

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 14:53):

No just a second

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:57):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 14:57):

Did you change any setting of the VScode extension?

view this post on Zulip Jens Kristian Egsgaard (Sep 20 2019 at 15:00):

Wait, i think it might be working now

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

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

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