nsmul and Lean 4

Stream: condensed mathematics

[Johan Commelin]

@Mario Carneiro @Leonardo de Moura Do you think that the nsmul/gsmul type of diamonds that we had before the refactor can be gracefully dealt with by Lean 4. Maybe not current stock Lean 4. But could we teach it to deal with such diamonds in principle?
(Asking on this stream instead of #lean4 because Peter is also interested in the question and answers.)

[Mario Carneiro]

I don't think that there is anything in particular about nsmul that is problematic

[Mario Carneiro]

The performance issues we are hitting are just because we have a large hierarchy, plus possibly something odd in the kernel settings

[Mario Carneiro]

I have no idea whether lean 4 will change things, because it will change so many things that this problem will barely be recognizable. We will have entirely different problems in lean 4 (hopefully less overall but there is no easy comparison)

[Leonardo de Moura]

@Johan Commelin We are committed to making sure Lean 4 serves all of our sub-communities. It would be great for us to have a (small) self-contained Lean file that exposes the problem you mentioned. Do you think you could it?

[Johan Commelin]

@Sebastien Gouezel did the refactor, so he might be in a better shape to do this.

[Mario Carneiro]

do we actually have an example of a slow definition?

[Johan Commelin]

We are trying to drill down to the bottom of the speed issue in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20repo.20GitHub.20actions.20queue

[Johan Commelin]

I think there are two issues:

1. Why is Lean 3 slow after the refactor. (That's not what my question in this thread is about.)
2. Can we make "minimalistic" definitions in Lean 4. Or do we need to have "forgetful inheritance" in many places. (That's what I was intending in OP.)

[Johan Commelin]

Examples where we use this pattern: metric_space includes a copy of uniform_space includes a copy of topological_space.
And now: add_comm_monoid includes (what amounts to) a copy of semimodule nat, and add_comm_group is about to include on top of that a "copy" of module int.
But there is now a pattern. Because [division_ring R] [char_zero R] will give an instance of algebra rat R. And so there's another "forgetful diamond" lurking around the corner.

[Sebastien Gouezel]

I think that what we see after the refactor is just a symptom, that kernel checking of definitional equality is very slow in some situations. Since I have added three fields to structures as basic as monoid and add_monoid, it made some iterated unfolding/refolding steps heavier, hence the slowness. Normally, this should be solved by not using old style structures (and Leo had warned us about this some time ago!)

[Johan Commelin]

It may certainly be a symptom of something else. But my question (2) is aiming more at the underlying philosophy of library design that we should aim for / adhere to. Can we "just" write down the "minimalist" definitions that are in some sense the Platonic "correct" ones. Or should we be prepared to have 3x more data in add_comm_group than one would (naively) expect.

[Johan Commelin]

There is a slight difference between the topological and the algebraic examples. For topology, you want the product topology and the metric topology on $X \times Y$ to be defeq. But there isn't some universal theorem telling you that it should (afaik).
In the algebraic examples, we have instances subsingleton (module int A) for arbitrary abelian groups A, and similarly subsingleton (algebra int R) for arbitrary rings R, etc...

[Johan Commelin]

It seems to me that a typechecker could in principle take advantage of such subsingletons at a low level.
But I can absolutely understand that this may be a completely ridiculous idea from a performance point of view.
I just don't have enough understanding to know whether it is just a tiny bit ridiculous or super-duper ridiculous.

[Johan Commelin]

In general, I think I lean towards "first make it fast, then fix the UX". So if we need long-winded definitions in order to have a fast kernel, I'm very happy to make that trade off.

[Mario Carneiro]

It's more than a performance issue. You are talking about having multiple paths of typeclass inference that are not defeq. In order to make that work seamlessly lean has to be able to cast between types, and I think that getting good UX on this is an open problem

[Johan Commelin]

Ok, that's a useful answer. (I was hoping that maybe it was a problem that was solved in Lean 4.)

[Mario Carneiro]

The problem that is potentially solved in lean 4 is the performance issues we are having with deep algebraic hierarchies with many fields

[Johan Commelin]

Leonardo de Moura said:

Johan Commelin We are committed to making sure Lean 4 serves all of our sub-communities. It would be great for us to have a (small) self-contained Lean file that exposes the problem you mentioned. Do you think you could it?

Thanks a lot for your commitment to all these diverse sub-communities. Let me try to answer your question. In the last few days, I think I gained a better understanding of the issue, and more or less understand why the answer to my vague question is "you don't want this". The answer seems to be: use forgetful inheritance and new-style structures.

But at the same time I stumbled on a related issue. Let me first say that it is currently not a serious problem for LTE. So there is not really an urgent need to solve a particular problem.

The problem is the following. In mathlib we have the following definition (the details don't matter, what matters is that it is in mathlib):

/-- A seminormed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥`
defines a pseudometric space structure. -/
class semi_normed_group (α : Type*) extends has_norm α, add_comm_group α, pseudo_metric_space α :=
(dist_eq : ∀ x y, dist x y = norm (x - y))

In LTE we have the following definition (again, the details don't really matter, what matters is that this definition is in LTE and contains data):

class pseudo_normed_group (M : Type*) :=
[to_add_comm_group : add_comm_group M]
(filtration [] : ℝ≥0 → set M)
/- snip -/

Finally, we have the following instance:

instance (V : Type*) [semi_normed_group V] : pseudo_normed_group V :=
{ filtration := λ c, {v | nnnorm v ≤ c},
  /- snip -/ }

Now this is a source of diamonds: we end up with two propeq-but-not-defeq instances on $\mathrm{Hom}(\Lambda, M)$ (whatever that may be).

The usual solution would be: refactor the definition of semi_normed_group so that it extends pseudo_normed_group using forgetful inheritance.

But since pseudo_normed_group is in LTE, this is not an option. And it is currently not clear that this definition belongs in mathlib.

Let me stress again that the diamond does not cause serious trouble in LTE. It shows up, but we can work around it with a couple lines of code.

But I do think that this is an example of a more general pattern: that "small" projects depending on a big library like mathlib will want to inject new definitions in the middle of the hierarchy. The current design strategy of forgetful inheritance only seems to work for monolithic libraries.
I hope the picture is somewhat clear, and I would be very interested in hearing your thoughts about strategies for working with multiple interdependent Lean packages that build and extend the same hierarchy.

[Kevin Buzzard]

class foo (X : Type) :=
(n : ℕ)

class bar (X : Type) :=
(m : ℕ)

instance foo.to_bar (X : Type) [i : foo X] : bar X :=
{ m := i.n }

instance prod.foo (X Y : Type) [i : foo X] [j : foo Y] : foo (X × Y) :=
{ n := i.n + j.n } -- X + Y

instance prod.bar (X Y : Type) [i : bar X] [j : bar Y] : bar (X × Y) :=
{ m := j.m + i.m } -- Y + X, i.e. opposite order

-- non-defeq diamond
example (X Y : Type) [foo X] [foo Y] : foo.to_bar (X × Y) = prod.bar X Y := sorry -- not `rfl`

-- fix: refactor foo
class foo_fixed (X : Type) :=
(n : ℕ)
(m : ℕ)
(h : m = n)

instance foo_fixed.to_bar (X : Type) [i : foo_fixed X] : bar X :=
{ m := i.m }

instance prod.foo_fixed (X Y : Type) [i : foo_fixed X] [j : foo_fixed Y] : foo_fixed (X × Y) :=
{ n := i.n + j.n,
  m := j.m + i.m,  -- makes diamond go away
  h := begin
    rw [i.h, j.h, nat.add_comm], -- proof now inserted into type class system
  end }

example (X Y : Type) [foo_fixed X] [foo_fixed Y] : foo_fixed.to_bar (X × Y) = prod.bar X Y := rfl

-- but what if `foo` is in a dependency so we can't refactor it?

[Kevin Buzzard]

An even better example would be m=2°n because this cannot be fixed with a change of definition of prod.bar -- will update tomorrow

[Kevin Buzzard]

Better example -- can't be fixed by refactoring bar:

class foo (X : Type) :=
(n : ℕ)

class bar (X : Type) :=
(m : ℕ)

instance foo.to_bar (X : Type) [i : foo X] : bar X :=
{ m := 2 * i.n }

instance prod.foo (X Y : Type) [i : foo X] [j : foo Y] : foo (X × Y) :=
{ n := i.n + j.n }

instance prod.bar (X Y : Type) [i : bar X] [j : bar Y] : bar (X × Y) :=
{ m := i.m + j.m }

-- important example with m odd means we can't refactor `bar` to include `foo`
instance : bar ℕ := {m := 1}

-- non-defeq diamond because `2*(a+b)` and `2*a+2*b` are not defeq
example (X Y : Type) [foo X] [foo Y] : foo.to_bar (X × Y) = prod.bar X Y := sorry -- not `rfl`

-- fix: refactor foo to include bar
class foo_fixed (X : Type) :=
(n : ℕ)
(m : ℕ)
(h : m = 2*n)

instance foo_fixed.to_bar (X : Type) [i : foo_fixed X] : bar X :=
{ m := i.m }

instance prod.foo_fixed (X Y : Type) [i : foo_fixed X] [j : foo_fixed Y] : foo_fixed (X × Y) :=
{ n := i.n + j.n,
  m := i.m + j.m,
  h := begin
    rw [i.h, j.h, nat.left_distrib], -- proof inserted into system here
  end }

example (X Y : Type) [foo_fixed X] [foo_fixed Y] : foo_fixed.to_bar (X × Y) = prod.bar X Y := rfl

-- but what if `foo` is in a dependency so we can't refactor it when we discover we need `bar`?

[Eric Wieser]

One possible way to handle the dependency is:

• Have foo_fixed extend foo
• attribute [-instance] every foo instance in the upstream project
• Write a foo_fixed version of every such instance.

However, even this can fail if lemma statements end up being about the old foo instance, and obviously this scales very poorly