(* -------------------------------------------------------------------------- *)
(* Generic associative map data structure, using balanced binary trees, based *)
(* on Data.Map from the Haskell standard library.                             *)
(* -------------------------------------------------------------------------- *)

include "arithmetics/nat.ma".
include "common/Order.ma".

(* for eq_rect_Type0_r *)
include "ASM/Util.ma".

inductive map (key_type: Type[0]) (elt_type: Type[0]): Type[0] ≝
  | map_nil: map key_type elt_type
  | map_fork: nat → key_type → elt_type → map key_type elt_type → map key_type elt_type → map key_type elt_type.

(* -------------------------------------------------------------------------- *)
(* Discrimination functions for structure of map.                             *)
(* -------------------------------------------------------------------------- *)

definition map_nil ≝
  λkey_type.
  λelt_type.
  λthe_map: map key_type elt_type.
  match the_map with
  [ map_nil ⇒ true
  | _       ⇒ false
  ].

definition map_not_nil ≝
  λkey_type.
  λelt_type.
  λthe_map: map key_type elt_type.
  match the_map with
  [ map_nil ⇒ false
  | _       ⇒ true
  ].
    
definition map_nil_p ≝
  λkey_type.
  λelt_type.
  λthe_map: map key_type elt_type.
  match the_map with
  [ map_nil ⇒ True
  | _       ⇒ False
  ].

definition map_not_nil_p ≝
  λkey_type.
  λelt_type.
  λthe_map: map key_type elt_type.
  match the_map with
  [ map_nil ⇒ False
  | _       ⇒ True
  ].
(* -------------------------------------------------------------------------- *)
(* Size, depth, etc.                                                          *)
(* -------------------------------------------------------------------------- *)
definition map_size ≝
  λkey_type.
  λelt_type.
  λm: map key_type elt_type.
  match m with
  [ map_nil ⇒ 0
  | map_fork sz key elt l r ⇒ sz
  ].

(* -------------------------------------------------------------------------- *)
(* Lookup of elements in map.                                                 *)
(* -------------------------------------------------------------------------- *)
let rec map_lookup
  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
  (to_search: key_type) (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil                 ⇒ None ?
  | map_fork sz key elt l r ⇒
    match ord to_search key with
    [ order_eq ⇒ Some ? elt
    | order_lt ⇒ map_lookup key_type elt_type ord to_search l
    | order_gt ⇒ map_lookup key_type elt_type ord to_search r
    ]
  ].

definition map_lookup_assoc ≝
  λkey_type.
  λelt_type.
  λord: key_type → key_type → order.
  λto_search: key_type.
  λthe_map: map key_type elt_type.
  match map_lookup key_type elt_type ord to_search the_map with
  [ None ⇒ None ?
  | Some found ⇒ Some ? 〈to_search, found〉
  ].

definition map_lookup_default ≝
  λkey_type.
  λelt_type.
  λord: key_type → key_type → order.
  λto_search: key_type.
  λdef: elt_type.
  λthe_map: map key_type elt_type.
  match map_lookup key_type elt_type ord to_search the_map with
  [ None ⇒ def
  | Some found ⇒ found
  ].

definition map_member ≝
  λkey_type.
  λelt_type.
  λord: key_type → key_type → order.
  λto_search: key_type.
  λthe_map: map key_type elt_type.
  match map_lookup key_type elt_type ord to_search the_map with
  [ None ⇒ false
  | Some found ⇒ true
  ].

definition map_not_member ≝
  λkey_type.
  λelt_type.
  λord: key_type → key_type → order.
  λto_search: key_type.
  λthe_map: map key_type elt_type.
  match map_lookup key_type elt_type ord to_search the_map with
  [ None ⇒ true
  | Some found ⇒ false
  ].

(* -------------------------------------------------------------------------- *)
(* Creation of maps.                                                          *)
(* -------------------------------------------------------------------------- *)
definition map_empty ≝
  λkey_type.
  λelt_type.
    map_nil key_type elt_type.

