decidability and axioms

Stream: general

[Damiano Testa]

Dear All,

in the recent PR #14095, it was suggested to add a decidable_eq assumption and remove classical from the proof. I am happy with this, but I now wonder what is the gain with this. For instance, the axioms used are the same:

import data.polynomial.degree.lemmas

open_locale polynomial
variables {R : Type*} [semiring R]

lemma nat_degree_monomial_eq [decidable_eq R] (i : ℕ) {r : R} (r0 : r ≠ 0) :
  (monomial i r).nat_degree = i :=
(nat_degree_monomial _ _).trans (if_neg r0)

lemma nat_degree_monomial_eq_class (i : ℕ) {r : R} (r0 : r ≠ 0) :
  (monomial i r).nat_degree = i :=
by classical; exact eq.trans (nat_degree_monomial _ _) (if_neg r0)

#print axioms nat_degree_monomial_eq
#print axioms nat_degree_monomial_eq_class
/-  both give
quot.sound
propext
classical.choice
-/
-/

Is there an advantage to the extra decidable_eq R assumption?

[Damiano Testa]

Nevermind, the linter just complained:

/- The `decidable_classical` linter reports: -/
/- USES OF `decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF. -/
-- data/polynomial/degree/definitions.lean
#check @polynomial.nat_degree_monomial_eq /- The following `decidable` hypotheses should be replaced with
                      `classical` in the proof. argument 3: [_inst_2 : decidable_eq R] -/
Error: polynomial.nat_degree_monomial_eq - The following `decidable` hypotheses should be replaced with
                      `classical` in the proof. argument 3: [_inst_2 : decidable_eq R]

Error: Process completed with exit code 1.

[Riccardo Brasca]

decidable_eq R is useful if you need it in the statement (I mean, it's better than open_locale classical).

[Damiano Testa]

Yes, and the statement of nat_degree_monomial involves an ite, hence assumes it. I removed decidable_eq R from my PR, and reverted to the original form of the lemma!