decidable_eq makes lemma fail

Stream: general

[Bolton Bailey]

import data.mv_polynomial.basic

noncomputable theory

open_locale classical big_operators

open set function finsupp add_monoid_algebra
open_locale big_operators

universes u
variables {R : Type u}


namespace mv_polynomial
variables {σ : Type*} {n m : σ} {s : σ →₀ ℕ}

variables [decidable_eq σ] -- if commented works fine


section comm_semiring

variables [comm_semiring R] {p q : mv_polynomial σ R}


section coeff


@[simp] lemma my_coeff_mul_X (m) (s : σ) (p : mv_polynomial σ R) :
  coeff (m + single s 1) (p * X s) = coeff m p :=
begin
  have : (m, single s 1) ∈ (m + single s 1).antidiagonal := mem_antidiagonal.2 rfl,
  rw [coeff_mul, ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
      finset.sum_eq_zero, add_zero, coeff_X, mul_one],
  rintros ⟨i,j⟩ hij,
  rw [finset.mem_erase, mem_antidiagonal] at hij,
  by_cases H : single s 1 = j,
  { subst j, simpa using hij },
  { rw [coeff_X', if_neg H, mul_zero] },
end

end coeff

end comm_semiring

end mv_polynomial

I am working on a lemma similar to the one above which is a duplicate of coeff_mul_X in data.mv_polynomial.basic. I copied over the proof from coeff_mul_X to get started, and noticed the proof was failing in my file. I isolated the problem to the variables [decidable_eq σ] line, which I have in my file for a different lemma. When this instance is included, I start getting the error

rewrite tactic failed, did not find instance of the pattern in the target expression
  ite (single s 1 = j) ?m_2 ?m_3

Why does the decidable_eq instance cause this?

[Yakov Pechersky]

Because you did open_locale classical, which already provides a decidable_eq instance for all types. And now you gave a second, non defeq one.

[Bolton Bailey]

Well if the problem is that I've defined something twice, why does the error manifest this way, instead of simply telling me that I've made two instances of one class?

[Eric Rodriguez]

Because one of the ites has one instance, and the rw has another, so rw sees two fundamentally different things

[Eric Rodriguez]

Turn on pp.implicit and you'll see

[Bolton Bailey]

Further question - now that I've open_locale classical, I would think by what you are saying that it would be totally unnecessary to have any decidable_eq declarations in the file. But indeed, the other lemma fails if I remove the decidable_eq declaration.

[Bolton Bailey]

Actually never mind, I see the only reason it fails is that the last finishing tactic is no longer needed

[Eric Wieser]

Which lemma introduces the ite into the goal?

[Bolton Bailey]

Seems the coeff_X' lemma introduces ite into the goal

[Bolton Bailey]

I understand that you all are telling me that there are two instances of the decidable_eq \sigma here, what I'm try to ask is why is this allowed at all. In this thread https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Type.20class.20resolution.20only.20works.20with.20a.20name I was told that the defining features of a class was that there was a unique one for each type. I'm pretty sure decidable_eq is implemented as a class. So why isn't some sort of error thrown when I write variables [decidable_eq σ]?

[Eric Wieser]

docs#mv_polynomial.coeff_X'?

[Eric Wieser]

That lemma is stated badly

[Eric Wieser]

It's missing a decidable argument

[Eric Wieser]

Uniqueness is a guideline for typeclasses, not something lean enforces.

[Bolton Bailey]

Good to know.

[Bolton Bailey]

There are several lemmas in data/mv_polynomial/basic that introduce ite without a decidable argument. Should all of them be changed?

[Yakov Pechersky]

The whole file where that lemma is defined is classical

[Bolton Bailey]

Yep, so why does @Eric Wieser say it's stated badly?

[Eric Wieser]

That lemma is a lemma about a classical if, not an arbitrary if

[Eric Wieser]

Which makes it difficult to use in exactly the way you were running into

[Eric Wieser]

With a [decidable_eq \sigma], the lemma becomes more general, not less.

[Kevin Buzzard]

I am a bit confused about this. I was expecting Yury's rule of thumb to apply (the statement of coeff_X' would not compile without decidability assumptions) but it does compile:

import data.mv_polynomial.basic

variables {R : Type*} [comm_semiring R] {σ : Type*} (i : σ) (m : σ →₀ ℕ)

namespace mv_polynomial

lemma coeff_X'' :
  coeff m (X i : mv_polynomial σ R) = ite (finsupp.single i 1 = m) 1 0 :=
sorry -- works fine

#check @decidable_eq_of_decidable_le

end mv_polynomial

noncomputable example : decidable (finsupp.single i 1 = m) :=
by show_term {apply_instance} -- works, uses decidable_eq_of_decidable_le

noncomputable example : decidable_eq (σ →₀ ℕ) := by apply_instance -- fails

#print decidable_eq_of_decidable_le -- an instance

noncomputable example : decidable_eq (σ →₀ ℕ) :=
decidable_eq_of_decidable_le -- works

example : decidable_rel ((≤) : (σ →₀ ℕ) → (σ →₀ ℕ) → Prop) :=
  by show_term {apply_instance} -- works, uses finsupp.decidable_le

[Eric Wieser]

Maybe I jumped to conclusions here

[Eric Wieser]

Or docs#finsupp.decidable_le is bad

[Eric Wieser]

(where bad = "spoilt by choice")

[Kevin Buzzard]

Heh, I like the name of docs#finsupp.finsupp.decidable_eq

[Kevin Buzzard]

#print axioms finsupp.decidable_le
/-
propext
quot.sound
classical.choice
-/

[Kevin Buzzard]

The classical instance is in the proof of docs#finsupp.le_iff .

[Mario Carneiro]

Kevin Buzzard said:

Heh, I like the name of docs#finsupp.finsupp.decidable_eq

Don't we have a linter for this?

[Eric Wieser]

What we actually care about is whether it's noncomputable, not whether its proof uses choice

[Eric Wieser]

#7817 fixes the mv_polynomial lemmas and the double name that Kevin Buzzard spotted.

[Eric Wieser]

What's going on with finsupp.decidable_le is a decidable diamond that doesn't involve choice. I'm going to pretend it doesn't exist until we run into a problem where it actually comes up.

[Shadman Sakib]

How do I write <- with keyboard shortcuts on lean?

[Johan Commelin]

\l -- if you use VScode

[Johan Commelin]

Also, this question should probably be put in a new thread

[Notification Bot]

This topic was moved by Bryan Gin-ge Chen to #new members > keyboard shortcuts