Bool from LT/LE

Stream: lean4

[Joscha Mennicken]

Comparing numbers like a < b && c <= d seems to result in a Bool, but after implementing LT, LE and Ord for a structure, lean complains that a < b is a Prop and not a Bool. However, there don't seem to be BLe or BLt classes like with BEq. When does this automatic conversion between Prop and Bool work?

[Chris B]

There are two coercions, one from Bool to Prop and one from Decidable Props to Bool

[Joscha Mennicken]

So I would need an instance (a b : MyStructure) : Decidable (a < b) (and the same for <=) in addition to my LT and LE instances to be able to use these comparisons in code

[Henrik Böving]

Yes, in general if then else statement can do a decision based on any proposition that implements the Decidable type class (either directly or through TC synthesis)

[Chris B]

If you're working with a structure and the fields implement DecidableEq and Ord, you can derive them for your new structure:

structure X where
  val : Nat
deriving DecidableEq, Ord

And Ord gets you instances of LT and LE.

[Joscha Mennicken]

Ah, ltOfOrd and leOfOrd give me the appropriate Decidable instances as a bonus

[Nicolas Rouquette]

I have a related question: how do I require an instance of Decidable for a comparison?

Here is a simple example:

import Std.Data.HashSet
open Std

-- Question: Can this be generalized to a HashSet of α if there is LT.lt α?
instance : Repr (HashSet String) where
  reprPrec hs _ :=
    let as : Array String := hs.toArray.qsort (fun a b => a < b)
    as.toList.toString

instance [comp: LT α] [Decidable comp.lt] [ToString α] [Inhabited α] [BEq α] [Repr α] [Hashable α]: Repr (HashSet α) where
  reprPrec hs x :=
    let as : Array α := hs.toArray.qsort (fun a b => a < b)
    as.toList.toString

This has two errors:

• [Decidable comp.lt] seems the wrong syntax to require a decidable comparison.
• The sort predicate is a Prop, not a Bool

How do I fix this?

[François G. Dorais]

There's a couple of common patterns:

• [LT α] [DecidableRel (α:=α) (.<.)]
• [LT α] [DecidableRel (.<. : α → α → Prop)]
• [LT α] [DecidableRel (@LT.lt α)]

Also consider using [Ord α] instead.

[Nicolas Rouquette]

Thanks @François G. Dorais !

I managed to make this work with all the patterns you suggested!

import Std.Data.HashSet
open Std

-- Question: Can this be generalized to a HashSet of α if there is LT.lt α?
instance : Repr (HashSet String) where
  reprPrec hs _ :=
    let as : Array String := hs.toArray.qsort (fun a b => a < b)
    as.toList.toString

instance [LT α] [DecidableRel (α:=α) (.<.)] [ToString α] [Inhabited α] [BEq α] [Repr α] [Hashable α]: Repr (HashSet α) where
  reprPrec hs _ :=
    let as : Array α := hs.toArray.qsort (.<.)
    as.toList.toString

instance [LT α] [DecidableRel (.<. : α → α → Prop)] [ToString α] [Inhabited α] [BEq α] [Repr α] [Hashable α]: Repr (HashSet α) where
  reprPrec hs _ :=
    let as : Array α := hs.toArray.qsort (.<.)
    as.toList.toString

instance [lt: LT α] [DecidableRel lt.lt] [ToString α] [Inhabited α] [BEq α] [Repr α] [Hashable α]: Repr (HashSet α) where
  reprPrec hs _ :=
    let as : Array α := hs.toArray.qsort (.<.)
    as.toList.toString

instance [LT α] [ord:Ord α] [ToString α] [Inhabited α] [BEq α] [Repr α] [Hashable α]: Repr (HashSet α) where
  reprPrec hs _ :=
    let as : Array α := hs.toArray.qsort (fun a b => ord.compare a b == Ordering.lt)
    as.toList.toString

The last one above seems to me like a TC bad smell since(fun a b => ord.compare a b == Ordering.lt) is clearly a duplication of Lean's TC instance:

instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
  inferInstanceAs (DecidableRel (fun a b => compare a b == Ordering.lt))

Is there a TC instantiation trick that would help avoid this unnecessary duplication?