Zulip Chat Archive

Stream: general

Topic: universe bug?


view this post on Zulip Reid Barton (Apr 30 2020 at 15:20):

MWE:

import topology.algebra.monoid

universes u v
variables {α : Type u} {β : Type v}
variables [topological_space α] [monoid α] [topological_monoid α]

attribute [irreducible] continuous

set_option pp.all true

lemma continuous.mul' [topological_space β] {f : β  α} {g : β  α}
  (hf : continuous f) (hg : continuous g) :
  continuous (λx, f x * g x) :=
continuous_mul.comp (hf.prod_mk hg)

Error:

/home/rwbarton/lean/mathlib/tmp/tmp.lean:14:14: error: failed to synthesize type class instance for
α : Type u,
β : Type v,
_inst_1 : topological_space.{u} α,
_inst_2 : monoid.{u} α,
_inst_3 : @topological_monoid.{u} α _inst_1 _inst_2,
_inst_4 : topological_space.{v} β,
f g : β  α,
hf : @continuous.{v u} β α _inst_4 _inst_1 f,
hg : @continuous.{v u} β α _inst_4 _inst_1 g
 topological_space.{(max u ?l_1)} (prod.{(max u ?l_1) (max u ?l_1)} α α)
/home/rwbarton/lean/mathlib/tmp/tmp.lean:14:14: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  
inferred
  @prod.topological_space.{(max u ?l_1) (max u ?l_1)} α α _inst_1 _inst_1

view this post on Zulip Reid Barton (Apr 30 2020 at 15:20):

There's more errors, which might also be relevant, but they are long.

view this post on Zulip Reid Barton (Apr 30 2020 at 15:20):

It works without attribute [irreducible] continuous (I just copied the lemma and proof from mathlib).

view this post on Zulip Reid Barton (Apr 30 2020 at 15:22):

I'm pretty confused--like prod.{(max u ?l_1) (max u ?l_1)} α α is already kind of bogus.

view this post on Zulip Sebastien Gouezel (Apr 30 2020 at 15:24):

If you just want a workaround, continuous_mul.comp (hf.prod_mk hg : _) works.

view this post on Zulip Reid Barton (Apr 30 2020 at 15:26):

Oh nice, I bet I can use this to simplify a couple of my other changes too.

view this post on Zulip Sebastien Gouezel (Apr 30 2020 at 15:28):

If you want to know more about why it works, with the words expected type/top-down/unifier, you will need someone else, though!

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:31):

I think there is a lemma that has been proven for all universes of the form max u v for some u,v and this is confusing the elaborator

view this post on Zulip Reid Barton (Apr 30 2020 at 15:33):

Well, prod.topological_space itself has a form like this

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:33):

continuous.comp has only two universe variables

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:33):

it should have three

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:34):

this causes this joint universe to get instanciated with a max and it gets messy after that

view this post on Zulip Reid Barton (Apr 30 2020 at 15:34):

Wait, I see three?

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:34):

no, false alarm

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:39):

Lean has no problems proving continuous ((λp:_×_, p.1 * p.2) ∘ λx, (f x, g x)) using that proof

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:40):

but somewhere between backward elaboration and the definitional reduction here it gets confused

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:50):

This demonstrates the problem somewhat:

lemma continuous.mul' [topological_space β] {f : β  α} {g : β  α}
  (hf : continuous f) (hg : continuous g) : true :=
begin
  have := continuous_mul.comp,
  have := continuous.prod_mk,
  have := λ x y, continuous_mul.comp (continuous.prod_mk x y),
end

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:52):

It is unifying

@continuous.{?l_9 (max ?l_10 ?l_16)} ?m_11 (prod.{?l_10 ?l_16} ?m_12 ?m_17) ?m_13
    (@prod.topological_space.{?l_10 ?l_16} ?m_12 ?m_17 ?m_14 ?m_18)
    (λ (x : ?m_11), @prod.mk.{?l_10 ?l_16} ?m_12 ?m_17 (?m_15 x) (?m_19 x))
=?=
@continuous.{?l_1 ?l_2} ?m_3 (prod.{?l_2 ?l_2} ?m_4 ?m_4) ?m_5
    (@prod.topological_space.{?l_2 ?l_2} ?m_4 ?m_4 ?m_6 ?m_6)
    ?m_7

and the resulting term

 (x : @continuous.{?l_20 (max ?l_21 ?l_22)} ?m_23 ?m_24 ?m_25 ?m_26 ?m_27)
  (y : @continuous.{?l_20 (max ?l_21 ?l_22)} ?m_23 ?m_24 ?m_25 ?m_26 ?m_28[x]),
    @continuous.{?l_20 (max ?l_21 ?l_22)} ?m_23 ?m_24 ?m_25 ?m_26
      (@function.comp.{?l_20+1 (max ?l_21 ?l_22)+1 (max ?l_21 ?l_22)+1} ?m_23
         (prod.{(max ?l_21 ?l_22) (max ?l_21 ?l_22)} ?m_24 ?m_24)
         ?m_24
         (λ (p : prod.{(max ?l_21 ?l_22) (max ?l_21 ?l_22)} ?m_24 ?m_24),
            @has_mul.mul.{(max ?l_21 ?l_22)} ?m_24
              (@semigroup.to_has_mul.{(max ?l_21 ?l_22)} ?m_24
                 (@monoid.to_semigroup.{(max ?l_21 ?l_22)} ?m_24 ?m_29[x, y]))
              (@prod.fst.{(max ?l_21 ?l_22) (max ?l_21 ?l_22)} ?m_24 ?m_24 p)
              (@prod.snd.{(max ?l_21 ?l_22) (max ?l_21 ?l_22)} ?m_24 ?m_24 p))
         (λ (x_1 : ?m_23), @prod.mk.{(max ?l_21 ?l_22) (max ?l_21 ?l_22)} ?m_24 ?m_24 (?m_27 x_1) (?m_28[x] x_1)))

