Cute instance loop

Stream: general

[Sebastien Gouezel]

I just ran into a cute instance loop. A : if K is a field, it is a (finite-dimensional) vector space over itself. B : if K is a complete normed field, then any finite dimensional vector space over K is complete (I have just completed the proof of this fact). Combining these two, to prove the completeness of a normed field K, Lean will try to use the completeness of K, and loop.

My problem is that these two instances are natural and useful, and I would like to keep both of them. In Lean 3, if I understand correctly, I can't, and I should not register B as an instance. @Daniel Selsam, can you confirm that this will not be a problem in Lean 4? (Another problem with this instance in Lean 3, by the way, is that to prove the completeness of E Lean will start to look for an instance of vector_space ?m1 E for whatever ?m1, and then it will try all the fields it knows about, and there are tons of them -- will this also be OK in Lean 4?)

[Johan Commelin]

Wait... so given a normed_field K that is complete K, you ask Lean to prove complete K, and it is like... yeah I know that K is a fin.dim vector space over this field K. So I can prove that K is complete, if this field K is a complete normed field. Hmmm... it's clear that K is a normed field, because the instance is staring me right in the face. Now let's see if I can prove that K is complete. Ooh, I know that K is a fin.dim vector space over... ... ...

[Johan Commelin]

Can't instances in the local context have some sort of infinite priority over instances coming from the library?

[Johan Commelin]

Oooh... never mind. It's more complicated.
If you don't have complete K in your context, and you still want to infer complete K for some reason (maybe it is a finite field extension of something complete)... then you can still run into this loop.

[Johan Commelin]

So somehow complete_of_fin_dim_over_complete should never be tried for vector space = base field.

[Johan Commelin]

So we need @[inference_hint := assert (¬ (E = K))]

[Sebastien Gouezel]

Yes, this is very funny. For instance, asking complete_space ℚ loops forever (or rather, it hits instance_max_depth quickly). Of course, I will never ask Lean to prove that ℚ is complete, but this might show up in some instance search if Lean is trying the wrong path.

[Mario Carneiro]

Could you show the types of these instances?

[Mario Carneiro]

Whichever instance involves looking for a field metavariable sounds like it shouldn't be an instance

[Mario Carneiro]

I don't think lean should always have every true relation between classes as an instance. It's not capitulation to say that some of them should be invoked explicitly

[Mario Carneiro]

If I understand correctly, instance A is vector_space K K <- field K, which seems fine, and B is complete V <- complete_normed_field K, vector_space K V which does not look fine because the K is free

[Mario Carneiro]

If B was complete_vector_space K V it wouldn't be a problem

[Mario Carneiro]

But given that completeness is a property only of V (and its metric structure), you should already "know" that it is complete without having to do proof search to find out. That is, I would expect instances of the form complete V for every concrete V (like real), or it should be in the context. Perhaps we want to prove that real is a complete space by proving that it is a vector space over another complete field, in which case we would apply that lemma (and supply the choice of K), but it's not a search lean should be doing on its own

[Johan Commelin]

Hmmm... you've told us this fact many times by now. For some reason it catches me by surprise time and again. I wonder when I will finitely learn this principle.

[Sebastien Gouezel]

I know, this is why I did not register it as an instance. But I find this a little bit sad, as this is an important, useful and nontrivial way to prove that a space is complete. Here is the type of the theorem

theorem finite_dimensional.complete : ∀ {𝕜 : Type u} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u} [_inst_2 : normed_group E]
[_inst_3 : normed_space 𝕜 E] [_inst_6 : complete_space 𝕜] [_inst_7 : finite_dimensional 𝕜 E], complete_space E

[Sebastien Gouezel]

A way out could be to define a class complete_nondiscrete_normed_field extending both nondiscrete_normed_field and complete_space, and use it in the assumption. What do you think of this approach?

[Mario Carneiro]

But I find this a little bit sad, as this is an important, useful and nontrivial way to prove that a space is complete

This is the sentiment I hope to combat by saying "it's not capitulation". Just because it's true doesn't mean it's a good way for lean to find out that a space is complete

[Mario Carneiro]

Are there any examples where this is the desired way to prove completeness of a space?

[Mario Carneiro]

I think this is a nice theorem, and the mere fact that it is entirely about typeclasses doesn't qualify it as an instance. There are plenty of other nice theorems which are not instances, it's not a second class status

[Mario Carneiro]

complete_nondiscrete_normed_field doesn't solve the problem, since it is only merging two assumptions on K without addressing the fact that K doesn't appear in the consequent complete_space E

