simplify nat-semiring

Stream: new members

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(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)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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.

[Thorsten Altenkirch]

file 'tactic' not found in the LEAN_PATH

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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

[Patrick Massot]

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

[Patrick Massot]

This is the only entry point you need.

[Patrick Massot]

Everything else is an unfortunate historical accident.

[Kevin Buzzard]

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.

[Thorsten Altenkirch]

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

[Patrick Massot]

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

[Thorsten Altenkirch]

And now? It is no installer.

[Thorsten Altenkirch]

I guess I have to run trylean?

[Thorsten Altenkirch]

Unter Darwin. It doesn't say OS X.

[Patrick Massot]

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.

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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.

[Thorsten Altenkirch]

I am using emacs.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Thorsten Altenkirch]

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".

[Thorsten Altenkirch]

macOS 10.15.5 (19F101

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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