lean4-htt/tests/elab/partial_fixpoint_aeneas2.lean

import Lean

/-!

Provided by Son Ho

I put together some of the files generated by Aeneas (they come from the models generated for a
hashmap, an AVL tree and a b-epsilon tree) into a single self-contained file: from what I remember
some definitions there triggered issues with divergent, so I think they should be good test cases
for partial_def, at least to see whether your implementation covers all my use cases. :-)

Note that many definitions are actually structurally terminating (I still added termination clauses
to them so that you can easily find them): they also are good test cases for partial_def. Also, as a
side note: whenever Aeneas generates a recursive definition, it adds the divergent keyword (because
I haven't implemented a termination checker, and I actually don't see the point of doing that).
-/

/- Duplicating some basic definitions -/
namespace Primitives
  inductive Error where
    | assertionFailure: Error
    | integerOverflow: Error
    | divisionByZero: Error
    | arrayOutOfBounds: Error
    | maximumSizeExceeded: Error
    | panic: Error
    -- Added by Joachim
    | nontermination : Error



  inductive Result (α : Type u) where
    | ok (v: α): Result α
    | fail (e: Error): Result α
    | div

  open Result

  def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
    match x with
    | ok v  => f v
    | fail v => fail v
    | div => div

  instance : Bind Result where
    bind := bind

  instance : Pure Result where
    pure := fun x => ok x


  -- Added by Joachim
  section Order
  open Lean.Order

  instance : PartialOrder (Result α) := inferInstanceAs (PartialOrder (FlatOrder (.fail .nontermination)))
  set_option backward.inferInstanceAs.wrap.reuseSubInstances false in
  noncomputable instance : CCPO (Result α) := inferInstanceAs (CCPO (FlatOrder (.fail .nontermination)))
  noncomputable instance : MonoBind Result where
    bind_mono_left h := by
      cases h
      · exact FlatOrder.rel.bot
      · exact FlatOrder.rel.refl
    bind_mono_right h := by
      cases ‹Result _›
      · exact h _
      · exact FlatOrder.rel.refl
      · exact FlatOrder.rel.refl
  end Order

  structure Isize where
    val : Int
    hmin : -2147483648 ≤ val
    hmax : val ≤ 2147483647

  @[reducible] def Isize.ofInt (x : Int)
    (hInBounds : -2147483648 ≤ x ∧ x ≤ 2147483647) : Isize :=
    ⟨ x, by simp [*], by simp [*] ⟩

  macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by decide))

  instance : LT Isize where lt a b := LT.lt a.val b.val
  instance : LE Isize where le a b := LE.le a.val b.val
  instance Isize.decLt (a b : Isize) : Decidable (LT.lt a b) := Int.decLt ..
  instance Isize.decLe (a b : Isize) : Decidable (LE.le a b) := Int.decLe ..

  theorem Isize.eq_of_val_eq : ∀ {i j : Isize}, Eq i.val j.val → Eq i j
    | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl

  theorem Isize.val_eq_of_eq {i j : Isize} (h : Eq i j) : Eq i.val j.val :=
    h ▸ rfl

  theorem Isize.ne_of_val_ne {i j : Isize} (h : Not (Eq i.val j.val)) : Not (Eq i j) :=
    fun h' => absurd (val_eq_of_eq h') h

  instance : DecidableEq Isize :=
    fun i j =>
      match decEq i.val j.val with
      | isTrue h  => isTrue (Isize.eq_of_val_eq h)
      | isFalse h => isFalse (Isize.ne_of_val_ne h)

  -- Using `sorry` rather than axiom so that I don't have to mark definitions as `noncomputable`
  -- We could also use variables...
  def Isize.add : Isize → Isize → Result Isize := sorry
  def Isize.sub : Isize → Isize → Result Isize := sorry
  def Isize.mul : Isize → Isize → Result Isize := sorry
  def Isize.mod : Isize → Isize → Result Isize := sorry
  def Isize.div : Isize → Isize → Result Isize := sorry

  instance : HAdd Isize Isize (Result Isize) where
    hAdd x y := Isize.add x y

  instance : HSub Isize Isize (Result Isize) where
    hSub x y := Isize.sub x y

  instance : HMul Isize Isize (Result Isize) where
    hMul x y := Isize.mul x y

  instance : HMod Isize Isize (Result Isize) where
    hMod x y := Isize.mod x y

  instance : HDiv Isize Isize (Result Isize) where
    hDiv x y := Isize.div x y

  def alloc.vec.Vec (T : Type) : Type := sorry
  def alloc.vec.Vec.len {T : Type} : alloc.vec.Vec T → Isize := sorry
  def alloc.vec.Vec.new : (T:Type) → alloc.vec.Vec T := sorry
  def alloc.vec.Vec.push {T : Type} : alloc.vec.Vec T → T → Result (alloc.vec.Vec T) := sorry
  def alloc.vec.Vec.index_isize {α : Type} (v: Vec α) (i: Isize) : Result α := sorry
  def alloc.vec.Vec.index_mut_isize {α : Type} (v: Vec α) (i: Isize) : Result (α × (α → Vec α)) := sorry

  opaque core.mem.replace {T : Type} : T → T → T × T := fun x _ => (x, x)
  def core.option.Option.unwrap {T : Type} : Option T → Result T := sorry

  def core_isize_max : Isize := 2147483647#isize

  structure core.clone.Clone (T : Type) where
    clone : T → Result T

  structure core.marker.Copy (T : Type) where
    cloneInst : core.clone.Clone T
end Primitives

open Primitives