contains only the universe (max ?l_21 ?l_22), which should just be one meta universe

view this post on Zulip Reid Barton (Apr 30 2020 at 18:40):

Oh interesting.

view this post on Zulip Reid Barton (Apr 30 2020 at 19:08):

This seems to be a recurring theme:

import topology.algebra.group

variables {α : Type} [topological_space α] [add_group α] [topological_add_group α]

attribute [irreducible] continuous

set_option pp.universes true
example (x : α) : true :=
begin
  have := continuous_sub.tendsto, -- fine, "filter.tendsto.{?l_1 ?l_1} ..."
  have := (continuous_sub.comp continuous_swap).tendsto,
  -- not fine, "filter.tendsto.{(max ?l_5 ?l_6) (max ?l_5 ?l_6)} ..."
  have := (continuous_sub.comp continuous_swap).tendsto (x, x), -- error
end

view this post on Zulip Reid Barton (Apr 30 2020 at 19:08):

Without attribute [irreducible] continuous the error goes away.

view this post on Zulip Reid Barton (Apr 30 2020 at 19:32):

I don't understand the mechanism by which Lean wants to unfold continuous when it is not irreducible (which it seems like it must be doing, right?)

view this post on Zulip Mario Carneiro (Apr 30 2020 at 19:33):

I think if you replace continuous with a constant it also works

view this post on Zulip Reid Barton (Apr 30 2020 at 20:00):

Also, I had no idea the library really used filters. Oh man.

view this post on Zulip Patrick Massot (Apr 30 2020 at 20:03):

What?

view this post on Zulip Reid Barton (Apr 30 2020 at 20:03):

I never touched filters before. Unless you count ultrafilters...

view this post on Zulip Patrick Massot (Apr 30 2020 at 20:03):

Of course it uses filters, how did you miss that?

view this post on Zulip Reid Barton (Apr 30 2020 at 20:03):

This is a lot harder than I expected

view this post on Zulip Reid Barton (Apr 30 2020 at 20:04):

Sure, but I thought it would only be for, like, 2 files.

view this post on Zulip Patrick Massot (Apr 30 2020 at 20:04):

What, filters or refactoring?

view this post on Zulip Reid Barton (Apr 30 2020 at 20:04):

Changing continuous to a structure

view this post on Zulip Patrick Massot (Apr 30 2020 at 20:04):

Nooo, they are everywhere :grinning:

view this post on Zulip Reid Barton (Apr 30 2020 at 20:08):

I've lost track of how many times I proved that multiplication is continuous because of some tendsto thing

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 20:11):

Can you do the perfectoid project afterwards?

view this post on Zulip Reid Barton (Apr 30 2020 at 20:13):

LOL no.

view this post on Zulip Reid Barton (Apr 30 2020 at 20:13):

I doubt I can even finish this.

view this post on Zulip Reid Barton (Apr 30 2020 at 20:19):

Hmm, emacs crashed. Maybe I should take that as a sign

view this post on Zulip Patrick Massot (Apr 30 2020 at 20:20):

Hey, I want that continuity tactic!

view this post on Zulip Sebastien Gouezel (Apr 30 2020 at 20:22):

You could have a baby continuity tactic by tagging some lemmas with [simp], the way I did for differentiability. And simp doesn't care about the apply bug.

view this post on Zulip Reid Barton (Apr 30 2020 at 20:41):

I think I'm giving up for now--changing hundreds of lines of filters isn't so bad, but there are also too many elaboration failures that need weird workarounds, and this universe issue with products is the worst part.

view this post on Zulip Patrick Massot (Apr 30 2020 at 20:42):

Thanks for trying!

view this post on Zulip Reid Barton (Apr 30 2020 at 20:42):

(The filters come in because I thought it would be a good idea to change the definition of continuous_at at the same time, which might have been wrong.)

view this post on Zulip Reid Barton (Apr 30 2020 at 20:44):

The "highlight" was the instance

instance {α : Type*} [uniform_space α] [add_comm_group α] [uniform_add_group α] : add_comm_group (completion α) := ...

getting an inferred type of Π {α : Type (max u_3 u_4)} ..., with max u_3 u_4 everywhere instead of a single variable.

view this post on Zulip Reid Barton (Apr 30 2020 at 20:45):

This caused some confusion later.

view this post on Zulip Mario Carneiro (May 01 2020 at 01:11):

I think it would be best to track down and fix the bug in this case rather than piling on lots of fixes that we will revert later


Last updated: May 13 2021 at 04:21 UTC