# Zulip Chat Archive

## Stream: general

### Topic: universe bug?

#### 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
```

#### Reid Barton (Apr 30 2020 at 15:20):

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

#### Reid Barton (Apr 30 2020 at 15:20):

It works without `attribute [irreducible] continuous`

(I just copied the lemma and proof from mathlib).

#### 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.

#### Sebastien Gouezel (Apr 30 2020 at 15:24):

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

works.

#### 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.

#### 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!

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

#### Reid Barton (Apr 30 2020 at 15:33):

Well, `prod.topological_space`

itself has a form like this

#### Mario Carneiro (Apr 30 2020 at 15:33):

`continuous.comp`

has only two universe variables

#### Mario Carneiro (Apr 30 2020 at 15:33):

it should have three

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

#### Reid Barton (Apr 30 2020 at 15:34):

Wait, I see three?

#### Mario Carneiro (Apr 30 2020 at 15:34):

no, false alarm

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

#### Mario Carneiro (Apr 30 2020 at 15:40):

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

#### 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
```

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

#### Reid Barton (Apr 30 2020 at 18:40):

Oh interesting.

#### 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
```

#### Reid Barton (Apr 30 2020 at 19:08):

Without `attribute [irreducible] continuous`

the error goes away.

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

#### Mario Carneiro (Apr 30 2020 at 19:33):

I think if you replace `continuous`

with a `constant`

it also works

#### Reid Barton (Apr 30 2020 at 20:00):

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

#### Patrick Massot (Apr 30 2020 at 20:03):

What?

#### Reid Barton (Apr 30 2020 at 20:03):

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

#### Patrick Massot (Apr 30 2020 at 20:03):

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

#### Reid Barton (Apr 30 2020 at 20:03):

This is a lot harder than I expected

#### Reid Barton (Apr 30 2020 at 20:04):

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

#### Patrick Massot (Apr 30 2020 at 20:04):

What, filters or refactoring?

#### Reid Barton (Apr 30 2020 at 20:04):

Changing `continuous`

to a structure

#### Patrick Massot (Apr 30 2020 at 20:04):

Nooo, they are everywhere :grinning:

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

#### Kevin Buzzard (Apr 30 2020 at 20:11):

Can you do the perfectoid project afterwards?

#### Reid Barton (Apr 30 2020 at 20:13):

LOL no.

#### Reid Barton (Apr 30 2020 at 20:13):

I doubt I can even finish this.

#### Reid Barton (Apr 30 2020 at 20:19):

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

#### Patrick Massot (Apr 30 2020 at 20:20):

Hey, I want that continuity tactic!

#### 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.

#### 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.

#### Patrick Massot (Apr 30 2020 at 20:42):

Thanks for trying!

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

#### 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.

#### Reid Barton (Apr 30 2020 at 20:45):

This caused some confusion later.

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