Zulip Chat Archive

Stream: maths

Topic: 2 = 2


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

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:08):

simp doesn't work for me :-/

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:09):

oh I see, after the convert. Thanks.

view this post on Zulip Mario Carneiro (Apr 05 2020 at 19:09):

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:09):

this is a bit more respectable, thanks.

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

view this post on Zulip Mario Carneiro (Apr 05 2020 at 19:10):

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:11):

Slightly ominous that the pp.all output ends with

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:11):

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:11):

Stupid computer doesn't understand equality properly

view this post on Zulip Mario Carneiro (Apr 05 2020 at 19:12):

I completely agree with you, this is ridiculous

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

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:14):

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:14):

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

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

view this post on Zulip Mario Carneiro (Apr 05 2020 at 19:15):

2+2=4 has nothing on 2=2

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

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:18):

with (n : R) I guess

view this post on Zulip Mario Carneiro (Apr 05 2020 at 19:18):

right

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

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 19:21):

Nice

view this post on Zulip Mario Carneiro (Apr 05 2020 at 19:22):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 05:23):

but C_bit0 is fast for me


Last updated: May 09 2021 at 10:11 UTC