crazy time-out

Stream: general

[Kevin Buzzard]

Maria found a way of getting subtype.val to time out. The example below isn't very minimal but it is pretty weird. The subtype foo below is defined with an ∃ and then bar times out. If you change the ∃ to a ∀ then the timeout goes away though?!

import algebraic_geometry.prime_spectrum.basic
import ring_theory.dedekind_domain
import topology.algebra.valued_field

open_locale classical

section valuation
variables {S : Type*} [ring S] {Γ₀ : Type*} [linear_ordered_comm_monoid_with_zero Γ₀]
  (v : valuation S Γ₀) {x y z : S}

lemma valuation.def : v x = v.to_fun x := rfl

end valuation

variables (R : Type) {K : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] [field K]
  [algebra R K] [is_fraction_ring R K]

-- Note : not the maximal spectrum if R is a field
def maximal_spectrum := {v : prime_spectrum R // v.as_ideal ≠ 0 }

variable (v : maximal_spectrum R)

variable {R}

noncomputable def ring.adic_valuation.def (v : maximal_spectrum R) (r : R) : with_zero (multiplicative ℤ) :=
dite (r = 0) (λ (h : r = 0), 0) (λ h : ¬ r = 0, (multiplicative.of_add
  (-(associates.mk v.val.as_ideal).count (associates.mk (ideal.span{r} : ideal R)).factors : ℤ)))

noncomputable def adic_valuation.def (v : maximal_spectrum R) (x : K) : (with_zero (multiplicative ℤ)) :=
let s := classical.some (classical.some_spec (is_localization.mk'_surjective
  (non_zero_divisors R) x)) in (ring.adic_valuation.def v (classical.some
    (is_localization.mk'_surjective (non_zero_divisors R) x)))/(ring.adic_valuation.def v s)

noncomputable def adic_valuation (v : maximal_spectrum R) : valuation K (with_zero (multiplicative ℤ)) := {
  to_fun    := adic_valuation.def v,
  map_zero' := sorry,
  map_one'  := sorry,
  map_mul'  := sorry,
  map_add'  := sorry }

noncomputable def v_valued_K (v : maximal_spectrum R) : valued K :=
{ Γ₀  := with_zero (multiplicative ℤ),
  grp := infer_instance,
  -- necessary
  v   := adic_valuation v }

noncomputable def ts' : topological_space K := @valued.topological_space K _ (v_valued_K v)
lemma tdr' : @topological_division_ring K _ (ts' v) := @valued.topological_division_ring K _ (v_valued_K v)
noncomputable def us' : uniform_space K := @topological_add_group.to_uniform_space K _ (ts' v) _
lemma ug' : @uniform_add_group K (us' v) _ := @topological_add_group_is_uniform K _ (ts' v) _

variables (K)
def K_v := @uniform_space.completion K (us' v)

noncomputable instance : field (K_v K v) := @field_completion K _ (us' v) (tdr' v) _ (ug' v) _

variables (R)

def K_hat := (Π (v : maximal_spectrum R), K_v K v)

-- change ∃ to ∀ and the problem goes away!
def foo := { x : (K_hat R K) // ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37 }

-- times out
def bar : foo R K → K_hat R K := λ x, x.1

[Adam Topaz]

this seems to work

-- Change // to | and it works!
def foo := { x : (K_hat R K) | ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37 }

def bar : foo R K → K_hat R K := λ x, x.1

[Adam Topaz]

Also this works:

def foo := { x : K_hat R K // true → ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37 }

def bar : foo R K → K_hat R K := λ x, x.1

[Adam Topaz]

And this

def baz (x : K_hat R K) : Prop := ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37

def foo := { x : K_hat R K //  baz _ _ x }

def bar : foo R K → K_hat R K := λ x, x.1

[Adam Topaz]

So as long as you put the smallest of wrappers around the proposition, it seems to be okay.

[Adam Topaz]

I think it's an issue with 37, or perhaps the inverse.

[Adam Topaz]

E.g. this works:

def foo := { x : K_hat R K // ∃ v : maximal_spectrum R, (x v) = (x v) }

def bar : foo R K → K_hat R K := λ x, x.1

[Kevin Buzzard]

Yes -- the inverse is causing the trouble because it uses the field structure. It's the field structure which is causing the kernel to get stuck. I think it must be the kernel because λ x, begin exact x.1, sorry, end gives "goals accomplished" and an error on the sorry. The issue is the field structure on K_v. Maria's fix was simply to define an auxiliary P x := ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37 and then use {x // P x}, which also works. But don't you think it's completely bizarre?

[Adam Topaz]

Yeah it's strange.