Arithmetic Basics in Lean

Stream: maths

[Nicholas McConnell]

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

[Kevin Buzzard]

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

[Nicholas McConnell]

Okay thanks

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Nicholas McConnell]

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

[Kevin Buzzard]

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?

[Nicholas McConnell]

Either of these seems fine to me

[Kevin Buzzard]

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

[Nicholas McConnell]

"import tactic" didn't work for me

[Kevin Buzzard]

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.

[Nicholas McConnell]

Alright thanks

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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