DepTree.lean

DepTree.lean

inductive Balance: Nat -> Nat -> Nat -> Type where
  | lefty : Balance n.succ n.succ.succ n
  | mid   : Balance n      n.succ      n
  | righty: Balance n      n.succ.succ n.succ

inductive Tree (a: Type u): Nat -> Type u where
  | leaf: Tree a 0
  | node: Balance l n r -> Tree a l -> a -> Tree a r-> Tree a n


def Tree.empty: Tree a 0 :=
    .leaf

def Tree.singleton (x: a): Tree a 1 :=
    .node .mid .leaf x .leaf


def member [Ord a] (t: Tree a n) (x: a): Bool :=
  match t with
  | .leaf => false
  | .node _ l y r => match compare x y with
    | .lt => member l x
    | .eq => true
    | .gt => member r x


def createR (l: Tree a n) (x: a) (r: Tree a n.succ): Tree a n.succ.succ :=
  .node .righty l x r

def createM (l: Tree a n) (x: a) (r: Tree a n): Tree a n.succ :=
  .node .mid l x r

def createL (l: Tree a n.succ) (x: a) (r: Tree a n): Tree a n.succ.succ :=
  .node .lefty l x r

def rotateL (l: Tree a n) (v: a) (r: Tree a n.succ.succ): (Tree a n.succ.succ) ⊕ (Tree a n.succ.succ.succ) :=
  match r with
  | .node .lefty (.node .lefty  rll rlv rlr) rv rr => .inl $ createM (createM l v rll) rlv (createR rlr rv rr)
  | .node .lefty (.node .mid    rll rlv rlr) rv rr => .inl $ createM (createM l v rll) rlv (createM rlr rv rr)
  | .node .lefty (.node .righty rll rlv rlr) rv rr => .inl $ createM (createL l v rll) rlv (createM rlr rv rr)
  | .node .mid                          rl   rv rr => .inr $ createL (createR l v rl)                   rv rr
  | .node .righty                       rl   rv rr => .inl $ createM (createM l v rl)                   rv rr

-- def rotateR (l: Tree a (.succ (.succ n))) (v: a) (r: Tree a n): (Tree a (.succ (.succ n))) ⊕ (Tree a (.succ (.succ (.succ n)))) :=
--   match l with
--   | .node .lefty  ll lv lr                          => .inl (createM ll lv (createM lr v r))
--   | .node .mid    ll lv lr                          => .inr (createR ll lv (createL lr v r))
--   | .node .righty ll lv (.node .lefty  lrl lrv lrr) => .inl (createM (createM ll lv lrl) lrv (createR lrr v r))
--   | .node .righty ll lv (.node .mid    lrl lrv lrr) => .inl (createM (createM ll lv lrl) lrv (createM lrr v r))
--   | .node .righty ll lv (.node .righty lrl lrv lrr) => .inl (createM (createL ll lv lrl) lrv (createM lrr v r))