feat(tactic/linter): add decidable_classical linter (#2352)

* feat(tactic/linter): add decidable_classical linter

* docstring

* cleanup

* fix build, cleanup

* fix test

* Update src/tactic/lint/type_classes.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/tactic/lint/type_classes.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/tactic/lint/default.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/tactic/lint/type_classes.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/data/dfinsupp.lean

Co-Authored-By: Yury G. Kudryashov <urkud@urkud.name>

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/big_operators.lean

@@ -911,7 +911,8 @@ end
 end decidable_linear_ordered_cancel_comm_monoid
 
 section linear_ordered_comm_ring
-variables [decidable_eq α] [linear_ordered_comm_ring β]
+variables [linear_ordered_comm_ring β]
+open_locale classical
 
 /- this is also true for a ordered commutative multiplicative monoid -/
 lemma prod_nonneg {s : finset α} {f : α → β}
@@ -949,11 +950,12 @@ end linear_ordered_comm_ring
 
 section canonically_ordered_comm_semiring
 
-variables [decidable_eq α] [canonically_ordered_comm_semiring β]
+variables [canonically_ordered_comm_semiring β]
 
 lemma prod_le_prod' {s : finset α} {f g : α → β} (h : ∀ i ∈ s, f i ≤ g i) :
   s.prod f ≤ s.prod g :=
 begin
+  classical,
   induction s using finset.induction with a s has ih h,
   { simp },
   { rw [finset.prod_insert has, finset.prod_insert has],
@@ -1062,7 +1064,7 @@ end multiset
 
 namespace with_top
 open finset
-variables [decidable_eq α]
+open_locale classical
 
 /-- sum of finite numbers is still finite -/
 lemma sum_lt_top [ordered_comm_monoid β] {s : finset α} {f : α → with_top β} :

src/algebra/euclidean_domain.lean

@@ -128,6 +128,22 @@ begin
   rw [mul_div_cancel_left _ hz, mul_left_comm, mul_div_cancel_left _ hz]
 end
 
+section
+open_locale classical
+
+@[elab_as_eliminator]
+theorem gcd.induction {P : α → α → Prop} : ∀ a b : α,
+  (∀ x, P 0 x) →
+  (∀ a b, a ≠ 0 → P (b % a) a → P a b) →
+  P a b
+| a := λ b H0 H1, if a0 : a = 0 then by rw [a0]; apply H0 else
+  have h:_ := mod_lt b a0,
+  H1 _ _ a0 (gcd.induction (b%a) a H0 H1)
+using_well_founded {dec_tac := tactic.assumption,
+  rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}
+
+end
+
 section gcd
 variable [decidable_eq α]
 
@@ -147,17 +163,6 @@ by rw gcd; split_ifs; simp only [h, zero_mod, gcd_zero_left]
 theorem gcd_val (a b : α) : gcd a b = gcd (b % a) a :=
 by rw gcd; split_ifs; [simp only [h, mod_zero, gcd_zero_right], refl]
 
-@[elab_as_eliminator]
-theorem gcd.induction {P : α → α → Prop} : ∀ a b : α,
-  (∀ x, P 0 x) →
-  (∀ a b, a ≠ 0 → P (b % a) a → P a b) →
-  P a b
-| a := λ b H0 H1, if a0 : a = 0 then by rw [a0]; apply H0 else
-  have h:_ := mod_lt b a0,
-  H1 _ _ a0 (gcd.induction (b%a) a H0 H1)
-using_well_founded {dec_tac := tactic.assumption,
-  rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}
-
 theorem gcd_dvd (a b : α) : gcd a b ∣ a ∧ gcd a b ∣ b :=
 gcd.induction a b
   (λ b, by rw [gcd_zero_left]; exact ⟨dvd_zero _, dvd_refl _⟩)

src/algebra/floor.lean

@@ -32,6 +32,8 @@ rounding
 
 variables {α : Type*}
 
+open_locale classical
+
 /--
 A `floor_ring` is a linear ordered ring over `α` with a function
 `floor : α → ℤ` satisfying `∀ (z : ℤ) (x : α), z ≤ floor x ↔ (z : α) ≤ x)`.
@@ -221,7 +223,7 @@ lemma ceil_pos {a : α} : 0 < ⌈a⌉ ↔ 0 < a :=
 
 @[simp] theorem ceil_zero : ⌈(0 : α)⌉ = 0 := by simp [ceil]
 
-lemma ceil_nonneg [decidable_rel ((<) : α → α → Prop)] {q : α} (hq : 0 ≤ q) : 0 ≤ ⌈q⌉ :=
+lemma ceil_nonneg {q : α} (hq : 0 ≤ q) : 0 ≤ ⌈q⌉ :=
 if h : q > 0 then le_of_lt $ ceil_pos.2 h
 else by rw [le_antisymm (le_of_not_lt h) hq, ceil_zero]; trivial
 
@@ -234,7 +236,7 @@ def nat_ceil (a : α) : ℕ := int.to_nat (⌈a⌉)
 theorem nat_ceil_le {a : α} {n : ℕ} : nat_ceil a ≤ n ↔ a ≤ n :=
 by rw [nat_ceil, int.to_nat_le, ceil_le]; refl
 
-theorem lt_nat_ceil {a : α} {n : ℕ} [decidable ((n : α) < a)] : n < nat_ceil a ↔ (n : α) < a :=
+theorem lt_nat_ceil {a : α} {n : ℕ} : n < nat_ceil a ↔ (n : α) < a :=
 not_iff_not.1 $ by rw [not_lt, not_lt, nat_ceil_le]
 
 theorem le_nat_ceil (a : α) : a ≤ nat_ceil a := nat_ceil_le.1 (le_refl _)
@@ -257,7 +259,7 @@ begin
   refl
 end
 
-theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) [decidable ((nat_ceil a : α) < a + 1)] :
+theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) :
   (nat_ceil a : α) < a + 1 :=
 lt_nat_ceil.1 $ by rw (
   show nat_ceil (a + 1) = nat_ceil a + 1, by exact_mod_cast (nat_ceil_add_nat a_nonneg 1));