definition map_singleton ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
    map_fork key_type elt_type 1 key elt (map_nil ? ?) (map_nil ? ?).

(* -------------------------------------------------------------------------- *)
(* Internal, related to balancing and rotating nodes.                         *)
(* -------------------------------------------------------------------------- *)
definition map_delta ≝ 4.
definition map_ratio ≝ 2.

definition map_binsert ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
    map_fork ? ? (1 + map_size ? ? left + map_size ? ? right) key elt left right.

(* Single rotations, left and right. *)
definition map_single_l ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match right with
  [ map_nil ⇒ None ?
  | map_fork r_sz r_key r_elt r_l r_r ⇒
      Some ? (map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r)
  ].

definition map_single_l_safe ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  λprf: map_not_nil_p key_type elt_type right.
  match right return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with
  [ map_nil ⇒ λright_nil_absrd. ?
  | map_fork r_sz r_key r_elt r_l r_r ⇒
    λright_fork_prf. map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r
  ] prf.
  normalize in right_nil_absrd;
  cases right_nil_absrd
qed.

definition map_single_r ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match left with
  [ map_nil ⇒ None ?
  | map_fork l_sz l_key l_elt l_l l_r ⇒
      Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right))
  ].

definition map_single_r_safe ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  λprf: map_not_nil_p key_type elt_type left.
  match left return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with
  [ map_nil ⇒ λleft_nil_absrd. ?
  | map_fork l_sz l_key l_elt l_l l_r ⇒
      λleft_fork_prf. map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right)
  ] prf.
  normalize in left_nil_absrd;
  cases left_nil_absrd
qed.

definition map_double_r_property_p ≝
  λkey_type.
  λelt_type.
  λleft: map key_type elt_type.
  match left with
  [ map_nil ⇒ False
  | map_fork l_sz l_key l_elt l_l l_r ⇒
    match l_r with
    [ map_nil ⇒ False
    | _ ⇒ True
    ]
  ].

lemma map_double_r_property_p_exists:
  ∀key_type.
  ∀elt_type.
  ∀left: map key_type elt_type.
    map_double_r_property_p key_type elt_type left →
      ∃l_sz, l_key, l_elt, l_l, l_r.
        left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r.
  #KEY_TYPE #ELT_TYPE #LEFT
  cases LEFT
  [ normalize #HYP cases HYP
  | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT
    #HYP
    @ex_intro
    [1: @L_SZ
    |2: @ex_intro
        [1: @L_KEY
        |2: @ex_intro
            [1: @L_ELT
            |2: @ex_intro
                [1: @L_LEFT
                |2: @ex_intro
                    [1: @L_RIGHT
                    |2: %
                    ]
                ]
            ]
        ]
    ]
  ]
qed.

lemma map_double_r_property_p_exists_l_r_not_nil_p:
  ∀key_type.
  ∀elt_type.
  ∀left: map key_type elt_type.
    map_double_r_property_p key_type elt_type left →
      ∃l_sz, l_key, l_elt, l_l, l_r.
        (left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r) ∧
        map_not_nil_p key_type elt_type l_r.
  #KEY_TYPE #ELT_TYPE #LEFT
  cases LEFT
  [ normalize #HYP cases HYP
  | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT
    #HYP
    @ex_intro
    [1: @L_SZ
    |2: @ex_intro
        [1: @L_KEY
        |2: @ex_intro
            [1: @L_ELT
            |2: @ex_intro
                [1: @L_LEFT
                |2: @ex_intro
                    [1: @L_RIGHT
                    |2: @conj
                        [1: %
                        |2: generalize in match HYP
                            cases L_RIGHT
                            [1: normalize //
                            |2: #NEW_SZ #NEW_KEY #NEW_ELT #NEW_L #NEW_R
                                normalize //
                            ]
                        ]
                    ]
                ]
            ]
        ]
    ]
  ]
qed.

