## Stream: maths

### Topic: Arithmetic Basics in Lean

#### 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

#### Kevin Buzzard (Feb 12 2020 at 16:32):

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

Okay thanks

#### Kevin Buzzard (Feb 12 2020 at 16:33):

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

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

#### 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

#### 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?

#### Nicholas McConnell (Feb 12 2020 at 16:35):

Either of these seems fine to me

#### Kevin Buzzard (Feb 12 2020 at 16:36):

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

#### Nicholas McConnell (Feb 12 2020 at 16:36):

"import tactic" didn't work for me

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

Alright thanks

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

#### 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

#### 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