Require Import Coqlib OptionMonad.
Require Import Impure.ImpHCons.
Import Notations.

Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.

Set Implicit Arguments.

Local Open Scope option_monad_scope.
Local Open Scope impure.


Inductive p_mostdef [A : Type] (p : A -> A -> A -> Prop): option A -> option A -> option A -> Prop :=
 | PMostDef2 (x0 x1 x : A) (P : p x0 x1 x) : p_mostdef p (Some x0) (Some x1) (Some x)
 | PMostDef1L (x : A) : p_mostdef p (Some x) None (Some x)
 | PMostDef1R (x : A) : p_mostdef p None (Some x) (Some x)
 | PMostDef0 : p_mostdef p None None None.

The abstract signatures of trees

Module Type TREE.
  Parameter elt: Type.
  Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}.
  Parameter t: Type -> Type.
  Parameter empty: forall (A: Type), t A.
  Parameter get: forall (A: Type), elt -> t A -> option A.
  Parameter set: forall (A: Type), elt -> A -> t A -> t A.
  Parameter remove: forall (A: Type), elt -> t A -> t A.

  Axiom gempty:
    forall (A: Type) (i: elt), get i (empty A) = None.
  Axiom gss:
    forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
  Axiom gso:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.
  Axiom gsspec:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    get i (set j x m) = if elt_eq i j then Some x else get i m.
  Axiom grs:
    forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
  Axiom gro:
    forall (A: Type) (i j: elt) (m: t A),
    i <> j -> get i (remove j m) = get i m.
  Axiom grspec:
    forall (A: Type) (i j: elt) (m: t A),
    get i (remove j m) = if elt_eq i j then None else get i m.

  Parameter beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
  Axiom beq_correct:
    forall (A: Type) (eqA: A -> A -> bool) (t1 t2: t A),
    beq eqA t1 t2 = true <->
    (forall (x: elt),
     match get x t1, get x t2 with
     | None, None => True
     | Some y1, Some y2 => eqA y1 y2 = true
     | _, _ => False
    end).

  Parameter map:
    forall (A B: Type), (elt -> A -> B) -> t A -> t B.
  Axiom gmap:
    forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),
    get i (map f m) = option_map (f i) (get i m).

  Parameter map1:
    forall (A B: Type), (A -> B) -> t A -> t B.
  Axiom gmap1:
    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
    get i (map1 f m) = option_map f (get i m).

  Parameter combine:
    forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C.
  Axiom gcombine:
    forall (A B C: Type) (f: option A -> option B -> option C),
    f None None = None ->
    forall (m1: t A) (m2: t B) (i: elt),
    get i (combine f m1 m2) = f (get i m1) (get i m2).

  Parameter combine_mostdef:
    forall (A: Type), (A -> A -> option A) -> t A -> t A -> option (t A).
  Parameter f_mostdef:
    forall (A: Type), (A -> A -> option A) -> option A -> option A -> option (option A).
  Axiom gcombine_mostdef:
    forall (A: Type) (mostdef: A -> A -> option A) (m1 m2 m3: t A) (a: option A) (i: elt),
    combine_mostdef mostdef m1 m2 = Some m3 ->
    f_mostdef mostdef (get i m1) (get i m2) = Some a ->
    get i m3 = a.
  Axiom fcombine_mostdef:
    forall (A: Type) (mostdef: A -> A -> option A) (m1 m2: t A),
    combine_mostdef mostdef m1 m2 = None ->
    (forall i a1 a2, (get i m1) = Some a1 -> (get i m2) = Some a2 ->
    mostdef a1 a2 <> None) ->
    False.
  Axiom gcombine_mostdef_ok:
    forall (A: Type) (mostdef: A -> A -> option A) (m1 m2 m3: t A) (i: elt) (a: A),
    combine_mostdef mostdef m1 m2 = Some m3 ->
    get i m3 = Some a ->
    f_mostdef mostdef (get i m1) (get i m2) = Some (Some a).
  Axiom gcombine_mostdef_only_l:
    forall (A: Type) (mostdef: A -> A -> option A) (m1: t A),
     combine_mostdef mostdef m1 (empty A) = Some m1.
  Axiom gcombine_mostdef_none_rev:
    forall (A: Type) (mostdef: A -> A -> option A) (m1 m2 m3: t A) (i: elt),
    combine_mostdef mostdef m1 m2 = Some m3 ->
    get i m3 = None ->
    get i m1 = None /\ get i m2 = None.


  Parameter elements:
    forall (A: Type), t A -> list (elt * A).
  Axiom elements_correct:
    forall (A: Type) (m: t A) (i: elt) (v: A),
    get i m = Some v -> In (i, v) (elements m).
  Axiom elements_complete:
    forall (A: Type) (m: t A) (i: elt) (v: A),
    In (i, v) (elements m) -> get i m = Some v.
  Axiom elements_keys_norepet:
    forall (A: Type) (m: t A),
    list_norepet (List.map (@fst elt A) (elements m)).
  Axiom elements_remove:
    forall (A: Type) i v (m: t A),
    get i m = Some v ->
    exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2.

  Parameter fold:
    forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B.
  Axiom fold_spec:
    forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A),
    fold f m v =
    List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
  Parameter fold1:
    forall (A B: Type), (B -> A -> B) -> t A -> B -> B.
  Axiom fold1_spec:
    forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A),
    fold1 f m v =
    List.fold_left (fun a p => f a (snd p)) (elements m) v.
End TREE.

The abstract signatures of maps

Module Type MAP.
  Parameter elt: Type.
  Parameter elt_eq: forall (a b: elt), {a = b} + {a <> b}.
  Parameter t: Type -> Type.
  Parameter init: forall (A: Type), A -> t A.
  Parameter get: forall (A: Type), elt -> t A -> A.
  Parameter set: forall (A: Type), elt -> A -> t A -> t A.
  Axiom gi:
    forall (A: Type) (i: elt) (x: A), get i (init x) = x.
  Axiom gss:
    forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
  Axiom gso:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.
  Axiom gsspec:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    get i (set j x m) = if elt_eq i j then x else get i m.
  Axiom gsident:
    forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
  Parameter map: forall (A B: Type), (A -> B) -> t A -> t B.
  Axiom gmap:
    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
    get i (map f m) = f(get i m).
End MAP.

An implementation of trees over type positive

Module PTree <: TREE.
  Definition elt := positive.
  Definition elt_eq := peq.

Representation of trees

  Inductive tree' (A: Type) : Type :=
  | Node001: tree' A -> tree' A
  | Node010: A -> tree' A
  | Node011: A -> tree' A -> tree' A
  | Node100: tree' A -> tree' A
  | Node101: tree' A -> tree' A ->tree' A
  | Node110: tree' A -> A -> tree' A
  | Node111: tree' A -> A -> tree' A -> tree' A.

  Inductive tree (A: Type) : Type :=
  | Empty : tree A
  | Nodes: tree' A -> tree A.

  Arguments Node001 {A} _.
  Arguments Node010 {A} _.
  Arguments Node011 {A} _ _.
  Arguments Node100 {A} _.
  Arguments Node101 {A} _ _.
  Arguments Node110 {A} _ _.
  Arguments Node111 {A} _ _ _.

  Arguments Empty {A}.
  Arguments Nodes {A} _.

  Scheme tree'_ind := Induction for tree' Sort Prop.

  Definition t := tree.


  Definition Node {A} (l: tree A) (o: option A) (r: tree A) : tree A :=
    match l,o,r with
    | Empty, None, Empty => Empty
    | Empty, None, Nodes r' => Nodes (Node001 r')
    | Empty, Some x, Empty => Nodes (Node010 x)
    | Empty, Some x, Nodes r' => Nodes (Node011 x r')
    | Nodes l', None, Empty => Nodes (Node100 l')
    | Nodes l', None, Nodes r' => Nodes (Node101 l' r')
    | Nodes l', Some x, Empty => Nodes (Node110 l' x)
    | Nodes l', Some x, Nodes r' => Nodes (Node111 l' x r')
    end.

