Zulip Chat Archive

Stream: maths

Topic: integral domain timeout


Kevin Buzzard (Jan 17 2020 at 17:26):

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 (Jan 17 2020 at 17:32):

-- 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 (Jan 17 2020 at 17:35):

-- 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 (Jan 17 2020 at 17:36):

-- 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 (Jan 17 2020 at 17:37):

And why did I not need them for comm_rings?

Kevin Buzzard (Jan 17 2020 at 17:40):

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 (Jan 17 2020 at 17:41):

why does it look so ugly?

Kevin Buzzard (Jan 17 2020 at 17:41):

I am trying to sell this software to mathematicians

Johan Commelin (Jan 17 2020 at 17:47):

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 (Jan 17 2020 at 17:47):

But such hacks will likely break down fast

Kevin Buzzard (Jan 17 2020 at 18:05):

Will Lean 4 be better in this regard?

Andrew Ashworth (Jan 17 2020 at 19:50):

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 (Jan 17 2020 at 20:01):

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

Daniel Selsam (Jan 17 2020 at 20:07):

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 (Jan 17 2020 at 20:08):

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.


Last updated: Dec 20 2023 at 11:08 UTC