Zulip Chat Archive

Stream: general

Topic: Cute instance loop


Sebastien Gouezel (Nov 07 2019 at 10:14):

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 (Nov 07 2019 at 10:29):

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 (Nov 07 2019 at 10:38):

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

Johan Commelin (Nov 07 2019 at 10:39):

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 (Nov 07 2019 at 10:40):

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

Johan Commelin (Nov 07 2019 at 10:43):

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

Sebastien Gouezel (Nov 07 2019 at 10:48):

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 (Nov 07 2019 at 11:14):

Could you show the types of these instances?

Mario Carneiro (Nov 07 2019 at 11:15):

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

Mario Carneiro (Nov 07 2019 at 11:17):

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 (Nov 07 2019 at 11:19):

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 (Nov 07 2019 at 11:20):

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

Mario Carneiro (Nov 07 2019 at 11:24):

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 (Nov 07 2019 at 11:47):

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 (Nov 07 2019 at 12:22):

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 (Nov 07 2019 at 12:23):

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 (Nov 07 2019 at 12:29):

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 (Nov 07 2019 at 12:29):

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

Mario Carneiro (Nov 07 2019 at 12:32):

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 (Nov 07 2019 at 12:34):

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 (Nov 07 2019 at 12:36):

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 (Nov 07 2019 at 12:37):

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 (Nov 07 2019 at 12:37):

Is R the reals?

Mario Carneiro (Nov 07 2019 at 12:37):

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

Sebastien Gouezel (Nov 07 2019 at 12:38):

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

Mario Carneiro (Nov 07 2019 at 12:38):

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

Sebastien Gouezel (Nov 07 2019 at 12:38):

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

Sebastien Gouezel (Nov 07 2019 at 12:39):

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

Mario Carneiro (Nov 07 2019 at 12:39):

you could also take it as an assumption, of course

Mario Carneiro (Nov 07 2019 at 12:40):

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

Mario Carneiro (Nov 07 2019 at 12:41):

What about complete_fd K E?

Mario Carneiro (Nov 07 2019 at 12:42):

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 (Nov 07 2019 at 12:42):

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 (Nov 07 2019 at 12:42):

complete_fd is the conjunction of those classes

Sebastien Gouezel (Nov 07 2019 at 12:43):

Yes, and therefore completely equivalent to finite_dimensional K E!

Mario Carneiro (Nov 07 2019 at 12:43):

These have data, though, don't they?

Mario Carneiro (Nov 07 2019 at 12:43):

complete_space E has to have a metric and stuff

Sebastien Gouezel (Nov 07 2019 at 12:43):

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

Sebastien Gouezel (Nov 07 2019 at 12:44):

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

Mario Carneiro (Nov 07 2019 at 12:44):

hm, maybe fix that then

Mario Carneiro (Nov 07 2019 at 12:44):

it's not mixin very well

Sebastien Gouezel (Nov 07 2019 at 12:45):

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 (Nov 07 2019 at 12:46):

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

Sebastien Gouezel (Nov 07 2019 at 12:47):

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 (Nov 07 2019 at 12:49):

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

Mario Carneiro (Nov 07 2019 at 12:49):

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

Sebastien Gouezel (Nov 07 2019 at 12:52):

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 (Nov 07 2019 at 12:53):

Yes, that should work

Mario Carneiro (Nov 07 2019 at 12:53):

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

Sebastien Gouezel (Nov 07 2019 at 12:55):

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 (Nov 07 2019 at 12:55):

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 (Nov 07 2019 at 12:56):

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 (Nov 07 2019 at 12:57):

I mean topological_property A

Mario Carneiro (Nov 07 2019 at 12:58):

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

Sebastien Gouezel (Nov 07 2019 at 12:59):

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 (Nov 07 2019 at 12:59):

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

Sebastien Gouezel (Nov 07 2019 at 13:00):

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

Mario Carneiro (Nov 07 2019 at 13:01):

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

Mario Carneiro (Nov 07 2019 at 13:02):

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

Sebastien Gouezel (Nov 07 2019 at 13:02):

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 (Nov 07 2019 at 13:03):

sounds like a search to me

Kevin Buzzard (Nov 07 2019 at 13:04):

You know, this is not really a trivial theorem.

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

Sebastien Gouezel (Nov 07 2019 at 13:04):

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

Mario Carneiro (Nov 07 2019 at 13:04):

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 (Nov 07 2019 at 13:06):

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 (Nov 07 2019 at 13:06):

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 (Nov 07 2019 at 13:08):

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

Mario Carneiro (Nov 07 2019 at 13:08):

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

Sebastien Gouezel (Nov 07 2019 at 13:09):

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 (Nov 07 2019 at 13:10):

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

Mario Carneiro (Nov 07 2019 at 13:12):

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 (Nov 07 2019 at 13:12):

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

Sebastien Gouezel (Nov 07 2019 at 13:13):

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

Mario Carneiro (Nov 07 2019 at 13:14):

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 (Nov 07 2019 at 13:16):

Yes, such a forward search would be very useful!

Mario Carneiro (Nov 07 2019 at 13:17):

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 (Nov 07 2019 at 13:17):

rather than trawling the entire algebraic hierarchy

Daniel Selsam (Nov 07 2019 at 14:45):

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 (Nov 07 2019 at 15:08):

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 (Nov 07 2019 at 15:22):

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 (Nov 07 2019 at 15:25):

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

Johan Commelin (Nov 07 2019 at 15:30):

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 (Nov 07 2019 at 15:34):

(deleted)

Daniel Selsam (Nov 07 2019 at 15:44):

(deleted)

Daniel Selsam (Nov 07 2019 at 15:45):

(deleted)

Sebastien Gouezel (Nov 07 2019 at 15:46):

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 (Nov 07 2019 at 15:51):

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 (Nov 07 2019 at 16:14):

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

Sebastien Gouezel (Nov 07 2019 at 17:26):

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 (Nov 07 2019 at 17:39):

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 (Nov 07 2019 at 17:46):

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 (Nov 07 2019 at 17:49):

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 (Nov 07 2019 at 18:09):

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 (Nov 07 2019 at 23:57):

@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 (Nov 08 2019 at 07:01):

That's extremely clever!

Johan Commelin (Nov 08 2019 at 09:09):

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


Last updated: Dec 20 2023 at 11:08 UTC