integral domain timeout

Stream: maths

[Kevin Buzzard]

Can others reproduce this:

import data.mv_polynomial
import ring_theory.ideal_operations

open mv_polynomial

variables {k : Type*} [comm_ring k]

variable {n : Type*}

def 𝕍 (S : set (mv_polynomial n k)) : set (n → k) :=
{x : n → k | ∀ f ∈ S, eval x f = 0} -- works BUT VARIABLES IN STUPID ORDER!

set_option profiler true

-- typechecks in under a second
theorem 𝕍_radical {k : Type*} [comm_ring k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

-- (deterministic) timeout
theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

[Kevin Buzzard]

-- works fine
noncomputable instance {k : Type*} [integral_domain k] {n : Type*} :
  has_coe (ideal (mv_polynomial n k)) (set (mv_polynomial n k)) := by apply_instance

-- times out
noncomputable theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

[Kevin Buzzard]

-- times out
noncomputable theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (I : set (mv_polynomial n k)) = 𝕍 ((ideal.radical I : ideal _) : set _) := sorry

[Kevin Buzzard]

-- works
theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (↑I : set (mv_polynomial n k)) = 𝕍 (↑(ideal.radical I : ideal _) : set _) := sorry

So when do I need the up-arrows?

[Kevin Buzzard]

And why did I not need them for comm_rings?

[Kevin Buzzard]

theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (↑I : set _) = 𝕍 (↑(ideal.radical I) : set _) := sorry
-- don't know how to synthesize placeholder

gaargh

[Kevin Buzzard]

why does it look so ugly?

[Kevin Buzzard]

I am trying to sell this software to mathematicians

[Johan Commelin]

I guess that you can play tricks, if you want. Where you make k \^n notation for fin n → k, similar to the way that Mario made the \bbV notation. Idem dito for k[X_1, ..., X_n].

[Johan Commelin]

But such hacks will likely break down fast

[Kevin Buzzard]

Will Lean 4 be better in this regard?

[Andrew Ashworth]

Do you need to have the displayed content equal to the keystrokes you type in? If not, then the VSCode plugin - if it was extended appropriately - could probably render formulas to latex

[Kevin Buzzard]

No I definitely don't need this. @Patrick Massot can hacking VSCode give me $k^n$ instead of fin n -> k?

[Daniel Selsam]

Can others reproduce this:

-- (deterministic) timeout
theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
  (I : ideal (mv_polynomial n k)) :
  𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

Diamonds. Two searches for has_coe_to_fun traverse discrete_linear_ordered_field 14,000x times each.

[Kevin Buzzard]

Daniel thank you so much for these advanced debugging comments. I am just writing MSc level mathematics in a mathematically normal way and coming up with these issues in Lean 3, I am quite excited about Lean 4 now.