# Zulip Chat Archive

## Stream: maths

### Topic: 2 = 2

#### Kevin Buzzard (Apr 05 2020 at 19:02):

import data.polynomial open polynomial set_option profiler true example (R : Type) [comm_ring R] : (2 : polynomial R) = C 2 := begin convert int_cast_eq_C 2; norm_cast, end

Am I missing a trick here? This takes nearly a second to elaborate. `int_cast_eq_C`

says that `n : polynomial R`

equals `C n`

but here `n : int`

and there are casts involved, hence the norm_cast applications at the end. 1 second seems a bit much for something like this.

#### Mario Carneiro (Apr 05 2020 at 19:07):

`simp`

also works, a bit slower (1.6 s) but if you squeeze it it goes down to 460 ms

#### Kevin Buzzard (Apr 05 2020 at 19:08):

`simp`

doesn't work for me :-/

#### Mario Carneiro (Apr 05 2020 at 19:08):

example (R : Type) [comm_ring R] : (2 : polynomial R) = C 2 := begin convert int_cast_eq_C 2; simp only [int.cast_bit0, int.cast_one], end

#### Kevin Buzzard (Apr 05 2020 at 19:09):

oh I see, after the convert. Thanks.

#### Mario Carneiro (Apr 05 2020 at 19:09):

you can also use `rw`

instead of `simp only`

for a little bit faster

#### Kevin Buzzard (Apr 05 2020 at 19:09):

this is a bit more respectable, thanks.

#### Kevin Buzzard (Apr 05 2020 at 19:10):

Of course if one could formalise and prove the general case then this would be great, stick it in mathlib -- but the problem seems to be that this is about numerals rather than ints or nats or whatever

#### Mario Carneiro (Apr 05 2020 at 19:10):

If you print the proof with `pp.all`

you might see why it takes this long

#### Kevin Buzzard (Apr 05 2020 at 19:11):

Slightly ominous that the pp.all output ends with

…) …)) …)) …) …) …)) … … …) …

#### Kevin Buzzard (Apr 05 2020 at 19:11):

I'm proving 2 = 2 for goodness' sake!

#### Kevin Buzzard (Apr 05 2020 at 19:11):

Stupid computer doesn't understand equality properly

#### Mario Carneiro (Apr 05 2020 at 19:12):

I completely agree with you, this is ridiculous

#### Mario Carneiro (Apr 05 2020 at 19:13):

I really need to write that deduplicating printer so I can see the actual size of the term

#### Mario Carneiro (Apr 05 2020 at 19:13):

the usual pp.all printout makes it look worse than it is because of all the duplicated subterms that are actually the same in memory

#### Kevin Buzzard (Apr 05 2020 at 19:14):

Oh that's interesting. I hadn't thought about how these were stored.

#### Kevin Buzzard (Apr 05 2020 at 19:14):

That is still the longest proof of 2 = 2 I've ever seen.

#### Mario Carneiro (Apr 05 2020 at 19:15):

lean also does its best to not e.g. re-typecheck the same expression if it appears in two places so a highly redundant term can still typecheck quickly

#### Mario Carneiro (Apr 05 2020 at 19:15):

2+2=4 has nothing on 2=2

#### Kevin Buzzard (Apr 05 2020 at 19:15):

(@bit0.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@distrib.to_has_add.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@ring.to_distrib.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@comm_ring.to_ring.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@polynomial.comm_ring.{0} R _inst_1)))) (@has_one.one.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@monoid.to_has_one.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@ring.to_monoid.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@comm_ring.to_ring.{0} (@polynomial.{0} R (@comm_ring.to_comm_semiring.{0} R _inst_1)) (@polynomial.comm_ring.{0} R _inst_1))))))

AKA 2

#### Mario Carneiro (Apr 05 2020 at 19:17):

I wonder if this proof is any better if you skip int cast and just use a theorem like `C (bit0 n) = bit0 (C n)`

#### Kevin Buzzard (Apr 05 2020 at 19:18):

with (n : R) I guess

#### Mario Carneiro (Apr 05 2020 at 19:18):

right

#### Mario Carneiro (Apr 05 2020 at 19:20):

theorem C_bit0 (R : Type) [comm_ring R] (x : R) : C (bit0 x) = bit0 (C x) := by simp only [bit0, C_add] example (R : Type) [comm_ring R] : (2 : polynomial R) = C 2 := by rw [C_bit0, C_1]

the proof of `C_bit0`

is still slow, but now the example is a respectable 50ms

#### Kevin Buzzard (Apr 05 2020 at 19:21):

Nice

#### Mario Carneiro (Apr 05 2020 at 19:22):

The example still looks ridiculous with pp.all but at least it doesn't end with `...`

#### Kenny Lau (Apr 06 2020 at 05:23):

but `C_bit0`

is fast for me

Last updated: May 09 2021 at 10:11 UTC