[Sebastien Gouezel]

This is definitely used to prove completeness. For instance, if you want to check completeness of euclidean space, you can either make a messy computation with a clever blend of epsilons and Cauchy-Schwarz, or apply directly the theorem. More importantly, I want to write theorems with an assumption [finite_dimensional R E] and be able to use the completeness of E in the proof. Of course, I can put haveI : complete_space E := ... at the beginning of each such proof, but it will be tedious to say the least.

[Sebastien Gouezel]

complete_nondiscrete_normed_field solves the looping problem, but I agree it does not solve the fact that there would be a metavariable in instance search.

[Mario Carneiro]

Is R the reals?

[Mario Carneiro]

I would solve that by having a class euclidean_space E that implies finite_dimensional R E and complete_space E

[Sebastien Gouezel]

Yes, sorry for the lack of unicode. Complex numbers and p-adics are also good examples.

[Mario Carneiro]

For those, you just prove complete_space C and complete_space Q_[p]

[Sebastien Gouezel]

Yes, but this looks like a useless class as it is exactly equivalent to finite_dimensional R E.

[Sebastien Gouezel]

What I mean is that I will want to use completeness of finite-dimensional spaces over C and Q_p.

[Mario Carneiro]

you could also take it as an assumption, of course

[Mario Carneiro]

this would be the obviously correct way to do it if complete_space had data

[Mario Carneiro]

What about complete_fd K E?

[Mario Carneiro]

seems like this isn't much different from having a class vector_space (which is completely useless since it means the same as module)

[Sebastien Gouezel]

You mean, two typeclass assumptions finite_dimensional K E and complete_space E, while the second one is implied by the first one? This looks like a hackish workaround instead of a real solution, but I agree it would work fine. I think I would rather go for the explicit instance at the beginning of each proof.

[Mario Carneiro]

complete_fd is the conjunction of those classes

[Sebastien Gouezel]

Yes, and therefore completely equivalent to finite_dimensional K E!

[Mario Carneiro]

These have data, though, don't they?

[Mario Carneiro]

complete_space E has to have a metric and stuff

[Sebastien Gouezel]

The difference with vector_space is that this class is just here to make mathematicians comfortable.

[Sebastien Gouezel]

No, complete_space is a mixin over metric_space, without data.

[Mario Carneiro]

hm, maybe fix that then

[Mario Carneiro]

it's not mixin very well

[Sebastien Gouezel]

The topological hierarchy has a spine topological_space <- uniform_space <- metric_space, and additional mixins specifying zillions of properties. It seems to work pretty well!

[Mario Carneiro]

If you want to build stuff on top of a mixin though, it needs to be merged in

[Sebastien Gouezel]

I don't get it. We have a lot of theorems with assumptions [topological_space \alpha] [t1_space \alpha] or [metric_space \alpha] [second_countable \alpha] [complete_space \alpha]. There are so many possibilitiesof combination of the mixins that I don't see how we could merge anything.

[Mario Carneiro]

Those are all over one type though. it's not like [complete_space A -> complete_space B] is a class

[Mario Carneiro]

but that's basically what finite_dimensional A B is doing here

[Sebastien Gouezel]

What I get from this discussion is the confirmation that my theorem finite_dimensional.complete should not be an instance, because of the metavariable in the search, and that I should rather instantiate it explicitly when I need it. Is that reasonable?

[Mario Carneiro]

Yes, that should work

[Mario Carneiro]

Why are these even typeclasses? They look like hypotheses to me

[Sebastien Gouezel]

You mean, finite_dimensional K E? It is a typeclass in the current linear algebra framework. This seems reasonable as then it can be derived automatically for products, for function types over a fintype, for K itself, and so on.

[Kevin Buzzard]

I love that a mathematician and a computer scientist are having a chat about a completely basic theorem but the chat actually has some content. Why hasn't this question been solved 20 years ago? Is there an analogous question for this theorem in Coq and Isabelle, and if so, then do the answers just not help at all? Or did they not get as far as this theorem yet?

[Kevin Buzzard]

When we start on local fields, which we'll have to do at some point, the first thing we'll need is that a finite dimensional field extension of the p-adic numbers is complete.

[Mario Carneiro]

I mean topological_property A

[Mario Carneiro]

They aren't being used to define anything, and they are rather more like mathematical assumptions than structures

[Sebastien Gouezel]

