DecidableLT for LawfulOrderLT

Stream: Is there code for X?

[Wrenna Robson]

Am I right in saying we don't have this instance? Is there a reason why?

instance (α : Type u) [LE α] [LT α] [Std.LawfulOrderLT α] [DecidableLE α] :
    DecidableLT α := (decidable_of_iff' _ <| Std.LawfulOrderLT.lt_iff · ·)

(Presumably it could go in Std but if that was not wanted, surely it at least has a place in Batteries?)

[Markus Himmel]

This is docs#Std.FactoryInstances.decidableLTOfLE. It doesn't make sense as a global instance because there might be a more efficient implementation of DecidableLT that you want to use instead.

The way this is supposed to work is that you define your type, and then use something like docs#Std.LinearPreorderPackage.ofLE to provide all of the order instances at once. At this point you can choose which of the function you want to provide with custom, efficient implementations, and all of the data that you choose not to provide yourself is filled using things like docs#Std.FactoryInstances.decidableLTOfLE.

[Wrenna Robson]

Got it, makes sense.

[Wrenna Robson]

And then decide (a < b) = decide (a <= b) || !decide (b <= a) is either a theorem somewhere or just a simple consequence of others.

[Wrenna Robson]

(i.e. when you have both decidability instances and it is lawful, you can prove that the decidability is compatible in this way)

[Markus Himmel]

Yes, something like this (I had to change your statement a bit, is this what you meant?):

example {α : Type} (a b : α) [LT α] [LE α] [Std.LawfulOrderLT α] [DecidableLT α] [DecidableLE α] :
    decide (a < b) = (decide (a <= b) && !decide (b <= a)) := by
  simp [Std.LawfulOrderLT.lt_iff]

[Wrenna Robson]

Yes, it is :)

[Wrenna Robson]

One could argue that might be worthwhile as a theorem somewhere but it's much of a muchness. Thanks!