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

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

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) :=

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

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