You know, this is not really a trivial theorem. I am sure it is not in Isabelle. I don't think it is in Coq either, as they don't have a lot of topology. The proof over real numbers is in the undergraduate cursus, and easy by compactness, but the proof for complete fields is really harder, by induction on the dimension. By the way, for the proof to compile in reasonable time, I had to add

local attribute [instance, priority 10000] pi.module normed_space.to_vector_space
  vector_space.to_module submodule.add_comm_group submodule.module
  linear_map.finite_dimensional_range Pi.complete nondiscrete_normed_field.to_normed_field

to help Lean a little bit!

[Mario Carneiro]

see, I don't want lean to choke on this instance

[Sebastien Gouezel]

For topological_property A, it is the same: these properties are typically derived automatically for products, function spaces, and so on.

[Mario Carneiro]

If this theorem were recast as a structural rule it would be unproblematic. Something like complete_space K -> complete_space (K^n)

[Mario Carneiro]

I guess this also has to do with the earlier move away from modules having a unique base field

[Sebastien Gouezel]

K^n comes with some metric (the sup metric), for which completeness is true and easy. The point of the theorem (and what makes it nontrivial) is that you get completeness whatever the metric.

[Mario Carneiro]

sounds like a search to me

[Kevin Buzzard]

You know, this is not really a trivial theorem.

I totally agree -- by "basic" I mean everyone knows it and assumes it.

[Sebastien Gouezel]

I would be very interested to read the thoughts of @Daniel Selsam about how we should do this in Lean 4.

[Mario Carneiro]

I mean, if you really want lean to do the search, I think you can do so, but you need a bunch more typeclasses to guide the search better

[Mario Carneiro]

I don't know what the best in-principle solution is, since I don't really know what you expect it to do here

[Mario Carneiro]

do you want every complete_space to search for a vector space instance, a field and all that? complete_spaces don't even have to be algebraic

[Mario Carneiro]

If we are just reasoning forward from the context then this seems like a good forward reasoning rule

[Mario Carneiro]

I don't know if lean 4 supports that but I would really like to see forward reasoning in typeclass search

[Sebastien Gouezel]

If Lean is quick enough to do the silly search in all cases, realize very quickly if my space is not algebraic, and go on a better path if needed, yes, I would be very happy. If this is not possible, I can live with it and give the instance myself :)

[Mario Carneiro]

Unfortunately I think that the lean 4 algorithm won't help here, because the failing search really is infinite

[Mario Carneiro]

There are an infinite number of fields, and an infinite number of failing assumptions finite_dimensional (real x real x ... x real) E

[Mario Carneiro]

actually those aren't fields, but I can't be bothered to think of an actual field constructor

[Sebastien Gouezel]

algebraic_closure (algebraic_closure (... algebraic_closure (C)))))

[Mario Carneiro]

The algorithm that I think would actually work would be to see that complete_space R and finite_dimensional R E are in the context, and derive complete_space E; then search for complete_space E and find it in the context

[Sebastien Gouezel]

Yes, such a forward search would be very useful!

[Mario Carneiro]

Forward reasoning also works really well for "parent" instances, like if I want has_add G I can start from add_group G and populate the context with all subinstances of it (add_monoid G, has_add G, has_zero G) followed by the usual backward search

[Mario Carneiro]

rather than trawling the entire algebraic hierarchy

[Daniel Selsam]

I would be very interested to read the thoughts of Daniel Selsam about how we should do this in Lean 4.

@Sebastien Gouezel Can you please share a minimal, self-contained example that loops? For this purpose, you can just make the classes empty as in https://github.com/leanprover/lean4/blob/master/tests/elabissues/typeclass_triggers_typeclass.lean

In general, the rule in Lean 4 is as follows:

- If you literally reach the same goal twice (upto alpha equivalence), Lean4 will detect and do the right thing.
- You can still cause typeclass resolution to run forever in some cases, but to do this the generated goals must be getting bigger and bigger.

[Sebastien Gouezel]

Here is the minimal example:

class Field (K : Type*)

class VectorSpace (K : Type*) [Field K] (E : Type*)

instance VectorSpaceSelf (K : Type*) [Field K] : VectorSpace K K := by constructor

class CompleteSpace (α : Type*)

instance bad (K : Type*) [Field K] (E : Type*) [VectorSpace K E] [CompleteSpace K] : CompleteSpace E :=
  by constructor

instance loops (K : Type*) [Field K] : CompleteSpace K := by apply_instance

loops should fail as there is no way to get completeness out of thin air, but Lean 3 will loop on it. It will try to apply the instance bad (as it sees K as a vector space over itself), and for this it will need the completeness of K, and therefore it loops. From what you say, your Lean 4 algorithm should succeed on that one, which is very nice.