src/algebra/module.lean

@@ -347,9 +347,12 @@ lemma add_mem_iff_left (h₁ : y ∈ p) : x + y ∈ p ↔ x ∈ p :=
 lemma add_mem_iff_right (h₁ : x ∈ p) : x + y ∈ p ↔ y ∈ p :=
 ⟨λ h₂, by simpa using sub_mem _ h₂ h₁, add_mem _ h₁⟩
 
-lemma sum_mem {ι : Type w} [decidable_eq ι] {t : finset ι} {f : ι → β} :
+lemma sum_mem {ι : Type w} {t : finset ι} {f : ι → β} :
   (∀c∈t, f c ∈ p) → t.sum f ∈ p :=
-finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
+begin
+  classical,
+  exact finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
+end
 
 lemma smul_mem_iff' (u : units α) : (u:α) • x ∈ p ↔ x ∈ p :=
 ⟨λ h, by simpa only [smul_smul, u.inv_mul, one_smul] using p.smul_mem ↑u⁻¹ h, p.smul_mem u⟩

src/algebra/order.lean

@@ -124,32 +124,34 @@ calc  c
 
 namespace decidable
 
-lemma lt_or_eq_of_le [partial_order α] [@decidable_rel α (≤)] {a b : α} (hab : a ≤ b) : a < b ∨ a = b :=
+local attribute [instance, priority 10] classical.prop_decidable
+
+lemma lt_or_eq_of_le [partial_order α] {a b : α} (hab : a ≤ b) : a < b ∨ a = b :=
 if hba : b ≤ a then or.inr (le_antisymm hab hba)
 else or.inl (lt_of_le_not_le hab hba)
 
-lemma eq_or_lt_of_le [partial_order α] [@decidable_rel α (≤)] {a b : α} (hab : a ≤ b) : a = b ∨ a < b :=
+lemma eq_or_lt_of_le [partial_order α] {a b : α} (hab : a ≤ b) : a = b ∨ a < b :=
 (lt_or_eq_of_le hab).swap
 
-lemma le_iff_lt_or_eq [partial_order α] [@decidable_rel α (≤)] {a b : α} : a ≤ b ↔ a < b ∨ a = b :=
+lemma le_iff_lt_or_eq [partial_order α] {a b : α} : a ≤ b ↔ a < b ∨ a = b :=
 ⟨lt_or_eq_of_le, le_of_lt_or_eq⟩
 
-lemma le_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ b < a) : a ≤ b :=
+lemma le_of_not_lt [linear_order α] {a b : α} (h : ¬ b < a) : a ≤ b :=
 decidable.by_contradiction $ λ h', h $ lt_of_le_not_le ((le_total _ _).resolve_right h') h'
 
