# Zulip Chat Archive

## Stream: new members

### Topic: Instance affects other sections

#### AHan (Jan 01 2019 at 12:34):

import data.finsupp variables {σ : Type*} {α : Type*} section a variables [comm_semiring α] [decidable_eq σ] [decidable_eq α] [linear_order (σ →₀ ℕ)] [@decidable_rel (σ →₀ ℕ) (≤)] instance : decidable_linear_order (σ →₀ ℕ) := { decidable_le := _inst_5, decidable_eq := by apply_instance, .._inst_4 } end a section b variables [integral_domain α] [decidable_eq σ] [decidable_eq α] [linear_order (σ →₀ ℕ)] [@decidable_rel (σ →₀ ℕ) (≤)] end b

The error message : "is maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')" at the `(≤)`

in `section b`

seems like `section b`

is affected by the `decidable_linear_order`

instance in `section a`

, but I don't understand why, and how to fix this...

#### Kevin Buzzard (Jan 01 2019 at 13:02):

I don't have access to Lean right now but is the issue that the instance gives you a linear order on the finsupp and then in section b you are putting another unrelated order on the finsupp and hence breaking the golden rule of typeclasses -- one instance per type?

#### Reid Barton (Jan 01 2019 at 13:33):

instances are not scoped to sections

#### Reid Barton (Jan 01 2019 at 13:34):

It's just as though you wrote `instance <long string of variables> : decidable_linear_order (σ →₀ ℕ)`

at the top level.

#### Reid Barton (Jan 01 2019 at 13:35):

If you want to make a scoped instance, you can write an ordinary definition and then give it `local attribute [instance]`

inside a `section`

#### Chris Hughes (Jan 01 2019 at 13:39):

Leaving aside the `section`

issue, I think this is a bad instance, because there's a cycle, there's a `linear_order`

to `decidable_linear_order`

instance, and a `decidable_linear_order`

to `linear_order`

instance somewhere in the library. This sort of thing can cause type class inference to get stuck.

#### AHan (Jan 01 2019 at 13:44):

@Kevin Buzzard actually the order in `section a`

and `section b`

are the same in my case, but some functions in `section a`

are only depend on `comm_semiring α`

, while functions in `section b`

are depend on `integral_domain α`

. I can only think of using seperate sections like this to avoid confilict between `comm_semiring α`

and `integral_domain α`

#### Reid Barton (Jan 01 2019 at 13:47):

From what you've provided so far it looks like the hypotheses involving $\alpha$ are independent of the hypotheses involving $\sigma$

#### Reid Barton (Jan 01 2019 at 13:47):

that is, no hypothesis involves both

#### AHan (Jan 01 2019 at 13:49):

@Reid Barton you mean like ?

def x [decidable_eq σ] [linear_order (σ →₀ ℕ)] [@decidable_rel (σ →₀ ℕ) (≤)] : decidable_linear_order (σ →₀ ℕ) := { decidable_le := _inst_3, decidable_eq := by apply_instance, .._inst_2 }

#### Reid Barton (Jan 01 2019 at 13:52):

Yes, or using `variables`

the way you do now is also fine.

#### AHan (Jan 01 2019 at 13:55):

Then when a lemma needs this decidable_linear_order instance, it won't automatically infer this instance right?

#### Reid Barton (Jan 01 2019 at 13:57):

That's right, but you can "install" the instance locally in a proof using `letI`

#### AHan (Jan 01 2019 at 13:58):

@Chris Hughes Yeah..you're right...

but I can't just add an instance `[decidable_linear_order (σ →₀ ℕ)]`

, as it might cause conflict between `finsupp.decidable_eq`

and `decidable_linear_order.decidable_eq`

#### Chris Hughes (Jan 01 2019 at 14:05):

`decidable_linear_order.decidable_eq`

isn't an instance, so it's okay.

#### AHan (Jan 01 2019 at 14:21):

But I do encounter such kind of error... some term looks just the same, and I couldn't use `rw`

tactic

#### AHan (Jan 01 2019 at 14:41):

This is the minimal example I can figure out so far...

there is a type mismatch at `rw union_min'`

which says `h₁`

uses `finsupp.decidable_eq`

but the third parameter of `union_min'`

is expected to use `eq.decidable`

import linear_algebra.multivariate_polynomial import data.finset variables {σ : Type*} {α : Type*} {β : Type*} lemma ne_empty_union [decidable_eq α] {s₁ s₂ : finset α} : ¬ (s₁ = ∅ ∧ s₂ = ∅) ↔ s₁ ∪ s₂ ≠ ∅ := sorry section a variables [has_zero β] [decidable_eq α] [decidable_eq β] lemma support_ne_empty (a : α →₀ β) : a ≠ 0 ↔ a.support ≠ ∅ := by finish end a section b variables [decidable_linear_order α] lemma union_min' {s₁ s₂ : finset α} (hs₁ : s₁ ≠ ∅) (hs₂ : s₂ ≠ ∅) (hs₃ : s₁ ∪ s₂ ≠ ∅): (s₁ ∪ s₂).min' hs₃ = min (s₁.min' hs₁) (s₂.min' hs₂) := sorry end b section c variables [decidable_eq σ] [decidable_eq α] [decidable_linear_order (σ →₀ ℕ)] variables [comm_semiring α] lemma x {p q : mv_polynomial σ α} (hp : p ≠ 0) (hq : q ≠ 0) (hpq : p + q ≠ 0) : p + q ≠ 0 := begin have h₁ := (ne_empty_union.1 (not_and_of_not_left (q.support = ∅) ((support_ne_empty p).1 hp))), let h : finset.min' _ h₁ = finset.min' _ h₁ := by refl, rw union_min' ((support_ne_empty p).1 hp) ((support_ne_empty q).1 hq) h₁ at h, end end c

#### Patrick Massot (Jan 01 2019 at 17:14):

I'm not sure I understand your question, but you may like:

lemma x {p q : mv_polynomial σ α} (hp : p ≠ 0) (hq : q ≠ 0) (hpq : p + q ≠ 0) : p + q ≠ 0 := begin have h₁ := ne_empty_union.1 (not_and_of_not_left (q.support = ∅) $ (support_ne_empty p).1 hp), have := union_min' ((support_ne_empty p).1 hp) ((support_ne_empty q).1 hq) (by convert h₁), exact hpq end

#### Patrick Massot (Jan 01 2019 at 17:36):

and I suspect that filling in the decidable_linear_order instance would help avoiding the problem

#### Chris Hughes (Jan 01 2019 at 17:46):

It's not a nice solution, but adding this line before `x`

works `local attribute [instance, priority 0] finsupp.decidable_eq`

. There's not a good solution for this sort of thing in general at the moment.

#### AHan (Jan 01 2019 at 18:22):

@Patrick Massot @Chris Hughes Thanks a lot! Both solutions seems to solve my problem.

Last updated: May 14 2021 at 12:18 UTC