definition map_double_r ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match left with
  [ map_nil ⇒ None ?
  | map_fork l_sz l_key l_elt l_l l_r ⇒
    match l_r with
    [ map_nil ⇒ None ?
    | map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒
      Some ? (map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right))
    ]
  ].

definition map_double_l ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match right with
  [ map_nil ⇒ None …
  | map_fork r_sz r_key r_elt r_l r_r ⇒
    match r_l with
    [ map_nil ⇒ None …
    | map_fork rl_sz rl_key rl_elt rl_l rl_r ⇒
      Some ? (map_binsert … rl_key rl_elt (map_binsert … key elt left rl_l) (map_binsert … r_key r_elt rl_r r_r))
    ]
  ].

definition map_rotate_r ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match left with
  [ map_nil ⇒ None ?
  | map_fork l_sz l_key l_elt l_l l_r ⇒
    if ltb (map_size ? ? l_r) (map_ratio * map_size ? ? l_l) then
      map_single_r ? ? key elt left right
    else
      map_double_r ? ? key elt left right
  ].

(* fails only when right = nil *)
definition map_rotate_l ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match right with
  [ map_nil ⇒ None ?
  | map_fork r_sz r_key r_elt r_l r_r ⇒
      if ltb (map_size ? ? r_l) (map_ratio * map_size ? ? r_r) then
        map_single_l ? ? key elt left right
      else
        map_double_l ? ? key elt left right
  ].
  
definition map_balance ≝
  λkey_type.
  λelt_type.
  λkey: key_type.
  λelt: elt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  let size_l ≝ map_size ? ? left in
  let size_r ≝ map_size ? ? right in
  let size_x ≝ 1 + size_l + size_r in
    if leb (size_l + size_r) 1 then
      Some ? (map_fork ? ? size_x key elt left right)
    else if geb size_r (map_delta * size_l) then
      map_rotate_l ? ? key elt left right
    else if geb size_l (map_delta * size_r) then
      map_rotate_r ? ? key elt left right
    else
      Some ? (map_fork ? ? size_x key elt left right).

let rec map_delete_find_min
  (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ None ?
  | map_fork sz key elt l r ⇒
    match l with
    [ map_nil ⇒ Some ? 〈〈key, elt〉, r〉
    | _ ⇒
      match map_delete_find_min key_type elt_type l with
      [ None ⇒ None ?
      | Some kmn ⇒
        let 〈km, new〉 ≝ kmn in
        match map_balance key_type elt_type key elt new r with
        [ None ⇒ None ?
        | Some balanced ⇒ Some ? 〈km, balanced〉
        ]
      ]
    ]
  ].

let rec map_delete_find_max
  (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ None ?
  | map_fork sz key elt l r ⇒
    match r with
    [ map_nil ⇒ Some ? 〈〈key, elt〉, l〉
    | _ ⇒
      match map_delete_find_max key_type elt_type r with
      [ None ⇒ None ?
      | Some kmn ⇒
        let 〈km, new〉 ≝ kmn in
        match map_balance key_type elt_type key elt l new with
        [ None ⇒ None ?
        | Some balanced ⇒ Some ? 〈km, balanced〉
        ]
      ]
    ]
  ].

definition map_glue ≝
  λkey_type.
  λelt_type.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match left with
  [ map_nil ⇒ Some ? right
  | map_fork l_sz l_key l_elt l_l l_r ⇒
    match right with
    [ map_nil ⇒ Some ? left
    | map_fork r_sz r_key r_elt r_l r_r ⇒
      if gtb l_sz r_sz then
        match map_delete_find_max key_type elt_type left with
        [ None ⇒ None ?
        | Some kmml' ⇒
          let 〈kmm, l'〉 ≝ kmml' in
          let 〈km, m〉 ≝ kmm in
            map_balance key_type elt_type km m l' right
        ]
      else
        match map_delete_find_min key_type elt_type right with
        [ None ⇒ None ?
        | Some kmmr' ⇒
          let 〈kmm, r'〉 ≝ kmmr' in
          let 〈km, m〉 ≝ kmm in
            map_balance key_type elt_type km m left r'
        ]
    ]
  ].

