Ideal has_mem

Stream: general

[AHan]

I don't get why test₁ type checked but test₂ will result in deterministic timeout...?

variables {α : Type*}
variables [discrete_field α]
variables [decidable_eq α] [decidable_linear_order α]
variables [comm_ring (mv_polynomial ℕ α)]

lemma test₁ (a : α) : a ∈ (ideal.span ({a} : set α)) := sorry

lemma test₂ (a : mv_polynomial ℕ α) : a ∈ (ideal.span ({a} : set (mv_polynomial ℕ α))) := sorry

[Johan Commelin]

@AHan What happens if you remove the [comm_ring ...] instance? It should derive it automatically, I hope.

[Patrick Massot]

And also the proof is only one rw long

[Patrick Massot]

If order to find out the relevant lemma, you start by writing ideal.mem_span because you want something about ideals saying something belongs to a span, then you pause to inspect what autocompletions are suggested, and choose the relevant one.

[Kevin Buzzard]

@AHan if you pasted minimal _working_ examples (i.e. with all the imports needed to run the example) then my life would be slightly easier -- I'd just be able to cut and paste.

import linear_algebra.multivariate_polynomial
import ring_theory.ideals

variables {α : Type*}
variables [discrete_field α]
variables [decidable_eq α] [decidable_linear_order α]
--variables [comm_ring (mv_polynomial ℕ α)]

example : comm_ring (mv_polynomial ℕ α) := by apply_instance -- this works

lemma test₁ (a : α) : a ∈ (ideal.span ({a} : set α)) := sorry

lemma test₂ (a : mv_polynomial ℕ α) :
a ∈ (ideal.span ({a} : set (mv_polynomial ℕ α))) := sorry -- no timeout any more

[Patrick Massot]

you second import is probably unnecessary

[Kevin Buzzard]

So your problem is what Johan suggested. If alpha is a field then Lean already knows that the multivariate polynomial ring over alpha is a commutative ring. This fact is already in the "type class inference system" because Lean spotted that it was true, and put it there automatically. My example above shows that the fact that the polynomial ring is a commutative ring can be proved using the apply_instance tactic -- which means that Lean already internally has a term of type comm_ring (mv_polynomial ℕ α). The line you wrote and I commented out makes a second term of that type. Now Lean's type class system works under the assumption that for typeclasses like comm_ring, there should be at most one term of each type, and if Lean has more than one term of a given typeclass then Lean can get confused. I don't know why this leads to a timeout in your case (some of the CS people here would be able to explain it I'm sure) but I can see the rule you broke, and breaking rules like this can lead to all sorts of random problems.

[Patrick Massot]

What is slightly more mysterious is why lemma test₂ (a : mv_polynomial ℕ α) : a ∈ (ideal.span ({a} : set (mv_polynomial ℕ α))) := by rw ideal.mem_span_singleton works without any extra step

[Patrick Massot]

The trick is https://github.com/leanprover/mathlib/blob/master/algebra/ring.lean#L73

[Patrick Massot]

Although dvd_refl is not definitionaly true, it is marked as refl, and it seems rw tries (all?) such lemmas to close goals

[Mario Carneiro]

it calls refl

[Patrick Massot]

How do you ask lean whether a particular lemma has been marked as refl and, if yes, where? I found the above line using grep

[Mario Carneiro]

if you print the lemma you can see any attributes

[Patrick Massot]

good

[Patrick Massot]

what about finding the line attaching the attribute?

[Mario Carneiro]

no luck

[Patrick Massot]

In @[refl, simp, priority 100] theorem dvd_refl what has priority 100?

[Patrick Massot]

priority in which process? simp?

[Kevin Buzzard]

Oh +1 to that question! I thought priority was just for type classes.

[Mario Carneiro]

I don't know why that's there. It's only for typeclasses

[Kevin Buzzard]

oh cool, I'm going back to mathlib and I'm going to give all the lemmas I proved priority 20000

[Johan Commelin]

You should give them priority 37. Just to make a point.

[Mario Carneiro]

maybe @Keeley Hoek can go code diving to ascertain if this is the case

[Mario Carneiro]

is it explicitly set by some line?

[Mario Carneiro]

or did lean do it

[Kevin Buzzard]

When Lean gets sponsored by Coca Cola and the user gets a little Coca Cola ad each time your lemma is used, every dev will want to make sure their lemmas are being used as much as possible.

[Mario Carneiro]

"This factorization was brought to you by the refreshing taste of... Coca Cola"

[Johan Commelin]

If (not when) that day arrives, I'll go back to pen and paper proofs.

[Edward Ayers]

Just install adblock on vscode

[Johan Commelin]

And waste precious CPU cycles. The real world is so debased. (And pure math is an ivory tower, yes I know.)

[Kevin Buzzard]

So if you write #print dvd_refl directly after the definition in core Lean in init/algebra/ring.lean, already the priority is 100. If you remove the simp tag then the priority also disappears.

[Kevin Buzzard]

Aah!

[Kevin Buzzard]

https://github.com/leanprover/lean/blob/master/library/init/algebra/ring.lean#L11

[Kevin Buzzard]

/- Make sure instances defined in this file have lower priority than the ones
   defined for concrete structures -/

And simp lemmas too :-)

[Kevin Buzzard]

Yeah that's it -- my dvd_refl now has priority 37.

[Patrick Massot]

MWE

set_option default_priority 100
@[simp]
lemma pat : 1+1 = 2 := dec_trivial

#print pat

[Patrick Massot]

gives @[simp, priority 100] theorem pat : 1 + 1 = 2 := of_as_true trivia

[Patrick Massot]

Removing the set_option line remove any priority number

[Patrick Massot]

Is this a bug in set_option @Sebastian Ullrich ?

[Mario Carneiro]

so, does it affect simp?

[Patrick Massot]

Yes!

[Patrick Massot]

@[simp, priority 200]
lemma pat : 1+1 = 2 := dec_trivial

@[simp, priority 37]
theorem kevin : 1 + 1 = 2 :=
of_as_true trivial

set_option trace.simplify.rewrite true
example : 1 + 1 = 2 := by simp

[Patrick Massot]

Changing priorities does change which lemma is used, so it's not a bug in set_option, it's an undocumented feature

[Reid Barton]

whoa!

[Patrick Massot]

Or maybe we didn't read the documentation seriously enough

[Patrick Massot]

For instance, maybe we didn't read the source code...

[Sebastian Ullrich]

Yeah, it's clearly spelled out in line 11386

[Patrick Massot]

The documentation file https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/library/tactic/simp_lemmas.cpp mentions priority all over the place

[AHan]

@Johan Commelin @Kevin Buzzard Thanks for the suggestion and explanation!!

[Patrick Massot]

I still wonder whether set_option default_priority setting both instance and simp priority is intended behavior. It would also be nice to know whether simp would be faster without this mechanism, which seems to be used nowhere

[Sebastian Ullrich]

I still wonder whether set_option default_priority setting both instance and simp priority is intended behavior.

The real problem is the priority attribute itself. It doesn't make any sense that it's [simp, priority 1000] instead of something like [simp:1000] in the first place (and when priority is gone, default_priority without any extra qualifier doesn't make much sense either). I doubt this will still be the case in Lean 4.

It would also be nice to know whether simp would be faster without this mechanism, which seems to be used nowhere

I don't think so, it's still using the head-symbol index.

[Patrick Massot]

The printing thing seems easy enough to correct at https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/library/tactic/simp_lemmas.cpp#L175-L180

[Patrick Massot]

but it's very probably not worth the trouble