## 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