Zulip Chat Archive

Stream: new members

Topic: simplify nat-semiring


view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 17:16):

Another beginners question: what is the incantation to tell the simplifier that nat is a smearing but if possible nothing else.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 17:18):

basically I need that 2(x+1) = 2x+2

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 17:18):

but because I am going to use this in my course I don't want any additional cleverness.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:31):

We gave up trying to make the simplifier prove things about semirings and someone wrote a ring tactic instead.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:32):

(BTW you can quote equations involving multiplication by enclosing them in ` quotes, like 2*(x+1)=2*x+2; then Zulip doesn't think it's emphasis). (You can look at the source of what other people post too)

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:34):

Distributivity is apparently what is missing in the simplifier:

import tactic

example (x : ) : 2*(x+1)=2*x+2 := by simp [mul_add]
example (x : ) : 2*(x+1)=2*x+2 := by ring

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 17:37):

Import-free: example (x : ℕ) : 2*(x+1)=2*x+2 := by simp [nat.left_distrib, nat.mul_one]

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

For more control over what lemmas the simplifier uses, it's possible to create a custom simp attribute semiring_simps and then tag all the lemmas you want to use with it. Then you could write simp only with semiring_simps (or define a new tactic semiring_simp that does the same). See mk_simp_attribute.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 18:57):

file 'tactic' not found in the LEAN_PATH

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 18:57):

I accuse you of not following the community installation instructions ;-)

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 18:58):

Dare I ask how you installed Lean and how you're using it?

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 18:58):

yes ring is easier - no problem with this. But you can still use it to solve equations over nat.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 18:59):

brew install lean. I didn't see any installation instructions. Where are they?

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:00):

https://leanprover-community.github.io/

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:00):

This is the only entry point you need.

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:00):

Everything else is an unfortunate historical accident.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 19:01):

I think that after brew install lean you might have an old lean and no mathlib. Mathlib is not just a maths library -- it also has a bunch of tactics.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:01):

I ended up on https://leanprover.github.io/download/ which is useless.

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:02):

No, it isn't. The first link on that page is the one I just gave you.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:02):

And now? It is no installer.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:03):

I guess I have to run trylean?

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:04):

Unter Darwin. It doesn't say OS X.

view this post on Zulip Patrick Massot (Sep 04 2020 at 19:04):

Do you mean a web page is not an installer? Yes, you need to read a couple of sentences. There are various options, with descriptions of target audiences.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:06):

I am not used to reading when installing... Actually that is not true I just know how to install Agda now. :-)

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:08):

And now. Ok I had to convince OSX to run trylean and then vscodium and now I have a vscodium window and I am not sure what to do next.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:08):

I am using emacs.

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

Ah, since (I'm guessing) you've committed to using Lean for more than a few days, I think this link under "regular install" is more suitable than the "trylean" bundle: https://leanprover-community.github.io/install/macos.html

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

I don't think the trylean bundle can be used easily with emacs, unfortunately. Probably we should add a warning.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:13):

Thank you - actually trylean seems to be broken on OSX. You end up starting VSCodium interactively but even if I open a .lean file it says "plain text".

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 19:13):

macOS 10.15.5 (19F101

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

Thanks! I'll try to look into it later this weekend. Let us know if you have any trouble with elan and / or leanproject.

view this post on Zulip Scott Morrison (Sep 05 2020 at 02:01):

(I wonder if we should just ditch the "trylean" bundles...?)

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

This might fix the issue with the macOS bundle: https://github.com/leanprover-community/azure-scripts/pull/5


Last updated: May 08 2021 at 19:11 UTC