another really horrible timeout

Stream: general

[Kevin Buzzard]

Found by Amelia:

import field_theory.is_alg_closed.algebraic_closure

variables (K : Type*) [field K] (Γ₀ : Type*)
  [linear_ordered_comm_monoid_with_zero Γ₀]

def hmm : valuation (algebraic_closure K) Γ₀ := sorry -- times out

Changing def hmm to example makes it work fine, exactly as in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/crazy.20time-out/near/263470182 . In particular all the typeclasses are fine. Has there been some change recently which is causing these timeouts?

[Eric Wieser]

I thought that def and example were indistinguishable!

[Kevin Buzzard]

Aah -- the thing they have in common is valuation.

[Kevin Buzzard]

import field_theory.is_alg_closed.algebraic_closure

def foo : valuation (algebraic_closure empty) empty := sorry -- times out

Just to be clear, empty doesn't have any of the relevant typeclasses, so now one gets typeclass errors about failing to find field empty and linear_ordered_comm_monoid_with_zero empty but you also get a deterministic timeout.

[Eric Wieser]

So to be clear, def fails but lemma and example both work? Perhaps it's the generating equation lemmas that times out?

[Kevin Buzzard]

Yes, def fails but lemma and example both work (well, in this empty example nothing works but amongst the errors you have a deterministic timeout with def and no timeout with the other two)

[Kevin Buzzard]

import field_theory.is_alg_closed.algebraic_closure

variables (K : Type) [field K] (Γ₀ : Type)
  [linear_ordered_comm_monoid_with_zero Γ₀]

lemma foo : valuation (algebraic_closure K) Γ₀ := sorry -- works
example : valuation (algebraic_closure K) Γ₀ := sorry -- works
def hmm : valuation (algebraic_closure K) Γ₀ := sorry -- times out

[Eric Wieser]

All three work fine on mathlib 7348f1b7fa7a80ce55b3d4c2dad07da93d7cd353 / lean 3.35.1 on my machine I think vscode tricked me

[Kevin Buzzard]

is your timeoutometer set to further than mine? I tried with various commits from three months ago and could reproduce (the file field_theory.is_alg_closed.algebraic_closure appeared three months ago)

[Eric Wieser]

Who knows, my orange bars have now vanished and won't come back...

[Eric Wieser]

This seems to work fine too:

constant bar : valuation (algebraic_closure K) Γ₀
noncomputable def hmm : valuation (algebraic_closure K) Γ₀ := bar _ _ -- works

suggesting the sorry is to blame

[Eric Wieser]

As does:

constant sorry_but_works {α : Sort*} : α
noncomputable def hmm : valuation (algebraic_closure K) Γ₀ := sorry_but_works -- works

[Kevin Buzzard]

Great, I'll tell Amelia to use that instead :-/

[Kevin Buzzard]

noncomputable def hmm : valuation (algebraic_closure K) Γ₀ :=
{ to_fun := λ x, 0,
  map_zero' := sorry,
  map_one' := sorry,
  map_mul' := sorry,
  map_add' := sorry } -- works

[Eric Wieser]

Yeah, it actually seems like the noncomputable is what causes the problem

[Eric Wieser]

In fact, maybe it's detecting _whether_ it's noncomputable that causes trouble

[Kevin Buzzard]

We saw this before in a thread that @Yakov Pechersky was involved in -- Yakov do you remember? There was a term which Lean would complain about whether you made it noncomputable or not, and you had some insights into why this was happening.

[Yakov Pechersky]

I think our case was something with the equation compiler not using "noncomputable" until it made the whole function?

[Reid Barton]

does noncomputable theory help?

[Kevin Buzzard]

Nope.

[Kevin Buzzard]

I'm trying to minimise. Does someone have a good tip to make a simple noncomputable function, i.e. some kind of "noncomputable stub"?

[Kevin Buzzard]

It's not valuations:

import field_theory.is_alg_closed.algebraic_closure

variables (K : Type) [field K]

structure foo (R : Type) [_inst_2 : ring R] : Type.

def hmm : foo (algebraic_closure K) := sorry -- times out

[Reid Barton]

Kevin Buzzard said:

I'm trying to minimise. Does someone have a good tip to make a simple noncomputable function, i.e. some kind of "noncomputable stub"?

constant?

[Kevin Buzzard]

It's more complicated than this. If I use the reals, things work fine.

import field_theory.is_alg_closed.algebraic_closure
import data.real.basic

variables (K : Type) [field K]

structure val (K : Type) [_inst_2 : field K] : Type.

def real' (K : Type) [field K] := ℝ

def algebraic_closure' (K : Type) [field K] : Type :=
ring.direct_limit (algebraic_closure.step K) (λ i j h, algebraic_closure.to_step_of_le K i j h)

noncomputable instance real'.field : field (real' K) := by unfold real'; apply_instance
noncomputable instance algebraic_closure'.field : field (algebraic_closure' K) := field.direct_limit.field _ _

