2 = 2

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

simp doesn't work for me :-/

[Mario Carneiro]

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]

oh I see, after the convert. Thanks.

[Mario Carneiro]

you can also use rw instead of simp only for a little bit faster

[Kevin Buzzard]

this is a bit more respectable, thanks.

[Kevin Buzzard]

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]

If you print the proof with pp.all you might see why it takes this long

[Kevin Buzzard]

Slightly ominous that the pp.all output ends with

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Stupid computer doesn't understand equality properly

[Mario Carneiro]

I completely agree with you, this is ridiculous

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

2+2=4 has nothing on 2=2

[Kevin Buzzard]

(@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]

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]

with (n : R) I guess

[Mario Carneiro]

right

[Mario Carneiro]

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]

Nice

[Mario Carneiro]

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

[Kenny Lau]

but C_bit0 is fast for me