Module Hash


Require Import ZArith NArith FastArith.
Require Import Recdef AdomLib Util ShareTree.
Require Import AST Coqlib Utf8.
Require Axioms.

Local Open Scope N_scope.

Class hashable (T:Type) := hash : Nfast -> T -> Nfast.

Definition max_uint32 : Nfast := 4294967295.

Definition MIX (h d:Nfast) : Nfast :=
  let h := Nfastadd h d in
  let h := Nfastland max_uint32 (Nfastadd h (Nfastshl h F10)) in
  let h := Nfastlxor h (Nfastshr h F6) in
  h.

Definition final_MIX (h:Nfast) : Nfast :=
  let h := Nfastland max_uint32 (Nfastadd h (Nfastshl h F3)) in
  let h := Nfastlxor h (Nfastshr h F11) in
  let h := Nfastland max_uint32 (Nfastadd h (Nfastshl h F15)) in
  h.

Function split_N (n:Nfast) (sz_acc:Nfast) (lst_acc:list Nfast) {measure N.to_nat n}
  : list Nfast * Nfast :=
  if Nfasteqb n F0 then (lst_acc, sz_acc)
  else split_N (Nfastshr n F8) (Nfastadd sz_acc F1) ((Nfastland n F255)::lst_acc).
Proof.
  intros. fastunwrap.
  cut (N.shiftr n 8 < n). simpl in *; Psatz.lia.
  rewrite N.shiftr_div_pow2.
  change (2 ^ 8)%N with 256%N.
  pose proof N.div_mod' n 256. apply N.eqb_neq in teq. Psatz.lia.
Qed.

Instance hash_N : hashable Nfast := fun (h n:Nfast) =>
  let '(l, sz) := split_N n F0 nil in
  List.fold_left MIX l (MIX h sz).

Instance hash_Z : hashable Zfast := fun (h:Nfast) (z:Zfast) =>
  if Zfastleb (F0) z then hash h (Nfast_of_Zfast (Zfastadd z z))
  else hash h (Nfast_of_Zfast (Zfastsub Fm1 (Zfastadd z z))).

Instance hash_ident : hashable ident :=
  fun h (i:ident) => hash h (N.pos i:Nfast).

Module Type Hashable.

  Parameter t : Type.
  Declare Instance eq : EqDec t.
  Declare Instance hash : hashable t.

  Parameter bits : Nfast.

End Hashable.

Module Hashtable(H:Hashable) <: SHARETREE.
  Import PShareTree.

  Definition elt := H.t.
  Definition elt_eq := H.eq.

  Definition mask : Nfast := Nfastones H.bits.

  Definition hash (x:elt) : positive :=
    N.succ_pos (Nfastland mask (final_MIX (hash F12 x))).

  Definition t (val:Type) :=
    { t : PShareTree.t (list (elt * val)) |
      forall h l, PShareTree.get h t = Some l ->
                  l <> nil /\
                  list_norepet (List.map fst l) /\
                  List.Forall (fun k => h = hash k) (List.map fst l) }.

  Lemma in_map_fst:
    forall val (l:list (elt * val)) k v,
      In (k, v) l -> In k (List.map fst l).
Proof.
intros. eapply in_map with (f:=fst) in H. auto. Qed.

  Lemma in_map_iff_fst:
    forall val (l:list (elt * val)) k,
      In k (List.map fst l) <-> ∃ v, In (k, v) l.
Proof.
    intros. rewrite in_map_iff. split.
    intros [[] [<- ?]]. eauto. intros [? ?]. eexists (k, x). auto.
  Qed.

  Program Definition empty val : t val := PShareTree.empty _.
Next Obligation.
rewrite PShareTree.gempty in H. discriminate. Qed.

  Definition get_lst {val:Type} (h:positive) (htbl:t val) : list (elt * val) :=
    match PShareTree.get h (proj1_sig htbl) with
      | None => nil
      | Some l => l
    end.

  Lemma get_lst_inv:
    forall val h (htbl:t val),
      let l := get_lst (val:=val) h htbl in
      list_norepet (List.map fst l) /\
      List.Forall (fun k => h = hash k) (List.map fst l).