def this_works : val (real' K) := sorry

def this_times_out : val (algebraic_closure' K) := sorry

[Eric Wieser]

(classical.choice ⟨0⟩, x).2 is an easy way to make x noncomputable

[Kevin Buzzard]

I think this is the root cause -- like Maria's earlier timeout it's probably something to do with noncomputable. Again it has to be a def -- lemma and example work fine.

import field_theory.is_alg_closed.algebraic_closure

def algebraic_closure'.comm_ring (K : Type) [field K] : comm_ring (algebraic_closure K) :=
begin
  exact ideal.quotient.comm_ring _,
  -- goals accomplished
  recover, -- goals accomplished
  -- delete the next line for a timeout
  sorry, -- tactic failed, no goals to be solved
end

[Kevin Buzzard]

The actual proof of comm_ring (algebraic_closure K) in mathlib unfolds to ideal.quotient.comm_ring _.

[Kevin Buzzard]

Note also that if you mark the def noncomputable then Lean complains that it's not noncomputable before the timeout occurs. (My guess is that it's noncomputable...)

[Kevin Buzzard]

import field_theory.is_alg_closed.algebraic_closure

noncomputable def foo (K : Type) [field K] : comm_ring (algebraic_closure K) :=
begin
  change comm_ring (ideal.quotient _), -- works fine
  exact ideal.quotient.comm_ring _, -- times out
end

[Kevin Buzzard]

This is the ring we're talking about:

def foo (K : Type) [field K] : comm_ring (algebraic_closure K) :=
begin
  change comm_ring (ideal.quotient
    (_ : ideal (free_comm_ring (Σ (i : ℕ), algebraic_closure.step K i)))), -- works fine
  refine ideal.quotient.comm_ring _, -- times out
end

[Kevin Buzzard]

timeout.png
I used pp.all to figure out what the ideal was (note line numbers). So now we're in the same sort of situation Maria was in, with innocuous working code which Lean can't handle for some reason.

[Kevin Buzzard]

I don't know where to go from here :-(

[Adam Topaz]

(deleted)

[Kevin Buzzard]

On the other hand, this works fine:

import field_theory.is_alg_closed.algebraic_closure

noncomputable def foo (K : Type) [field K] : comm_ring (algebraic_closure K) :=
begin
  change comm_ring (ideal.quotient _), -- works fine
  exact ring.direct_limit.comm_ring _ _, -- the definition of this is `ideal.quotient.comm_ring _`
end

So it looks like the problem is solved, but in fact all that happens is that it blows up in your face later.

[Kevin Buzzard]

Current state of things: it's something to do with (a) field (b) noncomputable. I'm posting this here because I want to switch computer and I wondered if people were interested in my progress. It doesn't compile with master mathlib -- for that you have to change J.quotient to _ \quot J in a couple of places (it compiles with mathlib from around a week ago). The game is to get the imports down to 0. Right now I've reduced them to just ring and field theory.

import ring_theory.free_comm_ring
import ring_theory.ideal.quotient

variables (K : Type) [field K]

structure foo (R : Type) [_inst_2 : has_add R] : Type :=
(b : bool)

namespace algebraic_closure'

-- important that this takes `[field]`
def monic_irreducible (K : Type) [field K] : Type := bool

noncomputable def max_ideal : ideal (mv_polynomial (monic_irreducible K) K) := 0

instance max_ideal.is_maximal : (max_ideal K).is_maximal := sorry

/-- The first step of constructing `algebraic_closure`: adjoin a root of all monic polynomials -/
def adjoin_monic : Type :=
(max_ideal K).quotient

noncomputable instance adjoin_monic.field : field (adjoin_monic K) :=
ideal.quotient.field _

/-- The canonical ring homomorphism to `adjoin_monic k`. -/
noncomputable def to_adjoin_monic : K →+* adjoin_monic K :=
(ideal.quotient.mk _).comp mv_polynomial.C

/-- The `n`th step of constructing `algebraic_closure`, together with its `field` instance. -/
noncomputable def step_aux (n : ℕ) : Σ α : Type, field α :=
nat.rec_on n ⟨K, infer_instance⟩ $ λ n ih,
  ⟨@algebraic_closure'.adjoin_monic ih.1 ih.2, @algebraic_closure'.adjoin_monic.field ih.1 ih.2⟩

/-- The `n`th step of constructing `algebraic_closure`. -/
def step (n : ℕ) : Type :=
(step_aux K n).1

noncomputable instance step.field (n : ℕ) : field (step K n) :=
(step_aux K n).2

-- if this is computable it works
noncomputable def to_step_succ (n : ℕ) : step K n → step K (n + 1) :=
@algebraic_closure'.to_adjoin_monic (step K n) (step.field K n)

-- if this is computable it works
noncomputable def to_step_of_le (m n : ℕ) (h : m ≤ n) : step K m → step K n :=
nat.le_rec_on h (λ n, to_step_succ K n)

end algebraic_closure'

def algebraic_closure' : Type :=
let G := algebraic_closure'.step K in
let f := algebraic_closure'.to_step_of_le K in
(ideal.span { a | (∃ i j H x, free_comm_ring.of (⟨j, f i j H x⟩ : Σ i, G i) = a)}).quotient

def foobar : comm_ring (algebraic_closure' K) := ideal.quotient.comm_ring _ -- timeout with def, fine with lemma/example

[Gabriel Ebner]

(deleted)