(* -------------------------------------------------------------------------- *)
(* Inserting elements.                                                        *)
(* -------------------------------------------------------------------------- *)

let rec map_insert
  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
  (key: key_type) (elt: elt_type) (the_map: map key_type elt_type) on the_map: option (map key_type elt_type) ≝
  match the_map with
  [ map_nil ⇒ Some ? (map_singleton … key elt)
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    match ord m_key key with
    [ order_lt ⇒
      match map_insert … ord key elt m_l with
      [ None ⇒ None ?
      | Some new_l ⇒ map_balance … m_key m_elt new_l m_r
      ]
    | order_eq ⇒ Some ? (map_fork key_type elt_type m_sz key elt m_l m_r)
    | order_gt ⇒
      match map_insert key_type elt_type ord key elt m_r with
      [ None ⇒ None ?
      | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r
      ]
    ]
  ].

(* -------------------------------------------------------------------------- *)
(* Deleting elements.                                                         *)
(* -------------------------------------------------------------------------- *)

let rec map_delete
  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
  (the_key: key_type) (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
  | map_fork sz key elt l r ⇒
    match ord the_key key with
    [ order_lt ⇒
      match map_delete key_type elt_type ord the_key l with
      [ None ⇒ None ?
      | Some new_l ⇒ map_balance key_type elt_type key elt new_l r
      ]
    | order_eq ⇒ map_glue key_type elt_type l r
    | order_gt ⇒
      match map_delete key_type elt_type ord the_key r with
      [ None ⇒ None ?
      | Some new_r ⇒ map_balance key_type elt_type key elt l new_r
      ]
    ]
  ].
  
(* -------------------------------------------------------------------------- *)
(* Folds.                                                                     *)
(* -------------------------------------------------------------------------- *)

let rec map_foldr_with_key
  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
  (f: key_type → dom_type → rng_type → rng_type) (e: rng_type)
  (the_map: map key_type dom_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ e
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    map_foldr_with_key key_type dom_type rng_type f (map_foldr_with_key key_type dom_type rng_type f e m_r) m_l
  ].

let rec map_foldl_with_key
  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
  (f: rng_type → key_type → dom_type → rng_type) (e: rng_type)
  (the_map: map key_type dom_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ e
  | map_fork m_sz m_key m_elt m_l m_r ⇒
      map_foldl_with_key key_type dom_type rng_type f (f (map_foldl_with_key key_type dom_type rng_type f e m_l) m_key m_elt) m_r
  ].

definition map_fold ≝
  λkey_type.
  λdom_type.
  λrng_type.
  λf: dom_type → rng_type → rng_type.
    map_foldr_with_key key_type dom_type rng_type (λi. λx'. λz'. f x' z').

(* -------------------------------------------------------------------------- *)
(* Maps.                                                                      *)
(* -------------------------------------------------------------------------- *)
    
let rec map_map_with_key
  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
  (f: key_type → dom_type → rng_type) (the_map: map key_type dom_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ map_nil key_type rng_type
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    map_fork key_type rng_type m_sz m_key (f m_key m_elt)
      (map_map_with_key key_type dom_type rng_type f m_l)
      (map_map_with_key key_type dom_type rng_type f m_r)
  ].

definition map_map ≝
  λkey_type.
  λdom_type.
  λrng_type.
  λf: dom_type → rng_type.
  λthe_map: map key_type dom_type.
    map_map_with_key key_type dom_type rng_type (λk. f) the_map.

(* -------------------------------------------------------------------------- *)
(* Unions.                                                                    *)
(* -------------------------------------------------------------------------- *)

let rec map_insert_max
  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
  (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt)
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    match map_insert_max key_type elt_type key elt m_r with
    [ None ⇒ None ?
    | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r
    ]
  ].

