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

-- matchを分割する
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 rb rl rv rr =>
    match rb with
    | .lefty  =>
      match rl with
      | .node rlb rll rlv rlr =>
        match rlb with
        | .lefty  => .inl $ createM (createM l v rll) rlv (createR rlr rv rr)
        | .mid    => .inl $ createM (createM l v rll) rlv (createM rlr rv rr)
        | .righty => .inl $ createM (createL l v rll) rlv (createM rlr rv rr)
    | .mid    => .inr $ createL (createR l v rl) rv rr
    | .righty => .inl $ createM (createM l v rl) rv rr

-- パラメータを明示するとなぜか通る
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 (l := _) (n := _) (r := _) .lefty  (.node (l := _) (n := _) (r := _) .lefty  rll rlv rlr) rv rr => .inl $ createM (createM l v rll) rlv (createR rlr rv rr)
  | .node (l := _) (n := _) (r := _) .lefty  (.node (l := _) (n := _) (r := _) .mid    rll rlv rlr) rv rr => .inl $ createM (createM l v rll) rlv (createM rlr rv rr)
  | .node (l := _) (n := _) (r := _) .lefty  (.node (l := _) (n := _) (r := _) .righty rll rlv rlr) rv rr => .inl $ createM (createL l v rll) rlv (createM rlr rv rr)
  | .node (l := _) (n := _) (r := _) .mid    rl rv rr => .inr $ createL (createR l v rl) rv rr
  | .node (l := _) (n := _) (r := _) .righty rl rv rr => .inl $ createM (createM l v rl) rv rr