Generalising Finset Nat proofs to SuccOrder

Stream: new members

[Simon Sorg]

I'm currently generalising some of the Finset proofs for Nat to any SuccOrder. This generally only involes replacing the Nat theorems used by similar theorems in the Order namespace. One of the theorems, Ico_succ_right, is more complicated than I initially thought.

I expected the following to work

variable [Preorder α] [LocallyFiniteOrder α] [NoMaxOrder α] [LinearOrder α] [SuccOrder α] {a b : α}
theorem Ico_succ_right : Ico a (Order.succ b) = Icc a b := by
  ext x
  rw [mem_Ico, mem_Icc, Order.lt_succ_iff]

but rw is not happy with this. If I manually instantiate the respective variables for Order.lt_succ_iff, i.e.

theorem Ico_succ_right : Ico a (Order.succ b) = Icc a b := by
  ext x
  rw [mem_Ico, mem_Icc]
  rw [← (Order.lt_succ_iff (a := x))]

the error message points me to the abscence of the SuccOrder typeclass, though it should be present:

failed to synthesize
  SuccOrder α

I would be very glad for any pointers on how to fix this.

[Matt Diamond]

I believe this is what they call an "instance diamond"... this works:

import Mathlib

open Set

variable {α : Type} [LinearOrder α] [LocallyFiniteOrder α] [NoMaxOrder α] [SuccOrder α] {a b : α}
theorem Ico_succ_right : Ico a (Order.succ b) = Icc a b := by
  ext x
  rw [mem_Ico, mem_Icc, Order.lt_succ_iff]

[Matt Diamond]

The issue is that you have redundant typeclasses and Lean gets confused

[Matt Diamond]

it happens when Lean encounters multiple ways of deriving the same instance

[Simon Sorg]

Thanks! So since LinearOrder is a PreOrder, it is redundant and SuccOrder might use the wrong one? I never had this issue before, thanks! I'll make sure to avoid it.