Option comparison

Stream: new members

[Mark R. Tuttle]

I would like to be able to write none < some 1 and some 1 < some 2.

I can write

def Option.LT (a: Option Nat) (b: Option Nat): Bool :=
  match a, b with
  | none, _ => false
  | some a, some b => a < b
  | _, _ => false

instance: LT (Option Nat) where
  lt := Option.LT

#eval (some 1) < (some 2)

but the instance declaration fails because Option.LT returns a Bool and not a Prop. I can change Option.LT to return a Prop, but now the eval fails because Lean can't synthesize Decidable (some 1 < some 2).

I am about to experiment with something like instance: Decidable Option.LT but I fear I'm starting down the wrong tunnel. Thanks for any pointers you can give me.

[Johan Commelin]

If you are using mathlib, this is docs#WithBot

[Eric Wieser]

I think this instance already exists in core?

[Mark R. Tuttle]

Thanks. For my education, can you help me understand why the instance WithBot.le is considered Decidable and my LT instance above is not?

[Kyle Miller]

It's not automatically opening up the LT instance to see that it's a decidable relation. The Option.LT function is already decidable because it returns a Bool (this means it will return true or false, there's an algorithm here), but in general LT returns a Prop, which is an algorithmless value.

Here's one way to tell Lean "my LT instance is decidable":

def Option.LT (a: Option Nat) (b: Option Nat): Bool :=
  match a, b with
  | none, _ => false
  | some a, some b => a < b
  | _, _ => false

instance: LT (Option Nat) where
  lt := (Option.LT · ·)

instance : DecidableRel (· < · : Option Nat → _ → _) :=
  inferInstanceAs <| DecidableRel (Option.LT · ·)

(I was getting a type mismatch error without using (Option.LT · ·) instead of Option.LT.)