Zulip Chat Archive

Stream: mathlib4

Topic: Non-defeq SuccOrder instances

David Loeffler (Dec 24 2024 at 16:27):

I'm getting a weird error in some code I'm writing which uses the notion of a docs#SuccOrder (an ordered set with a "successor" function); it doesn't work as expected if I apply it to the natural numbers.

I think the problem is that Mathlib has two distinct ways of synthesizing an instance of SuccOrder on ℕ:

via docs#SuccAddOrder.toSuccOrder, which provides an instance for which Order.succ n is definitionally Nat.succ n, i.e. n + 1;
or alternatively via docs#LinearLocallyFiniteOrder.instSuccOrderOfLocallyFiniteOrder, which provides a different instance, for which Order.succ n is defined as a choice of GLB of Ioi n.

The two are propositionally equal but not definitionally equal:

import Mathlib.Data.Nat.SuccPred
import Mathlib.Order.SuccPred.LinearLocallyFinite
import Mathlib.Order.Interval.Finset.Nat

example : False := by
  let o1 : SuccOrder ℕ := LinearLocallyFiniteOrder.instSuccOrderOfLocallyFiniteOrder
  let o2 : SuccOrder ℕ  := SuccAddOrder.toSuccOrder
  have : o1 = o2 := by rfl --fails

What's the best solution to this? Maybe LinearLocallyFiniteOrder.instSuccOrderOfLocallyFiniteOrder shouldn't be an instance?

(Tagging @Rémy Degenne, who seems to have been the author of LinearLocallyFiniteOrder.instSuccOrderOfLocallyFiniteOrder)

Rémy Degenne (Dec 24 2024 at 17:50):

I don't remember why I added that instance. Presumably it got me another instance on some type. If I worked on succ orders, it has to be as a tool for something else, not for themselves. If the instance is problematic and removing it does not break too much things, feel free to do it (or fix it in another way).