-- sorted set of natural numbers
structure NatSet where
  items : List Nat
  invariant : List.Pairwise (· < ·) items

namespace NatSet

-- TODO: binary search
instance : Membership Nat NatSet where
  mem l x := x ∈ l.items

instance (x : Nat) (l : NatSet) : Decidable (x ∈ l) :=
  List.instDecidableMemOfLawfulBEq x l.items

def empty : NatSet := ⟨[], by simp⟩

def singleton (x : Nat) : NatSet :=
  ⟨[x], by simp⟩

def remove (x : Nat) (l : NatSet) : NatSet where
  items := l.items.erase x
  invariant := List.Pairwise.erase x l.invariant

def insert (x : Nat) : NatSet → NatSet
| ⟨[], h⟩ => ⟨[x], List.pairwise_singleton ..⟩
| l@⟨a::as, h⟩ =>
  if a = x
  then l
  else if hlt : x < a
  then ⟨
    x::a::as,
    by
      apply List.pairwise_cons.mpr
      constructor
      · intro a' hmem
        have := List.Pairwise.iff
        sorry
      · assumption
  ⟩
  else
  let ⟨rest, hr⟩ := (NatSet.mk as (List.Pairwise.of_cons h)).insert x
  ⟨
    a::rest,
    by
      simp [*]
      sorry,
  ⟩