Require Import Equivalence EquivDec.
Require Import Coqlib.

LocalLocal
Set Implicit Arguments.

Module Type TREE.
  Variable elt: Type.
  Variable elt_eq: ∀ (a b: elt), {a = b} + {a ≠ b}.
  Variable t: Type → Type.
  Variable empty: ∀ (A: Type), t A.
  Variable get: ∀ (A: Type), elt → t A → option A.
  Variable set: ∀ (A: Type), elt → A → t A → t A.
  Variable remove: ∀ (A: Type), elt → t A → t A.

  Hypothesis gempty:
    ∀ (A: Type) (i: elt), get i (empty A) = None.
  Hypothesis gss:
    ∀ (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
  Hypothesis gso:
    ∀ (A: Type) (i j: elt) (x: A) (m: t A),
    i ≠ j → get i (set j x m) = get i m.
  Hypothesis gsspec:
    ∀ (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.
  Hypothesis gsident:
    ∀ (A: Type) (i: elt) (m: t A) (v: A),
    get i m = Some v → set i v m = m.
  Hypothesis grs:
    ∀ (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
  Hypothesis gro:
    ∀ (A: Type) (i j: elt) (m: t A),
    i ≠ j → get i (remove j m) = get i m.
  Hypothesis grspec:
    ∀ (A: Type) (i j: elt) (m: t A),
    get i (remove j m) = if elt_eq i j then None else get i m.

  Variable beq: ∀ (A: Type), (A → A → bool) → t A → t A → bool.
  Hypothesis beq_correct:
    ∀ (A: Type) (eqA: A → A → bool) (t1 t2: t A),
    beq eqA t1 t2 = true ↔
    (∀ (x: elt),
     match get x t1, get x t2 with
     | None, None ⇒ True
     | Some y1, Some y2 ⇒ eqA y1 y2 = true
     | _, _ ⇒ False
    end).

  Variable map:
    ∀ (A B: Type), (elt → A → B) → t A → t B.
  Hypothesis gmap:
    ∀ (A B: Type) (f: elt → A → B) (i: elt) (m: t A),
    get i (map f m) = option_map (f i) (get i m).

  Variable map1:
    ∀ (A B: Type), (A → B) → t A → t B.
  Hypothesis gmap1:
    ∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
    get i (map1 f m) = option_map f (get i m).

  Variable combine:
    ∀ (A B C: Type), (option A → option B → option C) → t A → t B → t C.
  Hypothesis gcombine:
    ∀ (A B C: Type) (f: option A → option B → option C),
    f None None = None →
    ∀ (m1: t A) (m2: t B) (i: elt),
    get i (combine f m1 m2) = f (get i m1) (get i m2).
  Hypothesis combine_commut:
    ∀ (A B: Type) (f g: option A → option A → option B),
    (∀ (i j: option A), f i j = g j i) →
    ∀ (m1 m2: t A),
    combine f m1 m2 = combine g m2 m1.

  Variable elements:
    ∀ (A: Type), t A → list (elt × A).
  Hypothesis elements_correct:
    ∀ (A: Type) (m: t A) (i: elt) (v: A),
    get i m = Some v → In (i, v) (elements m).
  Hypothesis elements_complete:
    ∀ (A: Type) (m: t A) (i: elt) (v: A),
    In (i, v) (elements m) → get i m = Some v.
  Hypothesis elements_keys_norepet:
    ∀ (A: Type) (m: t A),
    list_norepet (List.map (@fst elt A) (elements m)).

  Variable fold:
    ∀ (A B: Type), (B → elt → A → B) → t A → B → B.
  Hypothesis fold_spec:
    ∀ (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.

  Variable fold1:
    ∀ (A B: Type), (B → A → B) → t A → B → B.
  Hypothesis fold1_spec:
    ∀ (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.

Module Type MAP.
  Variable elt: Type.
  Variable elt_eq: ∀ (a b: elt), {a = b} + {a ≠ b}.
  Variable t: Type → Type.
  Variable init: ∀ (A: Type), A → t A.
  Variable get: ∀ (A: Type), elt → t A → A.
  Variable set: ∀ (A: Type), elt → A → t A → t A.
  Hypothesis gi:
    ∀ (A: Type) (i: elt) (x: A), get i (init x) = x.
  Hypothesis gss:
    ∀ (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
  Hypothesis gso:
    ∀ (A: Type) (i j: elt) (x: A) (m: t A),
    i ≠ j → get i (set j x m) = get i m.
  Hypothesis gsspec:
    ∀ (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.
  Hypothesis gsident:
    ∀ (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
  Variable map: ∀ (A B: Type), (A → B) → t A → t B.
  Hypothesis gmap:
    ∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
    get i (map f m) = f(get i m).
End MAP.

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

  Inductive tree (A : Type) : Type :=
    | Leaf : tree A
    | Node : tree A → option A → tree A → tree A.

  Implicit Arguments Leaf [A].
  Implicit Arguments Node [A].
  Scheme tree_ind := Induction for tree Sort Prop.

  Definition t := tree.

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

  Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
    match m with
    | Leaf ⇒ None
    | Node l o r ⇒
        match i with
        | xH ⇒ o
        | xO ii ⇒ get ii l
        | xI ii ⇒ get ii r
        end
    end.

  Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A :=
    match m with
    | Leaf ⇒
        match i with
        | xH ⇒ Node Leaf (Some v) Leaf
        | xO ii ⇒ Node (set ii v Leaf) None Leaf
        | xI ii ⇒ Node Leaf None (set ii v Leaf)
        end
    | Node l o r ⇒
        match i with
        | xH ⇒ Node l (Some v) r
        | xO ii ⇒ Node (set ii v l) o r
        | xI ii ⇒ Node l o (set ii v r)
        end
    end.

  Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A :=
    match i with
    | xH ⇒
        match m with
        | Leaf ⇒ Leaf
        | Node Leaf o Leaf ⇒ Leaf
        | Node l o r ⇒ Node l None r
        end
    | xO ii ⇒
        match m with
        | Leaf ⇒ Leaf
        | Node l None Leaf ⇒
            match remove ii l with
            | Leaf ⇒ Leaf
            | mm ⇒ Node mm None Leaf
            end
        | Node l o r ⇒ Node (remove ii l) o r
        end
    | xI ii ⇒
        match m with
        | Leaf ⇒ Leaf
        | Node Leaf None r ⇒
            match remove ii r with
            | Leaf ⇒ Leaf
            | mm ⇒ Node Leaf None mm
            end
        | Node l o r ⇒ Node l o (remove ii r)
        end
    end.

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

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

    Lemma gleaf : ∀ (A : Type) (i : positive), get i (Leaf : t A) = None.

  Theorem gso:
    ∀ (A: Type) (i j: positive) (x: A) (m: t A),
    i ≠ j → get i (set j x m) = get i m.

  Theorem gsspec:
    ∀ (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.

  Theorem gsident:
    ∀ (A: Type) (i: positive) (m: t A) (v: A),
    get i m = Some v → set i v m = m.

  Theorem set2:
    ∀ (A: Type) (i: elt) (m: t A) (v1 v2: A),
    set i v2 (set i v1 m) = set i v2 m.

  Lemma rleaf : ∀ (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.

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

  Theorem gro:
    ∀ (A: Type) (i j: positive) (m: t A),
    i ≠ j → get i (remove j m) = get i m.

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

  Section BOOLEAN_EQUALITY.

    Variable A: Type.
    Variable beqA: A → A → bool.

    Fixpoint bempty (m: t A) : bool :=
      match m with
      | Leaf ⇒ true
      | Node l None r ⇒ bempty l && bempty r
      | Node l (Some _) r ⇒ false
      end.

    Fixpoint beq (m1 m2: t A) {struct m1} : bool :=
      match m1, m2 with
      | Leaf, _ ⇒ bempty m2
      | _, Leaf ⇒ bempty m1
      | Node l1 o1 r1, Node l2 o2 r2 ⇒
          match o1, o2 with
          | None, None ⇒ true
          | Some y1, Some y2 ⇒ beqA y1 y2
          | _, _ ⇒ false
          end
          && beq l1 l2 && beq r1 r2
      end.

    Lemma bempty_correct:
      ∀ m, bempty m = true ↔ (∀ x, get x m = None).

    Lemma beq_correct:
      ∀ m1 m2,
      beq m1 m2 = true ↔
      (∀ (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.

    Fixpoint append (i j : positive) {struct i} : positive :=
      match i with
      | xH ⇒ j
      | xI ii ⇒ xI (append ii j)
      | xO ii ⇒ xO (append ii j)
      end.

    Lemma append_assoc_0 : ∀ (i j : positive),
                           append i (xO j) = append (append i (xO xH)) j.

    Lemma append_assoc_1 : ∀ (i j : positive),
                           append i (xI j) = append (append i (xI xH)) j.

    Lemma append_neutral_r : ∀ (i : positive), append i xH = i.

    Lemma append_neutral_l : ∀ (i : positive), append xH i = i.

    Fixpoint xmap (A B : Type) (f : positive → A → B) (m : t A) (i : positive)
             {struct m} : t B :=
      match m with
      | Leaf ⇒ Leaf
      | Node l o r ⇒ Node (xmap f l (append i (xO xH)))
                           (option_map (f i) o)
                           (xmap f r (append i (xI xH)))
      end.

  Definition map (A B : Type) (f : positive → A → B) m := xmap f m xH.

    Lemma xgmap:
      ∀ (A B: Type) (f: positive → A → B) (i j : positive) (m: t A),
      get i (xmap f m j) = option_map (f (append j i)) (get i m).

  Theorem gmap:
    ∀ (A B: Type) (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: Type) (f: A → B) (m: t A) {struct m} : t B :=
    match m with
    | Leaf ⇒ Leaf
    | Node l o r ⇒ Node (map1 f l) (option_map f o) (map1 f r)
    end.

  Theorem gmap1:
    ∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
    get i (map1 f m) = option_map f (get i m).

  Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A :=
    match l, x, r with
    | Leaf, None, Leaf ⇒ Leaf
    | _, _, _ ⇒ Node l x r
    end.

  Lemma gnode':
    ∀ (A: Type) (l r: t A) (x: option A) (i: positive),
    get i (Node' l x r) = get i (Node l x r).

  Fixpoint filter1 (A: Type) (pred: A → bool) (m: t A) {struct m} : t A :=
    match m with
    | Leaf ⇒ Leaf
    | Node l o r ⇒
        let o' := match o with None ⇒ None | Some x ⇒ if pred x then o else None end in
        Node' (filter1 pred l) o' (filter1 pred r)
    end.

  Theorem gfilter1:
    ∀ (A: Type) (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.

  Section COMBINE.

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

  Fixpoint xcombine_l (m : t A) {struct m} : t C :=
      match m with
      | Leaf ⇒ Leaf
      | Node l o r ⇒ Node' (xcombine_l l) (f o None) (xcombine_l r)
      end.

  Lemma xgcombine_l :
          ∀ (m: t A) (i : positive),
          get i (xcombine_l m) = f (get i m) None.

  Fixpoint xcombine_r (m : t B) {struct m} : t C :=
      match m with
      | Leaf ⇒ Leaf
      | Node l o r ⇒ Node' (xcombine_r l) (f None o) (xcombine_r r)
      end.

  Lemma xgcombine_r :
          ∀ (m: t B) (i : positive),
          get i (xcombine_r m) = f None (get i m).

  Fixpoint combine (m1: t A) (m2: t B) {struct m1} : t C :=
    match m1 with
    | Leaf ⇒ xcombine_r m2
    | Node l1 o1 r1 ⇒
        match m2 with
        | Leaf ⇒ xcombine_l m1
        | Node l2 o2 r2 ⇒ Node' (combine l1 l2) (f o1 o2) (combine r1 r2)
        end
    end.

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

  End COMBINE.

  Lemma xcombine_lr :
    ∀ (A B: Type) (f g : option A → option A → option B) (m : t A),
    (∀ (i j : option A), f i j = g j i) →
    xcombine_l f m = xcombine_r g m.

  Theorem combine_commut:
    ∀ (A B: Type) (f g: option A → option A → option B),
    (∀ (i j: option A), f i j = g j i) →
    ∀ (m1 m2: t A),
    combine f m1 m2 = combine g m2 m1.

    Fixpoint xelements (A : Type) (m : t A) (i : positive)
                       (k: list (positive × A)) {struct m}
                       : list (positive × A) :=
      match m with
      | Leaf ⇒ k
      | Node l None r ⇒
          xelements l (append i (xO xH)) (xelements r (append i (xI xH)) k)
      | Node l (Some x) r ⇒
          xelements l (append i (xO xH))
            ((i, x) :: xelements r (append i (xI xH)) k)
      end.

  Definition elements (A: Type) (m : t A) := xelements m xH nil.

    Lemma xelements_incl:
      ∀ (A: Type) (m: t A) (i : positive) k x,
      In x k → In x (xelements m i k).

    Lemma xelements_correct:
      ∀ (A: Type) (m: t A) (i j : positive) (v: A) k,
      get i m = Some v → In (append j i, v) (xelements m j k).

  Theorem elements_correct:
    ∀ (A: Type) (m: t A) (i: positive) (v: A),
    get i m = Some v → In (i, v) (elements m).

    Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=
      match i, j with
      | _, xH ⇒ get i m
      | xO ii, xO jj ⇒ xget ii jj m
      | xI ii, xI jj ⇒ xget ii jj m
      | _, _ ⇒ None
      end.

    Lemma xget_diag :
      ∀ (A : Type) (i : positive) (m1 m2 : t A) (o : option A),
      xget i i (Node m1 o m2) = o.

    Lemma xget_left :
      ∀ (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
      xget i (append j (xO xH)) m1 = Some v → xget i j (Node m1 o m2) = Some v.

    Lemma xget_right :
      ∀ (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
      xget i (append j (xI xH)) m2 = Some v → xget i j (Node m1 o m2) = Some v.

    Lemma xelements_complete:
      ∀ (A: Type) (m: t A) (i j : positive) (v: A) k,
      In (i, v) (xelements m j k) → xget i j m = Some v ∨ In (i, v) k.

    Lemma get_xget_h :
      ∀ (A: Type) (m: t A) (i: positive), get i m = xget i xH m.

  Theorem elements_complete:
    ∀ (A: Type) (m: t A) (i: positive) (v: A),
    In (i, v) (elements m) → get i m = Some v.

  Lemma in_xelements:
    ∀ (A: Type) (m: t A) (i k: positive) (v: A) l,
    In (k, v) (xelements m i l) →
    (∃ j, k = append i j) ∨ In (k, v) l.

  Definition xkeys (A: Type) (m: t A) (i: positive) (l: list (positive × A)) :=
    List.map (@fst positive A) (xelements m i l).

  Lemma in_xkeys:
    ∀ (A: Type) (m: t A) (i k: positive) l,
    In k (xkeys m i l) →
    (∃ j, k = append i j) ∨ In k (List.map fst l).

  Lemma append_injective:
    ∀ i j1 j2, append i j1 = append i j2 → j1 = j2.

  Lemma xelements_keys_norepet:
    ∀ (A: Type) (m: t A) (i: positive) l,
    (∀ k v, get k m = Some v → ¬In (append i k) (List.map fst l)) →
    list_norepet (List.map fst l) →
    list_norepet (xkeys m i l).

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

  Remark xelements_empty:
    ∀ (A: Type) (m: t A) i l, (∀ i, get i m = None) → xelements m i l = l.

  Theorem elements_canonical_order:
    ∀ (A B: Type) (R: A → B → Prop) (m: t A) (n: t B),
    (∀ i x, get i m = Some x → ∃ y, get i n = Some y ∧ R x y) →
    (∀ i y, get i n = Some y → ∃ 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:
    ∀ (A: Type) (m n: t A),
    (∀ i, get i m = get i n) →
    elements m = elements n.

  Fixpoint xfold (A B: Type) (f: B → positive → A → B)
                 (i: positive) (m: t A) (v: B) {struct m} : B :=
    match m with
    | Leaf ⇒ v
    | Node l None r ⇒
        let v1 := xfold f (append i (xO xH)) l v in
        xfold f (append i (xI xH)) r v1
    | Node l (Some x) r ⇒
        let v1 := xfold f (append i (xO xH)) l v in
        let v2 := f v1 i x in
        xfold f (append i (xI xH)) r v2
    end.

  Definition fold (A B : Type) (f: B → positive → A → B) (m: t A) (v: B) :=
    xfold f xH m v.

  Lemma xfold_xelements:
    ∀ (A B: Type) (f: B → positive → A → B) m i v l,
    List.fold_left (fun a p ⇒ f a (fst p) (snd p)) l (xfold f i m v) =
    List.fold_left (fun a p ⇒ f a (fst p) (snd p)) (xelements m i l) v.

  Theorem fold_spec:
    ∀ (A B: Type) (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: Type) (f: B → A → B) (m: t A) (v: B) {struct m} : B :=
    match m with
    | Leaf ⇒ v
    | Node l None r ⇒
        let v1 := fold1 f l v in
        fold1 f r v1
    | Node l (Some x) r ⇒
        let v1 := fold1 f l v in
        let v2 := f v1 x in
        fold1 f r v2
    end.

  Lemma fold1_xelements:
    ∀ (A B: Type) (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:
    ∀ (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 PTree.

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:
    ∀ (A: Type) (i: positive) (x: A), get i (init x) = x.

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

  Theorem gso:
    ∀ (A: Type) (i j: positive) (x: A) (m: t A),
    i ≠ j → get i (set j x m) = get i m.

  Theorem gsspec:
    ∀ (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:
    ∀ (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:
    ∀ (A B: Type) (f: A → B) (i: positive) (m: t A),
    get i (map f m) = f(get i m).

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

End PMap.

Module Type INDEXED_TYPE.
  Variable t: Type.
  Variable index: t → positive.
  Hypothesis index_inj: ∀ (x y: t), index x = index y → x = y.
  Variable eq: ∀ (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:
    ∀ (A: Type) (x: A) (i: X.t), get i (init x) = x.

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

  Lemma gso:
    ∀ (A: Type) (i j: X.t) (x: A) (m: t A),
    i ≠ j → get i (set j x m) = get i m.

  Lemma gsspec:
    ∀ (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:
    ∀ (A B: Type) (f: A → B) (i: X.t) (m: t A),
    get i (map f m) = f(get i m).

  Lemma set2:
    ∀ (A: Type) (i: elt) (x y: A) (m: t A),
    set i y (set i x m) = set i 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: ∀ (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: ∀ (x y: N), index x = index y → x = y.
  Lemma eq: ∀ (x y: N), {x = y} + {x ≠ y}.
End NIndexed.

Module NMap := IMap(NIndexed).

Module Type EQUALITY_TYPE.
  Variable t: Type.
  Variable eq: ∀ (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:
    ∀ (A: Type) (i: elt) (x: A), init x i = x.
  Lemma gss:
    ∀ (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.
  Lemma gso:
    ∀ (A: Type) (i j: elt) (x: A) (m: t A),
    i ≠ j → (set j x m) i = m i.
  Lemma gsspec:
    ∀ (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:
    ∀ (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:
    ∀ (A B: Type) (f: A → B) (i: elt) (m: t A),
    get i (map f m) = f(get i m).
End EMap.

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 → Prop.
Variable init: A.
Variable m_final: T.t V.

Hypothesis P_compat:
  ∀ m m' a,
  (∀ 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:
  ∀ 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).

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

Let P' (l: list (T.elt × V)) (a: A) : Prop :=
  ∀ m, list_equiv l (T.elements m) → P m a.

Remark H_base':
  P' nil init.

Remark H_rec':
  ∀ k v l a,
  ¬In k (List.map (@fst T.elt V) l) →
  In (k, v) (T.elements m_final) →
  P' l a →
  P' (l ++ (k, v) :: nil) (f a k v).

Lemma fold_rec_aux:
  ∀ l1 l2 a,
  list_equiv (l2 ++ l1) (T.elements m_final) →
  list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) →
  list_norepet (List.map (@fst T.elt V) l1) →
  P' l2 a → P' (l2 ++ l1) (List.fold_left f' l1 a).

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

End TREE_FOLD_IND.

Section MEASURE.

Variable V: Type.

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

Remark list_incl_length:
  ∀ (A: Type) (l1: list A), list_norepet l1 →
  ∀ (l2: list A), List.incl l1 l2 → (List.length l1 ≤ List.length l2)%nat.

Remark list_length_incl:
  ∀ (A: Type) (l1: list A), list_norepet l1 →
  ∀ l2, List.incl l1 l2 → List.length l1 = List.length l2 → List.incl l2 l1.

Remark list_strict_incl_length:
  ∀ (A: Type) (l1 l2: list A) (x: A),
  list_norepet l1 → List.incl l1 l2 → ¬In x l1 → In x l2 →
  (List.length l1 < List.length l2)%nat.

Remark list_norepet_map:
  ∀ (A B: Type) (f: A → B) (l: list A),
  list_norepet (List.map f l) → list_norepet l.

Theorem cardinal_remove:
  ∀ x m y, T.get x m = Some y → (cardinal (T.remove x m) < cardinal m)%nat.

End MEASURE.