# 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} + {ab})
(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 = m2ret = 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.