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.
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.
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.
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.
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.
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.
Lemma gss:
forall val i x (
htbl:
t val),
get i (
set i x htbl) =
Some x.
Proof.
Lemma gso:
forall val (
i j:
elt) (
x:
val) (
htbl:
t val),
i <>
j ->
get i (
set j x htbl) =
get i htbl.
Proof.
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.
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.
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.
Lemma grs:
forall val i (
m:
t val),
get i (
remove i m) =
None.
Proof.
Lemma gro:
forall val i j (
m:
t val),
i <>
j ->
get i (
remove j m) =
get i m.
Proof.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Lemma gmap1:
forall val1 val2 f i m,
get i (
map1 (
val1:=
val1) (
val2:=
val2)
f m) =
option_map f (
get i m).
Proof.
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.
Lemma elements_complete:
forall val (
m:
t val)
i v,
In (
i,
v) (
elements m) ->
get i m =
Some v.
Proof.
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.
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.
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.
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.
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.
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.
Next Obligation.
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.
Lemma shcombine_eq:
forall val comb Hcomb m,
shcombine (
val:=
val)
comb Hcomb m m =
m.
Proof.
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.
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.
Next Obligation.
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.
Lemma shcombine_diff_eq:
forall val1 val2 comb Hcomb m,
shcombine_diff (
val1:=
val1)
comb Hcomb m m =
empty val2.
Proof.
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.
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.
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.
End Hashtable.