Proof.
    unfold get_lst. intros. destruct htbl. simpl. specialize (a h).
    destruct get. specialize (a _ eq_refl); now intuition.
    split. constructor. constructor.
  Qed.

  Fixpoint extract_witness {val:Type} k (l:list (elt * val)) :=
    match l with
      | nil => (None, nil)
      | (k', v2) as t::q =>
        if eq_dec k k' then (Some v2, q)
        else match extract_witness k q with
               | (None, _) => (None, l)
               | (o, q) => (o, t::q)
             end
    end.

  Lemma extract_witness_spec:
    forall val k (l:list (elt * val)),
      list_norepet (List.map fst l) ->
      match extract_witness k l with
        | (None, l') =>
          l = l' /\ ~In k (List.map fst l)
        | (Some v, l') =>
          In (k, v) l /\
          list_norepet (List.map fst l') /\
          (forall k' v', In (k', v') l' <-> (k' <> k /\ In (k', v') l))
      end.
Proof.
    induction l as [|[]]; simpl. auto.
    intro. inv H. destruct eq_dec.
    - subst. split. auto. split. auto. split.
      intro. pose proof H. apply in_map_fst in H0. now intuition congruence.
      simpl. now intuition congruence.
    - specialize (IHl H3). destruct (extract_witness k l) as [[] ?].
      + simpl. split. now intuition. split.
        * constructor. 2:now intuition. rewrite in_map_iff_fst. intros [v'].
          rewrite (proj2 (proj2 IHl)). intros [_ ?]. apply in_map_fst in H. auto.
        * intros. rewrite (proj2 (proj2 IHl)). now intuition congruence.
      + now intuition.
  Qed.

  Lemma extract_witness_norepet:
    forall val k (l:list (elt * val)),
      list_norepet (List.map fst l) ->
      list_norepet (List.map fst (snd (extract_witness k l))).
Proof.
    intros. pose proof H. apply extract_witness_spec with (k:=k) in H.
    destruct (extract_witness k l) as [[] ?]. simpl. now intuition.
    simpl. now intuition congruence.
  Qed.

  Lemma extract_witness_fstIn:
    forall val k (l:list (elt * val)),
      list_norepet (List.map fst l) ->
      forall k',
        In k' (List.map fst (snd (extract_witness k l))) <->
        (k' <> k /\ In k' (List.map fst l)).
Proof.
    intros. pose proof H. apply extract_witness_spec with (k:=k) in H.
    destruct (extract_witness k l) as [[] ?].
    - simpl. rewrite !in_map_iff_fst. setoid_rewrite (proj2 (proj2 H)). firstorder.
    - simpl. now intuition congruence.
  Qed.

  Fixpoint assoc {val:Type} k (l:list (elt * val)) : option val :=
    match l with
      | nil => None
      | (k', v2) as t::q =>
        if eq_dec k k' then Some v2
        else assoc k q
    end.

  Lemma extract_witness_assoc:
    forall val k (l:list (elt * val)), fst (extract_witness k l) = assoc k l.
Proof.
    induction l as [|[]]. auto.
    simpl. destruct eq_dec. auto. destruct (extract_witness k l) as [[]?]; auto.
  Qed.

  Lemma assoc_spec:
    forall val k (l:list (elt * val)),
      list_norepet (List.map fst l) ->
    forall ov, assoc k l = ov <->
               match ov with
                 | None => ~In k (List.map fst l)
                 | Some v => In (k, v) l
               end.
Proof.
    intros. induction l as [|[]]. simpl. destruct ov; now intuition congruence. inv H.
    simpl. destruct eq_dec.
    subst. split.
    intro. subst. auto. destruct ov. intros [|?]. congruence. destruct H2. eapply in_map_fst. eauto.
    intuition congruence.
    rewrite IHl. 2:auto. destruct ov; intuition congruence.
  Qed.

  Lemma assoc_extract_witness:
    forall val i j (l:list (elt * val)),
      list_norepet (List.map fst l) ->
      assoc i (snd (extract_witness j l)) =
      if eq_dec i j then None else assoc i l.
Proof.
    intros.
    pose proof (extract_witness_norepet _ j l H).
    pose proof (extract_witness_spec _ j l H).
    destruct @extract_witness as [[] ?], eq_dec; subst; simpl in *;
    repeat match goal with H : _ /\ _ |- _ => destruct H end; auto.
    - rewrite assoc_spec, in_map_iff_fst by auto. setoid_rewrite H3. firstorder.
    - rewrite assoc_spec by auto. destruct (assoc i l) eqn:EQ; rewrite assoc_spec in EQ by auto.
      firstorder. rewrite in_map_iff_fst in *. firstorder.
    - rewrite assoc_spec by auto. congruence.
    - congruence.
  Qed.

  Program Definition get {val:Type} (x:elt) (htbl:t val) : option val :=
    assoc x (get_lst (hash x) htbl).

  Lemma gempty:
    forall val i, get i (empty val) = None.
Proof.
    intros. unfold get, empty, get_lst. simpl. rewrite PShareTree.gempty. auto.
  Qed.

  Program Definition set {val:Type} (k:elt) (v:val) (htbl:t val) : t val :=
    let '(o, s) := PShareTree.get_set (hash k) htbl return PShareTree.t _ in
    let q := snd (extract_witness k match o return _ with None => nil | Some l => l end) in
    s ((k, v)::q).
Next Obligation.
    destruct (PShareTree.get_set_spec (hash k) (proj1_sig htbl)).
    rewrite (surjective_pairing (get_set (hash k) (proj1_sig htbl))), H0, H1, PShareTree.gsspec in H.
    destruct (peq h (hash k)).
    - inv H. split. discriminate. simpl. split; constructor.
      + rewrite extract_witness_fstIn. now intuition. apply get_lst_inv.
      + apply extract_witness_norepet, get_lst_inv.
      + auto.
      + apply Forall_forall. intros.
        apply extract_witness_fstIn in H. 2:apply get_lst_inv.
        destruct (get_lst_inv _ (hash k) htbl). rewrite Forall_forall in H3. now intuition.
    - apply (proj2_sig htbl). auto.
  Qed.

  Lemma gss:
    forall val i x (htbl:t val), get i (set i x htbl) = Some x.
Proof.
    intros. unfold get, get_lst, set. simpl.
    destruct (get_set_spec (hash i) (proj1_sig htbl)).
    rewrite (surjective_pairing (get_set (hash i) (proj1_sig htbl))), H0, PShareTree.gss.
    simpl. destruct eq_dec. auto. congruence.
  Qed.

  Lemma gso:
    forall val (i j: elt) (x: val) (htbl: t val),
      i <> j -> get i (set j x htbl) = get i htbl.
Proof.
    intros. unfold get, get_lst at 1, set. simpl.
    destruct (get_set_spec (hash j) (proj1_sig htbl)).
    rewrite (surjective_pairing (get_set (hash j) (proj1_sig htbl))), H1, PShareTree.gsspec.
    destruct peq. 2:auto. simpl. destruct eq_dec. easy.
    rewrite H0, assoc_extract_witness by apply get_lst_inv.
    destruct (eq_dec i j). congruence. rewrite e. auto.
  Qed.

  Lemma gsspec:
    forall val i j (x: val) (m: t val),
    get i (set j x m) = if eq_dec i j then Some x else get i m.
Proof.
    intros. destruct elt_eq. subst. apply gss. apply gso. auto.
  Qed.

  Fixpoint remove_rec {val : Type} (i : positive) (k:elt) (m:PShareTree.t _) {struct i} :=
    match i return PShareTree.t (list (elt * val)) with
    | xH =>
        match m with
        | Leaf => Leaf
        | Node l None r => Node l None r
        | Node l ((Some lst) as o) r =>
          match extract_witness k lst with
            | (_, nil) => match l, r with
                            | Leaf, Leaf => Leaf
                            | _, _ => Node l None r
                          end
            | (_, lst) => Node l (Some lst) r
          end
        end
    | xO ii =>
        match m with
        | Leaf => Leaf

        | Node l None Leaf =>
            match remove_rec ii k l with
            | Leaf => Leaf
            | mm => Node mm None Leaf
            end
        | Node l o r => Node (remove_rec ii k l) o r
        end
    | xI ii =>
        match m with
        | Leaf => Leaf
        | Node Leaf None r =>
            match remove_rec ii k r with
            | Leaf => Leaf
            | mm => Node Leaf None mm
            end
        | Node l o r => Node l o (remove_rec ii k r)
        end
    end.

  Lemma grs_impl:
    forall val i k m,
      PShareTree.get i (remove_rec i k (proj1_sig m)) =
      match extract_witness k (get_lst i m) with
        | (_, nil) => @None (list (elt * val))
        | (_, lst) => Some lst
      end.
Proof.
    unfold get_lst. intros.
    generalize (proj1_sig m). clear m.
    induction i; destruct t0; simpl; auto.
    - rewrite <- IHi. destruct t0_1, o, (remove_rec i k t0_2); auto.
      rewrite PShareTree.gleaf. auto.
    - rewrite <- IHi. destruct o, t0_2, (remove_rec i k t0_1); auto.
      rewrite PShareTree.gleaf. auto.
    - destruct o, t0_1, t0_2; auto; destruct @extract_witness as [? []]; auto.
  Qed.

  Lemma gro_impl:
    forall val i j k m, i <> j ->
      PShareTree.get i (remove_rec (val:=val) j k m) = PShareTree.get i m.
Proof.
    induction i; destruct j, m; simpl; auto.
    - intro. assert (i <> j) by congruence.
      specialize (IHi _ k m2 H0).
      destruct m1; auto. destruct o; auto. destruct (remove_rec j k m2); auto.
      erewrite <- PShareTree.gleaf. eauto.
    - destruct o; auto. destruct m2; auto. destruct (remove_rec j k m1); auto.
      intro. rewrite PShareTree.gleaf. auto.
    - destruct o; auto. destruct @extract_witness as [? []]; auto. destruct m1, m2; auto.
      intro. rewrite PShareTree.gleaf. auto.
    - destruct m1; auto. destruct o; auto. destruct (remove_rec j k m2); auto.
      intro. rewrite PShareTree.gleaf. auto.
    - intro. assert (i <> j) by congruence.
      specialize (IHi _ k m1 H0).
      destruct o; auto. destruct m2; auto. destruct (remove_rec j k m1); auto.
      erewrite <- PShareTree.gleaf. eauto.
    - destruct o; auto. destruct @extract_witness as [? []]; auto. destruct m1, m2; auto.
      intro. rewrite PShareTree.gleaf. auto.
    - destruct m1; auto. destruct o; auto. destruct (remove_rec j k m2); auto.
    - destruct o; auto. destruct m2; auto. destruct (remove_rec j k m1); auto.
    - congruence.
  Qed.

  Program Definition remove {val:Type} (k:elt) (htbl:t val) : t val :=
    remove_rec (hash k) k htbl.
Next Obligation.
    destruct (eq_dec h (hash k)).
    - subst. rewrite grs_impl in H.
      assert (l = snd (extract_witness k (get_lst (hash k) htbl))).
      { destruct @extract_witness as [? []]. discriminate. simpl. congruence. }
      split.
      + destruct @extract_witness as [? []]; simpl in *; congruence.
      + subst l. clear H.
        split. apply extract_witness_norepet, get_lst_inv.
        apply Forall_forall. intros. rewrite extract_witness_fstIn in H.
        2:apply get_lst_inv. apply proj2 in H. eapply Forall_forall in H. 2:apply get_lst_inv. auto.
    - rewrite gro_impl in H by auto. eapply (proj2_sig htbl). eauto.
  Qed.

  Lemma grs_impl':
    forall val k m,
      get_lst (val:=val) (hash k) (remove k m) = snd (extract_witness k (get_lst (hash k) m)).
Proof.
    unfold get_lst at 1, remove. simpl. intros. rewrite grs_impl.
    destruct @extract_witness as [? []]; auto.
  Qed.

  Lemma grs:
    forall val i (m:t val), get i (remove i m) = None.
Proof.
    unfold get. intros. rewrite grs_impl'.
    rewrite assoc_extract_witness by apply get_lst_inv. destruct eq_dec; congruence.
  Qed.

  Lemma gro:
    forall val i j (m:t val), i <> j -> get i (remove j m) = get i m.
Proof.
    unfold get. intros. destruct (eq_dec (hash i) (hash j)).
    - rewrite e, grs_impl', assoc_extract_witness by apply get_lst_inv. destruct eq_dec; easy.
    - unfold get_lst, remove. simpl. rewrite gro_impl; auto.
  Qed.

  Lemma grspec:
    forall val i j (m: t val),
      get i (remove j m) = if eq_dec i j then None else get i m.
Proof.
    intros. destruct eq_dec. subst. apply grs. apply gro. auto.
  Qed.

  Program Definition get_set {val:Type} (k:elt) (htbl:t val) : option val * (val -> t val) :=
    let '(o, s) := PShareTree.get_set (hash k) htbl in
    let '(o, l) := extract_witness k match o return _ with None => nil | Some l => l end in
    (o, fun v => s ((k, v)::l)).
Next Obligation.
    destruct (PShareTree.get_set_spec (hash k) (proj1_sig htbl)).
    rewrite <- Heq_anonymous in H1, H0. simpl in *.
    rewrite H1, PShareTree.gsspec in H. subst o. clear s H1 Heq_anonymous.
    destruct (peq h (hash k)).
    - assert (l = snd (o0, l)) by reflexivity. rewrite Heq_anonymous0 in H0.
      clear Heq_anonymous0 o0. inv H. split. discriminate. simpl. split; constructor.
      + rewrite extract_witness_fstIn. now intuition. apply get_lst_inv.
      + apply extract_witness_norepet, get_lst_inv.
      + auto.
      + apply Forall_forall. intros.
        apply extract_witness_fstIn in H. 2:apply get_lst_inv.
        destruct (get_lst_inv _ (hash k) htbl). rewrite Forall_forall in H1. now intuition.
    - apply (proj2_sig htbl). auto.
  Qed.

  Lemma get_set_spec:
    forall (val: Type) (i:elt) (m:t val),
      fst (get_set i m) = get i m /\
      forall v, snd (get_set i m) v = set i v m.
Proof.
    intros. unfold get_set. generalize (get_set_obligation_1 val i m) as OBL.
    destruct (PShareTree.get_set_spec (hash i) (proj1_sig m)).
    destruct (PShareTree.get_set (hash i) (proj1_sig m)). simpl in H, H0 |- *. subst o.
    intros. generalize (OBL (PShareTree.get (hash i) (proj1_sig m)) t0 eq_refl) as OBL'. clear OBL.
    destruct (extract_witness i match PShareTree.get (hash i) (proj1_sig m) with
                                 | Some l0 => l0
                                 | None => nil
                                end)
             eqn:EQ.
    simpl. split.
    - unfold get. rewrite <- extract_witness_assoc.
      unfold get_lst. rewrite EQ. auto.
    - assert (forall (m1 m2:t val), proj1_sig m1 = proj1_sig m2 -> m1 = m2).
      { intros. destruct m1, m2. simpl in *. subst. f_equal. apply Axioms.proof_irr. }
      intros. apply H. unfold set. simpl.
      destruct (PShareTree.get_set_spec (hash i) (proj1_sig m)). destruct @PShareTree.get_set.
      simpl in *. rewrite H0, H1, H2, EQ. auto.
  Qed.

  Fixpoint combine_lists_r {val1 val2 val3:Type} (comb:option val1 -> option val2 -> option val3)
           (l:list (elt*val2)) : list (elt * val3) :=
    match l with
      | nil => nil
      | (k, v2)::q =>
        match comb None (Some v2) with
          | None => combine_lists_r comb q
          | Some v => (k, v)::combine_lists_r comb q
        end
    end.

  Lemma combine_lists_r_In:
    forall k val1 val2 val3 comb (l:list (elt*val2)),
      list_norepet (List.map fst l) ->
      In k (List.map fst (combine_lists_r (val1:=val1) (val3:=val3) comb l)) ->
      In k (List.map fst l).
Proof.
    induction l as [?|[]]. easy.
    simpl. intros. inv H. destruct (comb None (Some v)); simpl in *; now intuition.
  Qed.

  Lemma combine_lists_r_norepet:
    forall val1 val2 val3 comb (l:list (elt*val2)),
      list_norepet (List.map fst l) ->
      list_norepet (List.map fst (combine_lists_r (val1:=val1) (val3:=val3) comb l)).
Proof.
    induction l as [|[]]. auto. simpl.
    intros. inv H. destruct (comb None (Some v)). 2:auto. simpl. constructor. 2:auto.
    contradict H2. eapply combine_lists_r_In; eauto.
  Qed.

  Lemma combine_lists_r_ok:
    forall val1 val2 val3 comb (l:list (elt*val2)) k,
      list_norepet (List.map fst l) ->
      comb (@None val1) (@None val2) = (@None val3) ->
      assoc k (combine_lists_r comb l) = comb None (assoc k l).
Proof.
    intros. induction l as [|[]]. auto.
    pose proof combine_lists_r_norepet _ _ _ comb _ H.
    rewrite assoc_spec by (apply combine_lists_r_norepet; auto).
    simpl in *. inv H. specialize (IHl H5). destruct (eq_dec k e).
    - subst. destruct (comb None (Some v)). simpl. auto.
      contradict H4. eapply combine_lists_r_In; eauto.
    - rewrite assoc_spec in IHl by (apply combine_lists_r_norepet; auto).
      destruct (comb None (assoc k l)), (comb None (Some v)); simpl; now intuition.
  Qed.

  Fixpoint combine_lists {val1 val2 val3:Type} (comb:option val1 -> option val2 -> option val3)
           (l1:list (elt*val1)) (l2:list (elt*val2)) : list (elt*val3):=
    match l1 with
      | nil => combine_lists_r comb l2
      | (k, v1)::l1 =>
        let '(ov2, l2) := extract_witness k l2 in
        let q := combine_lists comb l1 l2 in
        match comb (Some v1) ov2 with
          | None => q
          | Some v => (k, v)::q
        end
    end.

  Lemma combine_lists_In:
    forall k val1 val2 val3 comb (l1:list (elt*val1)) (l2:list (elt*val2)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      In k (List.map fst (combine_lists (val3:=val3) comb l1 l2)) ->
      In k (List.map fst l1) \/ In k (List.map fst l2).
Proof.
    induction l1.
    + intros. right. eapply combine_lists_r_In; eauto.
    + destruct a. simpl. intros. inv H.
      pose proof (extract_witness_norepet _ e l2 H0).
      pose proof (extract_witness_fstIn _ e l2 H0).
      destruct (extract_witness e l2).
      destruct (comb (Some v) o). destruct H1. auto.
      specialize (IHl1 _ H5 H H1). destruct IHl1. auto. right. apply H2. auto.
      specialize (IHl1 _ H5 H H1). destruct IHl1. auto. right. apply H2. auto.
  Qed.

  Lemma combine_lists_norepet:
    forall val1 val2 val3 comb (l1:list (elt*val1)) (l2:list (elt*val2)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      list_norepet (List.map fst (combine_lists (val3:=val3) comb l1 l2)).
Proof.
    induction l1.
    - intros. apply combine_lists_r_norepet. auto.
    - destruct a. simpl. intros. inv H.
      pose proof (extract_witness_norepet _ e l2 H0).
      pose proof (extract_witness_fstIn _ e l2 H0).
      destruct (extract_witness e l2).
      destruct (comb (Some v) o); auto. simpl. constructor; auto.
      intro. apply combine_lists_In in H2; auto. destruct H2. now intuition.
      apply H1 in H2. now intuition.
  Qed.

  Lemma combine_lists_ok:
    forall val1 val2 val3 comb (l1:list (elt*val1)) (l2:list (elt*val2)) k,
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      comb None None = (@None val3) ->
      assoc k (combine_lists comb l1 l2) = comb (assoc k l1) (assoc k l2).
Proof.
    intros. revert l2 H0. induction l1 as [|[]]; intros.
    - apply combine_lists_r_ok. auto. auto.
    - rewrite assoc_spec by (apply combine_lists_norepet; auto).
      inv H. simpl.
      rewrite (surjective_pairing (extract_witness e l2)), extract_witness_assoc.
      refine (let H := IHl1 H5 (snd (extract_witness e l2)) _ in _ ); clear IHl1.
      apply extract_witness_norepet. auto.
      rewrite assoc_spec, assoc_extract_witness in H
        by (auto using combine_lists_norepet, extract_witness_norepet).
      destruct (eq_dec k e); simpl in *; subst.
       + destruct (comb (Some v) (assoc e l2)). simpl. auto.
         contradict H4. apply combine_lists_In in H4.
         rewrite extract_witness_fstIn in H4. intuition. auto. auto.
         apply extract_witness_norepet. auto.
       + destruct (comb (assoc k l1) (assoc k l2)), (comb (Some v) (assoc e l2)); simpl; intuition.
  Qed.

  Program Definition beq {val: Type} (eq:val -> val -> bool)
          (m1:t val) (m2:t val) : bool :=
    PShareTree.beq (fun l1 l2 =>
                      match combine_lists (fun ov1 ov2 =>
                                             match ov1, ov2 return _ with
                                               | Some v1, Some v2 =>
                                                 if eq v1 v2 then None else Some tt
                                               | None, None => None
                                               | _, _ => Some tt
                                             end) l1 l2
                      return _ with nil => true | _ => false end) m1 m2.

  Lemma beq_correct:
    forall val eq (t1 t2: t val),
      beq eq t1 t2 = true <->
      (forall x,
         match get x t1, get x t2 with
           | None, None => True
           | Some y1, Some y2 => eq y1 y2 = true
           | _, _ => False
         end).
Proof.
    unfold beq. intros. rewrite PShareTree.beq_correct. split.
    - intros. unfold get, get_lst. specialize (H (hash x)).
      destruct (PShareTree.get (hash x) (proj1_sig t1)) eqn:EQ1,
               (PShareTree.get (hash x) (proj1_sig t2)) eqn:EQ2; try easy.
      apply (proj2_sig t1) in EQ1. apply (proj2_sig t2) in EQ2. destruct EQ1 as [_ []], EQ2 as [_ []].
      match type of H with
        | context [combine_lists ?comb l l0] =>
          pose proof (combine_lists_ok _ _ _ comb l l0 x H0 H2 eq_refl)
      end.
      destruct @combine_lists. 2:discriminate.
      destruct (assoc x l), (assoc x l0); try easy.
      destruct (eq v v0). auto. discriminate.
    - unfold get, get_lst. intros.
      destruct (PShareTree.get x (proj1_sig t1)) eqn:EQ1,
               (PShareTree.get x (proj1_sig t2)) eqn:EQ2;
        try (pose proof EQ1; apply (proj2_sig t1) in EQ1; destruct EQ1 as [? []]);
        try (pose proof EQ2; apply (proj2_sig t2) in EQ2; destruct EQ2 as [? []]).
      + match goal with
          | |- context [combine_lists ?comb l l0] =>
            pose proof combine_lists_ok _ _ _ comb l l0
        end.
        destruct @combine_lists as [|[]]. auto. specialize (H8 e H2 H6 eq_refl).
        simpl in H8. destruct (eq_dec e e). 2:congruence.
        assert (hash e = x).
        { pose proof assoc_spec _ e l H2 (assoc e l). pose proof assoc_spec _ e l0 H6 (assoc e l0).
          destruct (assoc e l). 2:destruct (assoc e l0).
          - eapply Forall_forall in H3. eauto. eapply in_map_fst, H9, eq_refl.
          - eapply Forall_forall in H7. eauto. eapply in_map_fst, H10, eq_refl.
          - discriminate. }
        specialize (H e). rewrite H9, H0, H4 in H.
        destruct @assoc, @assoc. rewrite H in H8. discriminate. easy. easy. discriminate.
      + destruct l as [|[]]. auto. simpl in H3. inv H3. specialize (H e).
        rewrite EQ2, H0 in H. simpl in H. destruct (eq_dec e e); auto.
      + destruct l as [|[]]. auto. simpl in H3. inv H3. specialize (H e).
        rewrite EQ1, H0 in H. simpl in H. destruct (eq_dec e e); auto.
      + auto.
  Qed.

  Program Definition combine {val1 val2 val3: Type} (comb:option val1 -> option val2 -> option val3)
             (m1:t val1) (m2:t val2) : t val3 :=
    PShareTree.combine (fun lo1 lo2 =>
                          let l1 := match lo1 return _ with None => nil | Some l => l end in
                          let l2 := match lo2 return _ with None => nil | Some l => l end in
                          match combine_lists comb l1 l2 return _ with
                            | nil => None
                            | l => Some l
                          end) m1 m2.
Next Obligation.
    rewrite PShareTree.gcombine in H. 2:auto. split.
    - destruct @combine_lists; congruence.
    - fold (get_lst h m1) in H. fold (get_lst h m2) in H.
      replace l with (combine_lists comb (get_lst h m1) (get_lst h m2))
      by (destruct @combine_lists; congruence). clear H.
      split. apply combine_lists_norepet; apply get_lst_inv.
      apply Forall_forall. intros. apply combine_lists_In in H; try apply get_lst_inv.
      destruct H; eapply Forall_forall with (P:=fun k => h = hash k), H; apply get_lst_inv.
  Qed.

  Lemma gcombine:
    forall val1 val2 val3 (f: option val1 -> option val2 -> option val3),
    f None None = None ->
    forall (m1: t val1) (m2: t val2) i,
      get i (combine f m1 m2) = f (get i m1) (get i m2).
Proof.
    intros. unfold get, combine, get_lst. simpl.
    rewrite PShareTree.gcombine by auto.
    fold (get_lst (hash i) m1). fold (get_lst (hash i) m2).
    rewrite <- combine_lists_ok. destruct @combine_lists; auto.
    apply get_lst_inv. apply get_lst_inv. auto.
  Qed.

  Program Definition map {val1 val2} (f:elt -> val1 -> val2) (m:t val1) : t val2 :=
    PShareTree.map1 (List.map (fun kv => (fst kv, f (fst kv) (snd kv)))) m.
Next Obligation.
    rewrite PShareTree.gmap1 in H.
    pose proof (proj2_sig m h). destruct (PShareTree.get h (proj1_sig m)); inv H.
    specialize (H0 _ eq_refl).
    split. destruct l0; intuition discriminate. rewrite map_map. apply H0.
  Qed.

  Lemma gmap:
    forall val1 val2 f i m,
      get i (map (val1:=val1) (val2:=val2) f m) = option_map (f i) (get i m).
Proof.
    intros. unfold get, get_lst, map. simpl.
    rewrite PShareTree.gmap1. destruct PShareTree.get; simpl. 2:auto.
    induction l as [|[]]. auto. simpl. destruct eq_dec; simpl. congruence. auto.
  Qed.

  Program Definition map1 {val1 val2} (f:val1 -> val2) (m:t val1) : t val2 :=
    PShareTree.map1 (List.map (fun kv => (fst kv, f (snd kv)))) m.
Next Obligation.
    rewrite PShareTree.gmap1 in H.
    pose proof (proj2_sig m h). destruct (PShareTree.get h (proj1_sig m)); inv H.
    specialize (H0 _ eq_refl).
    split. destruct l0; intuition discriminate. rewrite map_map. apply H0.
  Qed.

  Lemma gmap1:
    forall val1 val2 f i m,
      get i (map1 (val1:=val1) (val2:=val2) f m) = option_map f (get i m).
Proof.
    intros. unfold get, get_lst, map. simpl.
    rewrite PShareTree.gmap1. destruct PShareTree.get; simpl. 2:auto.
    induction l as [|[]]. auto. simpl. destruct eq_dec; simpl. congruence. auto.
  Qed.

  Program Definition elements {val:Type} (m:t val) : list (elt * val) :=
    List.rev_append (PShareTree.fold1 (fun acc l => List.rev_append l acc) m nil) nil.

  Lemma elements_correct :
    forall val (m: t val) i v, get i m = Some v -> In (i, v) (elements m).
Proof.
    intros. unfold elements. rewrite <- rev_alt, <- in_rev, PShareTree.fold1_spec.
    unfold get in H. destruct (get_lst_inv _ (hash i) m) as [? _]. unfold get_lst in *.
    destruct (PShareTree.get (hash i) (proj1_sig m)) eqn:EQ. 2:discriminate.
    apply PShareTree.elements_correct in EQ.
    revert EQ. generalize (PShareTree.elements (proj1_sig m)).
    intros. assert (In (hash i, l) l0 \/ In (i, v) nil) by auto. clear EQ.
    generalize dependent (@nil (elt * val)).
    induction l0. simpl. intuition.
    intros; apply IHl0. rewrite rev_append_rev, in_app_iff, <- in_rev. destruct H1 as [[|]|].
    - subst. apply assoc_spec in H; auto.
    - auto.
    - auto.
  Qed.

  Lemma elements_complete:
    forall val (m: t val) i v,
      In (i, v) (elements m) -> get i m = Some v.
Proof.
    unfold get, elements. intros. rewrite <- rev_alt, PShareTree.fold1_spec, <- in_rev in H.
    refine (@or_ind _ (In (i, v) nil) _ (fun H => H) (fun (F:False) => match F with end) _).
    revert H. generalize (@nil (elt * val)) at 2 3.
    generalize (PShareTree.elements_complete (proj1_sig m)).
    induction (PShareTree.elements (proj1_sig m)) as [|[]]; simpl; intros. now intuition.
    edestruct IHl; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev in H1.
    destruct H1. 2:auto. left.
    specialize (H _ _ (or_introl eq_refl)).
    destruct (proj2_sig m _ _ H) as (_ & ? & ?).
    eapply Forall_forall in H3. 2:eapply in_map_fst, H1.
    subst. unfold get_lst. rewrite H. apply assoc_spec; auto.
  Qed.

  Lemma list_norepet_rev:
    forall T (l:list T), list_norepet (rev l) <-> list_norepet l.
Proof.
    induction l; simpl. now intuition.
    rewrite list_norepet_app, IHl. split.
    - constructor. 2:now intuition. intro. eapply H. apply -> in_rev. eauto. simpl. eauto. auto.
    - intro. inv H. split. auto. split. constructor. auto. constructor.
      repeat intro. destruct H0 as [|[]]. apply in_rev in H. congruence.
  Qed.

  Lemma elements_keys_norepet:
    forall val (m: t val), list_norepet (List.map fst (elements m)).
Proof.
    intros. unfold elements. rewrite fold1_spec.
    generalize (list_norepet_nil elt). change (@nil elt) with (List.map fst (@nil (elt*val))).
    assert (forall p l, In (p, l) (PShareTree.elements (proj1_sig m)) ->
                        list_disjoint (List.map fst l) (List.map fst (@nil (elt*val)))).
    { unfold list_disjoint. now intuition. } revert H.
    generalize (@nil (elt*val)) at 2 3 5.
    generalize (PShareTree.elements_keys_norepet (proj1_sig m)).
    generalize (PShareTree.elements_complete (proj1_sig m)).
    induction (PShareTree.elements (proj1_sig m)) as [|[]]; simpl; intros.
    - rewrite <- rev_alt, map_rev, list_norepet_rev. auto.
    - inv H0. apply IHl. auto. auto.
      + rewrite rev_append_rev, map_app, map_rev.
        repeat intro. rewrite in_app_iff, <- in_rev in H4. destruct H4. 2:eapply H1; eauto.
        assert (PShareTree.get p (proj1_sig m) = Some l) by auto.
        assert (PShareTree.get p0 (proj1_sig m) = Some l2) by auto.
        apply (proj2_sig m) in H8. destruct H8 as (_ & _ & ?). eapply Forall_forall in H8. 2:eauto.
        apply (proj2_sig m) in H9. destruct H9 as (_ & _ & ?). eapply Forall_forall in H9. 2:eauto.
        apply H5. eapply in_map with (f:=fst) in H0. simpl in H0. subst. auto.
      + rewrite rev_append_rev, map_app, map_rev. rewrite list_norepet_app, list_norepet_rev.
        split. eapply (proj2_sig m), H. eauto. split. eauto.
        repeat intro. eapply H1; eauto. apply in_rev, H0.
  Qed.

  Program Definition fold {val acc} (f:acc -> elt -> val -> acc) (m:t val) (a:acc) : acc :=
    PShareTree.fold1 (fun acc l => List.fold_left (fun acc kv => f acc (fst kv) (snd kv)) l acc) m a.

  Lemma fold_spec:
    forall val acc f (a:acc) (m:t val),
      fold f m a =
      List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) a.
Proof.
    intros. unfold fold, elements. rewrite !fold1_spec.
    rewrite <- !fold_left_rev_right with (l:=PShareTree.elements (proj1_sig m)).
    induction (rev (PShareTree.elements (proj1_sig m))); simpl. auto.
    rewrite IHl, !rev_append_rev, !rev_app_distr, rev_involutive, !app_nil_r, fold_left_app. auto.
  Qed.

  Program Definition fold1 {val acc} (f:acc -> val -> acc) (m:t val) (a:acc) : acc :=
    PShareTree.fold1 (fun acc l => List.fold_left (fun acc kv => f acc (snd kv)) l acc) m a.

  Lemma fold1_spec:
    forall val acc f (a:acc) (m:t val),
      fold1 f m a =
      List.fold_left (fun a p => f a (snd p)) (elements m) a.
Proof.
    intros. unfold fold1, elements. rewrite !fold1_spec.
    rewrite <- !fold_left_rev_right with (l:=PShareTree.elements (proj1_sig m)).
    induction (rev (PShareTree.elements (proj1_sig m))); simpl. auto.
    rewrite IHl, !rev_append_rev, !rev_app_distr, rev_involutive, !app_nil_r, fold_left_app. auto.
  Qed.

  Program Definition cons_sh {val}
          (l:list (elt * val)) (k:elt) (v:val) (q:list (elt * val)) (eql:l = (k, v)::q)
          (v':val) (q':list (elt * val)) (l':unit -> list (elt * val))
          (eql':l' tt = (k,v')::q') : list (elt * val) :=
    ifeq v == v' then (ifeq q == q' then l else l' tt) else l' tt.

  Fixpoint shcombine_lists_r_diff {val1 val2:Type}
           (comb:elt -> option val1 -> option val1 -> option val2)
           (l:list (elt*val1)) : list (elt * val2) :=
    match l as ll return l = ll -> _ with
      | nil => fun _ => nil
      | (k, v2)::q => fun EQ =>
        match comb k None (Some v2) with
          | None => shcombine_lists_r_diff comb q
          | Some v => (k, v) :: shcombine_lists_r_diff comb q
        end
    end eq_refl.

  Fixpoint shcombine_lists_r {val:Type} (comb:elt -> option val -> option val -> option val)
           (l:list (elt*val)) : list (elt * val) :=
    match l as ll return l = ll -> _ with
      | nil => fun _ => nil
      | (k, v2)::q => fun EQ =>
        match comb k None (Some v2) with
          | None => shcombine_lists_r comb q
          | Some v =>
            let q' := shcombine_lists_r comb q in
            cons_sh l k v2 q EQ v q' (fun _ => (k, v)::q') eq_refl
        end
    end eq_refl.

  Lemma shcombine_lists_r_shcombine_lists_r_diff:
    forall val comb l,
      shcombine_lists_r (val:=val) comb l = shcombine_lists_r_diff comb l.
Proof.
    intros. induction l. auto. simpl. unfold cons_sh, physEq. rewrite IHl. auto.
  Qed.

  Lemma shcombine_lists_r_In:
    forall k val1 val2 comb (l:list (elt*val1)),
      list_norepet (List.map fst l) ->
      In k (List.map fst (shcombine_lists_r_diff (val2:=val2) comb l)) ->
      In k (List.map fst l).
Proof.
    induction l as [?|[]]. easy.
    simpl. intros. inv H. destruct (comb e None (Some v)); simpl in *; now intuition.
  Qed.

  Lemma shcombine_lists_r_norepet:
    forall val1 val2 comb (l:list (elt*val1)),
      list_norepet (List.map fst l) ->
      list_norepet (List.map fst (shcombine_lists_r_diff (val2:=val2) comb l)).
Proof.
    induction l as [|[]]. auto. simpl.
    intros. inv H. destruct (comb e None (Some v)). 2:auto. simpl. constructor. 2:auto.
    contradict H2. eapply shcombine_lists_r_In; eauto.
  Qed.

  Lemma shcombine_lists_r_ok:
    forall val1 val2 comb (l:list (elt*val1)) k,
      list_norepet (List.map fst l) ->
      comb k None None = None ->
      assoc k (shcombine_lists_r_diff (val2:=val2) comb l) = comb k None (assoc k l).
Proof.
    intros. induction l as [|[]]. auto.
    pose proof shcombine_lists_r_norepet _ _ comb _ H.
    rewrite assoc_spec by (apply shcombine_lists_r_norepet; auto).
    simpl in *. inv H. specialize (IHl H5). destruct (eq_dec k e).
    - subst. destruct (comb e None (Some v)). simpl. auto.
      contradict H4. eapply shcombine_lists_r_In; eauto.
    - rewrite assoc_spec in IHl by (apply shcombine_lists_r_norepet; auto).
      destruct (comb k None (assoc k l)), (comb e None (Some v)); simpl; now intuition.
  Qed.

  Fixpoint shcombine_lists {val:Type}
           (comb:elt -> option val -> option val -> option val)
           (Hcomb:∀ x v, comb x v v = v)
           (l1:list (elt*val)) (l2:list (elt*val)) {struct l1} :
    { l : list (elt*val) | l1 = l2 -> l = l1 }.
    refine (exist _
        (ifeq l1 == l2 then l1
         else proj1_sig (P:=fun l => l1 = l2 -> l = l1)
          (match l1 as ll1 return l1 = ll1 -> _ with
          | nil => fun _ => exist _ (shcombine_lists_r comb l2) _
          | (k, v1)::l1' => fun EQl1 =>
            match l2 as ll2 return l2 = ll2 -> _ with
              | nil => fun _ => exist _ (shcombine_lists_r (fun k v1 v2 => comb k v2 v1) l1) _
              | (k2, v2)::l2' => fun EQl2 =>
                if eq_dec k k2 then
                  let q := proj1_sig (shcombine_lists _ comb Hcomb l1' l2') in
                  exist _
                    (ifeq v1 == v2 then
                       cons_sh l2 k2 v2 l2' EQl2 v2 q
                         (fun _ =>
                            cons_sh l1 k v1 l1' EQl1 v1 q (fun _ => (k, v1)::q) eq_refl
                         ) _
                     else match comb k (Some v1) (Some v2) with
                            | None => q
                            | Some v =>
                              cons_sh l2 k2 v2 l2' EQl2 v q
                                (fun _ =>
                                   cons_sh l1 k v1 l1' EQl1 v q (fun _ => (k, v)::q) eq_refl
                                ) _
                          end)
                      _
                else
                  let '(ov2, l2') := extract_witness k l2' in
                  match ov2 with
                  | None =>
                    let q := proj1_sig (shcombine_lists _ comb Hcomb l1' l2) in
                    exist _
                      (match comb k (Some v1) None with
                       | None => q
                       | Some v =>
                         cons_sh l1 k v1 l1' EQl1 v q (fun _ => (k, v)::q) eq_refl
                       end) _
                  | Some v2' =>
                    let q := proj1_sig (shcombine_lists _ comb Hcomb l1' ((k2, v2)::l2')) in
                    exist _
                      (ifeq v1 == v2' then
                         cons_sh l1 k v1 l1' EQl1 v1 q (fun _ => (k, v1)::q) eq_refl
                       else
                         (match comb k (Some v1) (Some v2') with
                            | None => q
                            | Some v =>
                              cons_sh l1 k v1 l1' EQl1 v q (fun _ => (k, v)::q) eq_refl
                          end))
                        _
                  end
            end eq_refl
          end eq_refl)) _).
Proof.
    unfold physEq. clear. match goal with |- _ -> proj1_sig ?X = l1 => apply (proj2_sig X) end.
    Grab Existential Variables.
    - simpl. intros. symmetry. match goal with |- proj1_sig ?X = l1 => apply (proj2_sig X e) end.
    - simpl. generalize q. clear - H2 EQl1 EQl2.
      abstract (intros; subst k0 k1; congruence).
    - simpl. unfold physEq. generalize q. clear - H2 EQl1 EQl2.
      abstract (intros; subst k0 k1; congruence).
    - simpl. generalize q. clear -Hcomb.
      abstract (intros; subst; subst; rewrite Hcomb; auto).
    - simpl. unfold cons_sh, physEq.
      pose proof (proj2_sig (shcombine_lists val comb Hcomb l1'0 l2'0)). fold q in H3. simpl in H3.
      generalize q H3. clear - H2 EQl1 EQl2 Hcomb.
      abstract (subst; subst; subst v0 l1'0; intros; inv H; rewrite Hcomb, H3; auto).
    - unfold cons_sh, physEq. generalize q. clear -Hcomb.
      abstract (intros; subst; subst; rewrite Hcomb; auto).
    - simpl. unfold cons_sh, physEq. generalize q. clear -H2. abstract congruence.
    - simpl. unfold physEq. generalize q. clear - H3 H2 EQl2.
      abstract (intros; destruct H3; subst; subst; auto).
    - simpl. clear - H1 EQl1. abstract congruence.
    - simpl. clear - H0. abstract (intros; subst; subst; auto).
  Defined.

  Lemma shcombine_lists_In:
    forall k val comb Hcomb (l1:list (elt*val)) (l2:list (elt*val)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      In k (List.map fst (proj1_sig (shcombine_lists comb Hcomb l1 l2))) ->
      In k (List.map fst l1) \/ In k (List.map fst l2).
Proof.
    induction l1.
    - intros. right. simpl in H1. unfold physEq in H1.
      rewrite shcombine_lists_r_shcombine_lists_r_diff in H1.
      eapply shcombine_lists_r_In in H1; eauto.
    - destruct a. simpl. unfold cons_sh, physEq. intros.
      destruct l2 as [|[]].
      simpl in H1. rewrite shcombine_lists_r_shcombine_lists_r_diff in H1.
      apply shcombine_lists_r_In with (comb := fun _ _ _ => _) (l:=(_, _)::_) in H1; auto.
      inv H. destruct (eq_dec e k). auto. destruct (eq_dec e e0).
      + inv H0. simpl in H1.
        specialize (IHl1 _ H5 H6). simpl. destruct IHl1; auto.
        destruct (comb e0 (Some v) (Some v0)). 2:auto. destruct H1. destruct n. auto. auto.
      + inv H0.
        pose proof (extract_witness_norepet _ e l2 H6).
        pose proof (extract_witness_fstIn _ e l2 H6).
        assert (list_norepet (List.map fst ((e0, v0)::snd (extract_witness e l2)))).
        { simpl. constructor. 2:auto. rewrite H0. now intuition. }
        specialize (IHl1 _ H5 H2).
        pose proof (extract_witness_spec _ e l2 H6).
        destruct (extract_witness e l2) as [[] ?]; simpl in H1.
        * destruct IHl1; auto. destruct (comb e (Some v) (Some v1)). 2:auto.
          destruct H1. now intuition. auto.
          simpl. destruct H8. auto. rewrite H0 in H8. destruct H8. auto.
        * destruct H7. subst. destruct IHl1; auto. destruct (comb e (Some v) None). 2:auto.
          destruct H1. now intuition. auto.
  Qed.

  Lemma shcombine_lists_norepet:
    forall val comb Hcomb (l1:list (elt*val)) (l2:list (elt*val)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      list_norepet (List.map fst (proj1_sig (shcombine_lists comb Hcomb l1 l2))).
Proof.
    induction l1.
    - intros. simpl. unfold physEq.
      rewrite shcombine_lists_r_shcombine_lists_r_diff. apply shcombine_lists_r_norepet. auto.
    - destruct a. simpl. unfold cons_sh, physEq. intros.
      destruct l2 as [|[]]. simpl. rewrite shcombine_lists_r_shcombine_lists_r_diff.
      apply shcombine_lists_r_norepet with (comb:=fun _ _ _ => _) (l:=(_,_)::_); auto.
      inv H. destruct eq_dec.
      + inv H0. simpl. destruct (comb e0 (Some v) (Some v0)). 2:auto.
        simpl. constructor. 2:auto. intro. apply shcombine_lists_In in H; now intuition.
      + inv H0.
        pose proof (extract_witness_norepet _ e l2 H5).
        pose proof (extract_witness_fstIn _ e l2 H5).
        pose proof (extract_witness_spec _ e l2 H5).
        destruct (extract_witness e l2) as [[] ?].
        * simpl. destruct (comb e (Some v) (Some v1)).
          simpl. constructor. intro. apply shcombine_lists_In in H6.
          simpl in *. rewrite H0 in H6. now intuition. auto.
          simpl. constructor. rewrite H0. now intuition. now intuition.
          apply IHl1. auto. simpl. constructor. rewrite H0. now intuition. auto.
          apply IHl1. auto. simpl. constructor. rewrite H0. now intuition. auto.
        * simpl. destruct (comb e (Some v) None).
          simpl. constructor. intro. apply shcombine_lists_In in H6.
          simpl in *. now intuition. auto.
          simpl. constructor; auto.
          apply IHl1. auto. simpl. constructor; auto.
          apply IHl1. auto. simpl. constructor; auto.
  Qed.

  Lemma shcombine_lists_ok:
    forall val comb Hcomb (l1:list (elt*val)) (l2:list (elt*val)) k,
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      assoc k (proj1_sig (shcombine_lists comb Hcomb l1 l2)) = comb k (assoc k l1) (assoc k l2).
Proof.
    intros. revert l2 H0. induction l1 as [|[]]; intros.
    - simpl. unfold physEq. rewrite shcombine_lists_r_shcombine_lists_r_diff.
      apply shcombine_lists_r_ok. auto. auto.
    - destruct l2 as [|[]].
      { simpl. unfold cons_sh, physEq. rewrite shcombine_lists_r_shcombine_lists_r_diff.
        now apply (shcombine_lists_r_ok _ _ (fun k x y => comb k y x) _ k H (Hcomb _ _)). }
      rewrite assoc_spec. 2:apply shcombine_lists_norepet; now auto.
      simpl. unfold cons_sh, physEq. simpl in H. inv H. specialize (IHl1 H4).
      destruct (eq_dec e e0); simpl.
      + subst. simpl in H0. inv H0. specialize (IHl1 _ H5).
        destruct (eq_dec k e0).
        * subst. destruct (comb e0 (Some v) (Some v0)). simpl. auto.
          intro. apply shcombine_lists_In in H. now intuition. auto. auto.
        * rewrite assoc_spec in IHl1 by (apply shcombine_lists_norepet; auto).
          destruct (comb k (assoc k l1) (assoc k l2)), (comb e0 (Some v) (Some v0)); simpl; now intuition.
      + pose proof extract_witness_spec _ e l2.
        rewrite (surjective_pairing (extract_witness e l2)), extract_witness_assoc in H |- *.
        refine (let H := IHl1 ((e0, v0)::snd (extract_witness e l2)) _ in _ ); clear IHl1.
        { inv H0. simpl. constructor. intro. apply extract_witness_fstIn in H0; now intuition.
          apply extract_witness_norepet. auto. }
        inv H0. simpl in H1. rewrite assoc_spec, assoc_extract_witness in H1.
        2:now auto.
        2:apply shcombine_lists_norepet; auto; simpl in *;
        constructor; [contradict H6; apply extract_witness_fstIn in H6; now intuition |
                      apply extract_witness_norepet, H7 ].
        specialize (H H7).
        destruct (eq_dec k e0), (eq_dec k e); simpl in H; subst.
        * now intuition.
        * destruct (comb e0 (assoc e0 l1) (Some v0)), (assoc e l2); try destruct H as [-> ?]; simpl.
          destruct (comb e (Some v) (Some v2)); simpl; now auto.
          destruct (comb e (Some v) None); simpl; now auto.
          destruct (comb e (Some v) (Some v1)); simpl; now intuition.
          destruct (comb e (Some v) None); simpl; now intuition.
        * destruct (comb e (Some v) (assoc e l2)) eqn:EQ, (assoc e l2); simpl; rewrite EQ; simpl; auto.
          { intro. apply shcombine_lists_In in H0. simpl in H0.
            rewrite extract_witness_fstIn in H0 by auto.
            now intuition. auto. simpl. constructor. intro. apply extract_witness_fstIn in H2.
            now intuition. auto. apply extract_witness_norepet. auto. }
          { intro. apply shcombine_lists_In in H0. simpl in H0. now intuition. auto.
            simpl. constructor; now auto. }
        * destruct (comb k (assoc k l1) (assoc k l2)), (assoc e l2); try destruct H as [-> ?]; simpl.
          destruct (comb e (Some v) (Some v2)); simpl; now auto.
          destruct (comb e (Some v) None); simpl; now auto.
          destruct (comb e (Some v) (Some v1)); simpl; now intuition.
          destruct (comb e (Some v) None); simpl; now intuition.
  Qed.

  Program Definition shcombine {val: Type} (comb:elt -> option val -> option val -> option val)
          (Hcomb:forall x v, comb x v v = v)
          (m1:t val) (m2:t val) : t val :=
    PShareTree.shcombine (fun _ lo1 lo2 =>
                            let l1 := match lo1 return _ with None => nil | Some l => l end in
                            let l2 := match lo2 return _ with None => nil | Some l => l end in
                            match shcombine_lists comb Hcomb l1 l2 return _ with
                              | nil =>
                                match lo1 return _ with
                                  | Some nil => Some nil
                                  | _ => None
                                end
                              | l => ifeq l == l1 then Some l1 else
                                       ifeq l == l2 then Some l2 else Some l
                            end) _ m1 m2.
Next Obligation.
congruence. Qed.
Next Obligation.
unfold physEq. congruence. Qed.
Next Obligation.
    unfold physEq. destruct @shcombine_lists; simpl. specialize (e eq_refl). subst x0.
    destruct v. 2:auto. destruct l; auto.
  Qed.
Next Obligation.
    unfold physEq in *. rewrite PShareTree.gshcombine in H.
    replace match PShareTree.get h (proj1_sig m1) return option (list (elt * val)) with
              | Some nil => Some nil
              | Some (_ :: _) => None
              | None => None
            end
    with (@None (list (elt * val))) in H.
    split.
    - destruct @shcombine_lists as [[] ?]; simpl in H; congruence.
    - fold (get_lst h m1) in H. fold (get_lst h m2) in H.
      replace l with (proj1_sig (shcombine_lists comb Hcomb (get_lst h m1) (get_lst h m2))).
      split. apply shcombine_lists_norepet; apply get_lst_inv.
      apply Forall_forall. intros. apply shcombine_lists_In in H0; try apply get_lst_inv.
      destruct H0; eapply Forall_forall with (P:=fun k => h = hash k), H0; apply get_lst_inv.
      destruct (proj1_sig (shcombine_lists comb Hcomb (get_lst h m1) (get_lst h m2))); congruence.
    - pose proof (proj2_sig m1 h).
      destruct PShareTree.get as [[]|]; auto.
      edestruct H0 as [[] _]; eauto.
  Qed.

  Lemma gshcombine:
    forall val comb Hcomb m1 m2 i,
      get (val:=val) i (shcombine comb Hcomb m1 m2) = comb i (get i m1) (get i m2).
Proof.
    intros. unfold get, combine, get_lst. simpl.
    rewrite PShareTree.gshcombine by auto.
    fold (get_lst (hash i) m1). fold (get_lst (hash i) m2). unfold physEq.
    rewrite <- shcombine_lists_ok with (Hcomb:=Hcomb). destruct @shcombine_lists; auto.
    simpl. destruct x; auto.
    pose proof (proj2_sig m1 (hash i)). destruct PShareTree.get as [[]|]; auto.
    apply get_lst_inv. apply get_lst_inv.
  Qed.

  Lemma shcombine_eq:
    forall val comb Hcomb m, shcombine (val:=val) comb Hcomb m m = m.
Proof.
    unfold shcombine. unfold physEq. intros.
    assert (forall (m1 m2:t val), proj1_sig m1 = proj1_sig m2 -> m1 = m2).
    { intros. destruct m1, m2. simpl in *. subst. f_equal. apply Axioms.proof_irr. }
    apply H. apply PShareTree.shcombine_eq.
  Qed.

  Fixpoint shcombine_lists_diff {val1 val2:Type}
           (comb:elt -> option val1 -> option val1 -> option val2)
           (Hcomb:∀ x v, comb x v v = None)
           (l1:list (elt*val1)) (l2:list (elt*val1)) {struct l1} :
    { l : list (elt*val2) | l1 = l2 -> l = nil }.
    refine (exist _
        (ifeq l1 == l2 then nil
         else proj1_sig (P:=fun l => l1 = l2 -> l = nil)
          (match l1 as ll1 return l1 = ll1 -> _ with
          | nil => fun _ => exist _ (shcombine_lists_r_diff comb l2) _
          | (k, v1)::l1' => fun EQl1 =>
            match l2 as ll2 return l2 = ll2 -> _ with
              | nil => fun _ => exist _ (shcombine_lists_r_diff (fun k v1 v2 => comb k v2 v1) l1) _
              | (k2, v2)::l2' => fun EQl2 =>
                if eq_dec k k2 then
                  let q := proj1_sig (shcombine_lists_diff _ _ comb Hcomb l1' l2') in
                  exist _
                    (ifeq v1 == v2 then q
                     else match comb k (Some v1) (Some v2) with
                            | None => q
                            | Some v => (k, v)::q
                          end)
                      _
                else
                  let '(ov2, l2') := extract_witness k l2' in
                  match ov2 with
                  | None =>
                    let q := proj1_sig (shcombine_lists_diff _ _ comb Hcomb l1' l2) in
                    exist _
                      (match comb k (Some v1) None with
                       | None => q
                       | Some v => (k, v)::q
                       end) _
                  | Some v2' =>
                    let q := proj1_sig (shcombine_lists_diff _ _ comb Hcomb l1' ((k2, v2)::l2')) in
                    exist _
                      (ifeq v1 == v2' then q
                       else
                         (match comb k (Some v1) (Some v2') with
                            | None => q
                            | Some v => (k, v)::q
                          end))
                        _
                  end
            end eq_refl
          end eq_refl)) _).
Proof.
    unfold physEq. clear. match goal with |- _ -> proj1_sig ?X = nil => apply (proj2_sig X) end.
    Grab Existential Variables.
    - simpl. intros. symmetry. match goal with |- proj1_sig ?X = nil => apply (proj2_sig X e) end.
    - simpl. generalize q. clear - H2 EQl1 EQl2.
      abstract (intros; subst k0 k1; congruence).
    - simpl. unfold physEq. generalize q. clear - H2 EQl1 EQl2.
      abstract (intros; subst k0 k1; congruence).
    - simpl. abstract (intros; subst; subst; rewrite Hcomb; auto).
    - simpl. unfold cons_sh, physEq.
      pose proof (proj2_sig (shcombine_lists_diff val1 val2 comb Hcomb l1'0 l2'0)). fold q in H3. simpl in H3.
      generalize q H3. clear - H2 EQl1 EQl2 Hcomb.
      abstract (subst; subst; subst v0 l1'0; intros; inv H; rewrite Hcomb, H3; auto).
    - unfold cons_sh, physEq. generalize q. clear -Hcomb.
      abstract (intros; subst; subst; rewrite Hcomb; auto).
    - simpl. clear - H1 EQl1. abstract congruence.
    - simpl. clear - H0. abstract (intros; subst; subst; auto).
  Defined.

  Lemma shcombine_lists_diff_In:
    forall k val1 val2 comb Hcomb (l1:list (elt*val1)) (l2:list (elt*val1)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      In k (List.map fst (proj1_sig (shcombine_lists_diff (val2:=val2) comb Hcomb l1 l2))) ->
      In k (List.map fst l1) \/ In k (List.map fst l2).
Proof.
    induction l1.
    - intros. right. simpl in H1. unfold physEq in H1. eapply shcombine_lists_r_In in H1; eauto.
    - destruct a. simpl. unfold cons_sh, physEq. intros.
      destruct l2 as [|[]]. apply shcombine_lists_r_In with (comb:=fun _ _ _ => _) (l:=(_, _)::_) in H1; auto.
      inv H. destruct (eq_dec e k). auto. destruct (eq_dec e e0).
      + inv H0. simpl in H1.
        specialize (IHl1 _ H5 H6). simpl. destruct IHl1; auto.
        destruct (comb e0 (Some v) (Some v0)). 2:auto. destruct H1. destruct n. auto. auto.
      + inv H0.
        pose proof (extract_witness_norepet _ e l2 H6).
        pose proof (extract_witness_fstIn _ e l2 H6).
        assert (list_norepet (List.map fst ((e0, v0)::snd (extract_witness e l2)))).
        { simpl. constructor. 2:auto. rewrite H0. now intuition. }
        specialize (IHl1 _ H5 H2).
        pose proof (extract_witness_spec _ e l2 H6).
        destruct (extract_witness e l2) as [[] ?]; simpl in H1.
        * destruct IHl1; auto. destruct (comb e (Some v) (Some v1)). 2:auto.
          destruct H1. now intuition. auto.
          simpl. destruct H8. auto. rewrite H0 in H8. destruct H8. auto.
        * destruct H7. subst. destruct IHl1; auto. destruct (comb e (Some v) None). 2:auto.
          destruct H1. now intuition. auto.
  Qed.

  Lemma shcombine_lists_diff_norepet:
    forall val1 val2 comb Hcomb (l1:list (elt*val1)) (l2:list (elt*val1)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      list_norepet (List.map fst (proj1_sig (shcombine_lists_diff (val2:=val2) comb Hcomb l1 l2))).
Proof.
    induction l1.
    - intros. simpl. unfold physEq. apply shcombine_lists_r_norepet. auto.
    - destruct a. simpl. unfold cons_sh, physEq. intros.
      destruct l2 as [|[]]. apply shcombine_lists_r_norepet with (comb:=fun _ _ _ => _) (l:=(_,_)::_); auto.
      inv H. destruct eq_dec.
      + inv H0. simpl. destruct (comb e0 (Some v) (Some v0)). 2:auto.
        simpl. constructor. 2:auto. intro. apply shcombine_lists_diff_In in H; now intuition.
      + inv H0.
        pose proof (extract_witness_norepet _ e l2 H5).
        pose proof (extract_witness_fstIn _ e l2 H5).
        pose proof (extract_witness_spec _ e l2 H5).
        destruct (extract_witness e l2) as [[] ?].
        * simpl. destruct (comb e (Some v) (Some v1)).
          simpl. constructor. intro. apply shcombine_lists_diff_In in H6.
          simpl in *. rewrite H0 in H6. now intuition. auto.
          simpl. constructor. rewrite H0. now intuition. now intuition.
          apply IHl1. auto. simpl. constructor. rewrite H0. now intuition. auto.
          apply IHl1. auto. simpl. constructor. rewrite H0. now intuition. auto.
        * simpl. destruct (comb e (Some v) None).
          simpl. constructor. intro. apply shcombine_lists_diff_In in H6.
          simpl in *. now intuition. auto.
          simpl. constructor; auto.
          apply IHl1. auto. simpl. constructor; auto.
          apply IHl1. auto. simpl. constructor; auto.
  Qed.

  Lemma shcombine_lists_diff_ok:
    forall val1 val2 comb Hcomb (l1:list (elt*val1)) (l2:list (elt*val1)) k,
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      assoc k (proj1_sig (shcombine_lists_diff (val2:=val2) comb Hcomb l1 l2)) =
      comb k (assoc k l1) (assoc k l2).
Proof.
    intros. revert l2 H0. induction l1 as [|[]]; intros.
    - apply shcombine_lists_r_ok. auto. auto.
    - destruct l2 as [|[]].
      now apply (shcombine_lists_r_ok _ _ (fun e v1 v2 => comb e v2 v1) _ k H (Hcomb _ _)).
      rewrite assoc_spec. 2:apply shcombine_lists_diff_norepet; now auto.
      simpl. unfold cons_sh, physEq. simpl in H. inv H. specialize (IHl1 H4).
      destruct (eq_dec e e0); simpl.
      + subst. simpl in H0. inv H0. specialize (IHl1 _ H5).
        destruct (eq_dec k e0).
        * subst. destruct (comb e0 (Some v) (Some v0)). simpl. auto.
          intro. apply shcombine_lists_diff_In in H. now intuition. auto. auto.
        * rewrite assoc_spec in IHl1 by (apply shcombine_lists_diff_norepet; auto).
          destruct (comb k (assoc k l1) (assoc k l2)), (comb e0 (Some v) (Some v0)); simpl; now intuition.
      + pose proof extract_witness_spec _ e l2.
        rewrite (surjective_pairing (extract_witness e l2)), extract_witness_assoc in H |- *.
        refine (let H := IHl1 ((e0, v0)::snd (extract_witness e l2)) _ in _ ); clear IHl1.
        { inv H0. simpl. constructor. intro. apply extract_witness_fstIn in H0; now intuition.
          apply extract_witness_norepet. auto. }
        inv H0. simpl in H1. rewrite assoc_spec, assoc_extract_witness in H1.
        2:now auto.
        2:apply shcombine_lists_diff_norepet; auto; simpl in *;
        constructor; [contradict H6; apply extract_witness_fstIn in H6; now intuition |
                      apply extract_witness_norepet, H7 ].
        specialize (H H7).
        destruct (eq_dec k e0), (eq_dec k e); simpl in H; subst.
        * now intuition.
        * destruct (comb e0 (assoc e0 l1) (Some v0)), (assoc e l2); try destruct H as [-> ?]; simpl.
          destruct (comb e (Some v) (Some v2)); simpl; now auto.
          destruct (comb e (Some v) None); simpl; now auto.
          destruct (comb e (Some v) (Some v1)); simpl; now intuition.
          destruct (comb e (Some v) None); simpl; now intuition.
        * destruct (comb e (Some v) (assoc e l2)) eqn:EQ, (assoc e l2); simpl; rewrite EQ; simpl; auto.
          { intro. apply shcombine_lists_diff_In in H0. simpl in H0.
            rewrite extract_witness_fstIn in H0 by auto.
            now intuition. auto. simpl. constructor. intro. apply extract_witness_fstIn in H2.
            now intuition. auto. apply extract_witness_norepet. auto. }
          { intro. apply shcombine_lists_diff_In in H0. simpl in H0. now intuition. auto.
            simpl. constructor; now auto. }
        * destruct (comb k (assoc k l1) (assoc k l2)), (assoc e l2); try destruct H as [-> ?]; simpl.
          destruct (comb e (Some v) (Some v2)); simpl; now auto.
          destruct (comb e (Some v) None); simpl; now auto.
          destruct (comb e (Some v) (Some v1)); simpl; now intuition.
          destruct (comb e (Some v) None); simpl; now intuition.
  Qed.

  Program Definition shcombine_diff {val1 val2: Type}
          (comb:elt -> option val1 -> option val1 -> option val2)
          (Hcomb:forall x v, comb x v v = None)
          (m1:t val1) (m2:t val1) : t val2 :=
    PShareTree.shcombine_diff (fun _ lo1 lo2 =>
                            let l1 := match lo1 return _ with None => nil | Some l => l end in
                            let l2 := match lo2 return _ with None => nil | Some l => l end in
                            match shcombine_lists_diff comb Hcomb l1 l2 return _ with
                              | nil => None
                              | l => Some l
                            end) _ m1 m2.
Next Obligation.
    destruct @shcombine_lists_diff; simpl. specialize (e eq_refl). subst x0. auto.
  Qed.
Next Obligation.
    rewrite PShareTree.gshcombine_diff in H.
    split.
    - destruct @shcombine_lists_diff as [[] ?]; simpl in H; congruence.
    - fold (get_lst h m1) in H. fold (get_lst h m2) in H.
      replace l with (proj1_sig (shcombine_lists_diff comb Hcomb (get_lst h m1) (get_lst h m2))).
      split. apply shcombine_lists_diff_norepet; apply get_lst_inv.
      apply Forall_forall. intros. apply shcombine_lists_diff_In in H0; try apply get_lst_inv.
      destruct H0; eapply Forall_forall with (P:=fun k => h = hash k), H0; apply get_lst_inv.
      destruct (proj1_sig (shcombine_lists_diff comb Hcomb (get_lst h m1) (get_lst h m2))); congruence.
  Qed.

  Lemma gshcombine_diff:
    forall val1 val2 comb Hcomb m1 m2 i,
      get (val:=val2) i (shcombine_diff (val1:=val1) comb Hcomb m1 m2) = comb i (get i m1) (get i m2).
Proof.
    intros. unfold get, combine, get_lst. simpl.
    rewrite PShareTree.gshcombine_diff by auto.
    fold (get_lst (hash i) m1). fold (get_lst (hash i) m2).
    rewrite <- shcombine_lists_diff_ok with (Hcomb:=Hcomb). destruct @shcombine_lists_diff; auto.
    simpl. destruct x; auto.
    apply get_lst_inv. apply get_lst_inv.
  Qed.

  Lemma shcombine_diff_eq:
    forall val1 val2 comb Hcomb m, shcombine_diff (val1:=val1) comb Hcomb m m = empty val2.
Proof.
    unfold shcombine_diff. intros.
    assert (forall (m1 m2:t val2), proj1_sig m1 = proj1_sig m2 -> m1 = m2).
    { intros. destruct m1, m2. simpl in *. subst. f_equal. apply Axioms.proof_irr. }
    apply H. apply PShareTree.shcombine_diff_eq.
  Qed.

  Fixpoint shforall2_lists {val:Type}
           (comb:elt -> option val -> option val -> bool)
           (Hcomb:forall k v, comb k v v = true)
           (l1:list (elt*val)) (l2:list (elt*val)) {struct l1}:
    { b:bool | l1 = l2 -> b = true }.
  refine (
    exist _
      (ifeq l1 == l2 then true
       else
         proj1_sig (P:=fun b=>l1=l2 -> b = true)
            (match l1 with
             | nil => exist _ (List.forallb (fun v => comb (fst v) None (Some (snd v))) l2) _
             | (k, v1)::l1 =>
               exist _
                 (let '(ov2, l2) := extract_witness k l2 in
                  (comb k (Some v1) ov2 && proj1_sig (shforall2_lists val comb Hcomb l1 l2)))
                 _
             end))
      _).
Proof.
    unfold physEq.
    match goal with |- _ -> proj1_sig ?X = true => apply (proj2_sig X) end.
    Grab Existential Variables.
    - simpl. intro. symmetry. match goal with |- proj1_sig ?X = true => apply (proj2_sig X e) end.
    - simpl. generalize (shforall2_lists val comb Hcomb l3). clear -Hcomb.
      abstract
        (intros; subst; subst k0 v0 l3; simpl; destruct eq_dec; [|congruence];
         rewrite (Hcomb k (Some v1)); simpl;
         match goal with |- proj1_sig ?X = true => apply (proj2_sig X eq_refl) end).
    - simpl. clear. abstract (intro; subst; auto).
  Defined.

  Lemma shforall2_lists_ok:
    forall val comb Hcomb (l1:list (elt*val)) (l2:list (elt*val)),
      list_norepet (List.map fst l1) -> list_norepet (List.map fst l2) ->
      (proj1_sig (shforall2_lists comb Hcomb l1 l2) = true <->
       forall k, comb k (assoc k l1) (assoc k l2) = true).
Proof.
    induction l1 as [|[]].
    - simpl. unfold physEq. induction l2 as [|[]]. intros. setoid_rewrite Hcomb. split; reflexivity.
      simpl. intros. rewrite Bool.andb_true_iff. inv H0. specialize (IHl2 H H4).
      split.
      + intros [? ?] ?. destruct eq_dec. congruence. apply IHl2. auto.
      + split.
        * specialize (H0 e). destruct (eq_dec e e); now intuition.
        * apply IHl2. intros. specialize (H0 k).
          pose proof assoc_spec _ k l2 H4 (assoc k l2).
          destruct (assoc k l2). 2:auto.
          destruct (eq_dec k e). 2:auto.
          destruct H3. subst. eapply in_map_fst, H1, eq_refl.
    - simpl. unfold physEq. intros. inv H.
      pose proof (fun k => assoc_extract_witness _ k e l2 H0).
      rewrite (surjective_pairing (extract_witness e l2)), extract_witness_assoc, Bool.andb_true_iff.
      split.
      + intros [? ?] ?. specialize (H k). destruct (eq_dec k e). congruence.
        rewrite <- H. apply IHl1. auto. apply extract_witness_norepet. auto. auto.
      + split.
        * specialize (H1 e). destruct (eq_dec e e); now intuition.
        * apply IHl1. auto. apply extract_witness_norepet. auto. intros.
          rewrite H. specialize (H1 k).
          destruct (eq_dec k e). 2:auto. subst.
          pose proof assoc_spec _ e l1 H4 (assoc e l1). destruct (assoc e l1). 2:auto.
          destruct H3. eapply in_map_fst. apply H2. auto.
  Qed.

  Program Definition shforall2 {val} comb Hcomb (m1 m2:t val) :=
    PShareTree.shforall2
      (fun _ lo1 lo2 =>
         let l1 := match lo1 return _ with None => nil | Some l => l end in
         let l2 := match lo2 return _ with None => nil | Some l => l end in
         proj1_sig (shforall2_lists (val:=val) comb Hcomb l1 l2)) _ m1 m2.
Next Obligation.
    destruct @shforall2_lists. auto.
  Qed.

  Lemma shforall2_correct:
    forall (A: Type)
           (comb: elt -> option A -> option A -> bool) (Hcomb:∀ x v, comb x v v = true),
    forall (m1 m2: t A),
      shforall2 comb Hcomb m1 m2 = true <->
      (forall x, comb x (get x m1) (get x m2) = true).
Proof.
    intros. unfold shforall2, get.
    rewrite PShareTree.shforall2_correct.
    split.
    - intros. eapply shforall2_lists_ok, H; apply get_lst_inv.
    - intros. eapply shforall2_lists_ok; try apply get_lst_inv.
      fold (get_lst i m1). fold (get_lst i m2).
      intros.
      destruct (eq_dec (hash k) i). subst. auto.
      destruct (get_lst_inv _ i m1). destruct (get_lst_inv _ i m2).
      pose proof (assoc_spec _ k (get_lst i m1) H0) None. simpl in H4. destruct H4. rewrite H5.
      pose proof (assoc_spec _ k (get_lst i m2) H2) None. simpl in H6. destruct H6. rewrite H7.
      auto.
      intro. eapply Forall_forall in H3. 2:eauto. congruence.
      intro. eapply Forall_forall in H1. 2:eauto. congruence.
  Qed.

End Hashtable.