universe bug?

Stream: general

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Sebastien Gouezel]

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

[Reid Barton]

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

[Sebastien Gouezel]

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

[Mario Carneiro]

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

[Reid Barton]

Well, prod.topological_space itself has a form like this

[Mario Carneiro]

continuous.comp has only two universe variables

[Mario Carneiro]

it should have three

[Mario Carneiro]

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

[Reid Barton]

Wait, I see three?

[Mario Carneiro]

no, false alarm

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

Oh interesting.

[Reid Barton]

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

[Reid Barton]

Without attribute [irreducible] continuous the error goes away.

[Reid Barton]

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?)

[Mario Carneiro]

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

[Reid Barton]

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

[Patrick Massot]

What?

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

This is a lot harder than I expected

[Reid Barton]

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

[Patrick Massot]

What, filters or refactoring?

[Reid Barton]

Changing continuous to a structure

[Patrick Massot]

Nooo, they are everywhere :grinning:

[Reid Barton]

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

[Kevin Buzzard]

Can you do the perfectoid project afterwards?

[Reid Barton]

LOL no.

[Reid Barton]

I doubt I can even finish this.

[Reid Barton]

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

[Patrick Massot]

Hey, I want that continuity tactic!

[Sebastien Gouezel]

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.

[Reid Barton]

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.

[Patrick Massot]

Thanks for trying!

[Reid Barton]

(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.)

[Reid Barton]

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.

[Reid Barton]

This caused some confusion later.

[Mario Carneiro]

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