let rec map_insert_min
  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
  (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt)
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    match map_insert_min key_type elt_type key elt m_l with
    [ None ⇒ None ?
    | Some new_l ⇒ map_balance key_type elt_type m_key m_elt new_l m_r
    ]
  ].

definition map_join_prf' ≝
  λkey_type.
  λelt_type.
  λmeasure: nat × nat.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  \fst measure = O → left = map_nil key_type elt_type →
  \snd measure = O → left = map_nil key_type elt_type →
  ∀n. ∀l_sz. ∀l_key. ∀l_elt. ∀l_l. ∀l_r.
    \fst measure = S n → left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r →
  ∀n. ∀r_sz. ∀r_key. ∀r_elt. ∀r_l. ∀r_r.
    \snd measure = S n → left = map_fork key_type elt_type r_sz r_key r_elt r_l r_r.

axiom map_join':
  ∀key_type.
  ∀elt_type.
  ∀key: key_type.
  ∀elt: elt_type.
  ∀left: map key_type elt_type.
  ∀right: map key_type elt_type.
  ∀measure: nat × nat.
  ∀prf: map_join_prf' key_type elt_type measure left right.
    option (map key_type elt_type).

(*
let rec map_join'
  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
  (left: map key_type elt_type) (right: map key_type elt_type)
  (measure: nat × nat)
  (prf: map_join_prf' key_type elt_type measure left right)
  on measure: option (map key_type elt_type) ≝
  let size_l ≝ \fst measure in
  let size_r ≝ \snd measure in
  match size_l return λx. map_join_prf' key_type elt_type 〈x, size_r〉 left right → option (map key_type elt_type) with
  [ O ⇒
    λprf_left_nil: map_join_prf' key_type elt_type 〈0, size_r〉 left right.
      map_insert_min key_type elt_type key elt right
  | S size_l' ⇒
    match left with
    [ map_nil ⇒
      λprf_left_nil_abs: map_join_prf' key_type elt_type 〈S size_l', size_r〉 left right. ?
    | map_fork l_sz l_key l_elt l_l l_r ⇒
      λprf_left_fork: map_join_prf' key_type elt_type 〈size_l', size_r〉 l_l l_r.
      match size_r return λy. map_join_prf' key_type elt_type 〈size_l', y〉 left right → option (map key_type elt_type) with
      [ O ⇒
        λprf_right_nil: map_join_prf' key_type elt_type 〈size_l', 0〉 left right.
          map_insert_max key_type elt_type key elt left
      | S size_r' ⇒
        match right with
        [ map_nil ⇒
          λprf_right_nil_abs: map_join_prf' key_type elt_type 〈S size_l', S size_r'〉 left right. ?
        | map_fork r_sz r_key r_elt r_l r_r ⇒
          λprf_right_fork: map_join_prf' key_type elt_type 〈size_l', size_r'〉 r_l r_r.
            if ltb (map_delta * l_sz) r_sz then
              match map_join' key_type elt_type key elt left r_l 〈S size_l', S size_r'〉 ? with
              [ None ⇒ None ?
              | Some joined ⇒
                  map_balance key_type elt_type r_key r_elt joined r_r
              ]
            else if ltb (map_delta * r_sz) l_sz then
              match map_join' key_type elt_type key elt l_r right 〈S size_l', S size_r'〉 ? with
              [ None ⇒ None ?
              | Some joined ⇒
                  map_balance key_type elt_type l_key l_elt l_l joined
              ]
            else
              Some ? (map_binsert key_type elt_type key elt left right)
         ]
       ] ?
     ]
   ] ?.
   [ 3: @prf_right_fork
   | 4: @prf_left_fork
*)

(* requires some crazy trick to convince termination checker *)
axiom map_join:
  ∀key_type.
  ∀elt_type.
  ∀key: key_type.
  ∀elt: elt_type.
  ∀left: map key_type elt_type.
  ∀right: map key_type elt_type.
    option (map key_type elt_type).

let rec map_filter_gt
  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order)
  (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    match ord m_key with
    [ order_eq ⇒ Some ? m_r
    | order_lt ⇒
      match map_filter_gt key_type elt_type ord m_l with
      [ None ⇒ None ?
      | Some filtered ⇒
          map_join key_type elt_type m_key m_elt filtered m_r
      ]
    | order_gt ⇒ map_filter_gt key_type elt_type ord m_r
    ]
  ].

let rec map_filter_lt
  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order)
  (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    match ord m_key with
    [ order_eq ⇒ Some ? m_l
    | order_lt ⇒ map_filter_lt key_type elt_type ord m_l
    | order_gt ⇒
      match map_filter_lt key_type elt_type ord m_r with
      [ None ⇒ None ?
      | Some filtered ⇒ map_join key_type elt_type m_key m_elt m_l filtered
      ]
    ]
  ].

