Custom inequality operators

Stream: new members

[Arjun Vedantham]

Silly question, but is there a way to define custom inequality operators (less than, greater than, etc.) for inductive types?

[Eric Wieser]

Yes, write

instance : LE YourInductiveType where
  le x y := sorry

[Arjun Vedantham]

Great, thanks. Posting this for posterity: https://lean-lang.org/functional_programming_in_lean/type-classes/standard-classes.html

[edklencl]

(deleted)

[Arjun Vedantham]

How can I use these operations in a proof? For context, I have a type like

inductive NatOrBool : Type where
  | natural (n: ℕ)
  | boolean (b: Bool)

and I want to prove something like

NatOrBool.natural 0 < NatOrBool.natural 1

but I'm not sure how to actually use the lt definition for this type, or how to destructure the type to use Nat inequality here

[Arjun Vedantham]

I tried using apply NatOrBool.natural, but that doesn't make any progress (probably not using it correctly?)

[Kevin Buzzard]

You're going to have to define lt on your type first. Is .natural 1 < .boolean true for example? You need to make an instance of LT NatOrBool.

[Arjun Vedantham]

Right, I have an lt definition for this type that looks like:

instance : LT NatOrBool where
  lt x y := match x with
    | NatOrBool.natural n => match y with
      | NatOrBool.natural n' => n > n'
      | NatOrBool.boolean _ => False
    | NatOrBool.boolean _ => False

[Kevin Buzzard]

Well then you can't prove NatOrBool.natural 0 < NatOrBool.natural 1 because it's false :-)

[Kevin Buzzard]

import Mathlib

inductive NatOrBool : Type where
  | natural (n: ℕ)
  | boolean (b: Bool)

instance : LT NatOrBool where
  lt x y := match x with
    | NatOrBool.natural n => match y with
      | NatOrBool.natural n' => n > n'
      | NatOrBool.boolean _ => False
    | NatOrBool.boolean _ => False

example : NatOrBool.natural 0 > NatOrBool.natural 1 := by
  change 0 < 1
  omega

[Arjun Vedantham]

...oh

right. lol. Thanks

[Kevin Buzzard]

Here's the kind of low-level API which you want to prove immediately after your definition, and then everything should be straightforward.

import Mathlib

inductive NatOrBool : Type where
  | natural (n: ℕ)
  | boolean (b: Bool)

instance : LT NatOrBool where
  lt x y := match x with
    | NatOrBool.natural n => match y with
      | NatOrBool.natural n' => n < n' -- changed from >
      | NatOrBool.boolean _ => False
    | NatOrBool.boolean _ => False

namespace NatOrBool

lemma natural_lt_natural (a b : ℕ) : natural a < natural b ↔ a < b := by rfl

lemma not_lt_boolean (n : NatOrBool) (x : Bool) : ¬ n < boolean x := by
  cases n
  · rintro ⟨⟩
  · rintro ⟨⟩

lemma boolean_not_lt (x : Bool) (n : NatOrBool) : ¬ boolean x < n := by
  rintro ⟨⟩

end NatOrBool