Zulip Chat Archive

Stream: maths

Topic: defeq of reals


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 03 2020 at 10:10):

all three should work?

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 10:11):

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

view this post on Zulip Chris Hughes (Jul 03 2020 at 10:11):

The final one

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 10:11):

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

view this post on Zulip Chris Hughes (Jul 03 2020 at 10:12):

Because 4 is bit0 2

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Jul 03 2020 at 10:12):

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

view this post on Zulip Kenny Lau (Jul 03 2020 at 10:12):

but rfl still works with irreducible right

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 10:12):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 10:14):

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

view this post on Zulip 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