Zulip Chat Archive

Stream: maths

Topic: Arithmetic Basics in Lean


view this post on Zulip Nicholas McConnell (Feb 12 2020 at 16:31):

def even (n : ) : Prop :=  k, n = 2*k
def odd (n : ) : Prop :=  k, n = 2*k+1

lemma luckyseven : odd 7 :=
begin
rw odd,
existsi 3,

end

"existsi 3," takes the goal to 7 = 2*3+1, but I'm not sure how to get it to evaluate the expression

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:32):

7=2*3+1 is true by definition so you can finish the proof with refl

view this post on Zulip Nicholas McConnell (Feb 12 2020 at 16:32):

Okay thanks

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:33):

If you put ```lean above your code and ``` under it, you'll get syntax highlighting etc.

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:34):

If you use mathlib and write import tactic at the top of your code, you can use the slightly less bizarrely named use tactic: use 3 does the same as existsi 3.

view this post on Zulip Nicholas McConnell (Feb 12 2020 at 16:34):

1 goal
d k : ,
q : d = 2 * k + 1
 nat.succ d = 2 * (k + 1)

I'm also not sure how to deal with this goal, specifically how to distribute the multiplication over the addition at the start

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:35):

Big question: do you just want to destroy this quickly with a tactic which proves all such equalities in general rings, or do you want to do all the steps by yourself?

view this post on Zulip Nicholas McConnell (Feb 12 2020 at 16:35):

Either of these seems fine to me

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:36):

If the former, then rw q, ring (assuming you have mathlib tactics imported)

view this post on Zulip Nicholas McConnell (Feb 12 2020 at 16:36):

"import tactic" didn't work for me

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:36):

if the latter, then rw mul_add is what you need to apply the distributivity. It's also called left_distrib or something, but mul_add is easier to remember.

view this post on Zulip Nicholas McConnell (Feb 12 2020 at 16:37):

Alright thanks

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:37):

import tactic not working just means that you don't have Lean's maths library set up to work with your project.

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:39):

https://github.com/leanprover-community/mathlib#installation and then download the sample project and make a new file in it with your Lean code and it will work. Alternatively use the online editor

view this post on Zulip Kevin Buzzard (Feb 12 2020 at 16:40):

The natural number game teaches you stuff like mul_add (disclaimer: I was involved in writing it)


Last updated: May 19 2021 at 03:22 UTC