Then, there is a second potential issue. When applying the instance bad, Lean knows the vector space E (from the type of the desired conclusion), but it does not know which field to choose, so it will try every field it has at its disposal. In this example, it can not go wild. But what happens if one adds, say,

def AlgebraicClosure (K : Type*) [Field K] : Type* := K

instance AlgebraicClosure.Field (K : Type*) [Field K] : Field (AlgebraicClosure K) := by constructor

instance loops_even_more (K : Type*) [Field K] : CompleteSpace K := by apply_instance

Here, I guess loops_even_more will also fail in Lean 4 as it will try to apply bad to more and more complicated fields, constructed by iterated algebraic closure. Is that indeed the case?

[Daniel Selsam]

Thanks. The first example will fail quickly in Lean4 since it is the same goals being solved over and over again, and Lean4 will detect this and do the right thing.

[Johan Commelin]

I hope that there is also a cheap heuristic that gives the loop in the second example a very low priority

[Johan Commelin]

Sometimes you need to alternate some constructions several times in a row, but it isn't very common. One example is:

• Take the field Q. this field is not algebraically closed, and not complete
• complete for the p-adic valuation to get Q_p. this field is not algebraically closed, it is complete
• take the algebraic closure to get Q_p-bar. this field is algebraically closed, it is not complete
• take the completion, to get C_p. this field is algebraically closed and it is complete.

However, I certainly don't expect the typeclass system to figure out such things for me. So in general, I would like the type class system to be very hesitant to apply such constructors multiple times.

[Daniel Selsam]

(deleted)

[Daniel Selsam]

(deleted)

[Daniel Selsam]

(deleted)

[Sebastien Gouezel]

Great! I was afraid it would do the following: try to apply bad ?K K where ?K is an unknown complete field over which one would like K to have a vector space structure. Since it doesn't know which field to use, what does Lean4 do to fill the meta-variable ?K? Does it try all the fields it knows about, like AlgebraicClosure K, or is it more clever?

[Sebastien Gouezel]

For instance, in Lean 3,

instance works_fine (K : Type*) [Field K] [CompleteSpace (AlgebraicClosure K)]
  (E : Type*) [VectorSpace (AlgebraicClosure K) E] : CompleteSpace E := by apply_instance

works fine, so Lean3 is clever enough to try to fill the metavariable with AlgebraicClosure K (probably using what it sees in the context?)

[Daniel Selsam]

What I wrote before was wrong. Lean4 will indeed still loop in your second example. I apologize for the confusion.

[Sebastien Gouezel]

Would it be reasonable to change the behavior to the following one: if one encounters an instance in which there are Type variables which can not be inferred directly, then

• either there is something in the context which matches the instance, then use it
• or fail

This would prevent the search from getting completely crazy, and still it would allow instances with Type metavariables, which can be handy in situations like the one discussed in the above thread. Are there situations where this is obviously wrong? (Or, as a middle ground, could one have an attribute on instances to say that they should follow this behavior -- all this is for Lean4, of course).

[Sebastien Gouezel]

Or an attribute instance_search.restricted or whatever, that one could set to choose the behavior between the current one and the less recursive one?

[Daniel Selsam]

How about just having a maxGoalSize flag, and refusing to consider any intermediate goals beyond that size? This works for your second example, and fails quickly even when set very high. Con: it would not work well if there were a combinatorial number of pretty-big-but-not-too-big undesired goals.

[Daniel Selsam]

Otherwise typeclass resolution might still run forever when it is e.g. bigger Nats that are being created, as opposed to bigger types.

[Sebastien Gouezel]

Or even max recursion size. Currently, when the maximal recursion depth is reached, instance search fails with an error message. It could instead fail on the branch it is, and resume the search on the next branch. I am still afraid that this or your maxGoalSize could lead to a combinatorial explosion.

In Lean3, we avoid completely instances with Type metavariables because of this risk of combinatorial explosion. I think only allowing them when one can solve them from the context would solve most of our use cases.

[Daniel Selsam]

@Sebastien Gouezel See https://github.com/leanprover/lean4/blob/9a7354633a18ce73039549cfb4a019fe74e7d09f/tests/elabissues/typeclass_nested_validate.lean for more analysis, suggested workaround, and tentative plan for Lean4.

[Sebastien Gouezel]

That's extremely clever!

[Johan Commelin]

@Daniel Selsam That's a really nice idea. And if I understand correctly, we can even try to use this already in Lean 3. That's cool.