Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 2f5b500

Browse files
eric-wiesereric-wieser
committed
fix(data/mv_polynomial): add missing decidable_eq arguments to lemmas (#18848)
This does not change the type of any definitions; the effect of this PR is to make the *statement* of the lemmas syntactically more general. To ensure this catches them all, this removes `open_locale classical` from the beginning of every file in `data/mv_polynomial` and `ring_theory/mv_polynomial`. For definitions which bake in a `classical.dec_eq` assumption, this adds a lemma proven by `convert rfl` that unfolds them to a version with an arbitrary `decidable_eq` instance, following a pattern established elsewhere. Unlike previous refactors of this style this doesn't seemed to have helped any downstream proofs much.
1 parent 7ad820c commit 2f5b500

13 files changed

Lines changed: 153 additions & 90 deletions

File tree

‎src/data/mv_polynomial/basic.lean‎

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ polynomial, multivariate polynomial, multivariable polynomial
7272

7373
noncomputable theory
7474

75-
open_locale classical big_operators
75+
open_locale big_operators
7676

7777
open set function finsupp add_monoid_algebra
7878
open_locale big_operators
@@ -417,22 +417,22 @@ by convert rfl
417417
lemma support_monomial_subset : (monomial s a).support ⊆ {s} :=
418418
support_single_subset
419419

420-
lemma support_add : (p + q).support ⊆ p.support ∪ q.support := finsupp.support_add
420+
lemma support_add [decidable_eq σ] : (p + q).support ⊆ p.support ∪ q.support := finsupp.support_add
421421

422422
lemma support_X [nontrivial R] : (X n : mv_polynomial σ R).support = {single n 1} :=
423-
by rw [X, support_monomial, if_neg]; exact one_ne_zero
423+
by classical; rw [X, support_monomial, if_neg]; exact one_ne_zero
424424

425425
lemma support_X_pow [nontrivial R] (s : σ) (n : ℕ) :
426426
(X s ^ n : mv_polynomial σ R).support = {finsupp.single s n} :=
427-
by rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
427+
by classical; rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
428428

429429
@[simp] lemma support_zero : (0 : mv_polynomial σ R).support = ∅ := rfl
430430

431431
lemma support_smul {S₁ : Type*} [smul_zero_class S₁ R] {a : S₁} {f : mv_polynomial σ R} :
432432
(a • f).support ⊆ f.support :=
433433
finsupp.support_smul
434434

435-
lemma support_sum {α : Type*} {s : finset α} {f : α → mv_polynomial σ R} :
435+
lemma support_sum {α : Type*} [decidable_eq σ] {s : finset α} {f : α → mv_polynomial σ R} :
436436
(∑ x in s, f x).support ⊆ s.bUnion (λ x, (f x).support) := finsupp.support_finset_sum
437437

438438
end support
@@ -455,7 +455,7 @@ lemma sum_def {A} [add_comm_monoid A] {p : mv_polynomial σ R} {b : (σ →₀
455455
p.sum b = ∑ m in p.support, b m (p.coeff m) :=
456456
by simp [support, finsupp.sum, coeff]
457457

458-
lemma support_mul (p q : mv_polynomial σ R) :
458+
lemma support_mul [decidable_eq σ] (p q : mv_polynomial σ R) :
459459
(p * q).support ⊆ p.support.bUnion (λ a, q.support.bUnion $ λ b, {a + b}) :=
460460
by convert add_monoid_algebra.support_mul p q; ext; convert iff.rfl
461461

@@ -525,11 +525,12 @@ by rw [← coeff_X_pow, pow_one]
525525

526526
@[simp] lemma coeff_X (i : σ) :
527527
coeff (single i 1) (X i : mv_polynomial σ R) = 1 :=
528-
by rw [coeff_X', if_pos rfl]
528+
by classical; rw [coeff_X', if_pos rfl]
529529

530530
@[simp] lemma coeff_C_mul (m) (a : R) (p : mv_polynomial σ R) :
531531
coeff m (C a * p) = a * coeff m p :=
532532
begin
533+
classical,
533534
rw [mul_def, sum_C],
534535
{ simp [sum_def, coeff_sum] {contextual := tt} },
535536
simp
@@ -589,6 +590,7 @@ end
589590
lemma coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : mv_polynomial σ R) :
590591
coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 :=
591592
begin
593+
classical,
592594
obtain rfl | hr := eq_or_ne r 0,
593595
{ simp only [monomial_zero, coeff_zero, mul_zero, if_t_t], },
594596
haveI : nontrivial R := nontrivial_of_ne _ _ hr,
@@ -742,9 +744,12 @@ finsupp.sum_zero_index
742744
section
743745

744746
@[simp] lemma eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g :=
745-
finsupp.sum_add_index
746-
(by simp [f.map_zero])
747-
(by simp [add_mul, f.map_add])
747+
begin
748+
classical,
749+
exact finsupp.sum_add_index
750+
(by simp [f.map_zero])
751+
(by simp [add_mul, f.map_add])
752+
end
748753

749754
@[simp] lemma eval₂_monomial : (monomial s a).eval₂ f g = f a * s.prod (λn e, g n ^ e) :=
750755
finsupp.sum_single_index (by simp [f.map_zero])
@@ -761,6 +766,7 @@ by simp [eval₂_monomial, f.map_one, X, prod_single_index, pow_one]
761766
lemma eval₂_mul_monomial :
762767
∀{s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod (λn e, g n ^ e) :=
763768
begin
769+
classical,
764770
apply mv_polynomial.induction_on p,
765771
{ assume a' s a,
766772
simp [C_mul_monomial, eval₂_monomial, f.map_mul] },
@@ -994,6 +1000,7 @@ end
9941000

9951001
lemma coeff_map (p : mv_polynomial σ R) : ∀ (m : σ →₀ ℕ), coeff m (map f p) = f (coeff m p) :=
9961002
begin
1003+
classical,
9971004
apply mv_polynomial.induction_on p; clear p,
9981005
{ intros r m, rw [map_C], simp only [coeff_C], split_ifs, {refl}, rw f.map_zero },
9991006
{ intros p q hp hq m, simp only [hp, hq, (map f).map_add, coeff_add], rw f.map_add },

‎src/data/mv_polynomial/comm_ring.lean‎

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -38,8 +38,6 @@ This will give rise to a monomial in `mv_polynomial σ R` which mathematicians m
3838

3939
noncomputable theory
4040

41-
open_locale classical big_operators
42-
4341
open set function finsupp add_monoid_algebra
4442
open_locale big_operators
4543

@@ -70,7 +68,8 @@ variables (σ a a')
7068
@[simp] lemma support_neg : (- p).support = p.support :=
7169
finsupp.support_neg p
7270

73-
lemma support_sub (p q : mv_polynomial σ R) : (p - q).support ⊆ p.support ∪ q.support :=
71+
lemma support_sub [decidable_eq σ] (p q : mv_polynomial σ R) :
72+
(p - q).support ⊆ p.support ∪ q.support :=
7473
finsupp.support_sub
7574

7675
variables {σ} (p)
@@ -80,9 +79,9 @@ section degrees
8079
lemma degrees_neg (p : mv_polynomial σ R) : (- p).degrees = p.degrees :=
8180
by rw [degrees, support_neg]; refl
8281

83-
lemma degrees_sub (p q : mv_polynomial σ R) :
82+
lemma degrees_sub [decidable_eq σ] (p q : mv_polynomial σ R) :
8483
(p - q).degrees ≤ p.degrees ⊔ q.degrees :=
85-
by simpa only [sub_eq_add_neg] using le_trans (degrees_add p (-q)) (by rw degrees_neg)
84+
by classical; simpa only [sub_eq_add_neg, degrees_neg] using degrees_add p (-q)
8685

8786
end degrees
8887

@@ -93,13 +92,14 @@ variables (p q)
9392
@[simp] lemma vars_neg : (-p).vars = p.vars :=
9493
by simp [vars, degrees_neg]
9594

96-
lemma vars_sub_subset : (p - q).vars ⊆ p.vars ∪ q.vars :=
95+
lemma vars_sub_subset [decidable_eq σ] : (p - q).vars ⊆ p.vars ∪ q.vars :=
9796
by convert vars_add_subset p (-q) using 2; simp [sub_eq_add_neg]
9897

9998
variables {p q}
10099

101100
@[simp]
102-
lemma vars_sub_of_disjoint (hpq : disjoint p.vars q.vars) : (p - q).vars = p.vars ∪ q.vars :=
101+
lemma vars_sub_of_disjoint [decidable_eq σ] (hpq : disjoint p.vars q.vars) :
102+
(p - q).vars = p.vars ∪ q.vars :=
103103
begin
104104
rw ←vars_neg q at hpq,
105105
convert vars_add_of_disjoint hpq using 2;
@@ -148,6 +148,7 @@ lemma degree_of_sub_lt {x : σ} {f g : mv_polynomial σ R} {k : ℕ} (h : 0 < k)
148148
(hg : ∀ (m : σ →₀ ℕ), m ∈ g.support → (k ≤ m x) → coeff m f = coeff m g) :
149149
degree_of x (f - g) < k :=
150150
begin
151+
classical,
151152
rw degree_of_lt_iff h,
152153
intros m hm,
153154
by_contra hc,
@@ -169,9 +170,12 @@ by simp only [total_degree, support_neg]
169170

170171
lemma total_degree_sub (a b : mv_polynomial σ R) :
171172
(a - b).total_degree ≤ max a.total_degree b.total_degree :=
172-
calc (a - b).total_degree = (a + -b).total_degree : by rw sub_eq_add_neg
173-
... ≤ max a.total_degree (-b).total_degree : total_degree_add a (-b)
174-
... = max a.total_degree b.total_degree : by rw total_degree_neg
173+
begin
174+
classical,
175+
calc (a - b).total_degree = (a + -b).total_degree : by rw sub_eq_add_neg
176+
... ≤ max a.total_degree (-b).total_degree : total_degree_add a (-b)
177+
... = max a.total_degree b.total_degree : by rw total_degree_neg
178+
end
175179

176180
end total_degree
177181

‎src/data/mv_polynomial/equiv.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ equivalence, isomorphism, morphism, ring hom, hom
4646

4747
noncomputable theory
4848

49-
open_locale classical big_operators polynomial
49+
open_locale big_operators polynomial
5050

5151
open set function finsupp add_monoid_algebra
5252

‎src/data/mv_polynomial/monad.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -288,9 +288,8 @@ lemma bind₂_monomial_one (f : R →+* mv_polynomial σ S) (d : σ →₀ ℕ)
288288
by rw [bind₂_monomial, f.map_one, one_mul]
289289

290290
section
291-
open_locale classical
292291

293-
lemma vars_bind₁ (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) :
292+
lemma vars_bind₁ [decidable_eq τ] (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) :
294293
(bind₁ f φ).vars ⊆ φ.vars.bUnion (λ i, (f i).vars) :=
295294
begin
296295
calc (bind₁ f φ).vars
@@ -323,7 +322,8 @@ end
323322
lemma mem_vars_bind₁ (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) {j : τ}
324323
(h : j ∈ (bind₁ f φ).vars) :
325324
∃ (i : σ), i ∈ φ.vars ∧ j ∈ (f i).vars :=
326-
by simpa only [exists_prop, finset.mem_bUnion, mem_support_iff, ne.def] using vars_bind₁ f φ h
325+
by classical; simpa only [exists_prop, finset.mem_bUnion, mem_support_iff, ne.def]
326+
using vars_bind₁ f φ h
327327

328328
instance monad : monad (λ σ, mv_polynomial σ R) :=
329329
{ map := λ α β f p, rename f p,

‎src/data/mv_polynomial/pderiv.lean‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ namespace mv_polynomial
4747

4848

4949
open set function finsupp add_monoid_algebra
50-
open_locale classical big_operators
50+
open_locale big_operators
5151

5252
variables {R : Type u} {σ : Type v} {a a' a₁ a₂ : R} {s : σ →₀ ℕ}
5353

@@ -57,12 +57,16 @@ variables {R} [comm_semiring R]
5757

5858
/-- `pderiv i p` is the partial derivative of `p` with respect to `i` -/
5959
def pderiv (i : σ) : derivation R (mv_polynomial σ R) (mv_polynomial σ R) :=
60-
mk_derivation R $ pi.single i 1
60+
by letI := classical.dec_eq σ; exact (mk_derivation R $ pi.single i 1)
61+
62+
lemma pderiv_def [decidable_eq σ] (i : σ) : pderiv i = mk_derivation R (pi.single i 1) :=
63+
by convert rfl
6164

6265
@[simp] lemma pderiv_monomial {i : σ} :
6366
pderiv i (monomial s a) = monomial (s - single i 1) (a * (s i)) :=
6467
begin
65-
simp only [pderiv, mk_derivation_monomial, finsupp.smul_sum, smul_eq_mul,
68+
classical,
69+
simp only [pderiv_def, mk_derivation_monomial, finsupp.smul_sum, smul_eq_mul,
6670
← smul_mul_assoc, ← (monomial _).map_smul],
6771
refine (finset.sum_eq_single i (λ j hj hne, _) (λ hi, _)).trans _,
6872
{ simp [pi.single_eq_of_ne hne] },
@@ -74,14 +78,15 @@ lemma pderiv_C {i : σ} : pderiv i (C a) = 0 := derivation_C _ _
7478

7579
lemma pderiv_one {i : σ} : pderiv i (1 : mv_polynomial σ R) = 0 := pderiv_C
7680

77-
@[simp] lemma pderiv_X [d : decidable_eq σ] (i j : σ) :
78-
pderiv i (X j : mv_polynomial σ R) = @pi.single σ _ d _ i 1 j :=
79-
(mk_derivation_X _ _ _).trans (by congr)
81+
@[simp] lemma pderiv_X [decidable_eq σ] (i j : σ) :
82+
pderiv i (X j : mv_polynomial σ R) = @pi.single _ _ _ _ i 1 j :=
83+
by rw [pderiv_def, mk_derivation_X]
8084

81-
@[simp] lemma pderiv_X_self (i : σ) : pderiv i (X i : mv_polynomial σ R) = 1 := by simp
85+
@[simp] lemma pderiv_X_self (i : σ) : pderiv i (X i : mv_polynomial σ R) = 1 :=
86+
by classical; simp
8287

8388
@[simp] lemma pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv i (X j : mv_polynomial σ R) = 0 :=
84-
by simp [h]
89+
by classical; simp [h]
8590

8691
lemma pderiv_eq_zero_of_not_mem_vars {i : σ} {f : mv_polynomial σ R} (h : i ∉ f.vars) :
8792
pderiv i f = 0 :=

‎src/data/mv_polynomial/rename.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ This will give rise to a monomial in `mv_polynomial σ R` which mathematicians m
4141

4242
noncomputable theory
4343

44-
open_locale classical big_operators
44+
open_locale big_operators
4545

4646
open set function finsupp add_monoid_algebra
4747
open_locale big_operators
@@ -185,6 +185,7 @@ end
185185
theorem exists_finset_rename (p : mv_polynomial σ R) :
186186
∃ (s : finset σ) (q : mv_polynomial {x // x ∈ s} R), p = rename coe q :=
187187
begin
188+
classical,
188189
apply induction_on p,
189190
{ intro r, exact ⟨∅, C r, by rw rename_C⟩ },
190191
{ rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩,
@@ -241,6 +242,7 @@ section coeff
241242
lemma coeff_rename_map_domain (f : σ → τ) (hf : injective f) (φ : mv_polynomial σ R) (d : σ →₀ ℕ) :
242243
(rename f φ).coeff (d.map_domain f) = φ.coeff d :=
243244
begin
245+
classical,
244246
apply induction_on' φ,
245247
{ intros u r,
246248
rw [rename_monomial, coeff_monomial, coeff_monomial],
@@ -252,6 +254,7 @@ lemma coeff_rename_eq_zero (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →
252254
(h : ∀ u : σ →₀ ℕ, u.map_domain f = d → φ.coeff u = 0) :
253255
(rename f φ).coeff d = 0 :=
254256
begin
257+
classical,
255258
rw [rename_eq, ← not_mem_support_iff],
256259
intro H,
257260
replace H := map_domain_support H,
@@ -280,7 +283,8 @@ end coeff
280283

281284
section support
282285

283-
lemma support_rename_of_injective {p : mv_polynomial σ R} {f : σ → τ} (h : function.injective f) :
286+
lemma support_rename_of_injective {p : mv_polynomial σ R} {f : σ → τ} [decidable_eq τ]
287+
(h : function.injective f) :
284288
(rename f p).support = finset.image (map_domain f) p.support :=
285289
begin
286290
rw rename_eq,

‎src/data/mv_polynomial/supported.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ algebra.adjoin R (X '' s)
3838

3939
variables {σ R}
4040

41-
open_locale classical
4241
open algebra
4342

4443
lemma supported_eq_range_rename (s : set σ) :
@@ -67,6 +66,7 @@ variables {s t : set σ}
6766

6867
lemma mem_supported : p ∈ (supported R s) ↔ ↑p.vars ⊆ s :=
6968
begin
69+
classical,
7070
rw [supported_eq_range_rename, alg_hom.mem_range],
7171
split,
7272
{ rintros ⟨p, rfl⟩,

0 commit comments

Comments
 (0)