## Stream: general

### Topic: crazy time-out

#### Kevin Buzzard (Dec 02 2021 at 17:13):

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 ℤ)) := {
map_zero' := sorry,
map_one'  := sorry,
map_mul'  := sorry,

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

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 (Dec 02 2021 at 18:55):

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 (Dec 02 2021 at 18:57):

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 (Dec 02 2021 at 18:58):

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 (Dec 02 2021 at 18:59):

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

#### Adam Topaz (Dec 02 2021 at 19:09):

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

#### Adam Topaz (Dec 02 2021 at 19:09):

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 (Dec 02 2021 at 20:31):

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 (Dec 02 2021 at 20:58):

Yeah it's strange.

Last updated: Aug 03 2023 at 10:10 UTC