Module Maps


Applicative finite maps are the main data structure used in this project. A finite map associates data to keys. The two main operations are set k d m, which returns a map identical to m except that d is associated to k, and get k m which returns the data associated to key k in map m. In this library, we distinguish two kinds of maps: In this library, we provide efficient implementations of trees and maps whose keys range over the type positive of binary positive integers or any type that can be injected into positive. The implementation is based on radix-2 search trees (uncompressed Patricia trees) and guarantees logarithmic-time operations. An inefficient implementation of maps as functions is also provided.

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.

The ``good variables'' properties for trees, expressing commutations between get, set and remove.
  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.

Extensional equality between trees.
  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).

Applying a function to all data of a tree.
  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).

Same as map, but the function does not receive the elt argument.
  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).

Applying a function pairwise to all data of two trees.
  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).

A combine version that may fail, parametrized by a most defined function.
  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.

An impure combine version, parametrized by a most defined function.

Enumerating the bindings of a tree.
  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.

Folding a function over all bindings of a tree.
  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.
Same as fold, but the function does not receive the elt argument.
  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


The type tree' of nonempty trees. Each constructor is of the form NodeXYZ, where the bit X says whether there is a left subtree, Y whether there is a value at this node, and Z whether there is a right subtree.

  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.

A smart constructor for type tree: given a (possibly empty) left subtree, a (possibly absent) value, and a (possibly empty) right subtree, it builds the corresponding 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.

set0 p x constructs the singleton tree that maps p to x and has no other bindings.

  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.

Removal in a nonempty tree produces a possibly empty tree. To simplify the code, we use the Node smart constructor in the cases where the result can be empty or nonempty, depending on the results of the recursive calls.

  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.

This use of Node causes some run-time overhead, which we eliminate by partial evaluation within Coq.

  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.
  Proof.

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

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

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

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

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

  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.
  Proof.

  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.
  Proof.

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

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

  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.
  Proof.

Custom case analysis principles and induction principles


We can view trees as being of one of two (non-exclusive) cases: either Empty for an empty tree, or Node l o r for a nonempty tree, with l and r the left and right subtrees and o an optional value. The Empty constructor and the Node smart function defined above provide one half of the view: the one that lets us construct values of type tree A. We now define the other half of the view: the one that lets us inspect and recurse over values of type tree A. This is achieved by defining appropriate principles for case analysis and induction.

  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.

A case analysis principle

  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.
  Proof.

  End TREE_CASE.

A recursion principle

  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).
  Proof.

  End TREE_REC.

A double recursion principle

  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.
  Proof.

  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).
  Proof.

  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).
  Proof.

  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).
  Proof.

  End TREE_REC2.

An induction principle

  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.
  Proof.

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

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

Some consequences of extensionality

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

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

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).
    Proof.

    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).
    Proof.

  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.
  Proof.

  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'.
  Proof.

  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).
  Proof.

  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).
  Proof.

  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).
  Proof.

  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.
  Proof.
  
  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.
  Proof.

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

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

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

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

  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.
  Proof.

  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.
  Proof.

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

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

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

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

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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).
  Proof.

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

  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.
  Proof.
  
  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.
  Proof.

  Lemma f_imp_mostdef_l: forall a,
    WHEN f_imp_mostdef a None ~> a' THEN a = a'.
  Proof.
  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'.
  Proof.
  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.
  Proof.

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

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.
  
  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).
  Proof.

  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.
  Proof.
  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.
  Proof.
  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

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.
  Proof.

  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).
  Proof.

  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).
  Proof.

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

  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.
  Proof.

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

  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).
  Proof.

  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)).
  Proof.

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

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

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

  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).
  Proof.

  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).
  Proof.

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

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

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

  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).
  Proof.

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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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).
  Proof.
  
  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).
  Proof.

  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.
Proof.

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

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

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

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.
Proof.

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

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).
Proof.

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).
Proof.

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).
Proof.

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).
Proof.

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.
Proof.

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.
Proof.

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).
Proof.

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

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.
Proof.

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).
Proof.

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

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

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.
Proof.

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.
Proof.

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.
Proof.

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.
Proof.

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').
Proof.

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).
Proof.

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).
Proof.

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.
Proof.

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

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).
Proof.

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.
  Proof.

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

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

  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.
  Proof.

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

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

  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.
  Proof.

  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).
  Proof.

  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).
  Proof.

  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).
  Proof.

  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).
  Proof.

  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.
  Proof.

  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.
  Proof.

  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).
  Proof.

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

  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.
  Proof.

  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).
  Proof.

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

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

  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.
  Proof.

  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.
  Proof.

  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.
  Proof.

  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).
  Proof.

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.
  Proof.

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

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

  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.
  Proof.

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

  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).
  Proof.

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

  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).
  Proof.

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.
  Proof.

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

  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.
  Proof.

  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.
  Proof.

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

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

  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).
  Proof.
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.
  Proof.
  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.
  Proof.
  Lemma eq: forall (x y: N), {x = y} + {x <> y}.
  Proof.
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.
  Proof.
  Lemma gss:
    forall (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.
  Proof.
  Lemma gso:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> (set j x m) i = m i.
  Proof.
  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.
  Proof.
  Lemma gsident:
    forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
  Proof.
  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).
  Proof.
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.
  Proof.
  Theorem gss:
    forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
  Proof.
  Theorem gso:
    forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.
  Proof.
  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.
  Proof.
  Theorem grs:
    forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
  Proof.
  Theorem gro:
    forall (A: Type) (i j: elt) (m: t A),
    i <> j -> get i (remove j m) = get i m.
  Proof.
  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.
  Proof.

  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.
  Proof.

  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).
  Proof.
End ITree.

Module ZTree := ITree(ZIndexed).

Additional properties over trees


Require Import Equivalence EquivDec.

Module Tree_Properties(T: TREE).

Two induction principles over fold.

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.
Proof.

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).
Proof.

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).
Proof.

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

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).
Proof.

End TREE_FOLD_REC.

A nonnegative measure over trees

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.
Proof.

End MEASURE.

Forall and exists

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).
Proof.

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).
Proof.

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

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

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).
Proof.

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

End FORALL_EXISTS.

Extensional equality between trees

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.
Proof.

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

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

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.

Creating a tree from a list of (key, value) pairs.

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.
Proof.

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

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.
Proof.

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

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.
Proof.

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.
Proof.

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

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)).
Proof.

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).
Generated by coq2html