let rec map_trim
  (key_type: Type[0]) (elt_type: Type[0]) (lord: key_type → order)
  (hord: key_type → order) (the_map: map key_type elt_type) on the_map ≝
  match the_map with
  [ map_nil ⇒ map_nil key_type elt_type
  | map_fork m_sz m_key m_elt m_l m_r ⇒
    match lord m_key with
    [ order_lt ⇒
      match hord m_key with
      [ order_gt ⇒ the_map
      | _ ⇒ map_trim key_type elt_type lord hord m_l
      ]
    | _ ⇒ map_trim key_type elt_type lord hord m_r
    ]
  ].
  
axiom map_hedge_union:
  ∀key_type: Type[0].
  ∀elt_type: Type[0].
  ∀ord: key_type → key_type → order.
  ∀lord: key_type → order.
  ∀hord: key_type → order.
  ∀left: map key_type elt_type.
  ∀right: map key_type elt_type.
    option (map key_type elt_type).

(*
(* left biased hedge union *)
let rec map_hedge_union
  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
  (lord: key_type → order) (hord: key_type → order)
(*  (prod: (map key_type elt_type) × (map key_type elt_type)) on prod ≝ *)
  (left: map key_type elt_type) (right: map key_type elt_type) on right ≝
  let 〈left, right〉 ≝ prod in
  match right with
  [ map_nil ⇒ Some ? left
  | map_fork r_sz r_key r_elt r_l r_r ⇒
    match left with
    [ map_nil ⇒
      match map_filter_gt key_type elt_type lord r_l with
      [ None ⇒ None ?
      | Some filtered_gt ⇒
        match map_filter_lt key_type elt_type hord r_r with
        [ None ⇒ None ?
        | Some filtered_lt ⇒ map_join key_type elt_type r_key r_elt filtered_gt filtered_lt
        ]
      ]
    | map_fork l_sz l_key l_elt l_l l_r ⇒
      let xord ≝ λk: key_type. ord l_key k in
      let trimmed_l ≝ map_trim key_type elt_type lord xord right in
      let trimmed_r ≝ map_trim key_type elt_type xord hord right in
      match map_hedge_union key_type elt_type ord lord xord 〈l_l, trimmed_l〉 with
      [ None ⇒ None ?
      | Some hedged_l ⇒
        match map_hedge_union key_type elt_type ord xord hord 〈l_r, trimmed_r〉 with
        [ None ⇒ None ?
        | Some hedged_r ⇒ map_join key_type elt_type l_key l_elt hedged_l hedged_r
        ]
      ]
    ]
  ].
*)

definition map_union ≝
  λkey_type.
  λelt_type.
  λord: key_type → key_type → order.
  λleft: map key_type elt_type.
  λright: map key_type elt_type.
  match left with
  [ map_nil ⇒ Some ? right
  | _ ⇒
    match right with
    [ map_nil ⇒ Some ? left
    | _ ⇒ map_hedge_union key_type elt_type ord (λx. order_lt) (λx. order_gt) left right
    ]
  ].