Basic operations: empty, get, set, remove

  Definition empty (A: Type) : t A := Empty.

  Fixpoint get' {A} (p: positive) (m: tree' A) : option A :=
    match p, m with
    | xH, Node001 _ => None
    | xH, Node010 x => Some x
    | xH, Node011 x _ => Some x
    | xH, Node100 _ => None
    | xH, Node101 _ _ => None
    | xH, Node110 _ x => Some x
    | xH, Node111 _ x _ => Some x
    | xO q, Node001 _ => None
    | xO q, Node010 _ => None
    | xO q, Node011 _ _ => None
    | xO q, Node100 m' => get' q m'
    | xO q, Node101 m' _ => get' q m'
    | xO q, Node110 m' _ => get' q m'
    | xO q, Node111 m' _ _ => get' q m'
    | xI q, Node001 m' => get' q m'
    | xI q, Node010 _ => None
    | xI q, Node011 _ m' => get' q m'
    | xI q, Node100 m' => None
    | xI q, Node101 _ m' => get' q m'
    | xI q, Node110 _ _ => None
    | xI q, Node111 _ _ m' => get' q m'
    end.

  Definition get {A} (p: positive) (m: tree A) : option A :=
    match m with
    | Empty => None
    | Nodes m' => get' p m'
    end.


  Fixpoint set0 {A} (p: positive) (x: A) : tree' A :=
  match p with
  | xH => Node010 x
  | xO q => Node100 (set0 q x)
  | xI q => Node001 (set0 q x)
  end.

  Fixpoint set' {A} (p: positive) (x: A) (m: tree' A) : tree' A :=
  match p, m with
  | xH, Node001 r => Node011 x r
  | xH, Node010 _ => Node010 x
  | xH, Node011 _ r => Node011 x r
  | xH, Node100 l => Node110 l x
  | xH, Node101 l r => Node111 l x r
  | xH, Node110 l _ => Node110 l x
  | xH, Node111 l _ r => Node111 l x r
  | xO q, Node001 r => Node101 (set0 q x) r
  | xO q, Node010 y => Node110 (set0 q x) y
  | xO q, Node011 y r => Node111 (set0 q x) y r
  | xO q, Node100 l => Node100 (set' q x l)
  | xO q, Node101 l r => Node101 (set' q x l) r
  | xO q, Node110 l y => Node110 (set' q x l) y
  | xO q, Node111 l y r => Node111 (set' q x l) y r
  | xI q, Node001 r => Node001 (set' q x r)
  | xI q, Node010 y => Node011 y (set0 q x)
  | xI q, Node011 y r => Node011 y (set' q x r)
  | xI q, Node100 l => Node101 l (set0 q x)
  | xI q, Node101 l r => Node101 l (set' q x r)
  | xI q, Node110 l y => Node111 l y (set0 q x)
  | xI q, Node111 l y r => Node111 l y (set' q x r)
  end.

  Definition set {A} (p: positive) (x: A) (m: tree A) : tree A :=
  match m with
  | Empty => Nodes (set0 p x)
  | Nodes m' => Nodes (set' p x m')
  end.


  Fixpoint rem' {A} (p: positive) (m: tree' A) : tree A :=
  match p, m with
  | xH, Node001 r => Nodes m
  | xH, Node010 _ => Empty
  | xH, Node011 _ r => Nodes (Node001 r)
  | xH, Node100 l => Nodes m
  | xH, Node101 l r => Nodes m
  | xH, Node110 l _ => Nodes (Node100 l)
  | xH, Node111 l _ r => Nodes (Node101 l r)
  | xO q, Node001 r => Nodes m
  | xO q, Node010 y => Nodes m
  | xO q, Node011 y r => Nodes m
  | xO q, Node100 l => Node (rem' q l) None Empty
  | xO q, Node101 l r => Node (rem' q l) None (Nodes r)
  | xO q, Node110 l y => Node (rem' q l) (Some y) Empty
  | xO q, Node111 l y r => Node (rem' q l) (Some y) (Nodes r)
  | xI q, Node001 r => Node Empty None (rem' q r)
  | xI q, Node010 y => Nodes m
  | xI q, Node011 y r => Node Empty (Some y) (rem' q r)
  | xI q, Node100 l => Nodes m
  | xI q, Node101 l r => Node (Nodes l) None (rem' q r)
  | xI q, Node110 l y => Nodes m
  | xI q, Node111 l y r => Node (Nodes l) (Some y) (rem' q r)
  end.


  Definition remove' := Eval cbv [rem' Node] in @rem'.

  Definition remove {A} (p: positive) (m: tree A) : tree A :=
  match m with
  | Empty => Empty
  | Nodes m' => remove' p m'
  end.

Good variable properties for the basic operations

  Theorem gempty:
    forall (A: Type) (i: positive), get i (empty A) = None.

  Lemma gEmpty:
    forall (A: Type) (i: positive), get i (@Empty A) = None.

  Lemma gss0: forall {A} p (x: A), get' p (set0 p x) = Some x.

  Lemma gso0: forall {A} p q (x: A), p<>q -> get' p (set0 q x) = None.

  Theorem gss:
    forall (A: Type) (i: positive) (x: A) (m: tree A), get i (set i x m) = Some x.

  Theorem gso:
    forall (A: Type) (i j: positive) (x: A) (m: tree A),
    i <> j -> get i (set j x m) = get i m.

  Theorem gsspec:
    forall (A: Type) (i j: positive) (x: A) (m: t A),
    get i (set j x m) = if peq i j then Some x else get i m.

  Lemma gNode:
    forall {A} (i: positive) (l: tree A) (x: option A) (r: tree A),
    get i (Node l x r) = match i with xH => x | xO j => get j l | xI j => get j r end.

  Theorem grs:
    forall (A: Type) (i: positive) (m: tree A), get i (remove i m) = None.

  Theorem gro:
    forall (A: Type) (i j: positive) (m: tree A),
    i <> j -> get i (remove j m) = get i m.

  Theorem grspec:
    forall (A: Type) (i j: elt) (m: t A),
    get i (remove j m) = if elt_eq i j then None else get i m.

Custom case analysis principles and induction principles

  Definition not_trivially_empty {A} (l: tree A) (o: option A) (r: tree A) :=
    match l, o, r with
    | Empty, None, Empty => False
    | _, _, _ => True
    end.


  Section TREE_CASE.

  Context {A B: Type}
          (empty: B)
          (node: tree A -> option A -> tree A -> B).

  Definition tree_case (m: tree A) : B :=
    match m with
    | Empty => empty
    | Nodes (Node001 r) => node Empty None (Nodes r)
    | Nodes (Node010 x) => node Empty (Some x) Empty
    | Nodes (Node011 x r) => node Empty (Some x) (Nodes r)
    | Nodes (Node100 l) => node (Nodes l) None Empty
    | Nodes (Node101 l r) => node (Nodes l) None (Nodes r)
    | Nodes (Node110 l x) => node (Nodes l) (Some x) Empty
    | Nodes (Node111 l x r) => node (Nodes l) (Some x) (Nodes r)
    end.

  Lemma unroll_tree_case: forall l o r,
    not_trivially_empty l o r ->
    tree_case (Node l o r) = node l o r.

  End TREE_CASE.


  Section TREE_REC.

  Context {A B: Type}
          (empty: B)
          (node: tree A -> B -> option A -> tree A -> B -> B).

  Fixpoint tree_rec' (m: tree' A) : B :=
    match m with
    | Node001 r => node Empty empty None (Nodes r) (tree_rec' r)
    | Node010 x => node Empty empty (Some x) Empty empty
    | Node011 x r => node Empty empty (Some x) (Nodes r) (tree_rec' r)
    | Node100 l => node (Nodes l) (tree_rec' l) None Empty empty
    | Node101 l r => node (Nodes l) (tree_rec' l) None (Nodes r) (tree_rec' r)
    | Node110 l x => node (Nodes l) (tree_rec' l) (Some x) Empty empty
    | Node111 l x r => node (Nodes l) (tree_rec' l) (Some x) (Nodes r) (tree_rec' r)
    end.

  Definition tree_rec (m: tree A) : B :=
    match m with
    | Empty => empty
    | Nodes m' => tree_rec' m'
    end.

  Lemma unroll_tree_rec: forall l o r,
    not_trivially_empty l o r ->
    tree_rec (Node l o r) = node l (tree_rec l) o r (tree_rec r).

  End TREE_REC.


  Section TREE_REC2.

  Context {A B C: Type}
          (base: C)
          (base1: tree B -> C)
          (base2: tree A -> C)
          (nodes: forall (l1: tree A) (o1: option A) (r1: tree A)
                         (l2: tree B) (o2: option B) (r2: tree B)
                         (lrec: C) (rrec: C), C).

  Fixpoint tree_rec2' (m1: tree' A) (m2: tree' B) : C.

  Definition tree_rec2 (a: tree A) (b: tree B) : C :=
    match a, b with
    | Empty, Empty => base
    | Empty, _ => base1 b
    | _, Empty => base2 a
    | Nodes a', Nodes b' => tree_rec2' a' b'
    end.

  Lemma unroll_tree_rec2_NE:
    forall l1 o1 r1,
    not_trivially_empty l1 o1 r1 ->
    tree_rec2 (Node l1 o1 r1) Empty = base2 (Node l1 o1 r1).

  Lemma unroll_tree_rec2_EN:
    forall l2 o2 r2,
    not_trivially_empty l2 o2 r2 ->
    tree_rec2 Empty (Node l2 o2 r2) = base1 (Node l2 o2 r2).

  Lemma unroll_tree_rec2_NN:
    forall l1 o1 r1 l2 o2 r2,
    not_trivially_empty l1 o1 r1 -> not_trivially_empty l2 o2 r2 ->
    tree_rec2 (Node l1 o1 r1) (Node l2 o2 r2) =
    nodes l1 o1 r1 l2 o2 r2 (tree_rec2 l1 l2) (tree_rec2 r1 r2).

  End TREE_REC2.


  Section TREE_IND.

  Context {A: Type} (P: tree A -> Type)
          (empty: P Empty)
          (node: forall l, P l -> forall o r, P r -> not_trivially_empty l o r ->
                 P (Node l o r)).

  Program Fixpoint tree_ind' (m: tree' A) : P (Nodes m) :=
    match m with
    | Node001 r => @node Empty empty None (Nodes r) (tree_ind' r) _
    | Node010 x => @node Empty empty (Some x) Empty empty _
    | Node011 x r => @node Empty empty (Some x) (Nodes r) (tree_ind' r) _
    | Node100 l => @node (Nodes l) (tree_ind' l) None Empty empty _
    | Node101 l r => @node (Nodes l) (tree_ind' l) None (Nodes r) (tree_ind' r) _
    | Node110 l x => @node (Nodes l) (tree_ind' l) (Some x) Empty empty _
    | Node111 l x r => @node (Nodes l) (tree_ind' l) (Some x) (Nodes r) (tree_ind' r) _
    end.

  Definition tree_ind (m: tree A) : P m :=
    match m with
    | Empty => empty
    | Nodes m' => tree_ind' m'
    end.

  End TREE_IND.

Extensionality property

  Lemma tree'_not_empty:
    forall {A} (m: tree' A), exists i, get' i m <> None.

  Corollary extensionality_empty:
    forall {A} (m: tree A),
    (forall i, get i m = None) -> m = Empty.

  Theorem extensionality:
    forall (A: Type) (m1 m2: tree A),
    (forall i, get i m1 = get i m2) -> m1 = m2.


  Theorem gsident:
    forall {A} (i: positive) (m: t A) (v: A),
    get i m = Some v -> set i v m = m.

  Theorem set2:
    forall {A} (i: elt) (m: t A) (v1 v2: A),
    set i v2 (set i v1 m) = set i v2 m.

Boolean equality

  Section BOOLEAN_EQUALITY.

    Variable A: Type.
    Variable beqA: A -> A -> bool.

    Fixpoint beq' (m1 m2: tree' A) {struct m1} : bool :=
    match m1, m2 with
    | Node001 r1, Node001 r2 => beq' r1 r2
    | Node010 x1, Node010 x2 => beqA x1 x2
    | Node011 x1 r1, Node011 x2 r2 => beqA x1 x2 && beq' r1 r2
    | Node100 l1, Node100 l2 => beq' l1 l2
    | Node101 l1 r1, Node101 l2 r2 => beq' l1 l2 && beq' r1 r2
    | Node110 l1 x1, Node110 l2 x2 => beqA x1 x2 && beq' l1 l2
    | Node111 l1 x1 r1, Node111 l2 x2 r2 => beqA x1 x2 && beq' l1 l2 && beq' r1 r2
    | _, _ => false
    end.

    Definition beq (m1 m2: t A) : bool :=
    match m1, m2 with
    | Empty, Empty => true
    | Nodes m1', Nodes m2' => beq' m1' m2'
    | _, _ => false
    end.

    Let beq_optA (o1 o2: option A) : bool :=
      match o1, o2 with
      | None, None => true
      | Some a1, Some a2 => beqA a1 a2
      | _, _ => false
      end.

    Lemma beq_correct_bool:
      forall m1 m2,
      beq m1 m2 = true <-> (forall x, beq_optA (get x m1) (get x m2) = true).

    Theorem beq_correct:
      forall m1 m2,
      beq m1 m2 = true <->
      (forall (x: elt),
       match get x m1, get x m2 with
       | None, None => True
       | Some y1, Some y2 => beqA y1 y2 = true
       | _, _ => False
       end).

  End BOOLEAN_EQUALITY.

Collective operations

  Fixpoint prev_append (i j: positive) {struct i} : positive :=
    match i with
      | xH => j
      | xI i' => prev_append i' (xI j)
      | xO i' => prev_append i' (xO j)
    end.

  Definition prev (i: positive) : positive :=
    prev_append i xH.

  Lemma prev_append_prev i j:
    prev (prev_append i j) = prev_append j i.

  Lemma prev_involutive i :
    prev (prev i) = i.
  Proof (prev_append_prev i xH).

  Lemma prev_append_inj i j j' :
    prev_append i j = prev_append i j' -> j = j'.

  Fixpoint map' {A B} (f: positive -> A -> B) (m: tree' A) (i: positive)
           {struct m} : tree' B :=
    match m with
    | Node001 r => Node001 (map' f r (xI i))
    | Node010 x => Node010 (f (prev i) x)
    | Node011 x r => Node011 (f (prev i) x) (map' f r (xI i))
    | Node100 l => Node100 (map' f l (xO i))
    | Node101 l r => Node101 (map' f l (xO i)) (map' f r (xI i))
    | Node110 l x => Node110 (map' f l (xO i)) (f (prev i) x)
    | Node111 l x r => Node111 (map' f l (xO i)) (f (prev i) x) (map' f r (xI i))
    end.

  Definition map {A B} (f: positive -> A -> B) (m: tree A) :=
    match m with
    | Empty => Empty
    | Nodes m => Nodes (map' f m xH)
    end.

  Lemma gmap':
    forall {A B} (f: positive -> A -> B) (i j : positive) (m: tree' A),
    get' i (map' f m j) = option_map (f (prev (prev_append i j))) (get' i m).

  Theorem gmap:
    forall {A B} (f: positive -> A -> B) (i: positive) (m: t A),
    get i (map f m) = option_map (f i) (get i m).

  Fixpoint map1' {A B} (f: A -> B) (m: tree' A) {struct m} : tree' B :=
    match m with
    | Node001 r => Node001 (map1' f r)
    | Node010 x => Node010 (f x)
    | Node011 x r => Node011 (f x) (map1' f r)
    | Node100 l => Node100 (map1' f l)
    | Node101 l r => Node101 (map1' f l) (map1' f r)
    | Node110 l x => Node110 (map1' f l) (f x)
    | Node111 l x r => Node111 (map1' f l) (f x) (map1' f r)
    end.

  Definition map1 {A B} (f: A -> B) (m: t A) : t B :=
    match m with
    | Empty => Empty
    | Nodes m => Nodes (map1' f m)
    end.

  Theorem gmap1:
    forall {A B} (f: A -> B) (i: elt) (m: t A),
    get i (map1 f m) = option_map f (get i m).

  Definition map_filter1_nonopt {A B} (f: A -> option B) (m: tree A) : tree B :=
    tree_rec
      Empty
      (fun l lrec o r rrec => Node lrec (match o with None => None | Some a => f a end) rrec)
      m.

  Definition may_f {A B} (o: option A) (f: A -> option (option B)): option (option B) :=
    match o with
    | None => Some None
    | Some a => SOME fa <- f a IN Some fa
    end.

  Definition may_map_filter1_nonopt {A B} (f: A -> option (option B)) (m: tree A) : option (tree B) :=
    tree_rec
      (Some Empty)
      (fun l olrec o r orrec =>
        SOME lrec <- olrec IN
        SOME rrec <- orrec IN
        SOME ob <- may_f o f IN
        Some (Node lrec ob rrec))
      m.
  
  Definition imp_f {A B} (o: option A) (f: A -> ?? (option B)): ?? (option B) :=
    match o with
    | None => RET None
    | Some a => DO fa <~ f a;; RET fa
    end.
  
  Definition imp_map_filter1_nonopt {A B} (f: A -> ?? (option B)) (m: tree A) : ?? (tree B) :=
    tree_rec
      (RET Empty)
      (fun l olrec o r orrec =>
        DO lrec <~ olrec;;
        DO rrec <~ orrec;;
        DO ob <~ imp_f o f;;
        RET (Node lrec ob rrec))
      m.

  Local Transparent Node.

  Definition map_filter1 :=
    Eval cbv [map_filter1_nonopt tree_rec tree_rec' Node] in @map_filter1_nonopt.

  Lemma gmap_filter1:
    forall {A B} (f: A -> option B) (m: tree A) (i: positive),
    get i (map_filter1 f m) = match get i m with None => None | Some a => f a end.
  
  Definition may_map_filter1 :=
    Eval cbv [may_map_filter1_nonopt tree_rec tree_rec' Node] in @may_map_filter1_nonopt.

  Lemma gmay_map_filter1:
    forall {A B} (f: A -> option (option B)) (m: tree A) (fm: tree B) (i: positive),
    may_map_filter1 f m = Some fm ->
    get i fm = match get i m with None => None | Some a => SOME fa <- f a IN fa end.

  Lemma gmay_map_filter1_trivial:
    forall {A} (m: tree A),
    may_map_filter1 (fun a: A => Some (Some a)) m = Some m.

  Definition imp_map_filter1 :=
    Eval cbv [imp_map_filter1_nonopt tree_rec tree_rec' Node] in @imp_map_filter1_nonopt.

  Lemma gimp_map_filter1:
    forall {A B} (f: A -> ?? (option B)) (m: tree A) (ob: option B) (i: positive),
    WHEN imp_map_filter1 f m ~> fm THEN
    (match get i m with None => ob = None | Some a =>
        WHEN f a ~> fa THEN ob = fa end) ->
    get i fm = ob.

  Definition filter1 {A} (pred: A -> bool) (m: t A) : t A :=
    map_filter1 (fun a => if pred a then Some a else None) m.

  Theorem gfilter1:
    forall {A} (pred: A -> bool) (i: elt) (m: t A),
    get i (filter1 pred m) =
    match get i m with None => None | Some x => if pred x then Some x else None end.

  Fixpoint filter' {A} (f: positive -> A -> bool) (m: tree' A) (i: positive) : tree A :=
    match m with
    | Node001 r =>
        match filter' f r (xI i) with
        | Empty => Empty
        | Nodes t => Nodes (Node001 t)
        end
    | Node010 x => if f (prev i) x then Nodes m else Empty
    | Node011 x r =>
        match f (prev i) x, filter' f r (xI i) with
        | false, Empty => Empty
        | true, Empty => Nodes (Node010 x)
        | false, Nodes r => Nodes (Node001 r)
        | true, Nodes r => Nodes (Node011 x r)
        end
    | Node100 l =>
        match filter' f l (xO i) with
        | Empty => Empty
        | Nodes t => Nodes (Node100 t)
        end
    | Node101 l r =>
        match filter' f l (xO i), filter' f r (xI i) with
        | Empty, Empty => Empty
        | Nodes l, Empty => Nodes (Node100 l)
        | Empty, Nodes r => Nodes (Node001 r)
        | Nodes l, Nodes r => Nodes (Node101 l r)
        end
    | Node110 l x =>
        match filter' f l (xO i), f (prev i) x with
        | Empty, false => Empty
        | Empty, true => Nodes (Node010 x)
        | Nodes l, false => Nodes (Node100 l)
        | Nodes l, true => Nodes (Node110 l x)
        end
    | Node111 l x r =>
        match filter' f l (xO i), f (prev i) x, filter' f r (xI i) with
        | Empty, false, Empty => Empty
        | Empty, true, Empty => Nodes (Node010 x)
        | Nodes l, false, Empty => Nodes (Node100 l)
        | Nodes l, true, Empty => Nodes (Node110 l x)
        | Empty, false, Nodes r => Nodes (Node001 r)
        | Empty, true, Nodes r => Nodes (Node011 x r)
        | Nodes l, false, Nodes r => Nodes (Node101 l r)
        | Nodes l, true, Nodes r => Nodes (Node111 l x r)
        end
    end.

  Definition filter {A} (pred : positive -> A -> bool) (m: t A) : t A :=
    match m with
    | Empty => Empty
    | Nodes t => filter' pred t xH
    end.

  Section COMBINE.

  Variables A B C: Type.
  Variable f: option A -> option B -> option C.
  Hypothesis f_none_none: f None None = None.

  Let combine_l := map_filter1 (fun a => f (Some a) None).
  Let combine_r := map_filter1 (fun b => f None (Some b)).

  Let combine_nonopt (m1: tree A) (m2: tree B) : tree C :=
    tree_rec2
      Empty
      combine_r
      combine_l
      (fun l1 o1 r1 l2 o2 r2 lrec rrec =>
        Node lrec
             (match o1, o2 with None, None => None | _, _ => f o1 o2 end)
             rrec)
      m1 m2.

  Definition combine :=
    Eval cbv [combine_nonopt tree_rec2 tree_rec2'] in combine_nonopt.

  Lemma gcombine_l: forall m i, get i (combine_l m) = f (get i m) None.

  Lemma gcombine_r: forall m i, get i (combine_r m) = f None (get i m).

  Theorem gcombine:
      forall (m1: t A) (m2: t B) (i: positive),
      get i (combine m1 m2) = f (get i m1) (get i m2).

  End COMBINE.

  Section MOSTDEF_COMBINE.

  Variables A: Type.
  Variable mostdef: A -> A -> option A.
  Definition f_mostdef (o1 o2: option A): option (option A) :=
    match o1, o2 with
    | Some a1, Some a2 =>
        SOME a3 <- mostdef a1 a2 IN Some (Some a3)
    | Some a, None
    | None, Some a => Some (Some a)
    | None, None => Some None
    end.

  Let combine_mostdef_l := may_map_filter1 (fun a => f_mostdef (Some a) None).
  Let combine_mostdef_r := may_map_filter1 (fun a => f_mostdef None (Some a)).

  Definition may_f2 (o1 o2: option A): option (option A) :=
    match o1, o2 with
    | None, None => Some None
    | _, _ => SOME fc <- f_mostdef o1 o2 IN Some fc
    end.

  Let combine_mostdef_nonopt (m1 m2: tree A) : option (tree A) :=
    tree_rec2
      (Some Empty)
      combine_mostdef_r
      combine_mostdef_l
      (fun l1 o1 r1 l2 o2 r2 olrec orrec =>
        SOME lrec <- olrec IN
        SOME rrec <- orrec IN
        SOME oa <- may_f2 o1 o2 IN
        Some (Node lrec oa rrec))
      m1 m2.

  Definition combine_mostdef :=
    Eval cbv [combine_mostdef_nonopt tree_rec2 tree_rec2'] in combine_mostdef_nonopt.

  Lemma gcombine_mostdef_l: forall m fm oa i,
    combine_mostdef_l m = Some fm ->
    f_mostdef (get i m) None = Some oa ->
    get i fm = oa.

  Lemma gcombine_mostdef_r: forall m fm oa i,
    combine_mostdef_r m = Some fm ->
    f_mostdef None (get i m) = Some oa ->
    get i fm = oa.

  Lemma gcombine_mostdef_l_rev: forall m fm oa i,
    combine_mostdef_l m = Some fm ->
    get i fm = oa ->
    get i m = oa.

  Lemma gcombine_mostdef_r_rev: forall m fm oa i,
    combine_mostdef_r m = Some fm ->
    get i fm = oa ->
    get i m = oa.

  Lemma fcombine_mostdef_l: forall m fm i,
    combine_mostdef_l m = Some fm ->
    f_mostdef (get i m) None = None ->
    False.

  Lemma fcombine_mostdef_r: forall m fm i,
    combine_mostdef_r m = Some fm ->
    f_mostdef None (get i m) = None ->
    False.

  Lemma combine_mostdef_nonopt_decompose l l0 o o0 r r0:
    not_trivially_empty l o r ->
    not_trivially_empty l0 o0 r0 ->
    combine_mostdef_nonopt (Node l o r) (Node l0 o0 r0) = None ->
    combine_mostdef_nonopt r r0 = None
    \/ combine_mostdef_nonopt l l0 = None
    \/ may_f2 o o0 = None.

  Theorem gcombine_mostdef:
      forall (m1 m2 m3: t A) (oa: option A) (i: positive),
      combine_mostdef m1 m2 = Some m3 ->
      f_mostdef (get i m1) (get i m2) = Some oa ->
      get i m3 = oa.

  Theorem fcombine_mostdef:
      forall (m1 m2: t A),
      combine_mostdef m1 m2 = None ->
      (forall i a1 a2, (get i m1) = Some a1 -> (get i m2) = Some a2 ->
      mostdef a1 a2 <> None) ->
      False.

  Set Apply With Renaming.
  Theorem gcombine_mostdef_ok:
      forall (m1 m2 m3: t A) (i: positive) (a: A),
      combine_mostdef m1 m2 = Some m3 ->
      get i m3 = Some a ->
      f_mostdef (get i m1) (get i m2) = Some (Some a).

  Theorem gcombine_mostdef_only_l:
      forall (m1: t A),
      combine_mostdef m1 Empty = Some m1.

  Theorem gcombine_mostdef_none_rev:
      forall (m1 m2 m3: t A) (i: positive),
      combine_mostdef m1 m2 = Some m3 ->
      get i m3 = None ->
      get i m1 = None /\ get i m2 = None.
  
  End MOSTDEF_COMBINE.

  Section IMPURE_MOSTDEF_COMBINE.

  Variables A: Type.
  Variable imp_mostdef: A -> A -> ?? A.

  Definition f_imp_mostdef (o1 o2: option A): ?? (option A) :=
    match o1, o2 with
    | Some a1, Some a2 =>
        DO a3 <~ imp_mostdef a1 a2;; RET (Some a3)
    | Some a, None
    | None, Some a => RET (Some a)
    | None, None => RET None
    end.

  Lemma f_imp_mostdef_none:
    WHEN f_imp_mostdef None None ~> exta THEN exta=None.

  Lemma f_imp_mostdef_l: forall a,
    WHEN f_imp_mostdef a None ~> a' THEN a = a'.
  Local Hint Resolve f_imp_mostdef_l: wlp.

  Lemma f_imp_mostdef_r: forall a,
    WHEN f_imp_mostdef None a ~> a' THEN a = a'.
  Local Hint Resolve f_imp_mostdef_r: wlp.

  Let combine_imp_mostdef_l := imp_map_filter1 (fun a => f_imp_mostdef (Some a) None).
  Let combine_imp_mostdef_r := imp_map_filter1 (fun a => f_imp_mostdef None (Some a)).

  Definition imp_f2 (o1 o2: option A): ?? (option A) :=
    match o1, o2 with
    | None, None => RET None
    | _, _ => DO fc <~ f_imp_mostdef o1 o2;; RET fc
    end.

  Let combine_imp_mostdef_nonopt (m1 m2: tree A) : ?? (tree A) :=
    tree_rec2
      (RET Empty)
      combine_imp_mostdef_r
      combine_imp_mostdef_l
      (fun l1 o1 r1 l2 o2 r2 olrec orrec =>
        DO lrec <~ olrec;;
        DO rrec <~ orrec;;
        DO oa <~ imp_f2 o1 o2;;
        RET (Node lrec oa rrec))
      m1 m2.

  Definition combine_imp_mostdef :=
    Eval cbv [combine_imp_mostdef_nonopt tree_rec2 tree_rec2'] in combine_imp_mostdef_nonopt.

  Lemma gcombine_imp_mostdef_l_eq: forall m i,
    WHEN combine_imp_mostdef_l m ~> fm THEN
    get i fm = get i m.

  Lemma gcombine_imp_mostdef_r_eq: forall m i,
    WHEN combine_imp_mostdef_r m ~> fm THEN
    get i fm = get i m.

  Lemma gcombine_imp_mostdef_l: forall m oa i,
    WHEN combine_imp_mostdef_l m ~> fm THEN
    get i m = oa ->
    get i fm = oa.

  Lemma gcombine_imp_mostdef_r: forall m oa i,
    WHEN combine_imp_mostdef_r m ~> fm THEN
    get i m = oa ->
    get i fm = oa.

  Lemma gcombine_imp_mostdef_l_rev: forall m oa i,
    WHEN combine_imp_mostdef_l m ~> fm THEN
    get i fm = oa ->
    get i m = oa.

  Lemma gcombine_imp_mostdef_r_rev: forall m oa i,
    WHEN combine_imp_mostdef_r m ~> fm THEN
    get i fm = oa ->
    get i m = oa.
  
  Theorem gcombine_imp_mostdef_spec:
    forall (m1 m2 : t A),
    WHEN combine_imp_mostdef m1 m2 ~> m3 THEN
    forall (i : elt),
    p_mostdef (fun a1 a2 a3 => imp_mostdef a1 a2 ~~> a3) (get i m1) (get i m2) (get i m3).

  Hypothesis imp_mostdef_determ: forall a1 a2,
    WHEN imp_mostdef a1 a2 ~> exta1 THEN
    WHEN imp_mostdef a1 a2 ~> exta2 THEN
    exta1 = exta2.

  Lemma f_imp_mostdef_lr: forall a1 a2,
    WHEN f_imp_mostdef (Some a1) (Some a2) ~> oa3 THEN
    oa3 <> None.
  Local Hint Resolve f_imp_mostdef_lr: wlp.

  Lemma f_imp_mostdef_determ: forall oa1 oa2,
    WHEN f_imp_mostdef oa1 oa2 ~> exta1 THEN
    WHEN f_imp_mostdef oa1 oa2 ~> exta2 THEN
    exta1 = exta2.
  Opaque f_imp_mostdef.

  Theorem gcombine_imp_mostdef_or_ok:
      forall (m1 m2: t A) (a1 a2: A) (i: positive),
      WHEN combine_imp_mostdef m1 m2 ~> m3 THEN
      (forall a1 a2, WHEN f_imp_mostdef (Some a1) (Some a2) ~> oa
      THEN Some a1 = oa /\ Some a2 = oa) ->
      get i m1 = Some a1 \/ get i m2 = Some a1 ->
      get i m3 = Some a2 -> a1=a2.

  Theorem gcombine_imp_mostdef_and_ok:
      forall (m1 m2: t A) (a1 a2: A) (i: positive),
      WHEN combine_imp_mostdef m1 m2 ~> m3 THEN
      (forall a1 a2, WHEN f_imp_mostdef (Some a1) (Some a2) ~> oa
      THEN Some a1 = oa /\ Some a2 = oa) ->
      get i m1 = Some a1 /\ get i m2 = Some a2 ->
      a1=a2.

  Theorem gcombine_imp_mostdef_none:
      forall (m1 m2: t A) (i: positive),
      WHEN combine_imp_mostdef m1 m2 ~> m3 THEN
      get i m1 = None /\ get i m2 = None ->
      get i m3 = None.

  Theorem gcombine_imp_mostdef_none_rev:
      forall (m1 m2: t A) (i: positive),
      WHEN combine_imp_mostdef m1 m2 ~> m3 THEN
      get i m3 = None ->
      get i m1 = None /\ get i m2 = None.

  End IMPURE_MOSTDEF_COMBINE.

  Theorem combine_commut:
    forall (A B: Type) (f g: option A -> option A -> option B),
    f None None = None -> g None None = None ->
    (forall (i j: option A), f i j = g j i) ->
    forall (m1 m2: t A),
    combine f m1 m2 = combine g m2 m1.

List of all bindings

  Fixpoint xelements' {A} (m : tree' A) (i: positive) (k: list (positive * A))
                     {struct m} : list (positive * A) :=
    match m with
    | Node001 r => xelements' r (xI i) k
    | Node010 x => (prev i, x) :: k
    | Node011 x r => (prev i, x) :: xelements' r (xI i) k
    | Node100 l => xelements' l (xO i) k
    | Node101 l r => xelements' l (xO i) (xelements' r (xI i) k)
    | Node110 l x => xelements' l (xO i) ((prev i, x)::k)
    | Node111 l x r => xelements' l (xO i) ((prev i, x):: (xelements' r (xI i) k))
    end.

  Definition elements {A} (m : t A) : list (positive * A) :=
    match m with Empty => nil | Nodes m' => xelements' m' xH nil end.

  Definition xelements {A} (m : t A) (i: positive) : list (positive * A) :=
    match m with Empty => nil | Nodes m' => xelements' m' i nil end.

  Lemma xelements'_append:
    forall A (m: tree' A) i k1 k2,
    xelements' m i (k1 ++ k2) = xelements' m i k1 ++ k2.

  Lemma xelements_Node:
    forall A (l: tree A) (o: option A) (r: tree A) i,
    xelements (Node l o r) i =
       xelements l (xO i)
    ++ match o with None => nil | Some v => (prev i, v) :: nil end
    ++ xelements r (xI i).

  Lemma xelements_correct:
    forall A (m: tree A) i j v,
    get i m = Some v -> In (prev (prev_append i j), v) (xelements m j).

  Theorem elements_correct:
    forall A (m: t A) (i: positive) (v: A),
    get i m = Some v -> In (i, v) (elements m).

  Lemma in_xelements:
    forall A (m: tree A) (i k: positive) (v: A) ,
    In (k, v) (xelements m i) ->
    exists j, k = prev (prev_append j i) /\ get j m = Some v.

  Theorem elements_complete:
    forall A (m: t A) (i: positive) (v: A),
    In (i, v) (elements m) -> get i m = Some v.

  Definition xkeys {A} (m: t A) (i: positive) := List.map fst (xelements m i).

  Lemma xkeys_Node:
    forall A (m1: t A) o (m2: t A) i,
    xkeys (Node m1 o m2) i =
       xkeys m1 (xO i)
    ++ match o with None => nil | Some v => prev i :: nil end
    ++ xkeys m2 (xI i).

  Lemma in_xkeys:
    forall (A: Type) (m: t A) (i k: positive),
    In k (xkeys m i) ->
    (exists j, k = prev (prev_append j i)).

  Lemma xelements_keys_norepet:
    forall (A: Type) (m: t A) (i: positive),
    list_norepet (xkeys m i).

  Theorem elements_keys_norepet:
    forall A (m: t A),
    list_norepet (List.map (@fst elt A) (elements m)).

  Remark xelements_empty:
    forall A (m: t A) i, (forall i, get i m = None) -> xelements m i = nil.

  Theorem elements_canonical_order':
    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
    (forall i, option_rel R (get i m) (get i n)) ->
    list_forall2
      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
      (elements m) (elements n).

  Theorem elements_canonical_order:
    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
    list_forall2
      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
      (elements m) (elements n).

  Theorem elements_extensional:
    forall (A: Type) (m n: t A),
    (forall i, get i m = get i n) ->
    elements m = elements n.

  Lemma xelements_set:
    forall A v v' (m: t A) i j,
    get i m = Some v ->
    exists l1 l2,
    xelements m j = l1 ++ (prev (prev_append i j), v) :: l2
    /\ xelements (set i v' m) j = l1 ++ (prev (prev_append i j), v') :: l2.

  Theorem elements_set:
    forall A i v v' (m: t A),
    get i m = Some v ->
    exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (set i v' m) = l1 ++ (i,v') :: l2.

  Lemma xelements_remove:
    forall A v (m: t A) i j,
    get i m = Some v ->
    exists l1 l2,
    xelements m j = l1 ++ (prev (prev_append i j), v) :: l2
    /\ xelements (remove i m) j = l1 ++ l2.

  Theorem elements_remove:
    forall A i v (m: t A),
    get i m = Some v ->
    exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2.

  Lemma elements_xelements {A} : forall (m: t A),
      elements m = xelements m xH.

  Lemma elements_filter: forall A (pred: positive -> A -> bool) (m: t A),
      elements (filter pred m) = List.filter (fun x => pred (fst x) (snd x)) (elements m).

Folding over a tree

  Fixpoint fold' {A B} (f: B -> positive -> A -> B)
                 (i: positive) (m: tree' A) (v: B) {struct m} : B :=
    match m with
    | Node001 r => fold' f (xI i) r v
    | Node010 x => f v (prev i) x
    | Node011 x r => fold' f (xI i) r (f v (prev i) x)
    | Node100 l => fold' f (xO i) l v
    | Node101 l r => fold' f (xI i) r (fold' f (xO i) l v)
    | Node110 l x => f (fold' f (xO i) l v) (prev i) x
    | Node111 l x r => fold' f (xI i) r (f (fold' f (xO i) l v) (prev i) x)
    end.

  Definition fold {A B} (f: B -> positive -> A -> B) (m: t A) (v: B) :=
   match m with Empty => v | Nodes m' => fold' f xH m' v end.

  Lemma fold'_xelements':
    forall A B (f: B -> positive -> A -> B) m i v l,
    List.fold_left (fun a p => f a (fst p) (snd p)) l (fold' f i m v) =
    List.fold_left (fun a p => f a (fst p) (snd p)) (xelements' m i l) v.

  Theorem fold_spec:
    forall A B (f: B -> positive -> A -> B) (v: B) (m: t A),
    fold f m v =
    List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.

  Fixpoint fold1' {A B} (f: B -> A -> B) (m: tree' A) (v: B) {struct m} : B :=
    match m with
    | Node001 r => fold1' f r v
    | Node010 x => f v x
    | Node011 x r => fold1' f r (f v x)
    | Node100 l => fold1' f l v
    | Node101 l r => fold1' f r (fold1' f l v)
    | Node110 l x => f (fold1' f l v) x
    | Node111 l x r => fold1' f r (f (fold1' f l v) x)
    end.


  Definition fold1 {A B} (f: B -> A -> B) (m: t A) (v: B) : B :=
    match m with Empty => v | Nodes m' => fold1' f m' v end.

  Lemma fold1'_xelements':
    forall A B (f: B -> A -> B) m i v l,
    List.fold_left (fun a p => f a (snd p)) l (fold1' f m v) =
    List.fold_left (fun a p => f a (snd p)) (xelements' m i l) v.

  Theorem fold1_spec:
    forall A B (f: B -> A -> B) (v: B) (m: t A),
    fold1 f m v =
    List.fold_left (fun a p => f a (snd p)) (elements m) v.

  Local Open Scope positive.
  Lemma set_disjoint1:
    forall (A: Type)(i d : elt) (m: t A) (x y: A),
      set (i + d) y (set i x m) = set i x (set (i + d) y m).
  
  Local Open Scope positive.
  Lemma set_disjoint:
    forall (A: Type)(i j : elt) (m: t A) (x y: A),
      i <> j ->
      set j y (set i x m) = set i x (set j y m).

  Arguments empty A : simpl never.
  Arguments get {A} p m : simpl never.
  Arguments set {A} p x m : simpl never.
  Arguments remove {A} p m : simpl never.
End PTree.

An implementation trees of qualified identifiers

Module PTree_rec.

Fixpoint t (n:nat) (A: Type): Type :=
   match n with
   | O => unit
   | S n => PTree.t (option A * t n A)
   end.

Definition empty {A:Type} {n:nat} : t n A :=
  match n with
  | O => tt
  | S n' => @PTree.empty _
  end.

Fixpoint get {A:Type} {n:nat} (key: list positive): (t n A) -> option A :=
   match n with
   | O => fun _ => None
   | S n' =>
     fun map => match key with
     | nil => None
     | cons p k => SOME m <- PTree.get p map IN
                   match k with
                   | nil => fst m
                   | _ => get k (snd m)
                   end
     end
   end.

Fixpoint set {A:Type} {n:nat} (key: list positive) (v: A): (t n A) -> (t n A) :=
   match n return (t n A) -> (t n A) with
   | O => fun t => t
   | S n' =>
     fun map => match key with
             | nil => map
             | cons p k =>
                 let prev := match PTree.get p map with
                             | None => (None, empty)
                             | Some prev => prev
                             end in
                 PTree.set p (match k with
                              | nil => (Some v, snd prev)
                              | _ => (fst prev, set k v (snd prev))
                              end)
                           map
             end
   end.

Open Scope nat.

Fact get_length :
  forall A n i (m: t n A) v, get i m = Some v -> 0 < length i <= n.

Lemma gempty : forall A n i, get i (@empty A n) = None.

Lemma gss : forall A n i x (m: t n A),
    0 < length i <= n ->
    get i (set i x m) = Some x.

Lemma gso : forall A n i j x (m: t n A),
    i <> j ->
    get i (set j x m) = get i m.

Fixpoint remove {A:Type} {n:nat} (key: list positive): (t n A) -> (t n A) :=
   match n return (t n A) -> (t n A) with
   | O => fun t => t
   | S n' =>
     fun map => match key with
             | nil => map
             | cons p k =>
                 match PTree.get p map with
                 | Some t =>
                     PTree.set p
                       (match k with
                        | nil => (None, snd t)
                        | _ => (fst t, remove k (snd t))
                        end) map
                 | None => map
                 end
             end
   end.

Lemma grs : forall A n i (m: t n A),
    get i (remove i m) = None.

Lemma gro : forall A n i j (m: t n A),
    i <> j ->
    get i (remove j m) = get i m.

Import ListNotations.

Fixpoint map' {A B: Type} {n:nat} (f: list positive -> A -> B) xs : (t n A) -> (t n B) :=
  match n return (t n A) -> (t n B) with
  | O => fun tt => tt
  | S n' => fun t =>
             PTree.map (fun x t =>
                          let xs' := List.app xs [x] in
                          (option_map (f xs') (fst t), map' f xs' (snd t))) t
  end.
Definition map {A B: Type} {n:nat} (f: list positive -> A -> B) := @map' A B n f nil.

Lemma gmap' : forall A B n (f: _ -> A -> B) i xs (m : t n A),
    get i (map' f xs m) = option_map (f (xs ++ i)) (get i m).

Corollary gmap : forall A B n (f: _ -> A -> B) i (m : t n A),
    get i (map f m) = option_map (f i) (get i m).

Fixpoint map1 {A B: Type} {n:nat} (f: A -> B) : (t n A) -> (t n B) :=
  match n return (t n A) -> (t n B) with
  | O => fun tt => tt
  | S n' => fun t =>
             PTree.map (fun _ t => (option_map f (fst t), map1 f (snd t))) t
  end.

Lemma gmap1 : forall A B n (f: A -> B) i (m : t n A),
    get i (map1 f m) = option_map f (get i m).

Fixpoint combine {A B C: Type} {n:nat} (f: option A -> option B -> option C) : t n A -> t n B -> t n C :=
  match n return t n A -> t n B -> t n C with
  | O => fun _ _ => tt
  | S n' =>
      PTree.combine (fun ot1 ot2 =>
                       match ot1, ot2 with
                       | Some t1, Some t2 => Some (f (fst t1) (fst t2), combine f (snd t1) (snd t2))
                       | Some t1, None => Some (f (fst t1) None, combine f (snd t1) empty)
                       | None, Some t2 => Some (f None (fst t2), combine f empty (snd t2))
                       | None, None => None
                       end)
  end.

Lemma gcombine : forall A B C n (f: _ -> _ -> option C),
    f None None = None ->
    forall (m1: t n A) (m2: t n B) i,
      get i (combine f m1 m2) = f (get i m1) (get i m2).

Definition f_mostdef {A:Type} := @PTree.f_mostdef A.

Fixpoint combine_mostdef {A: Type} {n:nat} (f: A -> A -> option A) : t n A -> t n A -> option (t n A) :=
  match n return t n A -> t n A -> option (t n A) with
  | O => fun _ _ => Some tt
  | S n' => PTree.combine_mostdef
             (fun t1 t2 =>
                SOME v <- f_mostdef f (fst t1) (fst t2) IN
                SOME t <- combine_mostdef f (snd t1) (snd t2) IN
                Some (v, t))
  end.

Lemma gcombine_mostdef : forall A n (mostdef : A -> A -> option A) (m1 m2 m3 : t n A) a i,
  combine_mostdef mostdef m1 m2 = Some m3 ->
  f_mostdef mostdef (get i m1) (get i m2) = Some a ->
  get i m3 = a.

Lemma fcombine_mostdef : forall A n (mostdef : A -> A -> option A) (m1 m2 : t n A),
    combine_mostdef mostdef m1 m2 = None ->
    (forall i (a1 a2 : A),
        0 < length i <= n -> get i m1 = Some a1 -> get i m2 = Some a2 -> mostdef a1 a2 <> None) -> False.

Lemma gcombine_mostdef_ok : forall A n (mostdef : A -> A -> option A) (m1 m2 m3 : t n A) i a,
    combine_mostdef mostdef m1 m2 = Some m3 ->
    get i m3 = Some a -> f_mostdef mostdef (get i m1) (get i m2) = Some (Some a).

Lemma gcombine_mostdef_only_l :
  forall A n (mostdef : A -> A -> option A) (m1 : t n A),
    combine_mostdef mostdef m1 empty = Some m1.

Lemma gcombine_mostdef_none_rev :
  forall A n (mostdef : A -> A -> option A) (m1 m2 m3 : t n A) i,
    combine_mostdef mostdef m1 m2 = Some m3 ->
    get i m3 = None -> get i m1 = None /\ get i m2 = None.

Fixpoint elements {A: Type} {n} : t n A -> list (list positive * A) :=
  match n return t n A -> _ with
  | O => fun _ => nil
  | S _ => fun t1 =>
            List.flat_map
              (fun xv =>
                 let l := List.map (fun xsv => (fst xv::fst xsv, snd xsv)) (elements (snd (snd xv))) in
                 match fst (snd xv) with
                 | Some v => ([fst xv], v)::l
                 | None => l
                 end)
              (PTree.elements t1)
  end.

Lemma elements_correct :
  forall (A : Type) n (m : t n A) i (v : A), get i m = Some v -> In (i, v) (elements m).

Lemma elements_complete :
  forall (A : Type) n (m : t n A) i (v : A), In (i, v) (elements m) -> get i m = Some v.

Lemma elements_keys_norepet :
  forall (A : Type) n (m : t n A), list_norepet (List.map fst (elements m)).

Lemma elements_remove :
  forall (A : Type) n i (v : A) (m : t n A),
  get i m = Some v ->
  exists l1 l2 : list (_ * A),
    elements m = l1 ++ (i, v) :: l2 /\ elements (remove i m) = l1 ++ l2.

Fixpoint fold' {A B: Type} {n:nat} (f: B -> list positive -> A -> B) xs : t n A -> B -> B :=
  match n return t n A -> B -> B with
  | O => fun _ b => b
  | S _ => PTree.fold
            (fun b x t =>
               let xs' := List.app xs [x] in
               fold' f xs' (snd t) (match fst t with Some v => f b xs' v | None => b end))
  end.

Definition fold {A B: Type} {n:nat} (f: B -> list positive -> A -> B) : t n A -> B -> B :=
  fold' f nil.

Lemma fold'_spec :
  forall A B n (f : B -> list positive -> A -> B) xs (v : B) (m : t n A),
    fold' f xs m v = fold_left (fun a p => f a (xs++fst p) (snd p)) (elements m) v.

Corollary fold_spec :
  forall A B n (f : B -> list positive -> A -> B) (v : B) (m : t n A),
    fold f m v = fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.

Fixpoint fold1 {A B: Type} {n} (f: B -> A -> B) : t n A -> B -> B :=
  match n return t n A -> B -> B with
  | O => fun _ b => b
  | S _ => PTree.fold1
              (fun b t => fold1 f (snd t) (match fst t with Some v => f b v | None => b end))
  end.

Lemma fold1_spec :
  forall A B n (f : B -> A -> B) (v : B) (m : t n A),
    fold1 f m v = fold_left (fun a p => f a (snd p)) (elements m) v.

Lemma flat_map_remove_nils: forall A B (f: _ -> list B) (t: PTree.t A),
    exists t', flat_map f (PTree.elements t) = flat_map f (PTree.elements t')
          /\ Forall (fun x => f x <> nil) (PTree.elements t').

Lemma list_forall2_flat_map : forall A1 A2 B1 B2 (f1: A1 -> list B1) (f2: A2 -> list B2) P l1 l2,
    list_forall2 (fun x1 x2 => list_forall2 P (f1 x1) (f2 x2)) l1 l2 ->
    list_forall2 P (flat_map f1 l1) (flat_map f2 l2).

Theorem elements_canonical_order':
  forall A B n (R: A -> B -> Prop) (t1: t n A) (t2: t n B),
  (forall i, (0 < length i <= n)%nat -> option_rel R (get i t1) (get i t2)) ->
  list_forall2
    (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
    (elements t1) (elements t2).

Fixpoint list_beq {A: Type} (beqA: A -> A -> bool) (l1 l2: list A) : bool :=
  match l1, l2 with
  | [], [] => true
  | hd1::tl1, hd2::tl2 => (beqA hd1 hd2) && (list_beq beqA tl1 tl2)
  | _, _ => false
  end.

Lemma list_beq_correct {A: Type} (beqA: A -> A -> bool) : forall l1 l2,
  list_beq beqA l1 l2 = true <-> list_forall2 (fun x1 x2 => beqA x1 x2 = true) l1 l2.

Lemma list_forall2_same {A: Type} (P: A -> A -> Prop) : forall l,
    Forall (fun x => P x x) l -> list_forall2 P l l.

Definition beq {A: Type} {n} (beqA: A -> A -> bool) (m1 m2: t n A) : bool :=
  list_beq (fun x1 x2 => list_beq Pos.eqb (fst x1) (fst x2) && beqA (snd x1) (snd x2))
    (elements m1) (elements m2).

Lemma beq_correct:
  forall {A} {n} (eqA: A -> A -> bool) (t1 t2: t n A),
  beq eqA t1 t2 = true <->
  (forall (x: list positive),
    0 < length x <= n ->
    match get x t1, get x t2 with
    | None, None => True
    | Some y1, Some y2 => eqA y1 y2 = true
    | _, _ => False
  end).

End PTree_rec.

Module Type QUALIDENT.
  Parameter depth : nat.
  Parameter t : Type.

  Parameter eq : forall (id1 id2 : t), { id1 = id2 } + { id1 <> id2 }.
  Parameter to_list : t -> list positive.

  Parameter to_list_length : forall id,
      (0 < length (to_list id) <= depth)%nat.

  Parameter to_list_injective : forall i j,
      to_list i = to_list j ->
      i = j.

  Parameter of_list : list positive -> t.

  Parameter of_list_injective : forall i j,
      (0 < length i <= depth)%nat ->
      (0 < length j <= depth)%nat ->
      of_list i = of_list j ->
      i = j.

  Parameter to_of_list : forall l, of_list (to_list l) = l.
  Parameter of_to_list : forall l, (0 < length l <= depth)%nat -> to_list (of_list l) = l.
End QUALIDENT.

Module QITree(QI: QUALIDENT) <: TREE.
  Definition elt := QI.t.
  Definition elt_eq := QI.eq.
  Definition t := PTree_rec.t QI.depth.

  Definition empty {A: Type} : t A := @PTree_rec.empty A QI.depth.

  Definition get {A: Type} key := @PTree_rec.get A QI.depth (QI.to_list key).
  Definition set {A: Type} key := @PTree_rec.set A QI.depth (QI.to_list key).
  Definition remove {A: Type} key := @PTree_rec.remove A QI.depth (QI.to_list key).

  Lemma gempty : forall A i, get i (@empty A) = None.

  Lemma gss : forall A i x (m: t A), get i (set i x m) = Some x.

  Lemma gso : forall A i j x (m: t A), i <> j -> get i (set j x m) = get i m.

  Lemma gsspec : forall A i j x (m: t A),
      get i (set j x m) = if (elt_eq i j) then Some x else get i m.

  Lemma grs : forall A i (m: t A), get i (remove i m) = None.

  Lemma gro : forall A i j (m: t A), i <> j -> get i (remove j m) = get i m.

  Lemma grspec : forall A i j (m: t A),
      get i (remove j m) = if (elt_eq i j) then None else get i m.

  Definition beq {A: Type} (beqA: A -> A -> bool) (m1 m2: t A) : bool :=
    PTree_rec.beq beqA m1 m2.

  Lemma beq_correct:
    forall {A} (eqA: A -> A -> bool) (t1 t2: t A),
      beq eqA t1 t2 = true <->
        (forall x,
            match get x t1, get x t2 with
            | None, None => True
            | Some y1, Some y2 => eqA y1 y2 = true
            | _, _ => False
            end).

  Definition map {A B: Type} f := @PTree_rec.map A B QI.depth (fun qi => f (QI.of_list qi)).

  Lemma gmap : forall A B (f: _ -> A -> B) i (m : t A),
      get i (map f m) = option_map (f i) (get i m).

  Definition map1 {A B: Type} := @PTree_rec.map1 A B QI.depth.

  Lemma gmap1 : forall A B (f: A -> B) i (m : t A),
      get i (map1 f m) = option_map f (get i m).

  Definition combine {A B C: Type} := @PTree_rec.combine A B C QI.depth.

  Lemma gcombine : forall A B C (f: _ -> _ -> option C),
      f None None = None ->
      forall (m1: t A) (m2: t B) i,
        get i (combine f m1 m2) = f (get i m1) (get i m2).

  Definition combine_mostdef {A} := @PTree_rec.combine_mostdef A QI.depth.
  Definition f_mostdef {A} := @PTree_rec.f_mostdef A.

  Lemma gcombine_mostdef :
    forall (A : Type) (mostdef : A -> A -> option A) (m1 m2 m3 : t A) (a : option A) (i : elt),
      combine_mostdef mostdef m1 m2 = Some m3 ->
      f_mostdef mostdef (get i m1) (get i m2) = Some a -> get i m3 = a.

  Lemma fcombine_mostdef :
    forall (A : Type) (mostdef : A -> A -> option A) (m1 m2 : t A),
      combine_mostdef mostdef m1 m2 = None ->
      (forall i (a1 a2 : A),
          get i m1 = Some a1 -> get i m2 = Some a2 -> mostdef a1 a2 <> None) -> False.

  Lemma gcombine_mostdef_ok :
    forall (A : Type) (mostdef : A -> A -> option A) (m1 m2 m3 : t A) (i : elt) (a : A),
      combine_mostdef mostdef m1 m2 = Some m3 ->
      get i m3 = Some a -> f_mostdef mostdef (get i m1) (get i m2) = Some (Some a).

  Lemma gcombine_mostdef_only_l :
    forall (A : Type) (mostdef : A -> A -> option A) (m1 : t A),
      combine_mostdef mostdef m1 empty = Some m1.

  Lemma gcombine_mostdef_none_rev :
    forall (A : Type) (mostdef : A -> A -> option A) (m1 m2 m3 : t A) (i : elt),
      combine_mostdef mostdef m1 m2 = Some m3 ->
      get i m3 = None -> get i m1 = None /\ get i m2 = None.

  Definition elements {A} m :=
    List.map (fun x => (QI.of_list (fst x), snd x)) (@PTree_rec.elements A QI.depth m).

  Lemma elements_correct :
    forall (A : Type) (m : t A) (i : elt) (v : A), get i m = Some v -> In (i, v) (elements m).

  Lemma elements_complete :
    forall (A : Type) (m : t A) (i : elt) (v : A), In (i, v) (elements m) -> get i m = Some v.

  Lemma elements_keys_norepet :
    forall (A : Type) (m : t A), list_norepet (List.map fst (elements m)).

  Lemma elements_remove :
    forall (A : Type) (i : elt) (v : A) (m : t A),
    get i m = Some v ->
    exists l1 l2 : list (elt * A),
      elements m = l1 ++ (i, v) :: l2 /\ elements (remove i m) = l1 ++ l2.

  Definition fold {A B: Type} (f: B -> elt -> A -> B) : t A -> B -> B :=
    @PTree_rec.fold A B QI.depth (fun b xs => f b (QI.of_list xs)).

  Lemma fold_spec :
    forall (A B : Type) (f : B -> elt -> A -> B) (v : B) (m : t A),
      fold f m v = fold_left (fun (a : B) (p : elt * A) => f a (fst p) (snd p)) (elements m) v.

  Definition fold1 {A B: Type} (f: B -> A -> B) : t A -> B -> B :=
    @PTree_rec.fold1 A B QI.depth f.

  Lemma fold1_spec :
    forall (A B : Type) (f : B -> A -> B) (v : B) (m : t A),
      fold1 f m v = fold_left (fun (a : B) (p : elt * A) => f a (snd p)) (elements m) v.

  Theorem elements_canonical_order':
    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
      (forall i, option_rel R (get i m) (get i n)) ->
      list_forall2
        (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
        (elements m) (elements n).

End QITree.

An implementation of maps over type positive

Module PMap <: MAP.
  Definition elt := positive.
  Definition elt_eq := peq.

  Definition t (A : Type) : Type := (A * PTree.t A)%type.

  Definition init (A : Type) (x : A) :=
    (x, PTree.empty A).

  Definition get (A : Type) (i : positive) (m : t A) :=
    match PTree.get i (snd m) with
    | Some x => x
    | None => fst m
    end.

  Definition set (A : Type) (i : positive) (x : A) (m : t A) :=
    (fst m, PTree.set i x (snd m)).

  Theorem gi:
    forall (A: Type) (i: positive) (x: A), get i (init x) = x.

  Theorem gss:
    forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = x.

  Theorem gso:
    forall (A: Type) (i j: positive) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.

  Theorem gsspec:
    forall (A: Type) (i j: positive) (x: A) (m: t A),
    get i (set j x m) = if peq i j then x else get i m.

  Theorem gsident:
    forall (A: Type) (i j: positive) (m: t A),
    get j (set i (get i m) m) = get j m.

  Definition map (A B : Type) (f : A -> B) (m : t A) : t B :=
    (f (fst m), PTree.map1 f (snd m)).

  Theorem gmap:
    forall (A B: Type) (f: A -> B) (i: positive) (m: t A),
    get i (map f m) = f(get i m).

  Theorem set2:
    forall (A: Type) (i: elt) (x y: A) (m: t A),
    set i y (set i x m) = set i y m.

  Local Open Scope positive.
  Lemma set_disjoint:
    forall (A: Type) (i j : elt) (x y: A) (m: t A),
      i <> j ->
      set j y (set i x m) = set i x (set j y m).

End PMap.

An implementation of maps over any type that injects into type positive

Module Type INDEXED_TYPE.
  Parameter t: Type.
  Parameter index: t -> positive.
  Axiom index_inj: forall (x y: t), index x = index y -> x = y.
  Parameter eq: forall (x y: t), {x = y} + {x <> y}.
End INDEXED_TYPE.

Module IMap(X: INDEXED_TYPE).

  Definition elt := X.t.
  Definition elt_eq := X.eq.
  Definition t : Type -> Type := PMap.t.
  Definition init (A: Type) (x: A) := PMap.init x.
  Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m.
  Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
  Definition map (A B: Type) (f: A -> B) (m: t A) : t B := PMap.map f m.

  Lemma gi:
    forall (A: Type) (x: A) (i: X.t), get i (init x) = x.

  Lemma gss:
    forall (A: Type) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.

  Lemma gso:
    forall (A: Type) (i j: X.t) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.

  Lemma gsspec:
    forall (A: Type) (i j: X.t) (x: A) (m: t A),
    get i (set j x m) = if X.eq i j then x else get i m.

  Lemma gmap:
    forall (A B: Type) (f: A -> B) (i: X.t) (m: t A),
    get i (map f m) = f(get i m).

  Lemma set2:
    forall (A: Type) (i: elt) (x y: A) (m: t A),
    set i y (set i x m) = set i y m.

  Lemma set_disjoint:
    forall (A: Type) (i j : elt) (x y: A) (m: t A),
      i <> j ->
      set j y (set i x m) = set i x (set j y m).
End IMap.

Module ZIndexed.
  Definition t := Z.
  Definition index (z: Z): positive :=
    match z with
    | Z0 => xH
    | Zpos p => xO p
    | Zneg p => xI p
    end.
  Lemma index_inj: forall (x y: Z), index x = index y -> x = y.
  Definition eq := zeq.
End ZIndexed.

Module ZMap := IMap(ZIndexed).

Module NIndexed.
  Definition t := N.
  Definition index (n: N): positive :=
    match n with
    | N0 => xH
    | Npos p => xO p
    end.
  Lemma index_inj: forall (x y: N), index x = index y -> x = y.
  Lemma eq: forall (x y: N), {x = y} + {x <> y}.
End NIndexed.

Module NMap := IMap(NIndexed).

An implementation of maps over any type with decidable equality

Module Type EQUALITY_TYPE.
  Parameter t: Type.
  Parameter eq: forall (x y: t), {x = y} + {x <> y}.
End EQUALITY_TYPE.

Module EMap(X: EQUALITY_TYPE) <: MAP.

  Definition elt := X.t.
  Definition elt_eq := X.eq.
  Definition t (A: Type) := X.t -> A.
  Definition init (A: Type) (v: A) := fun (_: X.t) => v.
  Definition get (A: Type) (x: X.t) (m: t A) := m x.
  Definition set (A: Type) (x: X.t) (v: A) (m: t A) :=
    fun (y: X.t) => if X.eq y x then v else m y.
  Lemma gi:
    forall (A: Type) (i: elt) (x: A), init x i = x.
  Lemma gss:
    forall (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.
  Lemma gso:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> (set j x m) i = m i.
  Lemma gsspec:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    get i (set j x m) = if elt_eq i j then x else get i m.
  Lemma gsident:
    forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
  Definition map (A B: Type) (f: A -> B) (m: t A) :=
    fun (x: X.t) => f(m x).
  Lemma gmap:
    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
    get i (map f m) = f(get i m).
End EMap.

A partial implementation of trees over any type that injects into type positive

Module ITree(X: INDEXED_TYPE).

  Definition elt := X.t.
  Definition elt_eq := X.eq.
  Definition t : Type -> Type := PTree.t.

  Definition empty (A: Type): t A := PTree.empty A.
  Definition get (A: Type) (k: elt) (m: t A): option A := PTree.get (X.index k) m.
  Definition set (A: Type) (k: elt) (v: A) (m: t A): t A := PTree.set (X.index k) v m.
  Definition remove (A: Type) (k: elt) (m: t A): t A := PTree.remove (X.index k) m.

  Theorem gempty:
    forall (A: Type) (i: elt), get i (empty A) = None.
  Theorem gss:
    forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
  Theorem gso:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.
  Theorem gsspec:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    get i (set j x m) = if elt_eq i j then Some x else get i m.
  Theorem grs:
    forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
  Theorem gro:
    forall (A: Type) (i j: elt) (m: t A),
    i <> j -> get i (remove j m) = get i m.
  Theorem grspec:
    forall (A: Type) (i j: elt) (m: t A),
    get i (remove j m) = if elt_eq i j then None else get i m.

  Definition beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool := PTree.beq.
  Theorem beq_sound:
    forall (A: Type) (eqA: A -> A -> bool) (t1 t2: t A),
    beq eqA t1 t2 = true ->
    forall (x: elt),
     match get x t1, get x t2 with
     | None, None => True
     | Some y1, Some y2 => eqA y1 y2 = true
     | _, _ => False
    end.

  Definition combine: forall (A B C: Type), (option A -> option B -> option C) -> t A -> t B -> t C := PTree.combine.
  Theorem gcombine:
    forall (A B C: Type) (f: option A -> option B -> option C),
    f None None = None ->
    forall (m1: t A) (m2: t B) (i: elt),
    get i (combine f m1 m2) = f (get i m1) (get i m2).
End ITree.

Module ZTree := ITree(ZIndexed).

Additional properties over trees

Require Import Equivalence EquivDec.

Module Tree_Properties(T: TREE).


Section TREE_FOLD_IND.

Variables V A: Type.
Variable f: A -> T.elt -> V -> A.
Variable P: T.t V -> A -> Type.
Variable init: A.
Variable m_final: T.t V.

Hypothesis H_base:
  forall m,
  (forall k, T.get k m = None) ->
  P m init.

Hypothesis H_rec:
  forall m a k v,
  T.get k m = Some v -> T.get k m_final = Some v ->
  P (T.remove k m) a -> P m (f a k v).

Let f' (p : T.elt * V) (a: A) := f a (fst p) (snd p).

Let P' (l: list (T.elt * V)) (a: A) : Type :=
  forall m, (forall k v, In (k, v) l <-> T.get k m = Some v) -> P m a.

Let H_base':
  P' nil init.

Let H_rec':
  forall k v l a,
  ~In k (List.map fst l) ->
  T.get k m_final = Some v ->
  P' l a ->
  P' ((k, v) :: l) (f a k v).

Lemma fold_ind_aux:
  forall l,
  (forall k v, In (k, v) l -> T.get k m_final = Some v) ->
  list_norepet (List.map fst l) ->
  P' l (List.fold_right f' init l).

Theorem fold_ind:
  P m_final (T.fold f m_final init).

End TREE_FOLD_IND.

Section TREE_FOLD_REC.

Variables V A: Type.
Variable f: A -> T.elt -> V -> A.
Variable P: T.t V -> A -> Prop.
Variable init: A.
Variable m_final: T.t V.

Hypothesis P_compat:
  forall m m' a,
  (forall x, T.get x m = T.get x m') ->
  P m a -> P m' a.

Hypothesis H_base:
  P (T.empty _) init.

Hypothesis H_rec:
  forall m a k v,
  T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v).

Theorem fold_rec:
  P m_final (T.fold f m_final init).

End TREE_FOLD_REC.


Section MEASURE.

Variable V: Type.

Definition cardinal (x: T.t V) : nat := List.length (T.elements x).

Theorem cardinal_remove:
  forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat.

End MEASURE.


Section FORALL_EXISTS.

Variable A: Type.

Definition for_all (m: T.t A) (f: T.elt -> A -> bool) : bool :=
  T.fold (fun b x a => b && f x a) m true.

Lemma for_all_correct:
  forall m f,
  for_all m f = true <-> (forall x a, T.get x m = Some a -> f x a = true).

Definition exists_ (m: T.t A) (f: T.elt -> A -> bool) : bool :=
  T.fold (fun b x a => b || f x a) m false.

Lemma exists_correct:
  forall m f,
  exists_ m f = true <-> (exists x a, T.get x m = Some a /\ f x a = true).

Remark exists_for_all:
  forall m f,
  exists_ m f = negb (for_all m (fun x a => negb (f x a))).

Remark for_all_exists:
  forall m f,
  for_all m f = negb (exists_ m (fun x a => negb (f x a))).

Lemma for_all_false:
  forall m f,
  for_all m f = false <-> (exists x a, T.get x m = Some a /\ f x a = false).

Lemma exists_false:
  forall m f,
  exists_ m f = false <-> (forall x a, T.get x m = Some a -> f x a = false).

End FORALL_EXISTS.


Section EXTENSIONAL_EQUALITY.

Variable A: Type.
Variable eqA: A -> A -> Prop.
Hypothesis eqAeq: Equivalence eqA.

Definition Equal (m1 m2: T.t A) : Prop :=
  forall x, match T.get x m1, T.get x m2 with
                | None, None => True
                | Some a1, Some a2 => a1 === a2
                | _, _ => False
            end.

Lemma Equal_refl: forall m, Equal m m.

Lemma Equal_sym: forall m1 m2, Equal m1 m2 -> Equal m2 m1.

Lemma Equal_trans: forall m1 m2 m3, Equal m1 m2 -> Equal m2 m3 -> Equal m1 m3.

Global Instance Equal_Equivalence : Equivalence Equal := {
  Equivalence_Reflexive := Equal_refl;
  Equivalence_Symmetric := Equal_sym;
  Equivalence_Transitive := Equal_trans
}.

Hypothesis eqAdec: EqDec A eqA.


End EXTENSIONAL_EQUALITY.


Section OF_LIST.

Variable A: Type.

Let f := fun (m: T.t A) (k_v: T.elt * A) => T.set (fst k_v) (snd k_v) m.

Definition of_list (l: list (T.elt * A)) : T.t A :=
  List.fold_left f l (T.empty _).

Lemma in_of_list:
  forall l k v, T.get k (of_list l) = Some v -> In (k, v) l.

Lemma of_list_dom:
  forall l k, In k (map fst l) -> exists v, T.get k (of_list l) = Some v.

Remark of_list_unchanged:
  forall k l m, ~In k (map fst l) -> T.get k (List.fold_left f l m) = T.get k m.

Lemma not_in_of_list:
  forall l k, ~In k (map fst l) <-> T.get k (of_list l) = None.

Lemma of_list_unique:
  forall k v l1 l2,
  ~In k (map fst l2) -> T.get k (of_list (l1 ++ (k, v) :: l2)) = Some v.

Lemma of_list_norepet:
  forall l k v, list_norepet (map fst l) -> In (k, v) l -> T.get k (of_list l) = Some v.

Lemma of_list_elements:
  forall m k, T.get k (of_list (T.elements m)) = T.get k m.

End OF_LIST.

Lemma of_list_related:
  forall (A B: Type) (R: A -> B -> Prop) k l1 l2,
  list_forall2 (fun ka kb => fst ka = fst kb /\ R (snd ka) (snd kb)) l1 l2 ->
  option_rel R (T.get k (of_list l1)) (T.get k (of_list l2)).

End Tree_Properties.

Module PTree_Properties := Tree_Properties(PTree).

Useful notations

Notation "a ! b" := (PTree.get b a) (at level 1).
Notation "a !! b" := (PMap.get b a) (at level 1).