Module ShareTree


Require Import Utf8 Coqlib Maps.

Definition physEq {A B:Type} (x y:A) (eq:{_:unit | x = y} -> B) (neq:unit -> B)
                             (H:∀ (e:x = y), eq (exist _ tt e) = neq tt) : B := neq tt.

Extract Constant physEq =>
  "(fun x y eq neq -> if x == y then eq () else neq ())".

Notation "'ifeq' x == y 'then' A 'else' B" :=
  (physEq x y (fun _ => A) (fun _ => B) _) (at level 200).

Module Type SHARETREE.
  Include TREE.

  Variable shcombine:
    forall (A:Type)
           (f:elt -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v)
           (x y:t A), t A.
  Arguments shcombine {A} f Hf x y.
  Hypothesis gshcombine:
    forall (A: Type)
           (f: elt -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v),
    forall (m1 m2: t A) (i: elt),
      get i (shcombine f Hf m1 m2) = f i (get i m1) (get i m2).
  Hypothesis shcombine_eq:
    forall (A: Type)
           (f: elt -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v),
    forall (m: t A),
      shcombine f Hf m m = m.

  Variable shcombine_diff:
    forall (A B:Type)
           (f:elt -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None)
           (x y:t A), t B.
  Arguments shcombine_diff {A B} f Hf x y.
  Hypothesis gshcombine_diff:
    forall (A B: Type)
           (f: elt -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None),
    forall (m1 m2: t A) (i: elt),
      get i (shcombine_diff f Hf m1 m2) = f i (get i m1) (get i m2).
  Hypothesis shcombine_diff_eq:
    forall (A B: Type)
           (f: elt -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None),
    forall (m: t A),
      shcombine_diff f Hf m m = empty _.

  Variable shforall2:
    forall (A:Type)
           (f:elt -> option A -> option A -> bool) (Hf:∀ x v, f x v v = true)
           (x y:t A), bool.
  Arguments shforall2 {A} f Hf x y.
  Hypothesis shforall2_correct:
    forall (A: Type)
           (f: elt -> option A -> option A -> bool) (Hf:∀ x v, f x v v = true),
    forall (m1 m2: t A),
      shforall2 f Hf m1 m2 = true <->
      (forall x, f x (get x m1) (get x m2) = true).

End SHARETREE.

Module ShareTree_Properties(T:SHARETREE).

  Program Definition filter {A} (pred:T.elt -> A-> bool) (m:T.t A) :=
    T.shcombine (fun x a b =>
                 match a, b return _ with
                   | Some _, _ | None, None => a
                   | None, Some b' => if pred x b' then b else None
                 end)
              _ (T.empty A) m.
Next Obligation.
destruct v; auto. Qed.

  Lemma gfilter:
    forall (A: Type) (pred: T.elt -> A -> bool) (i: T.elt) (m: T.t A),
    T.get i (filter pred m) =
    match T.get i m with None => None | Some x => if pred i x then Some x else None end.
Proof.
    intros. unfold filter. rewrite T.gshcombine, T.gempty. destruct T.get; auto.
  Qed.

  Program Definition is_empty {A} (m:T.t A) : bool :=
    T.shforall2 (fun _ a b =>
                 match a, b return _ with
                   | Some _, Some _ | None, None => true
                   | _, _ => false
                 end)
                _ (T.empty A) m.
Next Obligation.
destruct v; auto. Qed.

  Lemma is_empty_correct:
    forall (A:Type) (m:T.t A),
      is_empty m = true <->
      forall (i:T.elt), T.get i m = None.
Proof.
    intros. unfold is_empty. rewrite T.shforall2_correct. setoid_rewrite T.gempty.
    split; intros H i; specialize (H i); destruct T.get; congruence.
  Qed.

  Program Definition map_changed {A} (eq:∀ a b : A, {a = b} + {a ≠ b})
          (f:T.elt -> option A -> option A)
          (m0:T.t A) (m:T.t A) : T.t A :=
    T.shcombine
      (fun k v0 v =>
         match v0, v return _ with
         | None, None => None
         | Some _, None => f k None
         | None, Some _ => f k v
         | Some v0', Some v' =>
           if eq v0' v' return _ then v else f k v
         end) _ m0 m.
Next Obligation.
destruct v. destruct eq. auto. congruence. auto. Qed.

  Lemma map_changed_correct:
    forall A eq f (m0 m:T.t A) k,
      T.get k m0 = T.get k m /\
      T.get k (map_changed eq f m0 m) = T.get k m
      \/
      T.get k m0 <> T.get k m /\
      T.get k (map_changed eq f m0 m) = f k (T.get k m).
