defeq of reals

Stream: maths

[Kevin Buzzard]

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]

all three should work?

[Kevin Buzzard]

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

[Chris Hughes]

The final one

[Kevin Buzzard]

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

[Chris Hughes]

Because 4 is bit0 2

[Kenny Lau]

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]

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

[Kenny Lau]

but rfl still works with irreducible right

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Rob Lewis]

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