decidability leakage

Stream: mathlib4

[Matthew Ballard]

I have a weird error over on port/Data/Polynomial/RingDivision.

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  fun a_1 => instDecidableNot
inferred
  fun a_1 => Not.decidable

Not.decidable arises from alias instDecidableNot <- Not.decidable

[Kevin Buzzard]

Are they defeq? Presumably, but it's claiming they're not? Nothing weird with pp.all going on? (unlikely)

[Matthew Ballard]

I've tried to minimize it but extracting that step out from the proof works fine

example (p : R[X])  (h : ∃ n, ¬ ((X - C a) ^ (n+1) ∣ p)) (n : ℕ) : n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬ ¬ ((X - C a) ^ (m+1) ∣ p) := by
  rw [Nat.le_find_iff]

[Adam Topaz]

Here's the pp.all output:
https://gist.github.com/adamtopaz/52a716719cf4c67f15d4da1e44aa97da

[Matthew Ballard]

etaExperiment does not help

[Reid Barton]

propDecidable appears exactly once in that output, so that is the problem

[Matthew Ballard]

Under a minute!

[Kevin Buzzard]

Oh so this is the standard "you put open_locale classical somewhere but then used something which had its own decidability instance" gotcha.

[Matthew Ballard]

Vs Polynomial.decidableDvdMonic

[Kevin Buzzard]

Polynomial.decidableDvdMonic also...darn, you got there first

[Matthew Ballard]

Another question: is it normal for the goal state to be written even with the error at rw?

[Adam Topaz]

Is there a way for classical to somehow turn off all other decidability instances?

[Matthew Ballard]

So Polynomial.decidableDvdMonic is not an instance

[Adam Topaz]

or is this a priority issue? shouldn't the classical instance just have the highest possible priority (when using classical reasoning, of course)

[Kevin Buzzard]

Experience shows that it's very difficult to get open_locale classical (or whatever the lean 4 equivalent is) working robustly everywhere. You prove some theorem for general rings using it and then you apply it to int and someone has annoyingly proved that int has decidable equality and this proof is used in some other lemma or definition which you are relying on and then you just can't shake it off. The solution we came up with a year or two ago, namely adding in [decidable] assumptions if the statement doesn't compile otherwise, seem to have solved most of these problems. Three or four years ago we were using open_locale classical and (even after messing with priorities) these problems would still spring up with annoying regularity (typically with finset, at least in my experience; this is why I strongly fell out of love with it and took years to be tempted back in again)

[Kevin Buzzard]

PS IIRC the conclusion a few years ago was that the classicaldecidability instances should have the lowest possible priority... (but this didn't work either)

[Adam Topaz]

right now Classical.propDecidable does indeed have (priority := low) in lean4

[Reid Barton]

Apparently low priority is still higher than something that isn't an instance at all.

[Adam Topaz]

docs4#Polynomial.decidableDvdMonic

[Adam Topaz]

where does this decidableDvdMonic actually come from in this file?

[Reid Barton]

I closed the tab already but if you search for it again in the file, it's used in something like rootMultiplicity

[Adam Topaz]

aha okay

[Reid Barton]

and maybe it leaks out into some other definition/theorem that way

[Reid Barton]

I'm still not sure specifically how this could cause a problem, so maybe it's some other use.

[Reid Barton]

Well, there is one way it could definitely happen, if you unfold the definition of rootMultiplicity

[Adam Topaz]

another strange thing that I noticed is that generalize_proofs can't name the unnamed proof in this problematic location in the proof.

[Matthew Ballard]

def rootMultiplicity (a : R) (p : R[X]) : ℕ :=
  if h0 : p = 0 then 0
  else
    let _ : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
      @Not.decidable _ (decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1)))
    Nat.find (multiplicity_X_sub_C_finite a h0)

for reference.

[Kevin Buzzard]

Isn't the fix not to chase decidableDvdMonic but to remove open Classical and then to fix up the statements which no longer compile by adding relevant decidability hypotheses, and fixing up the proofs which no longer compile by enabling classical within the proof?

[Adam Topaz]

I mentioned this to Matt privately already, but a hack of the following sort also works:

