AAtree.lean

section Saturday 

  variable 
    {A : Type} 
    [Ord A]

  inductive AAtree : Type 
  | E :  AAtree 
  | T : Nat -> AAtree -> A -> AAtree -> AAtree 
  open AAtree 


  def skew : @AAtree A -> @AAtree A  
  | t@(T lvx (T lvy a ky b) kx c) => 
    match lvx == lvy with 
    | true => T lvx a ky (T lvx b kx c) 
    | _ => t
  | t => t 


  def split : @AAtree A -> @AAtree A  
  | t@(T lvx a kx (T lvy b ky (T lvz c kz d))) =>
    match (lvx == lvy) && (lvy == lvz) with 
    | true => T (lvx + 1) (T lvx a kx b) ky (T lvx c kz d)
    | _ => t 
  | t => t 


  def insert : @AAtree A -> A -> @AAtree A 
  | E, k => T 1 E k E
  | t@(T lt a kt b), k => 
    match compare k kt with 
    | Ordering.lt => split (skew (T lt (insert a k) kt b))
    | Ordering.gt => split (skew (T lt a kt (insert b k)))
    | Ordering.eq => t 


  def lvl : @AAtree A -> Nat 
  | E => 0 
  | T lvt _ _ _ => lvt 


  def sngl : @AAtree A -> Bool 
  | E => false
  | T _ _ _ E => true 
  | T lvx _ _ (T lvy _ _ _ ) => lvy < lvx 


  /- 
    The level of every leaf node is one (zero?).
    This is by definition of E
  -/

  /-
  I am lazy to prove anything :)
  -/
  







      



end Saturday