## Stream: maths

### Topic: defeq of reals

#### Kevin Buzzard (Jul 03 2020 at 10:09):

No cheating and firing up Lean, now!

import data.real.basic

example : (2 : ℝ) + 0 = 2 := rfl
example : (0 : ℝ) + 2 = 2 := rfl
example : (2 : ℝ) + 2 = 4 := rfl


Which of these proofs do you think works? (a) 2 + 0 = 2, (b) 0 + 2 = 2 and (c) 2 + 2 = 4. I'm not asserting that precisely one works. I will tell you that at least one works though.

#### Kenny Lau (Jul 03 2020 at 10:10):

all three should work?

#### Kevin Buzzard (Jul 03 2020 at 10:11):

Whether or not they work is an implementation issue. They do not all work.

The final one

#### Kevin Buzzard (Jul 03 2020 at 10:11):

0 is broken for some reason. Positive integers are rfling fine.

#### Chris Hughes (Jul 03 2020 at 10:12):

Because 4 is bit0 2

#### Kenny Lau (Jul 03 2020 at 10:12):

the final one obviously works, but I'm wondering whether 2+0 would correspond to the Cauchy sequence fun n, (2+0 : \Q) and would therefore be defeq to fun n, (2 : \Q)

#### Chris Hughes (Jul 03 2020 at 10:12):

And the reals are irreducible now so the other two don't work.

#### Kenny Lau (Jul 03 2020 at 10:12):

but rfl still works with irreducible right

#### Kevin Buzzard (Jul 03 2020 at 10:12):

4 + 1 = 5 works and 1 + 4 = 5 doesn't.

#### Chris Hughes (Jul 03 2020 at 10:14):

There's some funny way of getting rfl to work with irreducible via tactic.add_decl or something like that.

#### Kevin Buzzard (Jul 03 2020 at 10:14):

0 + 0 = 0 isn't rfl (for real obviously: works fine for rat)

#### Rob Lewis (Jul 03 2020 at 10:17):

Chris is exactly right. The only reason rfl will work for you on real numerals is when the numerals unfold to the same sum of 0 and 1. You can change some reducibility settings to make more work.

import data.real.basic

local attribute [semireducible] real real.comm_ring_aux

example : (0 : ℝ) + 0 = 0 := rfl

example : (1 : ℝ) + 4 = 5 := rfl


Last updated: May 18 2021 at 07:19 UTC