another timeout

Stream: general

[Kevin Buzzard]

The perfectoid project currently compiles fine, according to Travis, but if I try it in VS Code I get deterministic timeouts! I have traced the issue back to VS Code feeding -T100000 to Lean (maximum number of memory allocations per task), but Travis not doing this.

If I have code which is timing out with -T100000 does this indicate that something is wrong with the code? Before, we had timeout issues which were fixed by making arbitrary universe changes. Maybe I'll try this now, but in general I am not sure what this means. I've seen my code give typeclass inference errors which could be fixed by changing the max depth, but this is the first time I've seen a timeout issue which could be fixed by changing the parameters.

[Scott Morrison]

Oh, I definitely get this when I let tactics go berserk. It's usually solved by splitting things into smaller lemmas.

[Kevin Buzzard]

I have managed to tame the timeouts but I don't think it's a tactic issue.

def presheaf_map {U V : opens (spa A)} (hUV : U ≤ V) :
  presheaf_value V → presheaf_value U :=
λ f, ⟨λ rd,
let TEMP := f.val in TEMP ⟨rd.val, set.subset.trans rd.2 hUV⟩,
--  f.val ⟨rd.val, set.subset.trans rd.2 hUV⟩, -- this times out with lean -T100000
λ rd1 rd2 h,
-- I do not particularly want to go into tactic mode right now
begin
  let TEMP2 := f.2 (rational_open_data_subsets.map hUV rd1)
    (rational_open_data_subsets.map hUV rd2) h,
  exact TEMP2,
  -- exact f.2 (rational_open_data... times out
  -- convert f.2 (rational_open_data... works
end⟩

This should be a purely term mode proof. The first problem is that f.val ⟨rd.val, set.subset.trans rd.2 hUV⟩ times out when applied directly; this let hack fixes the first timeout. The second timeout I solve in tactic mode (it's a prop) but it's the same story; a term should work, but exact fails and it's only convert or the let which save us. A convert can be used with the first timeout too, but this causes errors later in the file for some reason.

I would like to debug this further. I do not know what is going on at all. If this is happening because we have written bad code then I'd like to write better code but I don't know which code is bad. If this is happening because of some other reason I'd still like to know what is going on. I feel a bit helpless at the minute; I have no understanding why the first let changes anything. @Sebastian Ullrich @Mario Carneiro can either of you make some educated guesses about what is happening?

A completely compiled version of the perfectoid project, all the olean files, with current mathlib master, is available here:

wwwf.imperial.ac.uk/~buzzard/xena/perfectoid_20190513.tar

If you download this, and run lean --make in src the command returns very quickly with no output. The project is all compiled and all fine. Now open it in VS Code and in src/Spa.lean on line 720 there is a timeout, which can be fixed by changing -T100000 to a higher value in VS Code settings. Lean is working far too hard to compile this lemma. Changing f.val ⟨rd.val, set.subset.trans rd.2 hUV⟩, to let TEMP := f.val in TEMP ⟨rd.val, set.subset.trans rd.2 hUV⟩, fixes everything.

[Mario Carneiro]

what is the type of TEMP?

[Mario Carneiro]

and f and ⟨rd.val, set.subset.trans rd.2 hUV⟩

[Mario Carneiro]

Here's a working term mode proof:

def presheaf_map {U V : opens (spa A)} (hUV : U ≤ V)
  (f : presheaf_value V) : presheaf_value U :=
⟨_, λ rd1 rd2 h,
  (f.2 (rational_open_data_subsets.map hUV rd1)
    (rational_open_data_subsets.map hUV rd2) h : _)⟩

[Kevin Buzzard]

But what's going on? How is (blah : _) any different to blah?

[Kevin Buzzard]

This is my actual question. Is the point that your code is somehow better than my code in some intrinsic way -- I should never have written my code the way I wrote it? Or is the problem that I have made some ghastly types and the fact that they're difficult to manipulate is my fault and something should be changed? Or is the problem that Lean is not very good at something and you know how to work around the deficiency? What is actually happening?

[Mario Carneiro]

(blah : _) says "ignore the expected type here, figure out the type of blah first and then unify with the goal"

[Kevin Buzzard]

But doesn't (blah) also say that?

[Mario Carneiro]

blah says "use the expected type to elaborate blah"

[Mario Carneiro]

usually this is a good thing, but occasionally it gives a bad result

[Kevin Buzzard]

Aah. So the elaboration process of a term usually takes the type of this term into account, and this is a workaround to stop it doing this?

[Kevin Buzzard]

Running Lean with -T200000 succeeds, by the way -- so everything is consistent; this is just, for some reason, a way of making Lean succeed quicker.

[Mario Carneiro]

I think I figured out the problem (and I guess you could class it as "lean is not very good at something"). If I start with

def presheaf_map {U V : opens (spa A)} (hUV : U ≤ V)
  (f : presheaf_value V) : presheaf_value U :=
begin
  refine ⟨λ rd, _, _⟩,
  have := f.val,
end

I see that the goal has type r_o_d_completion (rd.val), and the have has type Π (rd : rational_open_data_subsets V), r_o_d_completion (rd.val). The obvious solution is to plug rd into f.val but this doesn't work because rd : rational_open_data_subsets U instead

[Kevin Buzzard]

I am deeply sorry about r_o_d_completion by the way. I got sick of typing rational_open_data. It's on my job list to change it to something more sensible.

[Mario Carneiro]

But the problem is that when you use refine f.val _ here lean thinks "okay, let's make r_o_d_completion (rd.val) =?= r_o_d_completion (?m.val). I know, let's try to make all the arguments to r_o_d_completion the same and rd =?= ?m. So I have to prove rational_open_data_subsets U =?= rational_open_data_subsets V." Lean then gets lost unfolding your tower of definitions, hoping that U doesn't actually appear in the definition so that rational_open_data_subsets U is defeq to rational_open_data_subsets V

[Kevin Buzzard]

but this doesn't work because rd : rational_open_data_subsets U instead

Right, that's what all the set.subset.trans rd.2 hUV is about.

[Kevin Buzzard]

Oh you have maybe completely debugged this. Many thanks as ever! Did you use some trace tools or was this just pure thought? I think it is worth my while thinking about what you're saying here. This is a trick I don't know yet.

[Mario Carneiro]

This is often the place where the :_ trick works

[Mario Carneiro]

I usually see this when you use congr_arg, which is another place where the heuristic f x =?= g y => f =?= g /\ x =?= y leads lean astray

[Kevin Buzzard]

I knew the maths I was formalising in the project (although as Patrick pointed out I didn't know all of the details in several places), but the timeouts were scary. Before we finished the project I was sometimes thinking "you know, Lean actually can't do this can it". I've been forced to wrestle with several timeouts.

[Kevin Buzzard]

But Lean always came through in the end, although the solutions were a bit random.

[Kevin Buzzard]

On line 744 of src/valuation/field.lean if you change Type u to Type* then Lean times out. That was the worst one. I have no idea why.

[Mario Carneiro]

For that one, I tried

[Mario Carneiro]

begin
  refine valuation.completion_extend _,
  -- try_for 10000 {
  --   exact valuation.completion_extend (valuation_field.canonical_valuation v)
  -- }
end

and it says

invalid type ascription, term has type
  valuation (ring_completion (valued_ring ?m_3 ?m_5)) ?m_1 : Type (max ? ?)
but is expected to have type
  valuation (ring_completion (valuation_field v)) (value_group v) : Type ?

[Mario Carneiro]

what is the relation between valuation_field and valued_ring?

[Mario Carneiro]

I see, valued_ring is a wrapper. This is not being very nice to lean, it has no idea what to unwrap here. I'm guessing valuation_field is much more complicated, so lean's heuristics say to unfold the more complicated one and it gets lost

[Kevin Buzzard]

That wrapper caused us problems.

[Kevin Buzzard]

It's funny that changing the universe made it work though.

[Kevin Buzzard]

In fact even with_zero caused us problems (a wrapper for option) -- we used with_zero a lot and at some point we seriously considered redefining it by just copying some option code; the option kept leaking out.

[Mario Carneiro]

have you tried printing the definition? It makes me weep to see

[Kevin Buzzard]

The definition of what?

[Mario Carneiro]

noncomputable def valuation_on_completion {R : Type u} [comm_ring R] (v : valuation R Γ) :
  valuation
    (ring_completion
      (valuation.valuation_field v))
    (value_group v) :=
valuation.completion_extend (valuation_field.canonical_valuation v)

set_option pp.all true
#print valuation_on_completion

[Mario Carneiro]

oh, actually that's not so bad

[Mario Carneiro]

this version looks much worse

begin
  have := valuation.completion_extend (valuation_field.canonical_valuation v),
  dunfold valued_ring at this,
  exact this
end

[Mario Carneiro]

I need a deduplicating pp printer

[Kevin Buzzard]

I don't really understand what you're saying.

[Mario Carneiro]

These printouts always make expressions look worse than they are

[Kevin Buzzard]

We just typed in normal maths

[Mario Carneiro]

but if expressions are much much worse under the hood than they appear then that's a bad sign

[Mario Carneiro]

and stuff like timeouts is just the symptom

[Mario Carneiro]

the moral of the story is "don't make lean work too hard"

[Mario Carneiro]

sometimes you accidentally ask lean to do something silly and then you get a timeout for no reason

[Kevin Buzzard]

We're just extending a valuation on a ring to a valuation on its completion. What's not to like?

[Kevin Buzzard]

You're saying we should be looking at our terms to see if any of them are getting suspiciously large?

[Kevin Buzzard]

But what can we do to stop this happening?

[Kevin Buzzard]

You shouldn't have unfolded our wrapper!

[Mario Carneiro]

The reason this happened was the first error message I posted:

invalid type ascription, term has type
  valuation (ring_completion (valued_ring ?m_3 ?m_5)) ?m_1 : Type (max ? ?)
but is expected to have type
  valuation (ring_completion (valuation_field v)) (value_group v) : Type ?

I think the problem is not actually valued_ring itself but all the instances on it

[Mario Carneiro]

valuation_field has a bunch of instances, and valued_ring has different instances, and a lot of unfolding needs to happen to see they are the same

[Mario Carneiro]

Why are you applying a theorem which isn't obviously applicable?

[Mario Carneiro]

what's the logic here? How does the stuff on valuation_field relate to valued_ring?

[Johan Commelin]

A valued ring is a ring together with a valuation. This valuation induces a topology, etc...

A valuation field is a particular example.

[Mario Carneiro]

maybe you need a typeclass for that

[Mario Carneiro]

rather than a type constructor

[Mario Carneiro]

i.e. valued_ring R v is a prop assertion that says that a topological ring is generated by a valuation

[Mario Carneiro]

that way you can assert that valuation_field is a valued ring, even though it isn't literally constructed as "adjoin this valuation to the ring"

[Mario Carneiro]

aka stricklandize it

[Johan Commelin]

Or we change it to valued_ring.mk? And we have class

class valued_ring (R : Type*) [ring R] :=
(v : valuation R Γ)

[Mario Carneiro]

I was going to say that, and then I realized that the gamma will give you problems

[Kevin Buzzard]

Sorry, my exam just finished and I had to pick up several hundred pieces of paper

[Kevin Buzzard]

With a random ring R there are lots of valuations, so lots of topologies. But given a valuation v we wanted a topology on R so we went with a wrapper because topological_space is a class I guess.

[Kevin Buzzard]

invalid type ascription, term has type
  valuation (ring_completion (valued_ring ?m_3 ?m_5)) ?m_1 : Type (max ? ?)
but is expected to have type
  valuation (ring_completion (valuation_field v)) (value_group v) : Type ?

valued_ring ?m_3 ?m_5 is just by definition ?m_3 but this is all about topology, and I can't put a topology on ?m_3 because it depends on ?m_5

[Kevin Buzzard]

We mathematicians need to learn the right way to think about this stuff.

[Johan Commelin]

@Mario Carneiro Can you formulate a general principal here? Why is valued_ring a bad type wrapper, but multiplicative a good one?

[Kevin Buzzard]

but if expressions are much much worse under the hood than they appear then that's a bad sign

Do you mean "much worse after you've unfolded absolutely everything" or something else?

[Mario Carneiro]

I mean much worse explicitly, before any unfolding

[Mario Carneiro]

or after any unfolding that needs to be done in the moment

[Kevin Buzzard]

like unfolding valued_ring.

[Mario Carneiro]

valued_ring is not a bad type wrapper, but it's not sufficient for all things. In particular, this is the same problem we've seen before with localization. Sometimes you want to perform the construction, and sometimes you want to say that an independently constructed type is isomorphic to the construction

[Mario Carneiro]

quotient is another example of this

[Mario Carneiro]

It doesn't apply if the type isn't actually quotient bla

[Kevin Buzzard]

I was going to say that, and then I realized that the gamma will give you problems

Because of universe issues or because we just need to input it directly with

class valued_ring (R : Type u) [ring R] :=
(Γ : Type u)
[totally_ordered_group Γ] -- or whatever we called it
(v : valuation R Γ)

[Mario Carneiro]

In this case you have valued_ring R v, the construction, and you want to apply it to valuation_field v, which after unfolding is not defined as valued_ring bla bla

[Kevin Buzzard]

There's something a bit wrong. Those v's are perhaps not the same.

[Kevin Buzzard]

valuation_field v has got a valuation on it but it's not v

[Mario Carneiro]

right, I'm not saying they are

[Kevin Buzzard]

Oh Ok

[Kevin Buzzard]

No, you're supposed to be unfolding valued_ring here, not valuation_field

[Mario Carneiro]

I'm saying that valuation_field v =?= valued_ring ?m1 ?m2 doesn't have a solution by unfolding valuation_field

[Kevin Buzzard]

Right!

[Kevin Buzzard]

Unfold the other one.

[Mario Carneiro]

Even if you unfold valued_ring here, it doesn't solve the problem of all the instances

[Kevin Buzzard]

I think that you're saying that if we're going to use a wrapper type, then we must be very careful to wrap everything up.

[Mario Carneiro]

valued_ring has a bunch of instances on it, a uniform structure and so on - does valuation_field v have the same structure?

[Kevin Buzzard]

No

[Mario Carneiro]

then you shouldn't apply this theorem

[Kevin Buzzard]

Hmm...we could put those structures on it.

[Kevin Buzzard]

We wrote the wrapper because for a general ring R and a general valuation v, we definitely don't want R to inherit the uniform structure from v, because often R will be fixed and v will change

[Mario Carneiro]

My guess is you want to prove is_valued_ring (valuation_field v) (valuation_field.canonical_valuation v)

[Kevin Buzzard]

valuation_field v is exactly the point where we've manipulated the ring so much that now we'll never put another valuation on it.

[Kevin Buzzard]

None of this conversation is about mathematics, in some sense.

[Mario Carneiro]

It's proof engineering stuff

[Kevin Buzzard]

So I'm a beginner here.

[Kevin Buzzard]

Yes exactly.

[Mario Carneiro]

You can have valued_ring R v as before, and prove is_valued_ring (valued_ring R v) v

[Kevin Buzzard]

So we keep the wrapper?

[Mario Carneiro]

and then completion_extend has the type valuation (ring_completion K) Γ where is_valued_ring K v

[Mario Carneiro]

I don't know if you need the wrapper, but I imagine that sometimes you just have a ring and need to put a valuation on it

[Mario Carneiro]

rather than asserting that a pre-existing topological ring is generated by a valuation

[Kevin Buzzard]

That's right.

[Mario Carneiro]

so you want both

[Kevin Buzzard]

In fact I think that always we just have the ring and need to put a topology on it coming from a valuation.

[Kevin Buzzard]

That's why we used a wrapper -- because the valuation can vary, but topological_space is a class.

[Mario Carneiro]

I think that's what you thought originally and that's why the code looks like it does, but it turns out not to be the case

[Mario Carneiro]

because valuation_field is clearly not of that form

[Johan Commelin]

It is of that form mathematically

[Johan Commelin]

But not Lean-ny

[Kevin Buzzard]

valuation_field was a field that didn't have a valuation for most of the projects, and then I realised far too late (because I never wrote a proper roadmap) that we needed a topology on it.

[Mario Carneiro]

and that's what is_valued_ring is for, to say "this ring is generated by this valuation"

[Mario Carneiro]

You might also consider writing valuation_field so it has the form valued_ring bla bla, but that will affect other things

[Kevin Buzzard]

Then Patrick found the part of Bourbaki that did what we wanted, and worked in what a library-builder would say was the correct generality: given a valuation on a ring, the ring gets a topology, and the valuation extends to the completion of the ring.

[Johan Commelin]

I guess an alternative would be to rename valuation_field to valuation_field.aux and then define valuation_field as valued_ring (valuation_field_aux _) _

[Mario Carneiro]

I thought about that too, but there are some nontrivial theorems here about how the topological ring structure is preserved

[Johan Commelin]

But I guess that Mario is saying that the predicate approach is better (because more flexible?)

[Kevin Buzzard]

I suspect that the only time we ever apply the valued_ring stuff is to valuation_field v (which is a field), however there were a bunch of general theorems about the topology on a ring induced by a valuation in Bourbaki and Patrick formalised those.

[Mario Carneiro]

the predicate approach means that the instances are not impacted - they are just the valuation_field instances

[Kevin Buzzard]

So Patrick was faced with the dilemma of having a ring R, and a valuation v on R, and he wanted to talk about the induced topology on R. So the wrapper was born.

[Kevin Buzzard]

This was almost certainly the correct generality for Bourbaki. But in retrospect it was more than we needed for our application.

[Kevin Buzzard]

Thanks for all these comments. I'll digest them slowly.