/- Hashmap -/
namespace hashmap
  inductive AList (T : Type) where
  | Cons : Isize → T → AList T → AList T
  | Nil : AList T

  structure Fraction where
    dividend : Isize
    divisor : Isize

  structure HashMap (T : Type) where
    num_entries : Isize
    max_load_factor : Fraction
    max_load : Isize
    saturated : Bool
    slots : alloc.vec.Vec (AList T)

  def hash_key (k : Isize) : Result Isize :=
    Result.ok k

  def ClonehashmapFraction.clone (self : Fraction) : Result Fraction :=
    Result.ok self

  @[reducible]
  def core.clone.ClonehashmapFraction : core.clone.Clone Fraction := {
    clone := ClonehashmapFraction.clone
  }

  @[reducible]
  def core.marker.CopyhashmapFraction : core.marker.Copy Fraction := {
    cloneInst := core.clone.ClonehashmapFraction
  }

  def HashMap.allocate_slots_loop
    {T : Type} (slots : alloc.vec.Vec (AList T)) (n : Isize) :
    Result (alloc.vec.Vec (AList T))
    :=
    if n > 0#isize
    then
      do
      let slots1 ← alloc.vec.Vec.push slots AList.Nil
      let n1 ← n - 1#isize
      HashMap.allocate_slots_loop slots1 n1
    else Result.ok slots
  partial_fixpoint

  def HashMap.allocate_slots
    {T : Type} (slots : alloc.vec.Vec (AList T)) (n : Isize) :
    Result (alloc.vec.Vec (AList T))
    :=
    HashMap.allocate_slots_loop slots n

  def HashMap.new_with_capacity
    (T : Type) (capacity : Isize) (max_load_factor : Fraction) :
    Result (HashMap T)
    :=
    do
    let slots ← HashMap.allocate_slots (alloc.vec.Vec.new (AList T)) capacity
    let i ← capacity * max_load_factor.dividend
    let i1 ← i / max_load_factor.divisor
    Result.ok
      {
        num_entries := 0#isize,
        max_load_factor,
        max_load := i1,
        saturated := false,
        slots
      }

  def HashMap.new (T : Type) : Result (HashMap T) :=
    HashMap.new_with_capacity T 32#isize
      { dividend := 4#isize, divisor := 5#isize }

  def HashMap.clear_loop
    {T : Type} (slots : alloc.vec.Vec (AList T)) (i : Isize) :
    Result (alloc.vec.Vec (AList T))
    :=
    let i1 := alloc.vec.Vec.len slots
    if i < i1
    then
      do
      let (_, index_mut_back) ← alloc.vec.Vec.index_mut_isize slots i
      let i2 ← i + 1#isize
      let slots1 := index_mut_back AList.Nil
      HashMap.clear_loop slots1 i2
    else Result.ok slots
  partial_fixpoint

  def HashMap.clear {T : Type} (self : HashMap T) : Result (HashMap T) :=
    do
    let hm ← HashMap.clear_loop self.slots 0#isize
    Result.ok { self with num_entries := 0#isize, slots := hm }

  def HashMap.len {T : Type} (self : HashMap T) : Result Isize :=
    Result.ok self.num_entries

  def HashMap.insert_in_list_loop
    {T : Type} (key : Isize) (value : T) (ls : AList T) :
    Result (Bool × (AList T))
    :=
    match ls with
    | AList.Cons ckey cvalue tl =>
      if ckey = key
      then Result.ok (false, AList.Cons ckey value tl)
      else
        do
        let (b, tl1) ← HashMap.insert_in_list_loop key value tl
        Result.ok (b, AList.Cons ckey cvalue tl1)
    | AList.Nil => Result.ok (true, AList.Cons key value AList.Nil)
  partial_fixpoint

  def HashMap.insert_in_list
    {T : Type} (key : Isize) (value : T) (ls : AList T) :
    Result (Bool × (AList T))
    :=
    HashMap.insert_in_list_loop key value ls

  def HashMap.insert_no_resize
    {T : Type} (self : HashMap T) (key : Isize) (value : T) :
    Result (HashMap T)
    :=
    do
    let hash ← hash_key key
    let i := alloc.vec.Vec.len self.slots
    let hash_mod ← hash % i
    let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize self.slots hash_mod
    let (inserted, a1) ← HashMap.insert_in_list key value a
    if inserted
    then
      do
      let i1 ← self.num_entries + 1#isize
      let v := index_mut_back a1
      Result.ok { self with num_entries := i1, slots := v }
    else
      let v := index_mut_back a1
      Result.ok { self with slots := v }

  def HashMap.move_elements_from_list_loop
    {T : Type} (ntable : HashMap T) (ls : AList T) : Result (HashMap T) :=
    match ls with
    | AList.Cons k v tl =>
      do
      let ntable1 ← HashMap.insert_no_resize ntable k v
      HashMap.move_elements_from_list_loop ntable1 tl
    | AList.Nil => Result.ok ntable
  partial_fixpoint

  def HashMap.move_elements_from_list
    {T : Type} (ntable : HashMap T) (ls : AList T) : Result (HashMap T) :=
    HashMap.move_elements_from_list_loop ntable ls

  def HashMap.move_elements_loop
    {T : Type} (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Isize)
    :
    Result ((HashMap T) × (alloc.vec.Vec (AList T)))
    :=
    let i1 := alloc.vec.Vec.len slots
    if i < i1
    then
      do
      let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize slots i
      let (ls, a1) := core.mem.replace a AList.Nil
      let ntable1 ← HashMap.move_elements_from_list ntable ls
      let i2 ← i + 1#isize
      let slots1 := index_mut_back a1
      HashMap.move_elements_loop ntable1 slots1 i2
    else Result.ok (ntable, slots)
  partial_fixpoint

  def HashMap.move_elements
    {T : Type} (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) :
    Result ((HashMap T) × (alloc.vec.Vec (AList T)))
    :=
    HashMap.move_elements_loop ntable slots 0#isize

  def HashMap.try_resize {T : Type} (self : HashMap T) : Result (HashMap T) :=
    do
    let capacity := alloc.vec.Vec.len self.slots
    let n1 ← core_isize_max / 2#isize
    let i ← n1 / self.max_load_factor.dividend
    if capacity <= i
    then
      do
      let i1 ← capacity * 2#isize
      let ntable ← HashMap.new_with_capacity T i1 self.max_load_factor
      let p ← HashMap.move_elements ntable self.slots
      let (ntable1, _) := p
      Result.ok
        { self with max_load := ntable1.max_load, slots := ntable1.slots }
    else Result.ok { self with saturated := true }

  def HashMap.insert
    {T : Type} (self : HashMap T) (key : Isize) (value : T) :
    Result (HashMap T)
    :=
    do
    let self1 ← HashMap.insert_no_resize self key value
    let i ← HashMap.len self1
    if i > self1.max_load
    then
      if self1.saturated
      then Result.ok self1
      else HashMap.try_resize self1
    else Result.ok self1

  def HashMap.contains_key_in_list_loop
    {T : Type} (key : Isize) (ls : AList T) : Result Bool :=
    match ls with
    | AList.Cons ckey _ tl =>
      if ckey = key
      then Result.ok true
      else HashMap.contains_key_in_list_loop key tl
    | AList.Nil => Result.ok false
  partial_fixpoint

  def HashMap.contains_key_in_list
    {T : Type} (key : Isize) (ls : AList T) : Result Bool :=
    HashMap.contains_key_in_list_loop key ls

  def HashMap.contains_key
    {T : Type} (self : HashMap T) (key : Isize) : Result Bool :=
    do
    let hash ← hash_key key
    let i := alloc.vec.Vec.len self.slots
    let hash_mod ← hash % i
    let a ← alloc.vec.Vec.index_isize self.slots hash_mod
    HashMap.contains_key_in_list key a

  def HashMap.get_in_list_loop
    {T : Type} (key : Isize) (ls : AList T) : Result (Option T) :=
    match ls with
    | AList.Cons ckey cvalue tl =>
      if ckey = key
      then Result.ok (some cvalue)
      else HashMap.get_in_list_loop key tl
    | AList.Nil => Result.ok none
  partial_fixpoint

  def HashMap.get_in_list
    {T : Type} (key : Isize) (ls : AList T) : Result (Option T) :=
    HashMap.get_in_list_loop key ls

  def HashMap.get
    {T : Type} (self : HashMap T) (key : Isize) : Result (Option T) :=
    do
    let hash ← hash_key key
    let i := alloc.vec.Vec.len self.slots
    let hash_mod ← hash % i
    let a ← alloc.vec.Vec.index_isize self.slots hash_mod
    HashMap.get_in_list key a

  def HashMap.get_mut_in_list_loop
    {T : Type} (ls : AList T) (key : Isize) :
    Result ((Option T) × (Option T → AList T))
    :=
    match ls with
    | AList.Cons ckey cvalue tl =>
      if ckey = key
      then
        let back :=
          fun ret =>
            let t := match ret with
                    | some t1 => t1
                    | _ => cvalue
            AList.Cons ckey t tl
        Result.ok (some cvalue, back)
      else
        do
        let (o, back) ← HashMap.get_mut_in_list_loop tl key
        let back1 := fun ret => let tl1 := back ret
                                AList.Cons ckey cvalue tl1
        Result.ok (o, back1)
    | AList.Nil => let back := fun _ret => AList.Nil
                  Result.ok (none, back)
  partial_fixpoint

  def HashMap.get_mut_in_list
    {T : Type} (ls : AList T) (key : Isize) :
    Result ((Option T) × (Option T → AList T))
    :=
    HashMap.get_mut_in_list_loop ls key

  def HashMap.get_mut
    {T : Type} (self : HashMap T) (key : Isize) :
    Result ((Option T) × (Option T → HashMap T))
    :=
    do
    let hash ← hash_key key
    let i := alloc.vec.Vec.len self.slots
    let hash_mod ← hash % i
    let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize self.slots hash_mod
    let (o, get_mut_in_list_back) ← HashMap.get_mut_in_list a key
    let back :=
      fun ret =>
        let a1 := get_mut_in_list_back ret
        let v := index_mut_back a1
        { self with slots := v }
    Result.ok (o, back)

  def HashMap.remove_from_list_loop
    {T : Type} (key : Isize) (ls : AList T) : Result ((Option T) × (AList T)) :=
    match ls with
    | AList.Cons ckey t tl =>
      if ckey = key
      then
        let (mv_ls, _) := core.mem.replace ls AList.Nil
        match mv_ls with
        | AList.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
        | AList.Nil => Result.fail .panic
      else
        do
        let (o, tl1) ← HashMap.remove_from_list_loop key tl
        Result.ok (o, AList.Cons ckey t tl1)
    | AList.Nil => Result.ok (none, AList.Nil)
  partial_fixpoint

  def HashMap.remove_from_list
    {T : Type} (key : Isize) (ls : AList T) : Result ((Option T) × (AList T)) :=
    HashMap.remove_from_list_loop key ls

  def HashMap.remove
    {T : Type} (self : HashMap T) (key : Isize) :
    Result ((Option T) × (HashMap T))
    :=
    do
    let hash ← hash_key key
    let i := alloc.vec.Vec.len self.slots
    let hash_mod ← hash % i
    let (a, index_mut_back) ← alloc.vec.Vec.index_mut_isize self.slots hash_mod
    let (x, a1) ← HashMap.remove_from_list key a
    match x with
    | none =>
      let v := index_mut_back a1
      Result.ok (none, { self with slots := v })
    | some _ =>
      do
      let i1 ← self.num_entries - 1#isize
      let v := index_mut_back a1
      Result.ok (x, { self with num_entries := i1, slots := v })

end hashmap

namespace betree

  inductive betree.List (T : Type) where
  | Cons : T → betree.List T → betree.List T
  | Nil : betree.List T

  inductive betree.UpsertFunState where
  | Add : Isize → betree.UpsertFunState
  | Sub : Isize → betree.UpsertFunState

  inductive betree.Message where
  | Insert : Isize → betree.Message
  | Delete : betree.Message
  | Upsert : betree.UpsertFunState → betree.Message

  structure betree.Leaf where
    id : Isize
    size : Isize

  mutual

  inductive betree.Internal where
  | mk : Isize → Isize → betree.Node → betree.Node → betree.Internal

  inductive betree.Node where
  | Internal : betree.Internal → betree.Node
  | Leaf : betree.Leaf → betree.Node

  end

  @[reducible]
  def betree.Internal.id (x : betree.Internal) :=
    match x with | betree.Internal.mk x1 _ _ _ => x1

  @[reducible]
  def betree.Internal.pivot (x : betree.Internal) :=
    match x with | betree.Internal.mk _ x1 _ _ => x1

  @[reducible]
  def betree.Internal.left (x : betree.Internal) :=
    match x with | betree.Internal.mk _ _ x1 _ => x1

  @[reducible]
  def betree.Internal.right (x : betree.Internal) :=
    match x with | betree.Internal.mk _ _ _ x1 => x1

  /- [betree::betree::Params]
    Source: 'src/betree.rs', lines 187:0-199:1 -/
  structure betree.Params where
    min_flush_size : Isize
    split_size : Isize

  /- [betree::betree::NodeIdCounter]
    Source: 'src/betree.rs', lines 201:0-203:1 -/
  structure betree.NodeIdCounter where
    next_node_id : Isize

  /- [betree::betree::BeTree]
    Source: 'src/betree.rs', lines 218:0-225:1 -/
  structure betree.BeTree where
    params : betree.Params
    node_id_cnt : betree.NodeIdCounter
    root : betree.Node

  def betree_utils.load_internal_node
  :
  Isize → State → Result (State × (betree.List (Isize × betree.Message))) :=
  fun _ _ => .fail .panic

  def betree_utils.store_internal_node
    :
    Isize → betree.List (Isize × betree.Message) → State → Result (State
      × Unit) :=
    fun _ _ _ => .fail .panic

  def betree_utils.load_leaf_node
    : Isize → State → Result (State × (betree.List (Isize × Isize))) :=
    fun _ _ => .fail .panic

  def betree_utils.store_leaf_node
    : Isize → betree.List (Isize × Isize) → State → Result (State × Unit) :=
    fun _ _ _ => .fail .panic

  def betree.load_internal_node
    (id : Isize) (st : State) :
    Result (State × (betree.List (Isize × betree.Message)))
    :=
    betree_utils.load_internal_node id st

  def betree.store_internal_node
    (id : Isize) (content : betree.List (Isize × betree.Message)) (st : State) :
    Result (State × Unit)
    :=
    betree_utils.store_internal_node id content st

  def betree.load_leaf_node
    (id : Isize) (st : State) : Result (State × (betree.List (Isize × Isize))) :=
    betree_utils.load_leaf_node id st

  def betree.store_leaf_node
    (id : Isize) (content : betree.List (Isize × Isize)) (st : State) :
    Result (State × Unit)
    :=
    betree_utils.store_leaf_node id content st

  def betree.fresh_node_id (counter : Isize) : Result (Isize × Isize) :=
    do
    let counter1 ← counter + 1#isize
    Result.ok (counter, counter1)

  def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
    Result.ok { next_node_id := 0#isize }

  def betree.NodeIdCounter.fresh_id
    (self : betree.NodeIdCounter) : Result (Isize × betree.NodeIdCounter) :=
    do
    let i ← self.next_node_id + 1#isize
    Result.ok (self.next_node_id, { next_node_id := i })

  def betree.upsert_update
    (prev : Option Isize) (st : betree.UpsertFunState) : Result Isize :=
    match prev with
    | none =>
      match st with
      | betree.UpsertFunState.Add v => Result.ok v
      | betree.UpsertFunState.Sub _ => Result.ok 0#isize
    | some prev1 =>
      match st with
      | betree.UpsertFunState.Add v =>
        do
        let margin ← core_isize_max - prev1
        if margin >= v
        then prev1 + v
        else Result.ok core_isize_max
      | betree.UpsertFunState.Sub v =>
        if prev1 >= v
        then prev1 - v
        else Result.ok 0#isize

  def betree.List.len_loop
    {T : Type} (self : betree.List T) (len : Isize) : Result Isize :=
    match self with
    | betree.List.Cons _ tl =>
      do
      let len1 ← len + 1#isize
      betree.List.len_loop tl len1
    | betree.List.Nil => Result.ok len
  partial_fixpoint

  def betree.List.len {T : Type} (self : betree.List T) : Result Isize :=
    betree.List.len_loop self 0#isize

  def betree.List.reverse_loop
    {T : Type} (self : betree.List T) (out : betree.List T) :
    Result (betree.List T)
    :=
    match self with
    | betree.List.Cons hd tl =>
      betree.List.reverse_loop tl (betree.List.Cons hd out)
    | betree.List.Nil => Result.ok out
  partial_fixpoint

  def betree.List.reverse
    {T : Type} (self : betree.List T) : Result (betree.List T) :=
    betree.List.reverse_loop self betree.List.Nil

  def betree.List.split_at_loop
    {T : Type} (n : Isize) (beg : betree.List T) (self : betree.List T) :
    Result ((betree.List T) × (betree.List T))
    :=
    if n > 0#isize
    then
      match self with
      | betree.List.Cons hd tl =>
        do
        let n1 ← n - 1#isize
        betree.List.split_at_loop n1 (betree.List.Cons hd beg) tl
      | betree.List.Nil => Result.fail .panic
    else do
        let l ← betree.List.reverse beg
        Result.ok (l, self)
  partial_fixpoint

  def betree.List.split_at
    {T : Type} (self : betree.List T) (n : Isize) :
    Result ((betree.List T) × (betree.List T))
    :=
    betree.List.split_at_loop n betree.List.Nil self

  def betree.List.push_front
    {T : Type} (self : betree.List T) (x : T) : Result (betree.List T) :=
    let (tl, _) := core.mem.replace self betree.List.Nil
    Result.ok (betree.List.Cons x tl)

  def betree.List.pop_front
    {T : Type} (self : betree.List T) : Result (T × (betree.List T)) :=
    let (ls, _) := core.mem.replace self betree.List.Nil
    match ls with
    | betree.List.Cons x tl => Result.ok (x, tl)
    | betree.List.Nil => Result.fail .panic

  def betree.List.hd {T : Type} (self : betree.List T) : Result T :=
    match self with
    | betree.List.Cons hd _ => Result.ok hd
    | betree.List.Nil => Result.fail .panic

  def betree.ListPairIsizeT.head_has_key
    {T : Type} (self : betree.List (Isize × T)) (key : Isize) : Result Bool :=
    match self with
    | betree.List.Cons hd _ =>
      let (i, _) := hd
      Result.ok (i = key)
    | betree.List.Nil =>
      Result.ok false

  def betree.ListPairIsizeT.partition_at_pivot_loop
    {T : Type} (pivot : Isize) (beg : betree.List (Isize × T))
    (end1 : betree.List (Isize × T)) (self : betree.List (Isize × T)) :
    Result ((betree.List (Isize × T)) × (betree.List (Isize × T)))
    :=
    match self with
    | betree.List.Cons hd tl =>
      let (i, _) := hd
      if i >= pivot
      then
        betree.ListPairIsizeT.partition_at_pivot_loop pivot beg (betree.List.Cons
          hd end1) tl
      else
        betree.ListPairIsizeT.partition_at_pivot_loop pivot (betree.List.Cons hd
          beg) end1 tl
    | betree.List.Nil =>
      do
      let l ← betree.List.reverse beg
      let l1 ← betree.List.reverse end1
      Result.ok (l, l1)
  partial_fixpoint

  def betree.ListPairIsizeT.partition_at_pivot
    {T : Type} (self : betree.List (Isize × T)) (pivot : Isize) :
    Result ((betree.List (Isize × T)) × (betree.List (Isize × T)))
    :=
    betree.ListPairIsizeT.partition_at_pivot_loop pivot betree.List.Nil
      betree.List.Nil self

  def betree.Leaf.split
    (self : betree.Leaf) (content : betree.List (Isize × Isize))
    (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
    Result (State × (betree.Internal × betree.NodeIdCounter))
    :=
    do
    let p ← betree.List.split_at content params.split_size
    let (content0, content1) := p
    let p1 ← betree.List.hd content1
    let (pivot, _) := p1
    let (id0, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
    let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1
    let (st1, _) ← betree.store_leaf_node id0 content0 st
    let (st2, _) ← betree.store_leaf_node id1 content1 st1
    let n := betree.Node.Leaf { id := id0, size := params.split_size }
    let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
    Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))

  def betree.Node.lookup_in_bindings_loop
    (key : Isize) (bindings : betree.List (Isize × Isize)) : Result (Option Isize) :=
    match bindings with
    | betree.List.Cons hd tl =>
      let (i, i1) := hd
      if i = key
      then Result.ok (some i1)
      else
        if i > key
        then Result.ok none
        else betree.Node.lookup_in_bindings_loop key tl
    | betree.List.Nil => Result.ok none
  partial_fixpoint

  def betree.Node.lookup_in_bindings
    (key : Isize) (bindings : betree.List (Isize × Isize)) : Result (Option Isize) :=
    betree.Node.lookup_in_bindings_loop key bindings

  def betree.Node.lookup_first_message_for_key_loop
    (key : Isize) (msgs : betree.List (Isize × betree.Message)) :
    Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize ×
      betree.Message) → betree.List (Isize × betree.Message)))
    :=
    match msgs with
    | betree.List.Cons x next_msgs =>
      let (i, _) := x
      if i >= key
      then Result.ok (msgs, fun ret => ret)
      else
        do
        let (l, back) ←
          betree.Node.lookup_first_message_for_key_loop key next_msgs
        let back1 :=
          fun ret => let next_msgs1 := back ret
                    betree.List.Cons x next_msgs1
        Result.ok (l, back1)
    | betree.List.Nil => Result.ok (betree.List.Nil, fun ret => ret)
  partial_fixpoint

  def betree.Node.lookup_first_message_for_key
    (key : Isize) (msgs : betree.List (Isize × betree.Message)) :
    Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize ×
      betree.Message) → betree.List (Isize × betree.Message)))
    :=
    betree.Node.lookup_first_message_for_key_loop key msgs

  def betree.Node.apply_upserts_loop
    (msgs : betree.List (Isize × betree.Message)) (prev : Option Isize) (key : Isize)
    :
    Result (Isize × (betree.List (Isize × betree.Message)))
    :=
    do
    let b ← betree.ListPairIsizeT.head_has_key msgs key
    if b
    then
      do
      let (msg, msgs1) ← betree.List.pop_front msgs
      let (_, m) := msg
      match m with
      | betree.Message.Insert _ => Result.fail .panic
      | betree.Message.Delete => Result.fail .panic
      | betree.Message.Upsert s =>
        do
        let v ← betree.upsert_update prev s
        betree.Node.apply_upserts_loop msgs1 (some v) key
    else
      do
      let v ← core.option.Option.unwrap prev
      let msgs1 ← betree.List.push_front msgs (key, betree.Message.Insert v)
      Result.ok (v, msgs1)
  partial_fixpoint

  def betree.Node.apply_upserts
    (msgs : betree.List (Isize × betree.Message)) (prev : Option Isize) (key : Isize)
    :
    Result (Isize × (betree.List (Isize × betree.Message)))
    :=
    betree.Node.apply_upserts_loop msgs prev key

  mutual
  def betree.Internal.lookup_in_children
    (self : betree.Internal) (key : Isize) (st : State) :
    Result (State × ((Option Isize) × betree.Internal))
    :=
    if key < self.pivot
    then
      do
      let (st1, (o, n)) ← betree.Node.lookup self.left key st
      Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right))
    else
      do
      let (st1, (o, n)) ← betree.Node.lookup self.right key st
      Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
  partial_fixpoint

  def betree.Node.lookup
    (self : betree.Node) (key : Isize) (st : State) :
    Result (State × ((Option Isize) × betree.Node))
    :=
    match self with
    | betree.Node.Internal node =>
      do
      let (st1, msgs) ← betree.load_internal_node node.id st
      let (pending, lookup_first_message_for_key_back) ←
        betree.Node.lookup_first_message_for_key key msgs
      match pending with
      | betree.List.Cons p _ =>
        let (k, msg) := p
        if k != key
        then
          do
          let (st2, (o, node1)) ←
            betree.Internal.lookup_in_children node key st1
          Result.ok (st2, (o, betree.Node.Internal node1))
        else
          match msg with
          | betree.Message.Insert v => Result.ok (st1, (some v, self))
          | betree.Message.Delete => Result.ok (st1, (none, self))
          | betree.Message.Upsert _ =>
            do
            let (st2, (v, node1)) ←
              betree.Internal.lookup_in_children node key st1
            let (v1, pending1) ← betree.Node.apply_upserts pending v key
            let msgs1 := lookup_first_message_for_key_back pending1
            let (st3, _) ← betree.store_internal_node node1.id msgs1 st2
            Result.ok (st3, (some v1, betree.Node.Internal node1))
      | betree.List.Nil =>
        do
        let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1
        Result.ok (st2, (o, betree.Node.Internal node1))
    | betree.Node.Leaf node =>
      do
      let (st1, bindings) ← betree.load_leaf_node node.id st
      let o ← betree.Node.lookup_in_bindings key bindings
      Result.ok (st1, (o, self))
  partial_fixpoint

  end

  def betree.Node.filter_messages_for_key_loop
    (key : Isize) (msgs : betree.List (Isize × betree.Message)) :
    Result (betree.List (Isize × betree.Message))
    :=
    match msgs with
    | betree.List.Cons p _ =>
      let (k, _) := p
      if k = key
      then
        do
        let (_, msgs1) ← betree.List.pop_front msgs
        betree.Node.filter_messages_for_key_loop key msgs1
      else Result.ok msgs
    | betree.List.Nil => Result.ok betree.List.Nil
  partial_fixpoint

  def betree.Node.filter_messages_for_key
    (key : Isize) (msgs : betree.List (Isize × betree.Message)) :
    Result (betree.List (Isize × betree.Message))
    :=
    betree.Node.filter_messages_for_key_loop key msgs

  def betree.Node.lookup_first_message_after_key_loop
    (key : Isize) (msgs : betree.List (Isize × betree.Message)) :
    Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize ×
      betree.Message) → betree.List (Isize × betree.Message)))
    :=
    match msgs with
    | betree.List.Cons p next_msgs =>
      let (k, _) := p
      if k = key
      then
        do
        let (l, back) ←
          betree.Node.lookup_first_message_after_key_loop key next_msgs
        let back1 :=
          fun ret => let next_msgs1 := back ret
                    betree.List.Cons p next_msgs1
        Result.ok (l, back1)
      else Result.ok (msgs, fun ret => ret)
    | betree.List.Nil => Result.ok (betree.List.Nil, fun ret => ret)
  partial_fixpoint

  def betree.Node.lookup_first_message_after_key
    (key : Isize) (msgs : betree.List (Isize × betree.Message)) :
    Result ((betree.List (Isize × betree.Message)) × (betree.List (Isize ×
      betree.Message) → betree.List (Isize × betree.Message)))
    :=
    betree.Node.lookup_first_message_after_key_loop key msgs

  def betree.Node.apply_to_internal
    (msgs : betree.List (Isize × betree.Message)) (key : Isize)
    (new_msg : betree.Message) :
    Result (betree.List (Isize × betree.Message))
    :=
    do
    let (msgs1, lookup_first_message_for_key_back) ←
      betree.Node.lookup_first_message_for_key key msgs
    let b ← betree.ListPairIsizeT.head_has_key msgs1 key
    if b
    then
      match new_msg with
      | betree.Message.Insert _ =>
        do
        let msgs2 ← betree.Node.filter_messages_for_key key msgs1
        let msgs3 ← betree.List.push_front msgs2 (key, new_msg)
        Result.ok (lookup_first_message_for_key_back msgs3)
      | betree.Message.Delete =>
        do
        let msgs2 ← betree.Node.filter_messages_for_key key msgs1
        let msgs3 ← betree.List.push_front msgs2 (key, betree.Message.Delete)
        Result.ok (lookup_first_message_for_key_back msgs3)
      | betree.Message.Upsert s =>
        do
        let p ← betree.List.hd msgs1
        let (_, m) := p
        match m with
        | betree.Message.Insert prev =>
          do
          let v ← betree.upsert_update (some prev) s
          let (_, msgs2) ← betree.List.pop_front msgs1
          let msgs3 ←
            betree.List.push_front msgs2 (key, betree.Message.Insert v)
          Result.ok (lookup_first_message_for_key_back msgs3)
        | betree.Message.Delete =>
          do
          let (_, msgs2) ← betree.List.pop_front msgs1
          let v ← betree.upsert_update none s
          let msgs3 ←
            betree.List.push_front msgs2 (key, betree.Message.Insert v)
          Result.ok (lookup_first_message_for_key_back msgs3)
        | betree.Message.Upsert _ =>
          do
          let (msgs2, lookup_first_message_after_key_back) ←
            betree.Node.lookup_first_message_after_key key msgs1
          let msgs3 ← betree.List.push_front msgs2 (key, new_msg)
          let msgs4 := lookup_first_message_after_key_back msgs3
          Result.ok (lookup_first_message_for_key_back msgs4)
    else
      do
      let msgs2 ← betree.List.push_front msgs1 (key, new_msg)
      Result.ok (lookup_first_message_for_key_back msgs2)

  def betree.Node.apply_messages_to_internal_loop
    (msgs : betree.List (Isize × betree.Message))
    (new_msgs : betree.List (Isize × betree.Message)) :
    Result (betree.List (Isize × betree.Message))
    :=
    match new_msgs with
    | betree.List.Cons new_msg new_msgs_tl =>
      do
      let (i, m) := new_msg
      let msgs1 ← betree.Node.apply_to_internal msgs i m
      betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl
    | betree.List.Nil => Result.ok msgs
  partial_fixpoint

  def betree.Node.apply_messages_to_internal
    (msgs : betree.List (Isize × betree.Message))
    (new_msgs : betree.List (Isize × betree.Message)) :
    Result (betree.List (Isize × betree.Message))
    :=
    betree.Node.apply_messages_to_internal_loop msgs new_msgs

  def betree.Node.lookup_mut_in_bindings_loop
    (key : Isize) (bindings : betree.List (Isize × Isize)) :
    Result ((betree.List (Isize × Isize)) × (betree.List (Isize × Isize) →
      betree.List (Isize × Isize)))
    :=
    match bindings with
    | betree.List.Cons hd tl =>
      let (i, _) := hd
      if i >= key
      then Result.ok (bindings, fun ret => ret)
      else
        do
        let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl
        let back1 := fun ret => let tl1 := back ret
                                betree.List.Cons hd tl1
        Result.ok (l, back1)
    | betree.List.Nil => Result.ok (betree.List.Nil, fun ret => ret)
  partial_fixpoint

  def betree.Node.lookup_mut_in_bindings
    (key : Isize) (bindings : betree.List (Isize × Isize)) :
    Result ((betree.List (Isize × Isize)) × (betree.List (Isize × Isize) →
      betree.List (Isize × Isize)))
    :=
    betree.Node.lookup_mut_in_bindings_loop key bindings

  def betree.Node.apply_to_leaf
    (bindings : betree.List (Isize × Isize)) (key : Isize) (new_msg : betree.Message)
    :
    Result (betree.List (Isize × Isize))
    :=
    do
    let (bindings1, lookup_mut_in_bindings_back) ←
      betree.Node.lookup_mut_in_bindings key bindings
    let b ← betree.ListPairIsizeT.head_has_key bindings1 key
    if b
    then
      do
      let (hd, bindings2) ← betree.List.pop_front bindings1
      match new_msg with
      | betree.Message.Insert v =>
        do
        let bindings3 ← betree.List.push_front bindings2 (key, v)
        Result.ok (lookup_mut_in_bindings_back bindings3)
      | betree.Message.Delete =>
        Result.ok (lookup_mut_in_bindings_back bindings2)
      | betree.Message.Upsert s =>
        do
        let (_, i) := hd
        let v ← betree.upsert_update (some i) s
        let bindings3 ← betree.List.push_front bindings2 (key, v)
        Result.ok (lookup_mut_in_bindings_back bindings3)
    else
      match new_msg with
      | betree.Message.Insert v =>
        do
        let bindings2 ← betree.List.push_front bindings1 (key, v)
        Result.ok (lookup_mut_in_bindings_back bindings2)
      | betree.Message.Delete =>
        Result.ok (lookup_mut_in_bindings_back bindings1)
      | betree.Message.Upsert s =>
        do
        let v ← betree.upsert_update none s
        let bindings2 ← betree.List.push_front bindings1 (key, v)
        Result.ok (lookup_mut_in_bindings_back bindings2)

  def betree.Node.apply_messages_to_leaf_loop
    (bindings : betree.List (Isize × Isize))
    (new_msgs : betree.List (Isize × betree.Message)) :
    Result (betree.List (Isize × Isize))
    :=
    match new_msgs with
    | betree.List.Cons new_msg new_msgs_tl =>
      do
      let (i, m) := new_msg
      let bindings1 ← betree.Node.apply_to_leaf bindings i m
      betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl
    | betree.List.Nil => Result.ok bindings
  partial_fixpoint

  def betree.Node.apply_messages_to_leaf
    (bindings : betree.List (Isize × Isize))
    (new_msgs : betree.List (Isize × betree.Message)) :
    Result (betree.List (Isize × Isize))
    :=
    betree.Node.apply_messages_to_leaf_loop bindings new_msgs

  mutual def betree.Internal.flush
    (self : betree.Internal) (params : betree.Params)
    (node_id_cnt : betree.NodeIdCounter)
    (content : betree.List (Isize × betree.Message)) (st : State) :
    Result (State × ((betree.List (Isize × betree.Message)) × (betree.Internal
      × betree.NodeIdCounter)))
    :=
    do
    let p ← betree.ListPairIsizeT.partition_at_pivot content self.pivot
    let (msgs_left, msgs_right) := p
    let len_left ← betree.List.len msgs_left
    if len_left >= params.min_flush_size
    then
      do
      let (st1, p1) ←
        betree.Node.apply_messages self.left params node_id_cnt msgs_left st
      let (n, node_id_cnt1) := p1
      let len_right ← betree.List.len msgs_right
      if len_right >= params.min_flush_size
      then
        do
        let (st2, p2) ←
          betree.Node.apply_messages self.right params node_id_cnt1 msgs_right
            st1
        let (n1, node_id_cnt2) := p2
        Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot
          n n1, node_id_cnt2)))
      else
        Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n
          self.right, node_id_cnt1)))
    else
      do
      let (st1, p1) ←
        betree.Node.apply_messages self.right params node_id_cnt msgs_right st
      let (n, node_id_cnt1) := p1
      Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot
        self.left n, node_id_cnt1)))
  partial_fixpoint

  def betree.Node.apply_messages
    (self : betree.Node) (params : betree.Params)
    (node_id_cnt : betree.NodeIdCounter)
    (msgs : betree.List (Isize × betree.Message)) (st : State) :
    Result (State × (betree.Node × betree.NodeIdCounter))
    :=
    match self with
    | betree.Node.Internal node =>
      do
      let (st1, content) ← betree.load_internal_node node.id st
      let content1 ← betree.Node.apply_messages_to_internal content msgs
      let num_msgs ← betree.List.len content1
      if num_msgs >= params.min_flush_size
      then
        do
        let (st2, (content2, p)) ←
          betree.Internal.flush node params node_id_cnt content1 st1
        let (node1, node_id_cnt1) := p
        let (st3, _) ← betree.store_internal_node node1.id content2 st2
        Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1))
      else
        do
        let (st2, _) ← betree.store_internal_node node.id content1 st1
        Result.ok (st2, (self, node_id_cnt))
    | betree.Node.Leaf node =>
      do
      let (st1, content) ← betree.load_leaf_node node.id st
      let content1 ← betree.Node.apply_messages_to_leaf content msgs
      let len ← betree.List.len content1
      let i ← 2#isize * params.split_size
      if len >= i
      then
        do
        let (st2, (new_node, node_id_cnt1)) ←
          betree.Leaf.split node content1 params node_id_cnt st1
        let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
        Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1))
      else
        do
        let (st2, _) ← betree.store_leaf_node node.id content1 st1
        Result.ok (st2, (betree.Node.Leaf { node with size := len },
          node_id_cnt))
  partial_fixpoint

  end

  def betree.Node.apply
    (self : betree.Node) (params : betree.Params)
    (node_id_cnt : betree.NodeIdCounter) (key : Isize) (new_msg : betree.Message)
    (st : State) :
    Result (State × (betree.Node × betree.NodeIdCounter))
    :=
    betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key,
      new_msg) betree.List.Nil) st

  def betree.BeTree.new
    (min_flush_size : Isize) (split_size : Isize) (st : State) :
    Result (State × betree.BeTree)
    :=
    do
    let node_id_cnt ← betree.NodeIdCounter.new
    let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
    let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
    Result.ok (st1,
      {
        params := { min_flush_size, split_size },
        node_id_cnt := node_id_cnt1,
        root := (betree.Node.Leaf { id, size := 0#isize })
      })

  def betree.BeTree.apply
    (self : betree.BeTree) (key : Isize) (msg : betree.Message) (st : State) :
    Result (State × betree.BeTree)
    :=
    do
    let (st1, p) ←
      betree.Node.apply self.root self.params self.node_id_cnt key msg st
    let (n, nic) := p
    Result.ok (st1, { self with node_id_cnt := nic, root := n })

  def betree.BeTree.insert
    (self : betree.BeTree) (key : Isize) (value : Isize) (st : State) :
    Result (State × betree.BeTree)
    :=
    betree.BeTree.apply self key (betree.Message.Insert value) st

  def betree.BeTree.delete
    (self : betree.BeTree) (key : Isize) (st : State) :
    Result (State × betree.BeTree)
    :=
    betree.BeTree.apply self key betree.Message.Delete st

  def betree.BeTree.upsert
    (self : betree.BeTree) (key : Isize) (upd : betree.UpsertFunState) (st : State)
    :
    Result (State × betree.BeTree)
    :=
    betree.BeTree.apply self key (betree.Message.Upsert upd) st

  def betree.BeTree.lookup
    (self : betree.BeTree) (key : Isize) (st : State) :
    Result (State × ((Option Isize) × betree.BeTree))
    :=
    do
    let (st1, (o, n)) ← betree.Node.lookup self.root key st
    Result.ok (st1, (o, { self with root := n }))

end betree

namespace avl

  inductive Ordering where
  | Less : Ordering
  | Equal : Ordering
  | Greater : Ordering

  structure Ord (Self : Type) where
    cmp : Self → Self → Result Ordering

  inductive Node (T : Type) where
  | mk : T → Option (Node T) → Option (Node T) → Isize → Node T

  @[reducible]
  def Node.value {T : Type} (x : Node T) :=
    match x with | Node.mk x1 _ _ _ => x1

  @[reducible]
  def Node.left {T : Type} (x : Node T) :=
    match x with | Node.mk _ x1 _ _ => x1

  @[reducible]
  def Node.right {T : Type} (x : Node T) :=
    match x with | Node.mk _ _ x1 _ => x1

  @[reducible]
  def Node.balance_factor {T : Type} (x : Node T) :=
    match x with | Node.mk _ _ _ x1 => x1

  structure Tree (T : Type) where
    root : Option (Node T)

  def OrdIsize.cmp (self : Isize) (other : Isize) : Result Ordering :=
    if self < other
    then Result.ok Ordering.Less
    else
      if self = other
      then Result.ok Ordering.Equal
      else Result.ok Ordering.Greater

  /- Trait implementation: [avl::{avl::Ord for Isize}]
    Source: 'src/avl.rs', lines 7:0-17:1 -/
  @[reducible]
  def OrdIsize : Ord Isize := {
    cmp := OrdIsize.cmp
  }

  /- [avl::{avl::Node<T>}#1::rotate_left]:
    Source: 'src/avl.rs', lines 41:4-90:5 -/
  def Node.rotate_left
    {T : Type} (root : Node T) (z : Node T) : Result (Node T) :=
    let (b, o) := core.mem.replace z.left none
    let (x, root1) :=
      core.mem.replace (Node.mk root.value root.left b root.balance_factor)
        (Node.mk z.value o z.right z.balance_factor)
    if root1.balance_factor = 0#isize
    then
      Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right 1#isize))
        root1.right (-1)#isize)
    else
      Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right 0#isize))
        root1.right 0#isize)

  /- [avl::{avl::Node<T>}#1::rotate_right]:
    Source: 'src/avl.rs', lines 92:4-136:5 -/
  def Node.rotate_right
    {T : Type} (root : Node T) (z : Node T) : Result (Node T) :=
    let (b, o) := core.mem.replace z.right none
    let (x, root1) :=
      core.mem.replace (Node.mk root.value b root.right root.balance_factor)
        (Node.mk z.value z.left o z.balance_factor)
    if root1.balance_factor = 0#isize
    then
      Result.ok (Node.mk root1.value root1.left (some (Node.mk x.value
        x.left x.right (-1)#isize)) 1#isize)
    else
      Result.ok (Node.mk root1.value root1.left (some (Node.mk x.value
        x.left x.right 0#isize)) 0#isize)

  /- [avl::{avl::Node<T>}#1::rotate_left_right]:
    Source: 'src/avl.rs', lines 138:4-186:5 -/
  def Node.rotate_left_right
    {T : Type} (root : Node T) (z : Node T) : Result (Node T) :=
    do
    let (o, _) := core.mem.replace z.right none
    let y ← core.option.Option.unwrap o
    let (a, o1) := core.mem.replace y.left none
    let (b, o2) := core.mem.replace y.right none
    let (x, root1) :=
      core.mem.replace (Node.mk root.value b root.right root.balance_factor)
        (Node.mk y.value o1 o2 y.balance_factor)
    if root1.balance_factor = 0#isize
    then
      Result.ok (Node.mk root1.value (some (Node.mk z.value z.left a 0#isize)) (some
        (Node.mk x.value x.left x.right 0#isize)) 0#isize)
    else
      if root1.balance_factor < 0#isize
      then
        Result.ok (Node.mk root1.value (some (Node.mk z.value z.left a 0#isize))
          (some (Node.mk x.value x.left x.right 1#isize)) 0#isize)
      else
        Result.ok (Node.mk root1.value (some (Node.mk z.value z.left a (-1)#isize))
          (some (Node.mk x.value x.left x.right 0#isize)) 0#isize)

  /- [avl::{avl::Node<T>}#1::rotate_right_left]:
    Source: 'src/avl.rs', lines 188:4-236:5 -/
  def Node.rotate_right_left
    {T : Type} (root : Node T) (z : Node T) : Result (Node T) :=
    do
    let (o, _) := core.mem.replace z.left none
    let y ← core.option.Option.unwrap o
    let (b, o1) := core.mem.replace y.left none
    let (a, o2) := core.mem.replace y.right none
    let (x, root1) :=
      core.mem.replace (Node.mk root.value root.left b root.balance_factor)
        (Node.mk y.value o1 o2 y.balance_factor)
    if root1.balance_factor = 0#isize
    then
      Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right 0#isize))
        (some (Node.mk z.value a z.right 0#isize)) 0#isize)
    else
      if root1.balance_factor > 0#isize
      then
        Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right
          (-1)#isize)) (some (Node.mk z.value a z.right 0#isize)) 0#isize)
      else
        Result.ok (Node.mk root1.value (some (Node.mk x.value x.left x.right
          0#isize)) (some (Node.mk z.value a z.right 1#isize)) 0#isize)

  /- [avl::{avl::Node<T>}#2::insert_in_left]:
    Source: 'src/avl.rs', lines 240:4-275:5 -/
  mutual def Node.insert_in_left
    {T : Type} (OrdInst : Ord T) (node : Node T) (value : T) :
    Result (Bool × (Node T))
    :=
    do
    let (b, o) ← Tree.insert_in_opt_node OrdInst node.left value
    if b
    then
      do
      let i ← node.balance_factor - 1#isize
      if i = (-2)#isize
      then
        do
        let (o1, o2) := core.mem.replace o none
        let left ← core.option.Option.unwrap o1
        if left.balance_factor <= 0#isize
        then
          do
          let node1 ←
            Node.rotate_right (Node.mk node.value o2 node.right i) left
          Result.ok (false, node1)
        else
          do
          let node1 ←
            Node.rotate_left_right (Node.mk node.value o2 node.right i) left
          Result.ok (false, node1)
      else Result.ok (i != 0#isize, Node.mk node.value o node.right i)
    else Result.ok (false, Node.mk node.value o node.right node.balance_factor)
  partial_fixpoint

  def Tree.insert_in_opt_node
    {T : Type} (OrdInst : Ord T) (node : Option (Node T)) (value : T) :
    Result (Bool × (Option (Node T)))
    :=
    match node with
    | none => let n := Node.mk value none none 0#isize
              Result.ok (true, some n)
    | some node1 =>
      do
      let (b, node2) ← Node.insert OrdInst node1 value
      Result.ok (b, some node2)
  partial_fixpoint

  def Node.insert_in_right
    {T : Type} (OrdInst : Ord T) (node : Node T) (value : T) :
    Result (Bool × (Node T))
    :=
    do
    let (b, o) ← Tree.insert_in_opt_node OrdInst node.right value
    if b
    then
      do
      let i ← node.balance_factor + 1#isize
      if i = 2#isize
      then
        do
        let (o1, o2) := core.mem.replace o none
        let right ← core.option.Option.unwrap o1
        if right.balance_factor >= 0#isize
        then
          do
          let node1 ←
            Node.rotate_left (Node.mk node.value node.left o2 i) right
          Result.ok (false, node1)
        else
          do
          let node1 ←
            Node.rotate_right_left (Node.mk node.value node.left o2 i) right
          Result.ok (false, node1)
      else Result.ok (i != 0#isize, Node.mk node.value node.left o i)
    else Result.ok (false, Node.mk node.value node.left o node.balance_factor)
  partial_fixpoint

  def Node.insert
    {T : Type} (OrdInst : Ord T) (node : Node T) (value : T) :
    Result (Bool × (Node T))
    :=
    do
    let ordering ← OrdInst.cmp value node.value
    match ordering with
    | Ordering.Less => Node.insert_in_left OrdInst node value
    | Ordering.Equal => Result.ok (false, node)
    | Ordering.Greater => Node.insert_in_right OrdInst node value
  partial_fixpoint

  end

  def Tree.new {T : Type} (_OrdInst : Ord T) : Result (Tree T) :=
    Result.ok { root := none }

  def Tree.find_loop
    {T : Type} (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) :
    Result Bool
    :=
    match current_tree with
    | none => Result.ok false
    | some current_node =>
      do
      let o ← OrdInst.cmp current_node.value value
      match o with
      | Ordering.Less => Tree.find_loop OrdInst value current_node.right
      | Ordering.Equal => Result.ok true
      | Ordering.Greater => Tree.find_loop OrdInst value current_node.left
  partial_fixpoint

  def Tree.find
    {T : Type} (OrdInst : Ord T) (self : Tree T) (value : T) : Result Bool :=
    Tree.find_loop OrdInst value self.root

  def Tree.insert
    {T : Type} (OrdInst : Ord T) (self : Tree T) (value : T) :
    Result (Bool × (Tree T))
    :=
    do
    let (b, o) ← Tree.insert_in_opt_node OrdInst self.root value
    Result.ok (b, { root := o })

end avl