Type classes again

Stream: general

[Sebastien Gouezel]

Trying to fix the normed_space issue, I ran into a weird behavior of typeclass resolution. The definition is now

class normed_space (α : Type*) (β : Type*) [normed_field α] [normed_group β]
  extends vector_space α β :=
(norm_smul : ∀ (a:α) (b:β), norm (a • b) = has_norm.norm a * norm b)

Then, to define a normed space structure on the space of continuous linear maps between two normed spaces, I write

instance to_normed_group : normed_group (E →L[k] F) :=
normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_triangle, op_norm_neg⟩

instance to_normed_space : normed_space k (E →L[k] F) :=
⟨op_norm_smul⟩

The surprising behavior is that Lean can not infer the normed group structure on E →L[k] (F × G).

instance to_normed_group_prod : normed_group (E →L[k] (F × G)) :=
continuous_linear_map.to_normed_group

works, but using by apply_instance instead of continuous_linear_map.to_normed_group fails. I can register this instance by hand as I just did, and then everything works fine, but I am afraid this shows there is something wrong with my definitions.

[Sebastien Gouezel]

If I try with apply_instance, the context is

1 goal
k : Type u_1,
E : Type u_2,
F : Type u_3,
G : Type u_4,
_inst_1 : nondiscrete_normed_field k,
_inst_2 : normed_group E,
_inst_3 : normed_space k E,
_inst_4 : normed_group F,
_inst_5 : normed_space k F,
_inst_6 : normed_group G,
_inst_7 : normed_space k G
⊢ normed_group (E →L[k] F × G)

and in the instance search trace I find the line

[class_instances] (1) ?x_36 : @normed_space k G (@nondiscrete_normed_field.to_normed_field k _inst_1) _inst_6 := _inst_7
failed is_def_eq

I don't understand what is going on...

[Sebastien Gouezel]

Crap, universe issues: if I put all of them in Type, everything works...

[Kevin Buzzard]

Try changing Type* to Type u in some places, if you want to remain polymorphic. That sometimes changes things.

[Kevin Buzzard]

I have no proper understanding of why this helps, but apparently it changes elaboration. This might be an unrelated issue though of course.

[Sebastien Gouezel]

I just tried this, but the problem remains.

[Kevin Buzzard]

Well spotted though; universe problems are hard to debug.

[Kevin Buzzard]

I have in the past suggested that mathematicians would be better off working in only one universe -- after all, that's how mathematics of this nature actually works in practice. Since when did any mathematician ever want to consider two normed fields in two different universes? Universes are for people wrestling with categories in a serious way, not for people doing "normal" mathematics like this.

[Kevin Buzzard]

I don't necessarily mean Type, but I'm suggesting Type u for everything.

[Kevin Buzzard]

The CS guys like this "maximally universe polymorphic" approach but I have never seen a benefit when doing this kind of mathematics. Are these issues present in Isabelle/HOL?

[Kevin Buzzard]

If Lean struggles with them, and we don't actually need them, then this is an argument for just using one universe.

[Kevin Buzzard]

What is done in Coq? Does anyone know?

[Sebastien Gouezel]

