Lvc.Constr.MapUpdate
Require Export Setoid Coq.Classes.Morphisms.
Require Import EqDec Computable Util LengthEq AutoIndTac Get LengthEq.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapLookup MapAgreement.
Set Implicit Arguments.
Section MapUpdate.
Open Scope fmap_scope.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Fixpoint update_list (m:X → Y) (f:X → Y) (L:list X) :=
match L with
| nil ⇒ m
| x::L ⇒ (update_list m f L) [x <- f x]
end.
Lemma update_list_agree_minus {R} `{Symmetric Y R} `{Transitive Y R} lv (E E' f:X → Y) XL
: agree_on R lv E' E
→ agree_on R (lv\of_list XL) (update_list E' f XL) E.
Proof.
intros. general induction XL; simpl.
rewrite minus_empty. eassumption.
rewrite add_union_singleton. rewrite union_comm. rewrite <- minus_union.
eapply agree_on_update_dead. cset_tac.
eauto using agree_on_incl, incl_minus.
Qed.
Corollary update_list_agree_self {R} `{Equivalence Y R} lv (E:X → Y) L f
: agree_on R (lv\of_list L) (update_list E f L) E.
Proof.
eapply update_list_agree_minus. reflexivity.
Qed.
Lemma update_list_no_upd (m:X → Y) f L x
: x ∉ of_list L
→ (update_list m f L) x === m x.
Proof.
intros. general induction L; simpl; eauto. lud.
+ exfalso. eapply H0. simpl in × |- ×. rewrite e. eapply add_1; eauto.
+ assert (¬x ∈ of_list L).
- intro. eapply H0. simpl. eapply add_2; eauto.
- eauto.
Qed.
Lemma update_list_upd R `{Equivalence Y R} (m:X → Y) f L x
: x ∈ of_list L
→ Proper (_eq ==> R) f
→ (update_list m f L) x === f x.
Proof.
intros. general induction L; simpl; eauto.
+ lud.
- rewrite e; eauto.
- eapply IHL; eauto. eapply zadd_3; eauto.
Qed.
End MapUpdate.
Section MapUpdateList.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Open Scope fmap_scope.
Fixpoint update_with_list XL YL (m:X → Y) :=
match XL, YL with
| x::XL, y::YL ⇒ (update_with_list XL YL m)[x <- y]
| _, _ ⇒ m
end.
Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).
Lemma update_nodup_commute `{OrderedType Y} (XL:list X) (VL:list Y) E D x y
: length XL = length VL
→ NoDupA _eq (x::XL)
→ agree_on _eq D (E [x <- y] [XL <-- VL]) (E [XL <-- VL] [x <- y]).
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl in × |- *; dcr; simpl in *; eauto.
hnf; intros. lud; invt NoDupA.
- exfalso; eauto.
- invt NoDupA.
etransitivity; [eapply IHlength_eq|]; eauto; lud.
- invt NoDupA.
etransitivity; [eapply IHlength_eq|]; eauto; lud.
Qed.
Lemma update_nodup_commute_eq (XL:list X) (VL:list Y) E D x y
: length XL = length VL
→ NoDupA _eq (x::XL)
→ agree_on eq D (E [x <- y] [XL <-- VL]) (E [XL <-- VL] [x <- y]).
Proof.
intros LEN UNIQ. length_equify.
general induction LEN; simpl in × |- *; dcr; simpl in *; eauto.
hnf; intros. lud; invt NoDupA.
- exfalso; eauto.
- invt NoDupA; etransitivity; [eapply IHLEN|]; eauto; lud.
- invt NoDupA; etransitivity; [eapply IHLEN|]; eauto; lud.
Qed.
Lemma update_with_list_no_update (E:X → Y) Y' Z x
: x ∉ of_list Z
→ (E [ Z <-- Y' ]) x = E x.
Proof.
intros. general induction Z; simpl in *; destruct Y'; eauto.
lud; cset_tac.
Qed.
Context `{Equivalence Y}.
Lemma update_with_list_agree lv (E E':X → Y) XL YL
: agree_on R (lv\of_list XL) E E'
→ length XL = length YL
→ agree_on R lv (E [ XL <-- YL]) (E' [ XL <-- YL ]).
Proof.
intros. eapply length_length_eq in H2.
general induction XL; simpl in × |- ×.
- rewrite (@minus_empty _ _ lv) in H1; eauto.
- eapply agree_on_update_same. reflexivity.
eapply IHXL; eauto.
eapply agree_on_incl; eauto. cset_tac; intuition.
Qed.
Lemma update_with_list_agree_preserve lv (E E':X → Y) XL YL
: agree_on R lv E E'
→ agree_on R lv (E [ XL <-- YL]) (E' [ XL <-- YL ]).
Proof.
intros.
general induction XL; destruct YL; simpl in × |- *; eauto.
eapply agree_on_update_same; eauto. reflexivity.
eapply agree_on_incl; eauto.
Qed.
Lemma update_with_list_agree_minus lv (E E':X → Y) XL YL
: agree_on R lv E' E
→ agree_on R (lv\of_list XL) (E' [ XL <-- YL ]) E.
Proof.
intros.
general induction XL; simpl.
- rewrite minus_empty. eassumption.
- destruct YL; simpl.
+ eapply agree_on_incl; eauto.
+ rewrite add_union_singleton. rewrite union_comm. rewrite <- minus_union.
eapply agree_on_update_dead. cset_tac.
eauto using agree_on_incl, incl_minus.
Qed.
Hint Resolve minus_single_singleton minus_single_singleton' minus_single_singleton''.
Lemma update_with_list_agree_inv lv (E E':X → Y) XL YL
: length XL = length YL
→ agree_on R lv (E' [ XL <-- YL ]) E
→ agree_on R (lv\of_list XL) E' E.
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl in × |- ×.
- eapply agree_on_incl; eauto.
- rewrite add_union_singleton. rewrite <- minus_union.
eapply IHlength_eq; eauto.
eapply agree_on_update_inv; eauto.
Qed.
Lemma update_with_list_agree_self `{Defaulted X} lv (E:X → Y) XL YL
: agree_on R (lv\of_list XL) (E [ XL <-- YL]) E.
Proof.
general induction XL; simpl. rewrite minus_empty. reflexivity.
destruct YL. reflexivity.
rewrite add_union_singleton.
rewrite union_comm. rewrite <- minus_union. eapply agree_on_update_dead.
cset_tac.
eapply agree_on_incl. eapply IHXL; eauto.
instantiate (1:=lv). eapply incl_minus.
Qed.
Lemma update_id `{OrderedType Y} (m:X → Y) x `{Proper _ (_eq ==> _eq) m}
: @feq _ _ _eq (m [x <- m x]) m.
Proof.
intros y. lud. rewrite e; eauto.
Qed.
End MapUpdateList.
Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).
Lemma update_with_list_lookup_in_list X `{OrderedType X} B E
(Z:list X) (Y:list B) z
: length Z = length Y
→ z ∈ of_list Z
→ ∃ n y z', get Z n z' ∧ get Y n y ∧ E [Z <-- Y] z === y ∧ z === z'.
Proof.
intros. eapply length_length_eq in H0.
general induction H0; simpl in ×.
decide (z === x).
- ∃ 0, y, x; repeat split; eauto using get. lud.
- cset_tac'.
edestruct (IHlength_eq E z) as [? [? ]]; eauto; dcr.
∃ (S x0), x1, x2. eexists; repeat split; eauto using get.
lud. exfalso; eauto.
Qed.
Instance update_inst X `{OrderedType X} Y `{OrderedType Y} :
Proper ((@feq _ _ _eq) ==> _eq ==> _eq ==> (@feq _ _ _eq)) (@update X Y _).
Proof.
unfold respectful, Proper, update, feq; intros.
repeat cases; eqs; eauto.
exfalso. eapply H7. eapply H2.
exfalso. eapply H8. eapply H2.
Qed.
Instance update_inst_eq X `{OrderedType X} Y
: Proper ((@feq X Y eq) ==> eq ==> eq ==> (@feq _ _ eq)) (@update X Y _).
Proof.
unfold respectful, Proper, update, feq; intros.
repeat cases; eqs; eauto; congruence.
Qed.
Lemma update_with_list_id X `{OrderedType X} (l:list X)
: @feq _ _ _eq (update_with_list l l id) id.
Proof.
general induction l; simpl. reflexivity.
rewrite IHl. change a with (id a) at 2.
pose proof update_id. specialize (H0 X _ X _ id a).
eapply H0. firstorder.
Qed.
Lemma update_with_list_lookup_in {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y) Z Z' x
: length Z = length Z'
→ x ∈ of_list Z
→ f [ Z <-- Z' ] x ∈ of_list Z'.
Proof.
intros L. eapply length_length_eq in L.
general induction L; simpl in × |- ×.
eapply add_iff in H1. destruct H1.
lud; try eapply add_1; eauto.
lud. eapply add_1; eauto.
eapply add_iff. right. eapply IHL; eauto.
Qed.
Instance proper_update X `{OrderedType X} Y `{OrderedType Y} (ϱ:X → Y) (x : X) (y :Y)
: Proper (_eq ==> _eq) ϱ
→ Proper (_eq ==> _eq) (update ϱ x y) | 5.
Proof.
unfold Proper, respectful; intros; lud; intuition.
Qed.
Instance proper_update_with_list X `{OrderedType X} Y `{OrderedType Y} (f:X→Y) Z Z'
: Proper (_eq ==> _eq) f
→ Proper (_eq ==> _eq) (f [Z <-- Z']).
Proof.
intros.
general induction Z; eauto.
- destruct Z'; eauto. simpl.
eapply proper_update. eauto.
Qed.
Hint Resolve proper_update proper_update_with_list.
Lemma lookup_set_update_not_in_Z' X `{OrderedType X} Y `{OrderedType Y}
Z Z' (f: X→ Y) x
: f [Z <-- Z'] x ∉ of_list Z' → f [Z <-- Z'] x = f x.
Proof.
general induction Z; simpl in *; eauto.
destruct Z'; eauto.
lud. simpl in *; exfalso. cset_tac.
eapply IHZ; eauto. simpl in ×. cset_tac.
Qed.
Lemma lookup_set_update_not_in_Z X `{OrderedType X} Y
Z Z' (f: X→ Y) x
: x ∉ of_list Z → f [Z <-- Z'] x = f x.
Proof.
general induction Z; simpl in *; eauto.
destruct Z'; eauto.
lud. simpl in *; cset_tac.
eapply IHZ; eauto. cset_tac.
Qed.
Lemma lookup_set_update_not_in_Z'_not_in_Z {X} `{OrderedType X} {Y} `{OrderedType Y}
(f: X→ Y) x Z Z'
: length Z = length Z'
→ f [Z <-- Z'] x ∉ of_list Z'
→ Proper (_eq ==> _eq) f
→ x ∉ of_list Z.
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl in *; eauto.
- cset_tac; intuition.
- lud.
+ exfalso; cset_tac.
+ cset_tac; eauto.
Qed.
Lemma update_with_list_lookup_not_in {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) (Z:list X) (Z':list Y) x y
: x ∉ of_list Z
→ f [ Z <-- Z' ] x === y
→ f x === y.
Proof.
general induction Z; simpl in × |- *; eauto.
destruct Z'; eauto. lud.
- rewrite add_iff in H1;
exfalso; intuition.
- eapply IHZ; eauto. cset_tac.
Qed.
Lemma update_with_list_lookup_set_incl {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) Z Z' D
: length Z = length Z'
→ D ⊆ of_list Z
→ Proper (_eq ==> _eq) f
→ lookup_set (f [ Z <-- Z' ]) D ⊆ of_list Z'.
Proof.
intros. hnf; intros.
eapply lookup_set_spec in H4; try eapply proper_update_with_list; eauto.
destruct H4; dcr. rewrite H6. eapply update_with_list_lookup_in; eauto.
Qed.
Instance update_list_morphism {X} `{OrderedType X} {Y} `{OrderedType Y}
: Proper (@feq X _ _eq ==> @feq X _ _eq ==> eq ==> (@feq _ _ _eq)) (@update_list X _ Y).
Proof.
unfold Proper, respectful; intros. subst.
general induction y1. simpl. eauto. simpl.
rewrite IHy1; eauto. hnf; intros; lud. eapply H2.
Qed.
Lemma lookup_set_add_update {X} `{OrderedType X} {Y} `{OrderedType Y} (ϱ:X→Y) D x y
`{Proper _ (_eq ==> _eq) ϱ}
: x ∉ D
→ lookup_set (update ϱ x y) {x; D} [=] {y; lookup_set ϱ D}.
Proof.
intros. hnf; intros. lset_tac; lud; eauto.
- eexists x; lud; eauto.
- eexists x0; lud; eauto.
Qed.
Lemma lookup_update_same X `{OrderedType X} x Z (ϱ:X→X)
: x ∈ of_list Z
→ ϱ [Z <-- Z] x === x.
Proof.
general induction Z; simpl.
lud; eauto.
eapply IHZ. simpl in ×. cset_tac.
Qed.
Lemma lookup_set_update_union_minus X `{OrderedType X} Y `{OrderedType Y}
(f: X→Y) D x y `{Proper _ (_eq ==> _eq) f}
: lookup_set (update f x y) D \ {{y}} [=] lookup_set f (D \ {{x}}) \ {{ y }}.
Proof.
split; intros; lset_tac.
- lud; cset_tac; eauto.
- eexists x0; lud; cset_tac.
Qed.
Lemma lookup_set_update_union_minus_single X `{OrderedType X} Y `{OrderedType Y}
(f: X→Y) D x y `{Proper _ (_eq ==> _eq) f}
: lookup_set (update f x y) D \ singleton y [=] lookup_set f (D \ singleton x) \ singleton y.
Proof.
split; intros; lset_tac; eauto.
- lud; cset_tac; eauto.
- eexists x0; lud; cset_tac.
Qed.
Lemma lookup_set_update_union_minus_list X `{OrderedType X} Y `{OrderedType Y}
(f:X→Y) D Z Z' `{Proper _ (_eq ==> _eq) f}
: length Z = length Z'
→ lookup_set (f[ Z <-- Z']) D \ of_list Z' [=] lookup_set f (D \ of_list Z) \ of_list Z'.
Proof.
split; intros; lset_tac; eauto.
- rewrite H7 in H5.
eexists x; cset_tac'.
+ eapply lookup_set_update_not_in_Z'_not_in_Z in H5; eauto.
+ eapply lookup_set_update_not_in_Z' in H5; eauto.
rewrite <- H5; eauto.
- lud; cset_tac'.
eexists x; cset_tac'; eauto.
erewrite lookup_set_update_not_in_Z; eauto.
Qed.
Lemma update_with_list_lookup_list_eq {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) `{Proper _ (_eq ==> _eq) f} (Z:list X) Z' L
: ❬Z❭ = ❬L❭
→ NoDupA _eq Z
→ of_list Z [=] Z'
→ lookup_set (f [ Z <-- L ]) Z' [=] of_list L.
Proof.
intros Len ND EQ. rewrite <- EQ. clear EQ.
general induction Len; simpl in × |- *; dcr.
- rewrite lookup_set_empty; eauto.
- rewrite lookup_set_add; eauto. lud.
+ rewrite lookup_set_agree.
rewrite IHLen; eauto. eauto. eauto. eauto.
eapply agree_on_update_dead; eauto.
+ exfalso; eapply H2; reflexivity.
Qed.
Lemma update_with_list_lookup_list {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f} Z Z'
: length Z = length Z'
→ NoDupA _eq Z
→ lookup_set (f [ Z <-- Z' ]) (of_list Z) ⊆ of_list Z'.
Proof.
intros L. eapply length_length_eq in L.
general induction L; simpl in × |- *; dcr.
- rewrite lookup_set_empty; eauto.
- rewrite lookup_set_add; eauto. lud.
+ rewrite lookup_set_agree.
rewrite IHL; eauto. eauto. eauto.
eapply agree_on_update_dead; eauto.
+ exfalso; eapply H3; reflexivity.
Qed.
Lemma lookup_set_update_disj {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f} Z Z' G
: disj (of_list Z) G
→ lookup_set (f [ Z <-- Z' ]) G [=] lookup_set f G.
Proof.
intros. hnf; intros.
rewrite lookup_set_spec; eauto.
split; intros; dcr.
- rewrite H6. rewrite lookup_set_update_not_in_Z; eauto with cset.
- eapply lookup_set_spec in H3; eauto; dcr.
eexists x.
rewrite lookup_set_update_not_in_Z; eauto.
Qed.
Instance update_with_list_inst X `{OrderedType X} Y `{OrderedType Y} :
Proper (eq ==> (list_eq (option_eq eq)) ==> (@feq X (option Y) eq ) ==> (@feq _ _ eq))
(@update_with_list X _ (option Y)).
Proof.
unfold respectful, Proper; intros. subst.
general induction H2; simpl; eauto.
- destruct y; simpl; eauto.
- destruct y; simpl; eauto.
hnf; intros. lud.
inv H1; eauto.
eapply IHlist_eq; eauto.
Qed.
Lemma agree_on_update_list_dead X `{OrderedType X} Y (L:list X) (L':list Y) (V:X→Y)
V' D
: agree_on eq D V V'
→ disj (of_list L) D
→ agree_on eq D V (V'[L <-- L']).
Proof.
intros. hnf; intros.
rewrite lookup_set_update_not_in_Z; eauto.
Qed.
Lemma agree_on_update_list_dead_slot X `{OrderedType X} Y (L:list X) (L':list Y) (V:X→Y) (f:X→X)
`{Proper _ (_eq ==> _eq) f} V' D
: agree_on eq D V (fun x ⇒ V' (f x))
→ disj (of_list L) (map f D)
→ agree_on eq D V (fun x ⇒ V'[L <-- L'] (f x)).
Proof.
intros. hnf; intros.
rewrite lookup_set_update_not_in_Z; eauto.
intro. eauto with cset.
Qed.
Lemma update_with_list_lookup_in_list_first X `{OrderedType X} B E n
(Z:list X) (Y:list B) z
: length Z = length Y
→ get Z n z
→ (∀ n' z', n' < n → get Z n' z' → z' =/= z)
→ ∃ y, get Y n y ∧ E [Z <-- Y] z = y.
Proof.
intros. eapply length_length_eq in H0.
general induction H0; simpl in *; isabsurd.
inv H1.
- ∃ y; repeat split; eauto using get. lud. exfalso; eauto.
- edestruct (IHlength_eq E n0 z) as [? [? ]]; eauto using get; dcr.
+ intros. eapply (H2 (S n')); eauto using get. omega.
+ ∃ x0. eexists; repeat split; eauto using get.
exploit (H2 0); eauto using get; try omega.
lud.
Qed.
Lemma list_lookup_in_list_first X `{OrderedType X} B E
(Z:list X) (Y:list B) x y
: length Z = length Y
→ (E [Z <-- Y]) x = y
→ x ∈ of_list Z
→ ∃ n y', get Y n y' ∧ y === y' ∧ (∀ n' x', n' < n → get Z n' x' → x' =/= x).
Proof.
intros. length_equify.
general induction H0; simpl in *; isabsurd. decide (x0 === x).
- ∃ 0, y; repeat split; eauto using get. lud. intros; exfalso; omega.
- cset_tac'.
edestruct (IHlength_eq E x0) as [? [? ]]; eauto using get; dcr.
+ ∃ (S x1), x2. repeat split; eauto using get. lud; intuition.
intros. inv H4. intro; intuition. eapply H6; eauto. omega.
Qed.
Lemma lookup_set_update_with_list {X} `{OrderedType X} {Y} `{OrderedType Y}
Z Z' (f:X→Y) D `{Proper _ (_eq ==> _eq) f}
: of_list Z ⊆ D
→ NoDupA _eq Z
→ length Z = length Z'
→ of_list Z' ⊆ lookup_set (update_with_list Z Z' f) (of_list Z).
Proof.
intros; hnf; intros.
lset_tac.
length_equify.
general induction H4; simpl.
- simpl in ×. cset_tac'.
+ eexists x. lud; split; eauto.
+ edestruct IHlength_eq; eauto; dcr.
× invt NoDupA.
eexists x0. lud; eauto. cset_tac.
Qed.
Set Implicit Arguments.
Section MapUpdate'.
Open Scope fmap_scope.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Fixpoint update_with_list' XL YL (m:X → Y) :=
match XL, YL with
| x::XL, y::YL ⇒ update_with_list' XL YL (m[x <- y])
| _, _ ⇒ m
end.
Lemma update_with_list_agree' (XL:list X) (VL:list Y) E D
: length XL = length VL
→ NoDupA _eq XL
→ agree_on eq D (E [XL <-- VL]) (update_with_list' XL VL E).
Proof.
intros LEN UNIQ. length_equify.
general induction LEN; simpl in *; eauto.
- etransitivity. symmetry.
eapply update_nodup_commute_eq; eauto using length_eq_length.
eapply IHLEN; eauto.
Qed.
End MapUpdate'.
Notation "f [ w <-/- x ]" := (update_with_list' w x f) (at level 29, left associativity).
Require Import EqDec Computable Util LengthEq AutoIndTac Get LengthEq.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapLookup MapAgreement.
Set Implicit Arguments.
Section MapUpdate.
Open Scope fmap_scope.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Fixpoint update_list (m:X → Y) (f:X → Y) (L:list X) :=
match L with
| nil ⇒ m
| x::L ⇒ (update_list m f L) [x <- f x]
end.
Lemma update_list_agree_minus {R} `{Symmetric Y R} `{Transitive Y R} lv (E E' f:X → Y) XL
: agree_on R lv E' E
→ agree_on R (lv\of_list XL) (update_list E' f XL) E.
Proof.
intros. general induction XL; simpl.
rewrite minus_empty. eassumption.
rewrite add_union_singleton. rewrite union_comm. rewrite <- minus_union.
eapply agree_on_update_dead. cset_tac.
eauto using agree_on_incl, incl_minus.
Qed.
Corollary update_list_agree_self {R} `{Equivalence Y R} lv (E:X → Y) L f
: agree_on R (lv\of_list L) (update_list E f L) E.
Proof.
eapply update_list_agree_minus. reflexivity.
Qed.
Lemma update_list_no_upd (m:X → Y) f L x
: x ∉ of_list L
→ (update_list m f L) x === m x.
Proof.
intros. general induction L; simpl; eauto. lud.
+ exfalso. eapply H0. simpl in × |- ×. rewrite e. eapply add_1; eauto.
+ assert (¬x ∈ of_list L).
- intro. eapply H0. simpl. eapply add_2; eauto.
- eauto.
Qed.
Lemma update_list_upd R `{Equivalence Y R} (m:X → Y) f L x
: x ∈ of_list L
→ Proper (_eq ==> R) f
→ (update_list m f L) x === f x.
Proof.
intros. general induction L; simpl; eauto.
+ lud.
- rewrite e; eauto.
- eapply IHL; eauto. eapply zadd_3; eauto.
Qed.
End MapUpdate.
Section MapUpdateList.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Open Scope fmap_scope.
Fixpoint update_with_list XL YL (m:X → Y) :=
match XL, YL with
| x::XL, y::YL ⇒ (update_with_list XL YL m)[x <- y]
| _, _ ⇒ m
end.
Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).
Lemma update_nodup_commute `{OrderedType Y} (XL:list X) (VL:list Y) E D x y
: length XL = length VL
→ NoDupA _eq (x::XL)
→ agree_on _eq D (E [x <- y] [XL <-- VL]) (E [XL <-- VL] [x <- y]).
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl in × |- *; dcr; simpl in *; eauto.
hnf; intros. lud; invt NoDupA.
- exfalso; eauto.
- invt NoDupA.
etransitivity; [eapply IHlength_eq|]; eauto; lud.
- invt NoDupA.
etransitivity; [eapply IHlength_eq|]; eauto; lud.
Qed.
Lemma update_nodup_commute_eq (XL:list X) (VL:list Y) E D x y
: length XL = length VL
→ NoDupA _eq (x::XL)
→ agree_on eq D (E [x <- y] [XL <-- VL]) (E [XL <-- VL] [x <- y]).
Proof.
intros LEN UNIQ. length_equify.
general induction LEN; simpl in × |- *; dcr; simpl in *; eauto.
hnf; intros. lud; invt NoDupA.
- exfalso; eauto.
- invt NoDupA; etransitivity; [eapply IHLEN|]; eauto; lud.
- invt NoDupA; etransitivity; [eapply IHLEN|]; eauto; lud.
Qed.
Lemma update_with_list_no_update (E:X → Y) Y' Z x
: x ∉ of_list Z
→ (E [ Z <-- Y' ]) x = E x.
Proof.
intros. general induction Z; simpl in *; destruct Y'; eauto.
lud; cset_tac.
Qed.
Context `{Equivalence Y}.
Lemma update_with_list_agree lv (E E':X → Y) XL YL
: agree_on R (lv\of_list XL) E E'
→ length XL = length YL
→ agree_on R lv (E [ XL <-- YL]) (E' [ XL <-- YL ]).
Proof.
intros. eapply length_length_eq in H2.
general induction XL; simpl in × |- ×.
- rewrite (@minus_empty _ _ lv) in H1; eauto.
- eapply agree_on_update_same. reflexivity.
eapply IHXL; eauto.
eapply agree_on_incl; eauto. cset_tac; intuition.
Qed.
Lemma update_with_list_agree_preserve lv (E E':X → Y) XL YL
: agree_on R lv E E'
→ agree_on R lv (E [ XL <-- YL]) (E' [ XL <-- YL ]).
Proof.
intros.
general induction XL; destruct YL; simpl in × |- *; eauto.
eapply agree_on_update_same; eauto. reflexivity.
eapply agree_on_incl; eauto.
Qed.
Lemma update_with_list_agree_minus lv (E E':X → Y) XL YL
: agree_on R lv E' E
→ agree_on R (lv\of_list XL) (E' [ XL <-- YL ]) E.
Proof.
intros.
general induction XL; simpl.
- rewrite minus_empty. eassumption.
- destruct YL; simpl.
+ eapply agree_on_incl; eauto.
+ rewrite add_union_singleton. rewrite union_comm. rewrite <- minus_union.
eapply agree_on_update_dead. cset_tac.
eauto using agree_on_incl, incl_minus.
Qed.
Hint Resolve minus_single_singleton minus_single_singleton' minus_single_singleton''.
Lemma update_with_list_agree_inv lv (E E':X → Y) XL YL
: length XL = length YL
→ agree_on R lv (E' [ XL <-- YL ]) E
→ agree_on R (lv\of_list XL) E' E.
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl in × |- ×.
- eapply agree_on_incl; eauto.
- rewrite add_union_singleton. rewrite <- minus_union.
eapply IHlength_eq; eauto.
eapply agree_on_update_inv; eauto.
Qed.
Lemma update_with_list_agree_self `{Defaulted X} lv (E:X → Y) XL YL
: agree_on R (lv\of_list XL) (E [ XL <-- YL]) E.
Proof.
general induction XL; simpl. rewrite minus_empty. reflexivity.
destruct YL. reflexivity.
rewrite add_union_singleton.
rewrite union_comm. rewrite <- minus_union. eapply agree_on_update_dead.
cset_tac.
eapply agree_on_incl. eapply IHXL; eauto.
instantiate (1:=lv). eapply incl_minus.
Qed.
Lemma update_id `{OrderedType Y} (m:X → Y) x `{Proper _ (_eq ==> _eq) m}
: @feq _ _ _eq (m [x <- m x]) m.
Proof.
intros y. lud. rewrite e; eauto.
Qed.
End MapUpdateList.
Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).
Lemma update_with_list_lookup_in_list X `{OrderedType X} B E
(Z:list X) (Y:list B) z
: length Z = length Y
→ z ∈ of_list Z
→ ∃ n y z', get Z n z' ∧ get Y n y ∧ E [Z <-- Y] z === y ∧ z === z'.
Proof.
intros. eapply length_length_eq in H0.
general induction H0; simpl in ×.
decide (z === x).
- ∃ 0, y, x; repeat split; eauto using get. lud.
- cset_tac'.
edestruct (IHlength_eq E z) as [? [? ]]; eauto; dcr.
∃ (S x0), x1, x2. eexists; repeat split; eauto using get.
lud. exfalso; eauto.
Qed.
Instance update_inst X `{OrderedType X} Y `{OrderedType Y} :
Proper ((@feq _ _ _eq) ==> _eq ==> _eq ==> (@feq _ _ _eq)) (@update X Y _).
Proof.
unfold respectful, Proper, update, feq; intros.
repeat cases; eqs; eauto.
exfalso. eapply H7. eapply H2.
exfalso. eapply H8. eapply H2.
Qed.
Instance update_inst_eq X `{OrderedType X} Y
: Proper ((@feq X Y eq) ==> eq ==> eq ==> (@feq _ _ eq)) (@update X Y _).
Proof.
unfold respectful, Proper, update, feq; intros.
repeat cases; eqs; eauto; congruence.
Qed.
Lemma update_with_list_id X `{OrderedType X} (l:list X)
: @feq _ _ _eq (update_with_list l l id) id.
Proof.
general induction l; simpl. reflexivity.
rewrite IHl. change a with (id a) at 2.
pose proof update_id. specialize (H0 X _ X _ id a).
eapply H0. firstorder.
Qed.
Lemma update_with_list_lookup_in {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y) Z Z' x
: length Z = length Z'
→ x ∈ of_list Z
→ f [ Z <-- Z' ] x ∈ of_list Z'.
Proof.
intros L. eapply length_length_eq in L.
general induction L; simpl in × |- ×.
eapply add_iff in H1. destruct H1.
lud; try eapply add_1; eauto.
lud. eapply add_1; eauto.
eapply add_iff. right. eapply IHL; eauto.
Qed.
Instance proper_update X `{OrderedType X} Y `{OrderedType Y} (ϱ:X → Y) (x : X) (y :Y)
: Proper (_eq ==> _eq) ϱ
→ Proper (_eq ==> _eq) (update ϱ x y) | 5.
Proof.
unfold Proper, respectful; intros; lud; intuition.
Qed.
Instance proper_update_with_list X `{OrderedType X} Y `{OrderedType Y} (f:X→Y) Z Z'
: Proper (_eq ==> _eq) f
→ Proper (_eq ==> _eq) (f [Z <-- Z']).
Proof.
intros.
general induction Z; eauto.
- destruct Z'; eauto. simpl.
eapply proper_update. eauto.
Qed.
Hint Resolve proper_update proper_update_with_list.
Lemma lookup_set_update_not_in_Z' X `{OrderedType X} Y `{OrderedType Y}
Z Z' (f: X→ Y) x
: f [Z <-- Z'] x ∉ of_list Z' → f [Z <-- Z'] x = f x.
Proof.
general induction Z; simpl in *; eauto.
destruct Z'; eauto.
lud. simpl in *; exfalso. cset_tac.
eapply IHZ; eauto. simpl in ×. cset_tac.
Qed.
Lemma lookup_set_update_not_in_Z X `{OrderedType X} Y
Z Z' (f: X→ Y) x
: x ∉ of_list Z → f [Z <-- Z'] x = f x.
Proof.
general induction Z; simpl in *; eauto.
destruct Z'; eauto.
lud. simpl in *; cset_tac.
eapply IHZ; eauto. cset_tac.
Qed.
Lemma lookup_set_update_not_in_Z'_not_in_Z {X} `{OrderedType X} {Y} `{OrderedType Y}
(f: X→ Y) x Z Z'
: length Z = length Z'
→ f [Z <-- Z'] x ∉ of_list Z'
→ Proper (_eq ==> _eq) f
→ x ∉ of_list Z.
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl in *; eauto.
- cset_tac; intuition.
- lud.
+ exfalso; cset_tac.
+ cset_tac; eauto.
Qed.
Lemma update_with_list_lookup_not_in {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) (Z:list X) (Z':list Y) x y
: x ∉ of_list Z
→ f [ Z <-- Z' ] x === y
→ f x === y.
Proof.
general induction Z; simpl in × |- *; eauto.
destruct Z'; eauto. lud.
- rewrite add_iff in H1;
exfalso; intuition.
- eapply IHZ; eauto. cset_tac.
Qed.
Lemma update_with_list_lookup_set_incl {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) Z Z' D
: length Z = length Z'
→ D ⊆ of_list Z
→ Proper (_eq ==> _eq) f
→ lookup_set (f [ Z <-- Z' ]) D ⊆ of_list Z'.
Proof.
intros. hnf; intros.
eapply lookup_set_spec in H4; try eapply proper_update_with_list; eauto.
destruct H4; dcr. rewrite H6. eapply update_with_list_lookup_in; eauto.
Qed.
Instance update_list_morphism {X} `{OrderedType X} {Y} `{OrderedType Y}
: Proper (@feq X _ _eq ==> @feq X _ _eq ==> eq ==> (@feq _ _ _eq)) (@update_list X _ Y).
Proof.
unfold Proper, respectful; intros. subst.
general induction y1. simpl. eauto. simpl.
rewrite IHy1; eauto. hnf; intros; lud. eapply H2.
Qed.
Lemma lookup_set_add_update {X} `{OrderedType X} {Y} `{OrderedType Y} (ϱ:X→Y) D x y
`{Proper _ (_eq ==> _eq) ϱ}
: x ∉ D
→ lookup_set (update ϱ x y) {x; D} [=] {y; lookup_set ϱ D}.
Proof.
intros. hnf; intros. lset_tac; lud; eauto.
- eexists x; lud; eauto.
- eexists x0; lud; eauto.
Qed.
Lemma lookup_update_same X `{OrderedType X} x Z (ϱ:X→X)
: x ∈ of_list Z
→ ϱ [Z <-- Z] x === x.
Proof.
general induction Z; simpl.
lud; eauto.
eapply IHZ. simpl in ×. cset_tac.
Qed.
Lemma lookup_set_update_union_minus X `{OrderedType X} Y `{OrderedType Y}
(f: X→Y) D x y `{Proper _ (_eq ==> _eq) f}
: lookup_set (update f x y) D \ {{y}} [=] lookup_set f (D \ {{x}}) \ {{ y }}.
Proof.
split; intros; lset_tac.
- lud; cset_tac; eauto.
- eexists x0; lud; cset_tac.
Qed.
Lemma lookup_set_update_union_minus_single X `{OrderedType X} Y `{OrderedType Y}
(f: X→Y) D x y `{Proper _ (_eq ==> _eq) f}
: lookup_set (update f x y) D \ singleton y [=] lookup_set f (D \ singleton x) \ singleton y.
Proof.
split; intros; lset_tac; eauto.
- lud; cset_tac; eauto.
- eexists x0; lud; cset_tac.
Qed.
Lemma lookup_set_update_union_minus_list X `{OrderedType X} Y `{OrderedType Y}
(f:X→Y) D Z Z' `{Proper _ (_eq ==> _eq) f}
: length Z = length Z'
→ lookup_set (f[ Z <-- Z']) D \ of_list Z' [=] lookup_set f (D \ of_list Z) \ of_list Z'.
Proof.
split; intros; lset_tac; eauto.
- rewrite H7 in H5.
eexists x; cset_tac'.
+ eapply lookup_set_update_not_in_Z'_not_in_Z in H5; eauto.
+ eapply lookup_set_update_not_in_Z' in H5; eauto.
rewrite <- H5; eauto.
- lud; cset_tac'.
eexists x; cset_tac'; eauto.
erewrite lookup_set_update_not_in_Z; eauto.
Qed.
Lemma update_with_list_lookup_list_eq {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) `{Proper _ (_eq ==> _eq) f} (Z:list X) Z' L
: ❬Z❭ = ❬L❭
→ NoDupA _eq Z
→ of_list Z [=] Z'
→ lookup_set (f [ Z <-- L ]) Z' [=] of_list L.
Proof.
intros Len ND EQ. rewrite <- EQ. clear EQ.
general induction Len; simpl in × |- *; dcr.
- rewrite lookup_set_empty; eauto.
- rewrite lookup_set_add; eauto. lud.
+ rewrite lookup_set_agree.
rewrite IHLen; eauto. eauto. eauto. eauto.
eapply agree_on_update_dead; eauto.
+ exfalso; eapply H2; reflexivity.
Qed.
Lemma update_with_list_lookup_list {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f} Z Z'
: length Z = length Z'
→ NoDupA _eq Z
→ lookup_set (f [ Z <-- Z' ]) (of_list Z) ⊆ of_list Z'.
Proof.
intros L. eapply length_length_eq in L.
general induction L; simpl in × |- *; dcr.
- rewrite lookup_set_empty; eauto.
- rewrite lookup_set_add; eauto. lud.
+ rewrite lookup_set_agree.
rewrite IHL; eauto. eauto. eauto.
eapply agree_on_update_dead; eauto.
+ exfalso; eapply H3; reflexivity.
Qed.
Lemma lookup_set_update_disj {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f} Z Z' G
: disj (of_list Z) G
→ lookup_set (f [ Z <-- Z' ]) G [=] lookup_set f G.
Proof.
intros. hnf; intros.
rewrite lookup_set_spec; eauto.
split; intros; dcr.
- rewrite H6. rewrite lookup_set_update_not_in_Z; eauto with cset.
- eapply lookup_set_spec in H3; eauto; dcr.
eexists x.
rewrite lookup_set_update_not_in_Z; eauto.
Qed.
Instance update_with_list_inst X `{OrderedType X} Y `{OrderedType Y} :
Proper (eq ==> (list_eq (option_eq eq)) ==> (@feq X (option Y) eq ) ==> (@feq _ _ eq))
(@update_with_list X _ (option Y)).
Proof.
unfold respectful, Proper; intros. subst.
general induction H2; simpl; eauto.
- destruct y; simpl; eauto.
- destruct y; simpl; eauto.
hnf; intros. lud.
inv H1; eauto.
eapply IHlist_eq; eauto.
Qed.
Lemma agree_on_update_list_dead X `{OrderedType X} Y (L:list X) (L':list Y) (V:X→Y)
V' D
: agree_on eq D V V'
→ disj (of_list L) D
→ agree_on eq D V (V'[L <-- L']).
Proof.
intros. hnf; intros.
rewrite lookup_set_update_not_in_Z; eauto.
Qed.
Lemma agree_on_update_list_dead_slot X `{OrderedType X} Y (L:list X) (L':list Y) (V:X→Y) (f:X→X)
`{Proper _ (_eq ==> _eq) f} V' D
: agree_on eq D V (fun x ⇒ V' (f x))
→ disj (of_list L) (map f D)
→ agree_on eq D V (fun x ⇒ V'[L <-- L'] (f x)).
Proof.
intros. hnf; intros.
rewrite lookup_set_update_not_in_Z; eauto.
intro. eauto with cset.
Qed.
Lemma update_with_list_lookup_in_list_first X `{OrderedType X} B E n
(Z:list X) (Y:list B) z
: length Z = length Y
→ get Z n z
→ (∀ n' z', n' < n → get Z n' z' → z' =/= z)
→ ∃ y, get Y n y ∧ E [Z <-- Y] z = y.
Proof.
intros. eapply length_length_eq in H0.
general induction H0; simpl in *; isabsurd.
inv H1.
- ∃ y; repeat split; eauto using get. lud. exfalso; eauto.
- edestruct (IHlength_eq E n0 z) as [? [? ]]; eauto using get; dcr.
+ intros. eapply (H2 (S n')); eauto using get. omega.
+ ∃ x0. eexists; repeat split; eauto using get.
exploit (H2 0); eauto using get; try omega.
lud.
Qed.
Lemma list_lookup_in_list_first X `{OrderedType X} B E
(Z:list X) (Y:list B) x y
: length Z = length Y
→ (E [Z <-- Y]) x = y
→ x ∈ of_list Z
→ ∃ n y', get Y n y' ∧ y === y' ∧ (∀ n' x', n' < n → get Z n' x' → x' =/= x).
Proof.
intros. length_equify.
general induction H0; simpl in *; isabsurd. decide (x0 === x).
- ∃ 0, y; repeat split; eauto using get. lud. intros; exfalso; omega.
- cset_tac'.
edestruct (IHlength_eq E x0) as [? [? ]]; eauto using get; dcr.
+ ∃ (S x1), x2. repeat split; eauto using get. lud; intuition.
intros. inv H4. intro; intuition. eapply H6; eauto. omega.
Qed.
Lemma lookup_set_update_with_list {X} `{OrderedType X} {Y} `{OrderedType Y}
Z Z' (f:X→Y) D `{Proper _ (_eq ==> _eq) f}
: of_list Z ⊆ D
→ NoDupA _eq Z
→ length Z = length Z'
→ of_list Z' ⊆ lookup_set (update_with_list Z Z' f) (of_list Z).
Proof.
intros; hnf; intros.
lset_tac.
length_equify.
general induction H4; simpl.
- simpl in ×. cset_tac'.
+ eexists x. lud; split; eauto.
+ edestruct IHlength_eq; eauto; dcr.
× invt NoDupA.
eexists x0. lud; eauto. cset_tac.
Qed.
Set Implicit Arguments.
Section MapUpdate'.
Open Scope fmap_scope.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Fixpoint update_with_list' XL YL (m:X → Y) :=
match XL, YL with
| x::XL, y::YL ⇒ update_with_list' XL YL (m[x <- y])
| _, _ ⇒ m
end.
Lemma update_with_list_agree' (XL:list X) (VL:list Y) E D
: length XL = length VL
→ NoDupA _eq XL
→ agree_on eq D (E [XL <-- VL]) (update_with_list' XL VL E).
Proof.
intros LEN UNIQ. length_equify.
general induction LEN; simpl in *; eauto.
- etransitivity. symmetry.
eapply update_nodup_commute_eq; eauto using length_eq_length.
eapply IHLEN; eauto.
Qed.
End MapUpdate'.
Notation "f [ w <-/- x ]" := (update_with_list' w x f) (at level 29, left associativity).