rbt.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Module RBT := MSets.MSetRBT.Make Nat_as_OT.

Definition build_trees (leaves: list nat) :=
  List.fold_left (fun trs n =>
      RBT.add n (hd RBT.empty trs) :: trs)
    leaves [] |> List.rev.

Compute build_trees [1;2;3;4;5;6].= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '2'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } } }}]
: RBT.t |> list

Compute build_trees [2;1;4;3;6;5].= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '5'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }}]
: RBT.t |> list

Compute build_trees [6;5;4;1;2;3].= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '5'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }}]
: RBT.t |> list