-lemma not_lt [decidable_linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a :=
+lemma not_lt [linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a :=
 ⟨le_of_not_lt, not_lt_of_ge⟩
 
-lemma lt_or_le [decidable_linear_order α] (a b : α) : a < b ∨ b ≤ a :=
+lemma lt_or_le [linear_order α] (a b : α) : a < b ∨ b ≤ a :=
 if hba : b ≤ a then or.inr hba else or.inl $ not_le.1 hba
 
-lemma le_or_lt [decidable_linear_order α] (a b : α) : a ≤ b ∨ b < a :=
+lemma le_or_lt [linear_order α] (a b : α) : a ≤ b ∨ b < a :=
 (lt_or_le b a).swap
 
-lemma lt_trichotomy [decidable_linear_order α] (a b : α) : a < b ∨ a = b ∨ b < a :=
+lemma lt_trichotomy [linear_order α] (a b : α) : a < b ∨ a = b ∨ b < a :=
 (lt_or_le _ _).imp_right $ λ h, (eq_or_lt_of_le h).imp_left eq.symm
 
-lemma lt_or_gt_of_ne [decidable_linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ b < a :=
+lemma lt_or_gt_of_ne [linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ b < a :=
 (lt_trichotomy a b).imp_right $ λ h', h'.resolve_left h
 
 def lt_by_cases [decidable_linear_order α] (x y : α) {P : Sort*}
@@ -160,18 +162,18 @@ begin
   apply h₂, apply le_antisymm; apply le_of_not_gt; assumption
 end
 
-lemma ne_iff_lt_or_gt [decidable_linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ b < a :=
+lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ b < a :=
 ⟨lt_or_gt_of_ne, λo, o.elim ne_of_lt ne_of_gt⟩
 
-lemma le_imp_le_of_lt_imp_lt {β} [preorder α] [decidable_linear_order β]
+lemma le_imp_le_of_lt_imp_lt {β} [preorder α] [linear_order β]
   {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
 le_of_not_lt $ λ h', not_le_of_gt (H h') h
 
-lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [decidable_linear_order β]
+lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [linear_order β]
   {a b : α} {c d : β} : (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=
 ⟨lt_imp_lt_of_le_imp_le, le_imp_le_of_lt_imp_lt⟩
 
-lemma le_iff_le_iff_lt_iff_lt {β} [decidable_linear_order α] [decidable_linear_order β]
+lemma le_iff_le_iff_lt_iff_lt {β} [linear_order α] [linear_order β]
   {a b : α} {c d : β} : (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
 ⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ iff.trans (not_congr H) $ not_lt⟩
 

src/algebra/pi_instances.lean

@@ -221,9 +221,10 @@ variables {I : Type*} (Z : I → Type*)
 variables [Π i, comm_monoid (Z i)]
 
 @[simp, to_additive]
-lemma finset.prod_apply {γ : Type*} [decidable_eq γ] {s : finset γ} (h : γ → (Π i, Z i)) (i : I) :
+lemma finset.prod_apply {γ : Type*} {s : finset γ} (h : γ → (Π i, Z i)) (i : I) :
   (s.prod h) i = s.prod (λ g, h g i) :=
 begin
+  classical,
   induction s using finset.induction_on with b s nmem ih,
   { simp only [finset.prod_empty], refl },
   { simp only [nmem, finset.prod_insert, not_false_iff],

src/analysis/convex/specific_functions.lean

@@ -52,7 +52,7 @@ begin
 end
 
 lemma finset.prod_nonneg_of_card_nonpos_even
-  {α β : Type*} [decidable_eq α] [linear_ordered_comm_ring β]
+  {α β : Type*} [linear_ordered_comm_ring β]
   {f : α → β} [decidable_pred (λ x, f x ≤ 0)]
   {s : finset α} (h0 : (s.filter (λ x, f x ≤ 0)).card.even) :
   0 ≤ s.prod f :=

src/category_theory/graded_object.lean

@@ -170,7 +170,7 @@ def total : graded_object β C ⥤ C :=
 { obj := λ X, ∐ (λ i : ulift.{v} β, X i.down),
   map := λ X Y f, limits.sigma.map (λ i, f i.down) }.
 
-variables [decidable_eq β] [has_zero_morphisms.{v} C]
+variables [has_zero_morphisms.{v} C]
 
 /--
 The `total` functor taking a graded object to the coproduct of its graded components is faithful.
@@ -180,6 +180,7 @@ which follows from the fact we have zero morphisms and decidable equality for th
 instance : faithful.{v} (total.{v u} β C) :=
 { injectivity' := λ X Y f g w,
   begin
+    classical,
     ext i,
     replace w := sigma.ι (λ i : ulift β, X i.down) ⟨i⟩ ≫= w,
     erw [colimit.ι_map, colimit.ι_map] at w,
@@ -190,7 +191,7 @@ end graded_object
 
 namespace graded_object
 
-variables (β : Type) [decidable_eq β]
+variables (β : Type)
 variables (C : Type (u+1)) [large_category C] [𝒞 : concrete_category C]
   [has_coproducts.{u} C] [has_zero_morphisms.{u} C]
 include 𝒞

src/computability/halting.lean

@@ -200,6 +200,7 @@ theorem halting_problem (n) : ¬ computable_pred (λ c, (eval c n).dom)
 -- Post's theorem on the equivalence of r.e., co-r.e. sets and
 -- computable sets. The assumption that p is decidable is required
 -- unless we assume Markov's principle or LEM.
+@[nolint decidable_classical]
 theorem computable_iff_re_compl_re {p : α → Prop} [decidable_pred p] :
   computable_pred p ↔ re_pred p ∧ re_pred (λ a, ¬ p a) :=
 ⟨λ h, ⟨h.to_re, h.not.to_re⟩, λ ⟨h₁, h₂⟩, ⟨‹_›, begin