I agree with this (almost: I would be ready to have the field k in some universe -- think of the real numbers, they are in Type -- and the vector spaces in another one -- but in my example it doesn't work, they really all need to be in the same universe). I haven't seen any benefit of universe polymorphism either, and these issues don't exist in Isabelle. We really need the CS guys either to make it better, or to grant us the right to use only one universe :)

[Johan Commelin]

Linear equivalences between vector spaces are currently not universe polymorphic... so it's not like you can't have non-universe polymorphic stuff in mathlib. It works like a virus though

[Johan Commelin]

I fear that the ℚ_[ℓ]-vector space that rolls out of étale cohomology will not live in Type.

[Johan Commelin]

I would still like to be able to apply general theorems to it.

[Johan Commelin]

Currently mathlib makes it hard for me to express that it is isomorphic to its double dual... (assuming that this cohomology group is fin.dim., which is often the case).

[Sebastien Gouezel]

Just for the record, with pp.all I have in the context

_inst_7 : @normed_space.{u uG} k G (@nondiscrete_normed_field.to_normed_field.{u} k _inst_1) _inst_6

and the line that fails in instance search, if I read the trace correctly, is

[class_instances] (1) ?x_36 : @normed_space.{u uG} k G (@nondiscrete_normed_field.to_normed_field.{u} k _inst_1) _inst_6 := _inst_7
failed is_def_eq

This is really a mystery to me...

[Johan Commelin]

That's really crazy...

[Keeley Hoek]

Is this the same reluctance to unify universe metavariables that makes you have to specify the category_theory morphism universe sometimes?

[Reid Barton]

So the category theory one I understand

[Reid Barton]

The issue there is that, just like how in group theory we only talk about G : Type u and rely on the type class system to find [group G], in category theory we talk about C : Type u and rely on the type class system to find [category C]. But there is a difference, because category has a second universe parameter v which is not determined by C. If you're unlucky it might also not be determined by whatever context is requiring the category instance and then Lean will refuse to "guess" v for you.

[Reid Barton]

In that case you might need to add a .{v} somewhere.

[Reid Barton]

When I saw Sebastien's tactic state my first thought was that there is some problem about universe variables, but I don't understand what the problem was. It looks as though there is just a bug.

[Reid Barton]

I agree with this (almost: I would be ready to have the field k in some universe -- think of the real numbers, they are in Type -- and the vector spaces in another one -- but in my example it doesn't work, they really all need to be in the same universe). I haven't seen any benefit of universe polymorphism either, and these issues don't exist in Isabelle. We really need the CS guys either to make it better, or to grant us the right to use only one universe :)

I like the "Type u for everything" approach for all the parts of math that don't routinely use universes even in informal presentations.
For cases where you want to work over some particular base field in Type there's always ulift. If ulift real isn't already a field then we can have someone go and make algebra/ulift_instances.

[Keeley Hoek]

What actually is the point of Type u not being in Type u+2

[Kevin Buzzard]

I fear that the ℚ_[ℓ]-vector space that rolls out of étale cohomology will not live in Type.

Removing my computer science hat completely, you sound like you just said "I fear that the etale cohomology groups are not sets", to which I reply "Johan that is complete nonsense, of course they're sets! What are you talking about?"

[Reid Barton]

I think Johan means that the étale site of X is not small, but only essentially small. It's not clear what the best way to formalize this is--but informally we just pretend there's no difference at all.

[Johan Commelin]

I don't like have ulift ℤ and ulift ℝ all over the place... it's quite ugly. Otoh, battling universe issues is also ugly. I hope that we can jump between the two horns of this bull.

[Kevin Buzzard]

The issue there is that, just like how in group theory we only talk about G : Type u and rely on the type class system to find [group G], in category theory we talk about C : Type u and rely on the type class system to find [category C]. But there is a difference, because category has a second universe parameter v which is not determined by C. If you're unlucky it might also not be determined by whatever context is requiring the category instance and then Lean will refuse to "guess" v for you.

My way of thinking about this completely solves this issue. Every category that I run into as a "normal mathematician" who is not explicitly trying to prove theorems about categories but is instead just using them as a tool to do "normal mathematics", is either a category where the class of all objects is a set (e.g. a diagram category), or a category where the class of all objects is not a set, but Hom(X,Y) is a set for all objects X and Y (e.g. the categories of sets, groups, rings, vector spaces over a field, schemes, topological spaces, insert arbitrary sane mathematical object here i.e. not "category"). So in all of "normal mathematics" there are only two things: small categories and big categories. In both cases v is determined by u. Mathematicians use these two kinds of categories in different ways too; diagram categories are for taking limits, all the other categories are for giving us a unified language for managing data and theorems, giving us a general language such as "adjoint functor" to save pen when we're trying to say what we want to say.

So the extension of my "just use one universe" argument to the category theory situation is "if you want to make the category of perfectoid spaces, make it a "category of the second kind" with just one universe parameter u, and have X : Type u and Hom(X,Y) : Type u. One universe, doing the thing which the ZFC universe was invented to solve". Problem solved. Not as universe polymorphic as some people like -- but it works in Lean and it is enough for mathematicians.

Sure if you want to develop some theories about higher categories or whatever then feel free to wrestle with universes; I am not saying that all of the maths everyone does should stick to one universe. But I want to argue that for "normal" mathematics, being universe polymorphic is actively bad. It is bad because things don't work. It is bad because normal mathematicians say "why are you assuming the existence of universes?". I have no good answer to this question. I want to start a campaign for one universe.

[Kevin Buzzard]

I think Johan means that the étale site of X is not small, but only essentially small. It's not clear what the best way to formalize this is--but informally we just pretend there's no difference at all.

I must understand all the mathematics here. How do we define the constant sheaf Z/nZ on the etale site? Insert definition here. It's a sheaf. H^0 is then in Type, right?

[Kevin Buzzard]

There are various ways of defining the higher H^i. Can't I just take some cohomologically trivial cover and then do some Cech-like thing? Is there really an issue here?

[Neil Strickland]

I don't really buy this. It's a basic part of the formalism that any ring R is isomorphic to the ring of global sections of the structure sheaf on the Zariski site for R. But under the natural framework of definitions, the latter ring will be in a higher universe. You can probably avoid that, by some argument showing that it is sufficient to consider R-algebras of finite presentation, which can be specified by finite lists of elements of R. But that will take some work. However, there is some real mathematical content here: we have no right to expect that the obvious definition of etale cohomology does not lead to Russell-type paradoxes, and the reasons behind that are essentially the same as the universe considerations that we are discussing.

[Reid Barton]

Neil said basically what I was going to but just to spell out this "natural framework":
Etale cohomology is an instance of sheaf cohomology, which we can define for any site. If F is a sheaf on a site (C, J) then H^0(F) is the limit of F over C^{op}. In general if we allow C to be a large category then H^0(F) might really be too big to be a set even if all the values of F are sets.
Now in etale cohomology two things happen which each independently prevent this from occurring.

• The etale site of X has a terminal object (X itself) which means that H^0(F) is (isomorphic to) F(X). But we should regard this as a theorem, not a definition. Moreover we still have to do something about the higher H^i(F).
• The etale site of X is essentially small (by the kind of cardinality arguments Neil mentioned) and therefore we can compute all the H^i(F) by replacing the etale site by an equivalent small category. Again there are theorems involved here (these cardinality arguments, and the fact that cohomology is unchanged under an equivalence of sites) but perhaps it's most ergonomic to define etale cohomology as the sheaf cohomology over a genuinely small category equivalent to the etale site of X.

[Johan Commelin]

@Kevin Buzzard As mathematicians, we have Type u ⊆ Type (u+1). Hence you're definition can spit out something in Type (u+1) but you can later prove that it actually lives in a smaller universe. We can't do that in Lean :sad:

[Kevin Buzzard]

Conrad has thought hard about these issues and might have opinions on "the best way to do it". I'll see what he thinks. It will probably just be the "replace by an equivalent small category" argument.

[Kevin Buzzard]

I do think it's essential to prove that cohomology groups are in the right universe. Wait -- this is orthogonal to the underlying issue, isn't it? If I'm prepared once and for all to do some work (which should be done!) to prove that my cohomology groups are sets (which is one way of thinking about it with a ZFC perspective) then this is all just fine still; I still don't ever need more than one universe. I'm aware there's an issue, but I don't think universe polymorphism is the way to solve it; I think what Reid is saying is the way to solve it. This is hence not an argument for multiple universes.

[Johan Commelin]

It's not yet clear to me how we can define H^i_et to be in Type and also make it interact nicely with the sheaf cohomology machinery. The answer is probably to have comparison isomorphisms all over the place. And once we get sufficiently annoyed by them, we try to write a tactic that hides them for us.

[Johan Commelin]

I do think it's essential to prove that cohomology groups are in the right universe.

In Lean you cannot prove this. You have to make a definition, and that is the place where you have to get it right. If you mess up... bad luck.

[Johan Commelin]

But maybe we will have norm_ulift (-;

[Reid Barton]

I totally agree that having a field k and two k-algebras R and S and an S-module M all living in different universes is not sustainable and mathlib is probably close to exhausting the material for which it makes sense. If universes are causing any difficulty then just put everything in a single Type u. Kevin I'm not sure whether your "one universe" is Type u for a "fixed" u or genuinely Type--if the latter then I'm more skeptical.
The reason we have two parameters in category theory is just to avoid duplication between small and large categories. We have definitions with up to four category parameters, I think, so there would be a lot of combinations.

[Johan Commelin]

@Sebastien Gouezel But your problem didn't go away if you put everything in Type u, right? Only putting everything in Type worked, iirc...

[Sebastien Gouezel]

It works fine if everything is in Type u. If the field is in Type u and the normed spaces are in Type v, it doesn't.

[Mario Carneiro]

Coming back to the original question, is there a MWE?

[Kevin Buzzard]

From Brian:

You don’t mean “equivalent to the etale site” (that can and should have arbitrarily huge disjoint unions in it), but rather the sheaf theory on such a more limited site is naturally equivalent (via restriction) to the sheaf theory on the actual small etale site.

This latter sheaf theory has no set-theoretic issues (in terms of Hom-sets being sets, etc.) because the sheaf theory only needs a “base” for the topology to determine objects up to unique isomorphisms and maps between objects. So if for a scheme X you consider just affine schemes E equipped with an etale map f members U of a chosen base of Zariski open affines in X (to make it more “concrete”) then there’s a set of such triples (E, U, f) for which any triple is isomorphic to one of those, and if you throw in all finitely iterated fiber products among these then those objects and maps among them form a site and its sheaf theory is naturally equivalent to the one on X, so in that way you’ll get all the data you need to do the sheaf theory without set-theoretic issues. The sheaf theory on the small etale site (etale X-schemes and etale covers thereof) is all that is needed for any of the foundational theorems and applications thereof (e.g., Weil II, etc.) that I have ever seen.

In EGA there is the important theorem that if Spec(B) —> Spec(A) is etale, then Zariski-locally B looks “standard-etale” (i.e., (A[X]/(f))[1/f’]_h for some monic f and some h in A[X]), but in the Stacks Project this is improved to avoid needing to Zariski-localize upstairs. Same with smooth maps between affines. Maybe that would be useful to you?

Brian

[Sebastien Gouezel]

No MWE, it depends on two many modifications to mathlib. Once #1085 is merged, I will PR a branch with the workaround and showing the issue.

[Patrick Massot]

I'm working on it, but probably won't have time to finish before dinner, and then I need to bring one of my daughter to a spectacle...

[Jeremy Avigad]

While we are on the topic of universes, I'll point to a problem that I recently came across. When I was in Edinburgh, Marijn Heule wrote me and me that Donald Knuth had written him with a question about the Mycielskian (https://en.wikipedia.org/wiki/Mycielskian). Knuth remarked that he thought the construction would be hard to carry out in an interactive theorem prover like Coq. So, I tried it. Knuth was wrong; the construction is routine and the formalization did not take long at all. It is here: https://gist.github.com/avigad/6c1b7a2b771ac561425f50ffd69a4815.

There were a few issues I wanted to raise here. First, I made the constructions computable, since it would be a shame if we could not compute with finite graphs. But I ultimately decided it is a mistake to use fintypes, and if I ever get back to this, I'll rewrite the constructions to avoid them. The problem is that if α is a fintype, then card α = card α is not necessarily provable by reflexivity, since there is an implicit dependence on the list of elements that is inferred. This actually comes up; rewrites can fail since different ways of getting a term lead to different instances. I think the right way to go is to use finsets instead.

Second, a silly calculation in nat was much harder than it should have been: https://gist.github.com/avigad/6c1b7a2b771ac561425f50ffd69a4815#file-mycielskian-lean-L162-L168. (@Seul Baek I can show you some examples where the omega tactic gets confused.) I have been meaning to experiment some more before passing it off to all of you, but I will be interested in hearing if any of you can make the calculation more automatic.

Finally (and this is the place where universes come in), I said that a graph is k-colorable if there exists a type α of cardinality k and a coloring of the graph with elements from alpha. But I could not get the key proof to work without naming universes explicitly: https://gist.github.com/avigad/6c1b7a2b771ac561425f50ffd69a4815#file-mycielskian-lean-L125-L126. I messed around with proof terms and tactics for a while before resorting to that. I have been meaning to come back to it and experiment some more, but I am teaching a summer school workshop that has been absorbing all my energy. (I have ~25 really great undergraduates from all over, coming from math, computer science, and philosophy.) Anyhow, if anyone can tell me what I am doing wrong and why I need the universe annotations, I'd be interested in hearing it.

[Chris Hughes]

I strongly agree that the fintype thing is a major problem, but I wasn't sure of the best approach. It's a barrier to finite groups that never got resolved. I'm not sure how using finsets solves the issue, card α, would become finset.univ.card, but we still use a fintype instance. I thought it might be okay to just make fintype a proposition for most proof purposes, and keep the computable version just in case anyone wanted to compute with it. Either that or make Lean handle subsingletons better with rewrite / simp etc.

[Kevin Buzzard]

Chris pointed out the fintype issue to me nearly a year ago now.

Jeremy's silly nat calculation is this:

lemma silly (n d : ℕ) :  2 * (2 ^ n * d + 2 ^ n * 1) - 2 * 1 + 1 =
2 ^ n * 2 * 1 + 2 ^ n * 2 * d - 1 :=
begin
ring,
 rw [nat.sub_add_eq_add_sub],
  { apply nat.succ_sub_succ },
  change 2 * 1 ≤ _, apply mul_le_mul; try {simp},
  change 2^0 ≤ _, apply nat.pow_le_pow_of_le_right; norm_num
end

It's the sort of thing that would turn Patrick's stomach!

Universes are somehow beyond my ken.

[Mario Carneiro]

@Jeremy Avigad The universe issue is because colorable has an internal universe variable:

def colorable (G : graph) (k : nat) :=
  ∃ (α : Type*) [h : fintype α] [decidable_eq α] (c : coloring G α), @fintype.card α h = k

means

def colorable.{u v} (G : graph.{u}) (k : nat) :=
  ∃ (α : Type v) [h : fintype α] [decidable_eq α] (c : coloring G α), @fintype.card α h = k

where you almost certainly did not intend to have colorable take a second (input!) universe variable. It is not possible to existentially quantify over universe variables, so colorable.{u v} G k says that there is a coloring using some type in Type v. I would suggest either using Type u instead of Type v here, or even simpler, skipping general types entirely and using fin k:

def colorable (G : graph) (k : nat) := nonempty (coloring G (fin k))

Then the equivalence to the first definition (for an arbitrary fintype in any universe) is a theorem.

[Jeremy Avigad]

Thanks to all three of you for the quick responses!

@Chris Hughes You are right. It is convenient to use inductive types for graph-theoretic constructions, but then I don't see how to get a finset without avoiding the fintype problem. Probably the best solution, as you say, is to have a finite_type class in Prop that mirrors the fintype one (until rw and so on are able to handle subsingletons). The duplication would be unfortunate though. (Or does anyone really need the one in Type?)

@Mario Carneiro Thanks for the explanation. Forcing the colors to be in the same type as the graph might work. (But maybe one day someone will want to 2-color a huge graph with bool?) Using a general type rather than fin k was useful in the proofs, because in the key argument Wikipedia runs as follows: "Suppose you have a coloring of the original graph with {1,...,k}. Without loss of generality, we can assume the hub is colored k." Can you see a clever way to get the WLOG using fin k?

[Mario Carneiro]

I'm not saying you can't have coloring G A for some other type A, I'm saying to prove a lemma that this implies coloring G (fin (card A)) and hence colorable G (card A)

[Kevin Buzzard]

lemma what_is_this_called {a b c : ℕ} (h : a + c = b) : a = b - c :=
begin
  rw ←h,
  simp,
end

[Kevin Buzzard]

My library-search-fu is failing me.

[Mario Carneiro]

it's an iff, sub will be on the left, and on the left of the eq

[Mario Carneiro]

so nat.sub_eq_iff_add_eq or similar

[Jeremy Avigad]

Ah, got it. Yes, that seems the way to go.

[Mario Carneiro]

it's nat.sub_eq_iff_eq_add

[Kevin Buzzard]

It's not an iff because maybe a=0 and c>>b

[Mario Carneiro]

oh, you aren't assuming the subtraction works?

[Kevin Buzzard]

It's somehow not quite the right thing anyway. You do have to prove 1 ≤ 2 ^ n * 2 * 1 + 2 ^ n * 2 * d - 1 at some point -- yeah exactly, that the subtraction works.

[Mario Carneiro]

I don't think we have it; if there is an equality in the hypotheses we usually just substitute it in, so it's just saying a + b - b = a which is one of the variants of nat.add_sub_cancel

[Mario Carneiro]

(also I think this is the wrong thread)

[Kevin Buzzard]

this thread is already a mess ;-)

lemma silly (n d : ℕ) :  2 * (2 ^ n * d + 2 ^ n * 1) - 2 * 1 + 1 =
2 ^ n * 2 * 1 + 2 ^ n * 2 * d - 1 :=
begin
  symmetry,
  rw ←nat.sub_eq_iff_eq_add,
    ring,
--    ⊢ 1 ≤ 2 ^ n * 2 * 1 + 2 ^ n * 2 * d - 1
sorry
end

I don't see how one can get away from that silly inequality goal.

[Mario Carneiro]

oh I see this is Jeremy's nat equality issue

[Kevin Buzzard]

Right.

[Kevin Buzzard]

But he's doing exactly what I'm going to have to do now, n>=0 and d>=0 so done.

[Kevin Buzzard]

Maybe some sort of mono tactic saves you the pain?

[Mario Carneiro]

apply a + b <= c -> a <= c - b and then linarith

[Kevin Buzzard]

linarith was the first thing I tried. It doesn't work.

[Kevin Buzzard]

The lemma is basically equivalent to ⊢ 1 ≤ 2 ^ n * 2 * 1 + 2 ^ n * 2 * d - 1; if you can get the cancellation to work then ring does the job. But to prove this you need 2^n>=1 and now it's all going a bit meh.

[Mario Carneiro]

lemma silly (n d : ℕ) : 2 * (2 ^ n * d + 2 ^ n * 1) - 2 * 1 + 1 =
2 ^ n * 2 * 1 + 2 ^ n * 2 * d - 1 :=
begin
  symmetry,
  rw ←nat.sub_eq_iff_eq_add, {ring},
  apply nat.le_sub_left_of_add_le,
  linarith [nat.pow_pos (dec_trivial:2>0) n]
end

[Kevin Buzzard]

Aah you just beat me on length -- I didn't know about nat.pow_pos so used nat.pow_le_pow_of_le_right. I found nat.le_sub_right_of_add_le using library_search :D

[Mario Carneiro]

Better solution: don't use subtraction

theorem card_iterated_mycielskian (G : graph) [fintype G.vertex] (n : ℕ) :
  card (iterated_mycielskian G n).vertex + 1 = 2^n * (card G.vertex + 1) :=
begin
  induction n with n ih; simp only [iterated_mycielskian], {simp},
  rw [card_mycielskian, nat.pow_succ, mul_right_comm, ← ih], ring
end

[Kevin Buzzard]

That horrific function shouldn't even be called subtraction.

[Mario Carneiro]

monus then

[Kevin Buzzard]

I think Patrick would prefer moanus

[Jeremy Avigad]

I like Mario's last solution. I should have thought of it. I wonder: how can we record this general strategy so that others don't make the same mistake I did? We need a theorem linter that warns users away from subtraction on nat and suggests alternatives. (Similarly, one should replace division on int and nat by multiplication, despite Descartes' rule XX: https://en.wikisource.org/wiki/Rules_for_the_Direction_of_the_Mind.)

[Mario Carneiro]

Perhaps we should collect some tips and tricks. It's not quite the same as the style guide, and I don't think any of the other doc pages covers this area, but I think we have a decent collection of things to avoid and beginner mistakes

[Koundinya Vajjha]

"Work always in maximal generality" would be a good rule too.

[Floris van Doorn]

About the original question: are the lines the same with set_option pp.instantiate_mvars false (in addition to pp.all true )? I have no particular reason why they wouldn't be, but there was another case where this option showed a difference when pp.all didn't.

[Sebastien Gouezel]

With set_option pp.instantiate_mvars false, I still get in the trace

[class_instances] (1) ?x_36 : @normed_space.{u uG} k G (@nondiscrete_normed_field.to_normed_field.{u} k _inst_1) _inst_6 := _inst_7
failed is_def_eq

while I have in the context

_inst_7 : @normed_space.{u uG} k G (@nondiscrete_normed_field.to_normed_field.{u} k _inst_1) _inst_6

[Sebastien Gouezel]

If someone wants to play with this weird instance search behavior, the branch is now available at #1112

[Sebastien Gouezel]

@Daniel Selsam You were looking for weird instance behavior. The one at the beginning of this thread is still puzzling for me. To sum it up: in analysis/normed_space/operator_norm.lean, there are the lines

/-- Continuous linear maps themselves form a normed space with respect to
    the operator norm. -/
instance to_normed_group : normed_group (E →L[𝕜] F) :=
normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_triangle, op_norm_neg⟩

/- The next instance should be found automatically, but it is not.
TODO: fix me -/
instance to_normed_group_prod : normed_group (E →L[𝕜] (F × G)) :=
continuous_linear_map.to_normed_group

I don't know why the second instance is not found by apply_instance. The instance trace search contains the line

[class_instances] (1) ?x_36 : @normed_space.{u uG} k G (@nondiscrete_normed_field.to_normed_field.{u} k _inst_1) _inst_6 := _inst_7
failed is_def_eq

while the context contains

_inst_7 : @normed_space.{u uG} k G (@nondiscrete_normed_field.to_normed_field.{u} k _inst_1) _inst_6

If everything is put in Type (or even in the same universe), then the issue disappears.

[Daniel Selsam]

@Sebastien Gouezel Thanks. I'll look into it, though it seems to be just an issue with the unifier, not the typeclass resolution procedure itself. Note that you can trace the failed is_def_eq with set_option trace.type_context.is_def_eq and set_option trace.type_context.is_def_eq_detail.

[Sebastien Gouezel]

This is way too big for my eyes. I was wondering if this is was a problem with the unifier, or with typeclass resolution feeding something weird to the unifier.

[Sebastian Ullrich]

@Sebastien Gouezel Reading the unifier log is an art. Could you put it in a gist/...?

[Sebastien Gouezel]

Done at https://gist.github.com/sgouezel/8357413e4c91f1092993c7a2c04ee112. 2821 lines, so not sure this helps...

[Daniel Selsam]

@Sebastien Gouezel Thanks. Can you please enable pp.all? We need to see the universes.

[Sebastien Gouezel]

Sure. It is at https://gist.github.com/sgouezel/be6d961c87d2c6bb017a8fba2417d229, with

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true
set_option pp.all true
set_option trace.class_instances true

[Sebastien Gouezel]

4169 lines now...

[Daniel Selsam]

@Sebastien Gouezel Thanks. The message is so long that it got truncated though. One last request: can you please do the same thing but with pp.universes instead of pp.all?

[Daniel Selsam]

(My system is configured for Lean4 so it is not convenient for me to generate these myself right now)

[Sebastien Gouezel]

Ah, I didn't spot it got truncated. New version at https://gist.github.com/sgouezel/11afeb220ab65f45f4565c1f05c25546 with

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true
set_option pp.universes true
set_option trace.class_instances true

And I am happy to give you any output you need (you're trying to help, after all!)

[Sebastien Gouezel]

3144 lines

[Sebastien Gouezel]

Another version where it fails on

instance to_normed_group_prod : normed_group (E →L[𝕜] (E × E)) :=
by apply_instance

is available at https://gist.github.com/sgouezel/1bde1320a31474311bb4f1331ee58960. There are just 2 universes instead of 4, so this is maybe easier to read.