## Stream: general

### Topic: decidability and axioms

#### Damiano Testa (May 12 2022 at 07:03):

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 (May 12 2022 at 07:09):

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 (May 12 2022 at 07:12):

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

#### Damiano Testa (May 12 2022 at 07:15):

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!

Last updated: Aug 03 2023 at 10:10 UTC