theorem le_rootMultiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
    n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p := by
  dsimp [rootMultiplicity]
  rw [dif_neg p0]
  suffices : n ≤ Nat.find (multiplicity_X_sub_C_finite a p0) ↔ (X - C a)^n ∣ p
  convert this
  rw [Nat.le_find_iff]
  simp_rw [Classical.not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  cases' n with n;
  · rw [pow_zero]
    apply one_dvd;
  · exact h n n.lt_succ_self

[Matthew Ballard]

That can be done. You have to tell Lean about decidability of division in the proof (and elsewhere)

[Adam Topaz]

which is essentially what Matt already said above with the example

[Reid Barton]

I think unfolding a definition that uses non-instances as though they were instances is always going to lead to potential problems

[Reid Barton]

i.e. the "statement that doesn't compile" doesn't exist, it's the equational unfolding of rootMultiplicity

[Reid Barton]

So I guess then one option is to add rootMultiplicity_def, that does abstract over the decidability instance.

[Adam Topaz]

Adam Topaz said:

I mentioned this to Matt privately already, but a hack of the following sort also works:

theorem le_rootMultiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
    n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p := by
  dsimp [rootMultiplicity]
  rw [dif_neg p0]
  suffices : n ≤ Nat.find (multiplicity_X_sub_C_finite a p0) ↔ (X - C a)^n ∣ p
  convert this
  rw [Nat.le_find_iff]
  simp_rw [Classical.not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  cases' n with n;
  · rw [pow_zero]
    apply one_dvd;
  · exact h n n.lt_succ_self

Note that replacing convert by exact does NOT work here.

[Kevin Buzzard]

def decidableDvdMonic (p : R[X]) (hq : Monic q) : Decidable (q ∣ p) := ...

This can't be an instance, right? Because typeclass inference will never find hq.

[Reid Barton]

At the very least you'd expect the effect of

  dsimp [rootMultiplicity]
  rw [dif_neg p0]

to be a lemma

[Matthew Ballard]

It might be...Can't find it

[Kevin Buzzard]

This lemma would still use nat.find so would still want a decidability instance though, right?

[Adam Topaz]

but it works:

theorem le_rootMultiplicity_iff_aux {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
  n ≤ rootMultiplicity a p ↔ n ≤ Nat.find (multiplicity_X_sub_C_finite a p0) := by
  dsimp [rootMultiplicity]
  rw [dif_neg p0]

/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
  `(X - a) ^ n` divides `p`. -/
theorem le_rootMultiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
    n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p := by
  rw [le_rootMultiplicity_iff_aux, Nat.le_find_iff]
  simp_rw [Classical.not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  cases' n with n;
  · rw [pow_zero]
    apply one_dvd;
  · exact h n n.lt_succ_self
#align polynomial.le_root_multiplicity_iff Polynomial.le_rootMultiplicity_iff

[Adam Topaz]

oh wait maybe not

[Adam Topaz]

okay, this works:

theorem le_rootMultiplicity_iff_aux {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
    n ≤ rootMultiplicity a p ↔ n ≤ Nat.find (multiplicity_X_sub_C_finite a p0) := by
  dsimp [rootMultiplicity]
  rw [dif_neg p0]
  convert Iff.rfl

/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
  `(X - a) ^ n` divides `p`. -/
theorem le_rootMultiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
    n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p := by
  rw [le_rootMultiplicity_iff_aux p0, Nat.le_find_iff]
  simp_rw [Classical.not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  cases' n with n;
  · rw [pow_zero]
    apply one_dvd;
  · exact h n n.lt_succ_self

[Adam Topaz]

note the convert again

[Matthew Ballard]

Since there doesn't seem to a good general fix, I'll go with Adam's suggestion.

[Notification Bot]

Matthew Ballard has marked this topic as resolved.

[Reid Barton]

Is the first theorem with Classical open? I was expecting you'd have to write [Decidable (blah blah blah)]

[Reid Barton]

(Also, I think the theorem statement can just be rootMultiplicity a p = Nat.find ...)

[Adam Topaz]

yeah that's a much better lemma :)

[Matthew Ballard]

No. It was around the 6th that used classical

[Reid Barton]

I mean this le_rootMultiplicity_iff_aux

[Adam Topaz]

yeah classical was open for that one. The converthack works in that case.

[Matthew Ballard]

Classical is open for the definition of rootMultiplicity

[Reid Barton]

Then the party line is (& probably some linter will tell you) that you should take a decidability instance hypothesis for whatever Nat.find needs, just in case later you manage to cook up yet another distinct decidability instance

[Notification Bot]

Matthew Ballard has marked this topic as unresolved.

[Matthew Ballard]

I don't want to defy the party

[Kyle Miller]

Here's a question: how attached are you to Nat.find? Would you be ok with using the noncomputable infₛ? (See Nat.infₛ_def for the relationship to Nat.find.)

[Matthew Ballard]

Just to be clear, we are talking about redefining rootMultiplicity right?

[Matthew Ballard]

Other that minimizing changes while porting, I have no feelings

[Kyle Miller]

(Jumping up to your mwe, you'd write infₛ {n | ¬ ((X - C a) ^ (n+1) ∣ p)} rather than Nat.find h.)

[Matthew Ballard]

Ok. I guess if I am forced to feel, I would say that dividing polynomials should be as computable as possible.

[Kevin Buzzard]

Even though adding polynomials is not at all computable?

[Matthew Ballard]

But the whole file is noncomputable I think

[Kevin Buzzard]

and trying to make it computable caused problems

[Matthew Ballard]

Kevin Buzzard said:

Even though adding polynomials is not at all computable?

Over $\Z$?

[Ruben Van de Velde]

Over anything

[Kevin Buzzard]

IIRC then yes

[Matthew Ballard]

Ok, I need more information here

[Kevin Buzzard]

I remember when it happened because a student had some code which computed some Chebyshev polynomials over Z and he had to change refl to ring in a few places

[Matthew Ballard]

(Sorry for the detour)

[Matthew Ballard]

Is this an abstract problem or an implementation problem?

[Kevin Buzzard]

Trying to make them computable when R was computable just caused issues of the kind which you are seeing in this thread, and eventually someone threw their hands up in the air and switched it all off.

[Matthew Ballard]

Ah ok

[Kevin Buzzard]

And switching it off did solve a bunch of problems

[Kevin Buzzard]

If we knew then what we know now then I would imagine we might have had a better chance, and I think that occasionally people talk about re-instating computability

[Matthew Ballard]

Can something like csimp substitute a computable implementation if you ever wanted to generate code for general noncomputable things?

[Kevin Buzzard]

-- lean 3
import data.polynomial.algebra_map
import tactic

open_locale polynomial
open polynomial

example : (2 : ℤ) + 3 = 3 + 2 := rfl -- works
example : C (2 : ℤ) * X + 3 = 3 + C 2 * X := rfl -- fails
example : C (2 : ℤ) * X + 3 = 3 + C 2 * X := by ring -- works

[Matthew Ballard]

I can certainly imagine someone trying Faugère F4 or F5

[Matthew Ballard]

Especially with Lean 4 (vs 3)

[Kevin Buzzard]

Right, but somehow this was a disjoint problem to "develop the theory of single variable polynomials because we want to prove the fundamental theorem of Galois theory", where no computability at all was needed.

[Matthew Ballard]

Very fair

[Kevin Buzzard]

and somehow the momentum was with the Galois theory people

[Matthew Ballard]

(Aside if someone is interested in F4 or F5, call me maybe :wink:)

[Eric Wieser]

Matthew Ballard said:

Can something like csimp substitute a computable implementation if you ever wanted to generate code for general noncomputable things?

Right now no: csimp requires an exact match to the original signature

[Reid Barton]

But note that this so-called noncomputability does not prevent by ring from working, so I assume it would not affect your F4 algorithm either.

[Eric Wieser]

So if you have an algorithm that works if you have decidable equality, then your noncomputable def has to assume decidable equality too.

[Kyle Miller]

I've been toying with the idea of there being a compute% term elaborator that takes an expression and makes it computable (if possible). This is an extension of previous discussion about a computable typeclass (and it could make use of such a typeclass to store how to compute things), but it seems like it would be more robust.

[Matthew Ballard]

That would be pretty sweet

[Kyle Miller]

maybe the interface is that compute% e gives you a proof h : e = e' where e' is computable.

[Kyle Miller]

and there could be a #compute command where #compute e does #eval e' (I'm not really sure how this compares to #norm_num, other than #compute might evaluate faster at the cost of not being a verified evaluation).

[Matthew Ballard]

Circling back around, I have

theorem rootMultiplicity_eq_nat_find_of_nonzero {p : R[X]} (p0 : p ≠ 0) {a : R} :
  rootMultiplicity a p = Nat.find (multiplicity_X_sub_C_finite a p0) := by
  dsimp [rootMultiplicity]
  rw [dif_neg p0]
  convert rfl

and am leaving a note around rootMultiplicity about removing a blanket Classical for a specific assumption. Does this sound reasonable? My main motivation is not to seriously (or moderately) refactor things during porting.

[Eric Wieser]

Can you remind us of the original version that didn't work?

[Matthew Ballard]

theorem le_rootMultiplicity_iff {p : R[X]} (p0 : p ≠ 0) {a : R} {n : ℕ} :
     n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p :=
   by
   simp_rw [root_multiplicity, dif_neg p0, Nat.le_find_iff, Classical.not_not]
   refine' ⟨fun h => _, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
   cases n;
   · rw [pow_zero]
     apply one_dvd; · exact h n n.lt_succ_self

[Matthew Ballard]

from mathport

[Matthew Ballard]

Should I break out the computability discussion into a separate stream?

[Matthew Ballard]

I think it is quite valuable and don't want it buried