Zulip Chat Archive

Stream: new members

Topic: Instance affects other sections


view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jan 01 2019 at 13:33):

instances are not scoped to sections

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 α

view this post on Zulip 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

view this post on Zulip Reid Barton (Jan 01 2019 at 13:47):

that is, no hypothesis involves both

view this post on Zulip 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
}

view this post on Zulip Reid Barton (Jan 01 2019 at 13:52):

Yes, or using variables the way you do now is also fine.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jan 01 2019 at 13:57):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jan 01 2019 at 14:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 01 2019 at 17:36):

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

view this post on Zulip 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.

view this post on Zulip 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