How to constrain the elements in a bst to be an Ord

Stream: new members

[Shubham Kumar 🦀 (he/him)]

I am trying to implement a BST and I want to implement a member function, it looks like the following

section BinarySearchTree
  inductive Tree (α : Type)  where
  | Empty : Tree α
  | Node  : Tree α × α × Tree α -> Tree α

  def member {α : Type} [Ord α] (e : α) (t : Tree α) :=
    match e, t with
    | _, Tree.Empty => false
    | x, Tree.Node (a, y, b) =>
      if x < y then member x a
      else if x > y then member x b
      else true
end BinarySearchTree

There is still an issue where x and y don't have an implementation of LT

failed to synthesize instance
  LT α

how do I add an Ord constrain in Tree, deriving doesn't work

failed to synthesize instance
  Ord (Tree α✝ × α✝ × Tree α✝)Lean 4
Ord.{u} (α : Type u) : Type u

[Chris Bailey]

Some general advice for the second part of the question, you're almost always going to get better results by un-tupling arguments to inductives/constructors, in this case changing Tree.Node to 'uncurry' it makes deriving Ord work:

  inductive Tree (α : Type) where
  | Empty : Tree α
  | Node  : Tree α → α → Tree α → Tree α
  deriving Ord

To the first part, I think Ord doesn't get you an _instance_ of LT unless you ask for it to be an instance (ltOfOrd is a definition). So I think without that, the play is to use what functionality is built in to Ord:

  def member {α : Type} [Ord α] (e : α) (t : Tree α) :=
    match e, t with
    | _, Tree.Empty => false
    | x, Tree.Node (a, y, b) =>
      match Ord.compare x y with
      | .lt => member x a
      | .gt => member x b
      | .eq => true

[Shubham Kumar 🦀 (he/him)]

Chris Bailey said:

Some general advice for the second part of the question, you're almost always going to get better results by un-tupling arguments to inductives/constructors, in this case changing Tree.Node to 'uncurry' it makes deriving Ord work:

  inductive Tree (α : Type) where
  | Empty : Tree α
  | Node  : Tree α → α → Tree α → Tree α
  deriving Ord

To the first part, I think Ord doesn't get you an _instance_ of LT unless you ask for it to be an instance (ltOfOrd is a definition). So I think without that, the play is to use what functionality is built in to Ord:

  def member {α : Type} [Ord α] (e : α) (t : Tree α) :=
    match e, t with
    | _, Tree.Empty => false
    | x, Tree.Node (a, y, b) =>
      match Ord.compare x y with
      | .lt => member x a
      | .gt => member x b
      | .eq => true

Thanks! this makes more sense I'll make the changes!