Proof.
    intros. unfold map_changed. rewrite T.gshcombine.
    destruct (T.get k m), (T.get k m0).
    - destruct eq. subst. auto. right. intuition congruence.
    - right. intuition congruence.
    - right. intuition congruence.
    - auto.
  Qed.

End ShareTree_Properties.

Module PShareTree <: SHARETREE.
  Include PTree.

  Definition is_newLeaf {A} (l:t A) (o:option A) (r:t A) : bool :=
    match l, o, r with
      | Leaf, None, Leaf => true
      | _, _, _ => false
    end.

  Lemma is_newLeaf_Leaf:
    forall A l o r, is_newLeaf (A:=A) l o r = true -> l = Leaf /\ o = None /\ r = Leaf.
Proof.
intros A [] [] []; try discriminate. auto. Qed.

  Program Definition Node_sh {A}
             (m:t A) (l:t A) (o:option A) (r:t A) (eqm:m = Node l o r)
             (l':t A) (o':option A) (r':t A) (m':unit -> t A) (eqm':m' tt = Node l' o' r') : t A :=
    ifeq l == l' then
      match o, o' with
        | None, None => ifeq r == r' then m else m' tt
        | Some v, Some v' =>
          ifeq v == v' then (ifeq r == r' then m else m' tt) else m' tt
        | Some _, None | None, Some _ => m' tt
      end
    else
      m' tt.
Next Obligation.
unfold physEq. destruct o, o'; auto. Qed.

  Lemma Node_sh_Node:
    forall A m l o r eqm l' o' r' m' eqm',
      Node_sh (A:=A) m l o r eqm l' o' r' m' eqm' = Node l' o' r'.
Proof.
auto. Qed.

  Fixpoint xshcombine_l
           {A : Type} (f:positive -> option A -> option A -> option A)
           (m : t A) (i : rev_positive) : t A :=
    match m as m' return m = m' -> _ with
      | Leaf => fun _ => m
      | Node l o r => fun eqm =>
         let l' := xshcombine_l f l (rxO i) in
         let o' :=
           match o with
             | None => None
             | _ => f (prev i) o None
           end
         in
         let r' := xshcombine_l f r (rxI i) in
         if is_newLeaf l' o' r' then Leaf
         else Node_sh _ _ _ _ eqm l' o' r' (fun _ => Node l' o' r') eq_refl
    end eq_refl.

  Lemma xgshcombine_l:
    forall (A: Type) (f:positive -> option A -> option A -> option A) (m: t A)
           (i:positive) (j:rev_positive),
      (∀ i, f i None None = None) ->
      (xshcombine_l f m j) ! i = f (prev_append j i) m!i None.
Proof.
    intros A f. induction m; simpl.
    - intros. rewrite PTree.gleaf. auto.
    - intros. rewrite Node_sh_Node.
      match goal with
        | |- (if ?x then _ else _)!i = _ => destruct x eqn:EQ
      end.
      + apply is_newLeaf_Leaf in EQ. destruct EQ as (? & ? & ?).
        destruct i; simpl.
        specialize (IHm2 i (rxI j)). simpl in IHm2. rewrite <- IHm2, H2, PTree.gleaf; auto.
        specialize (IHm1 i (rxO j)). simpl in IHm1. rewrite <- IHm1, H0, PTree.gleaf; auto.
        destruct o; auto.
      + destruct i; simpl.
        apply IHm2 with (j:=rxI j). auto. apply IHm1 with (j:=rxO j). auto. destruct o; auto.
  Qed.
  Opaque xshcombine_l.

  Fixpoint xshcombine_r
           {A : Type} (f:positive -> option A -> option A -> option A)
           (m : t A) (i : rev_positive) : t A :=
    match m as m' return m = m' -> _ with
      | Leaf => fun _ => m
      | Node l o r => fun eqm =>
         let l' := xshcombine_r f l (rxO i) in
         let o' :=
           match o with
             | None => None
             | _ => f (prev i) None o
           end
         in
         let r' := xshcombine_r f r (rxI i) in
         if is_newLeaf l' o' r' then Leaf
         else Node_sh _ _ _ _ eqm l' o' r' (fun _ => Node l' o' r') eq_refl
    end eq_refl.

  Lemma xgshcombine_r:
    forall (A: Type) (f:positive -> option A -> option A -> option A) (m: t A)
           (i:positive) (j : rev_positive),
      (∀ i, f i None None = None) ->
      (xshcombine_r f m j) ! i = f (prev_append j i) None m!i.
Proof.
    intros A f. induction m; simpl.
    - intros. rewrite PTree.gleaf. auto.
    - intros. rewrite Node_sh_Node.
      match goal with
        | |- (if ?x then _ else _)!i = _ => destruct x eqn:EQ
      end.
      + apply is_newLeaf_Leaf in EQ. destruct EQ as (? & ? & ?).
        destruct i; simpl.
        specialize (IHm2 i (rxI j)). simpl in IHm2. rewrite <- IHm2, H2, PTree.gleaf; auto.
        specialize (IHm1 i (rxO j)). simpl in IHm1. rewrite <- IHm1, H0, PTree.gleaf; auto.
        destruct o; auto.
      + destruct i; simpl.
        apply IHm2 with (j:=rxI j). auto. apply IHm1 with (j:=rxO j). auto. destruct o; auto.
  Qed.
  Opaque xshcombine_r.

  Fixpoint xshcombine {A : Type}
           (f:positive -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v)
           (m1 m2 : t A) (i : rev_positive) {struct m1}: {ret : t A | m1 = m2 -> ret = m1}.
    refine
      (exist _
         (ifeq m1 == m2 then m1
          else proj1_sig (P:=fun ret => m1 = m2 -> ret = m1)
             (match m1 as m' return m1 = m' -> _ with
              | Leaf => fun _ => exist _ (xshcombine_r f m2 i) _
              | Node l1 o1 r1 => fun eqm1 =>
                match m2 as m' return m2 = m' -> _ with
                  | Leaf => fun _ => exist _ (xshcombine_l f m1 i) _
                  | Node l2 o2 r2 => fun eqm2 =>
                    let l' := xshcombine A f Hf l1 l2 (rxO i) in
                    let o' :=
                        match o1, o2 with
                          | None, None => None
                          | _, _ => f (prev i) o1 o2
                        end
                    in
                    let r' := xshcombine A f Hf r1 r2 (rxI i) in
                    exist _
                      (if is_newLeaf (proj1_sig l') o' (proj1_sig r') &&
                          (negb (is_newLeaf l1 o1 r1) || negb (is_newLeaf l2 o2 r2)) then
                         Leaf
                       else
                         Node_sh _ _ _ _ eqm1 (proj1_sig l') o' (proj1_sig r')
                           (fun _ => Node_sh _ _ _ _ eqm2 (proj1_sig l') o' (proj1_sig r')
                           (fun _ => Node (proj1_sig l') o' (proj1_sig r')) eq_refl) eq_refl) _
                end eq_refl
              end eq_refl))
         _).
Proof.
    unfold physEq. clear.
    match goal with |- _ -> proj1_sig ?X = m1 => apply (proj2_sig X) end.
    Grab Existential Variables.
    - simpl.
      intros; symmetry;
      match goal with |- proj1_sig ?X = m1 => apply (proj2_sig X e) end.
    - simpl. generalize l' r'. clear l' r' xshcombine.
      abstract (intros [l' eql'] [r' eqr'] eq; rewrite Node_sh_Node; simpl;
                subst o' l0 o0 r0 l3 o3 r3; destruct l1, o1, r1, l2, o2, r2; inv eq;
                rewrite eql', eqr', ?Hf; auto).
    - clear. simpl. abstract discriminate.
    - clear. simpl. abstract (intro; subst; auto).
  Defined.

  Lemma xgshcombine:
    forall (A: Type) (f:positive -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v)
           (m1 m2: t A) (i:positive) (j:rev_positive),
      (proj1_sig (xshcombine f Hf m1 m2 j)) ! i = f (prev_append j i) m1!i m2!i.
Proof.
    intros A f Hf. induction m1; destruct m2; simpl; intros; unfold physEq.
    - auto.
    - rewrite xgshcombine_r, PTree.gleaf; auto.
    - rewrite xgshcombine_l, PTree.gleaf; auto.
    - rewrite Node_sh_Node.
      match goal with
        | |- (if ?x then _ else _)!i = _ => destruct x eqn:EQ
      end.
      + apply andb_true_iff in EQ. destruct EQ as (EQ & _).
        apply is_newLeaf_Leaf in EQ. destruct EQ as (? & ? & ?).
        destruct i; simpl.
        specialize (IHm1_2 m2_2 i (rxI j)). simpl in IHm1_2. rewrite <- IHm1_2, H1, PTree.gleaf; auto.
        specialize (IHm1_1 m2_1 i (rxO j)). simpl in IHm1_1. rewrite <- IHm1_1, H, PTree.gleaf; auto.
        destruct o, o0; auto.
      + destruct i; simpl. apply IHm1_2 with (j:=rxI j). apply IHm1_1 with (j:=rxO j).
        destruct o, o0; auto.
  Qed.

  Definition shcombine {A:Type}
             (f:elt -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v)
             (x y:t A) : t A :=
    proj1_sig (xshcombine f Hf x y rpnil).

  Lemma gshcombine:
    forall (A: Type)
           (f: elt -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v),
    forall (m1: t A) (m2: t A) (i: elt),
    get i (shcombine f Hf m1 m2) = f i (get i m1) (get i m2).
Proof.
    intros. unfold shcombine. rewrite xgshcombine. auto.
  Qed.

  Lemma shcombine_eq:
    forall (A: Type)
           (f: elt -> option A -> option A -> option A) (Hf:∀ x v, f x v v = v),
    forall (m: t A),
      shcombine f Hf m m = m.
Proof.
    intros. unfold shcombine. destruct (xshcombine f Hf m m rpnil). auto.
  Qed.

  Fixpoint xshcombine_diff_l
           {A B: Type} (f:positive -> option A -> option A -> option B)
           (m : t A) (i : rev_positive) : t B :=
    match m as m' with
      | Leaf => Leaf
      | Node l o r =>
         let l' := xshcombine_diff_l f l (rxO i) in
         let o' :=
           match o with
             | None => None
             | _ => f (prev i) o None
           end
         in
         let r' := xshcombine_diff_l f r (rxI i) in
         Node' l' o' r'
    end.

  Lemma xgshcombine_diff_l:
    forall (A B: Type) (f:positive -> option A -> option A -> option B) (m: t A)
           (i:positive) (j:rev_positive),
      (∀ i, f i None None = None) ->
      (xshcombine_diff_l f m j) ! i = f (prev_append j i) m!i None.
Proof.
    intros A B f. induction m; simpl.
    - intros. rewrite !PTree.gleaf. auto.
    - intros. rewrite gnode'.
      destruct i; simpl. apply IHm2 with (j:=rxI j). auto. apply IHm1 with (j:=rxO j). auto.
      destruct o; auto.
  Qed.
  Opaque xshcombine_diff_l.

  Fixpoint xshcombine_diff_r
           {A B: Type} (f:positive -> option A -> option A -> option B)
           (m : t A) (i : rev_positive) : t B :=
    match m as m' with
      | Leaf => Leaf
      | Node l o r =>
         let l' := xshcombine_diff_r f l (rxO i) in
         let o' :=
           match o with
             | None => None
             | _ => f (prev i) None o
           end
         in
         let r' := xshcombine_diff_r f r (rxI i) in
         Node' l' o' r'
    end.

  Lemma xgshcombine_diff_r:
    forall (A B: Type) (f:positive -> option A -> option A -> option B) (m: t A)
           (i:positive) (j:rev_positive),
      (∀ i, f i None None = None) ->
      (xshcombine_diff_r f m j) ! i = f (prev_append j i) None m!i.
Proof.
    intros A B f. induction m; simpl.
    - intros. rewrite !PTree.gleaf. auto.
    - intros. rewrite gnode'.
      destruct i; simpl. apply IHm2 with (j:=rxI j). auto. apply IHm1 with (j:=rxO j). auto.
      destruct o; auto.
  Qed.
  Opaque xshcombine_diff_r.

  Fixpoint xshcombine_diff {A B: Type}
           (f:positive -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None)
           (m1 m2 : t A) (i : rev_positive) {struct m1}: {ret : t B | m1 = m2 -> ret = empty _}.
    refine
      (exist _
         (ifeq m1 == m2 then empty _
          else proj1_sig (P:=fun ret => m1 = m2 -> ret = empty _)
              (match m1 with
                 | Leaf => exist _ (xshcombine_diff_r f m2 i) _
                 | Node l1 o1 r1 =>
                   match m2 with
                     | Leaf => exist _ (xshcombine_diff_l f m1 i) _
                     | Node l2 o2 r2 =>
                       let l' := xshcombine_diff A B f Hf l1 l2 (rxO i) in
                       let o' :=
                           match o1, o2 with
                             | None, None => None
                             | _, _ => f (prev i) o1 o2
                           end
                       in
                       let r' := xshcombine_diff A B f Hf r1 r2 (rxI i) in
                       exist _ (Node' (proj1_sig l') o' (proj1_sig r')) _
                   end
               end))
         _).
Proof.
    unfold physEq.
    match goal with |- _ -> proj1_sig ?X = _ => apply (proj2_sig X) end.
    Grab Existential Variables.
    - simpl. intros. symmetry.
      match goal with |- proj1_sig ?X = _ => apply (proj2_sig X e) end.
    - generalize l' r'. clear l' r' xshcombine_diff.
      abstract (subst l0 o0 r0 l3 o3 r3 o';
                intros [l' eql'] [r' eqr'] eq; simpl; inv eq;
                rewrite eql', eqr', ?Hf; auto; destruct o2; auto).
    - clear. simpl. abstract discriminate.
    - clear. simpl. abstract (intro; subst; auto).
  Defined.

  Lemma xgshcombine_diff:
    forall (A B: Type) (f:positive -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None)
           (m1 m2: t A) (i:positive) (j:rev_positive),
      (proj1_sig (xshcombine_diff f Hf m1 m2 j)) ! i = f (prev_append j i) m1!i m2!i.
Proof.
    intros A B f Hf. induction m1; destruct m2; simpl; intros; unfold physEq.
    - rewrite xgshcombine_diff_r, PTree.gleaf; auto.
    - rewrite xgshcombine_diff_r, PTree.gleaf; auto.
    - rewrite xgshcombine_diff_l, PTree.gleaf; auto.
    - rewrite gnode'.
      destruct i; simpl. apply IHm1_2 with (j:=rxI j). apply IHm1_1 with (j:=rxO j).
      destruct o, o0; auto.
  Qed.

  Definition shcombine_diff {A B:Type}
             (f:elt -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None)
             (x y:t A) : t B :=
    proj1_sig (xshcombine_diff f Hf x y rpnil).

  Lemma gshcombine_diff:
    forall (A B: Type)
           (f: elt -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None),
    forall (m1 m2: t A) (i: elt),
    get i (shcombine_diff f Hf m1 m2) = f i (get i m1) (get i m2).
Proof.
    intros. unfold shcombine_diff. rewrite xgshcombine_diff. auto.
  Qed.

  Lemma shcombine_diff_eq:
    forall (A B: Type)
           (f: elt -> option A -> option A -> option B) (Hf:∀ x v, f x v v = None),
    forall (m: t A),
      shcombine_diff f Hf m m = empty _.
Proof.
    intros. unfold shcombine_diff. destruct (xshcombine_diff f Hf m m rpnil). auto.
  Qed.

  Fixpoint xshforall2_l
           {A : Type} (f:positive -> option A -> option A -> bool)
           (m : t A) (i : rev_positive) : bool :=
    match m with
      | Leaf => true
      | Node l o r =>
         xshforall2_l f l (rxO i) &&
         match o with None => true | _ => f (prev i) o None end &&
         xshforall2_l f r (rxI i)
    end.

  Lemma xshforall2_l_correct:
    forall (A: Type)
           (f: elt -> option A -> option A -> bool),
    forall (m: t A) (j:rev_positive),
    (∀ i, f i None None = true) ->
    (xshforall2_l f m j = true <->
     forall i, f (prev_append j i) (m!i) None = true).
Proof.
    intros A f. induction m; simpl.
    - split. intros. rewrite PTree.gleaf. auto. auto.
    - do 2 setoid_rewrite Bool.andb_true_iff. split; intros.
      + destruct H0 as [[] ?].
        destruct i; simpl. apply (IHm2 (rxI j)); auto. apply (IHm1 (rxO j)); auto.
        destruct o; auto.
      + split; [split|].
        apply IHm1. auto. intro. apply (H0 (xO _)).
        destruct o. apply (H0 xH). auto.
        apply IHm2. auto. intro. apply (H0 (xI _)).
  Qed.
  Opaque xshforall2_l.

  Fixpoint xshforall2_r
           {A : Type} (f:positive -> option A -> option A -> bool)
           (m : t A) (i : rev_positive) : bool :=
    match m with
      | Leaf => true
      | Node l o r =>
         xshforall2_r f l (rxO i) &&
         match o with None => true | _ => f (prev i) None o end &&
         xshforall2_r f r (rxI i)
    end.

  Lemma xshforall2_r_correct:
    forall (A: Type)
           (f: elt -> option A -> option A -> bool),
    forall (m: t A) (j: rev_positive),
    (∀ i, f i None None = true) ->
    (xshforall2_r f m j = true <->
     forall i, f (prev_append j i) None (m!i) = true).
Proof.
    intros A f. induction m; simpl.
    - split. intros. rewrite PTree.gleaf. auto. auto.
    - do 2 setoid_rewrite Bool.andb_true_iff. split; intros.
      + destruct H0 as [[] ?].
        destruct i; simpl. apply (IHm2 (rxI j)); auto. apply (IHm1 (rxO j)); auto.
        destruct o; auto.
      + split; [split|].
        apply IHm1. auto. intro. apply (H0 (xO _)).
        destruct o. apply (H0 xH). auto.
        apply IHm2. auto. intro. apply (H0 (xI _)).
  Qed.
  Opaque xshforall2_r.

  Fixpoint xshforall2 {A : Type}
           (f:positive -> option A -> option A -> bool) (Hf:∀ x v, f x v v = true)
           (m1 m2 : t A) (i : rev_positive) {struct m1}: {ret : bool | m1 = m2 -> ret = true}.
    refine
      (let r (_:unit) : {ret : bool | m1 = m2 → ret = true} :=
      match m1 with
      | Leaf => exist _ (xshforall2_r f m2 i) _
      | Node l1 o1 r1 =>
        match m2 with
          | Leaf => exist _ (xshforall2_l f m1 i) _
          | Node l2 o2 r2 =>
            exist _
            (proj1_sig (xshforall2 A f Hf l1 l2 (rxO i)) &&
            match o1, o2 with
              | None, None => true
              | _, _ => f (prev i) o1 o2
            end &&
            proj1_sig (xshforall2 A f Hf r1 r2 (rxI i)))
            _
        end
      end
      in _).
Proof.
    - clear. abstract (intro; subst; auto).
    - clear. abstract discriminate.
    - generalize (xshforall2 A f Hf l1 l2 (rxO i)%positive),
                 (xshforall2 A f Hf r1 r2 (rxI i)%positive).
      clear -Hf.
      abstract (intros s s0 eq; inv eq;
                rewrite (proj2_sig s), (proj2_sig s0), Hf by auto;
                destruct o2; auto).
    - clear -r.
      refine (exist _ (ifeq m1 == m2 then true else proj1_sig (r tt)) _).
      unfold physEq; destruct r; auto.
      Grab Existential Variables.
      abstract (simpl; destruct r; simpl; intro; symmetry; auto).
  Defined.

  Lemma xshforall2_correct:
    forall (A: Type)
           (f: elt -> option A -> option A -> bool) (Hf:∀ x v, f x v v = true),
    forall (m1 m2: t A) (j: rev_positive),
    (proj1_sig (xshforall2 f Hf m1 m2 j) = true <->
     forall i, f (prev_append j i) (m1!i) (m2!i) = true).
Proof.
    intros A f. induction m1; destruct m2; simpl; unfold physEq.
    - split. intros. rewrite PTree.gleaf. auto. auto.
    - intro. setoid_rewrite PTree.gleaf. apply xshforall2_r_correct. auto.
    - intro. setoid_rewrite PTree.gleaf. apply xshforall2_l_correct. auto.
    - do 2 setoid_rewrite Bool.andb_true_iff. split; intros.
      + destruct H as [[] ?].
        destruct i; simpl. apply IHm1_2 with (j:=rxI j); auto. apply IHm1_1 with (j:=rxO j); auto.
        destruct o, o0; auto.
      + split; [split|].
        apply IHm1_1. intro. apply (H (xO _)).
        destruct o, o0; try apply (H xH). auto.
        apply IHm1_2. intro. apply (H (xI _)).
  Qed.

  Definition shforall2 {A : Type}
             (f:positive -> option A -> option A -> bool) (Hf:∀ x v, f x v v = true)
             (m1 m2 : t A) : bool :=
    proj1_sig (xshforall2 f Hf m1 m2 rpnil).

  Lemma shforall2_correct:
    forall (A: Type)
           (f: elt -> option A -> option A -> bool) (Hf:∀ x v, f x v v = true),
    forall (m1 m2: t A),
    (shforall2 f Hf m1 m2 = true <->
     forall i, f i (m1!i) (m2!i) = true).
Proof.
    intros. unfold shforall2. rewrite xshforall2_correct. split; auto.
  Qed.

End PShareTree.
Generated by coq2html