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. intro; decompose records; eauto.
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.
+ simpl in *; cset_tac; firstorder.
+ 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_unique_commute `{OrderedType Y} (XL:list X) (VL:list Y) E D x y
: length XL = length VL
→ unique (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. reflexivity.
hnf; intros. lud. hnf in H2; simpl in ×.
dcr. exfalso. eapply H8. econstructor. eapply H5.
exploit (IHlength_eq H0 E {x1} x0 y0). simpl in *; intuition.
hnf; intros. eapply H9. econstructor 2; eauto.
exploit X0. cset_tac; reflexivity. rewrite X1. lud.
exploit (IHlength_eq H0 E {x1} x0 y0). simpl in *; intuition.
hnf; intros. eapply H8. econstructor 2; eauto.
exploit X0. cset_tac; reflexivity. rewrite X1. lud.
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.
inv H2. eapply agree_on_update_same. eapply H0; eauto.
eapply IHXL; eauto. rewrite minus_union; eauto.
rewrite add_union_singleton. rewrite (empty_union_2 (s:=∅)); eauto.
rewrite <- add_union_singleton; eauto.
eapply SetInterface.empty_1.
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; destruct Y´; eauto.
lud.
+ exfalso. eapply H1. simpl; cset_tac; intuition.
+ simpl in H1. assert (x ∉ of_list Z); eauto.
- cset_tac; intuition.
Qed.
Lemma update_with_list_agree_minus lv (E E´:X → Y) XL YL
: length XL = length YL
→ agree_on R lv E´ E
→ agree_on R (lv\of_list XL) (E´ [ XL <-- YL ]) E.
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl. rewrite minus_empty. eassumption.
rewrite add_union_singleton. rewrite union_comm. rewrite <- minus_union.
eapply agree_on_update_dead.
cset_tac. intro; decompose records; eauto.
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_incl; 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. intro; decompose records; eauto.
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 *; isabsurd.
decide (z === x).
- ∃ 0, y, x; repeat split; eauto using get. lud.
- cset_tac; intuition.
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 destruct if; eqs; eauto.
exfalso. eapply H7. eapply H2.
exfalso. eapply H8. eapply H2.
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 × |- ×. exfalso; cset_tac; firstorder.
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).
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; intuition.
- destruct Z´; intuition. simpl.
eapply proper_update. eauto.
Qed.
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; intuition.
eapply IHZ; eauto. simpl in ×. cset_tac; intuition.
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; intuition.
eapply IHZ; eauto. cset_tac; intuition.
Qed.
Lemma lookup_set_update_not_in_Z´_not_in_Z {X} `{OrderedType X} {Y} `{OrderedType Y}
(f: X→ Y) `{Proper _ (_eq ==> _eq) f} x Z Z´
: length Z = length Z´
→ f [Z <-- Z´] x ∉ of_list Z´ → x ∉ of_list Z.
Proof.
intros. eapply length_length_eq in H2.
general induction H2; simpl in *; eauto.
- cset_tac; intuition.
- lud.
+ exfalso; cset_tac; intuition.
+ cset_tac; intuition; 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; firstorder.
eapply IHZ; eauto. intro. eapply H1. eapply add_2; eauto.
Qed.
Lemma update_with_list_lookup_set_incl {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) Z Z´ `{Proper _ (_eq ==> _eq) f} D
: length Z = length Z´
→ D ⊆ of_list Z
→ 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. cset_tac.
repeat rewrite lookup_set_spec; try (now intuition).
split; intros; cset_tac.
lud; intuition.
right. eauto.
destruct H3.
eexists x. intuition. lud. intuition.
destruct H3; dcr. eexists x0.
intuition. lud. exfalso. eapply H2. cset_tac.
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; isabsurd.
lud; eauto.
eapply IHZ. simpl in ×. cset_tac; intuition.
Qed.
Hint Resolve proper_update proper_update_with_list.
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; cset_tac.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
lud; cset_tac; eauto; intuition. eapply lookup_set_spec; eauto.
eexists x0; cset_tac; eauto.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
lud; cset_tac; eauto; intuition. eapply lookup_set_spec; eauto.
eexists x0; cset_tac; eauto. lud; intuition.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
- eauto.
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; cset_tac; eauto.
- eapply lookup_set_spec in H4; destruct H4; dcr; eauto.
rewrite H6 in H5.
eapply lookup_set_spec; eauto.
eexists x; cset_tac; intuition; eauto.
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 in H6; eauto.
- eapply lookup_set_spec in H4; destruct H4; dcr; eauto.
lud; cset_tac; eauto; intuition. eapply lookup_set_spec; eauto.
eexists x; cset_tac; eauto.
erewrite lookup_set_update_not_in_Z; eauto.
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´
→ unique 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. intro. eapply InA_in in H2. eauto.
+ exfalso; eapply H2; reflexivity.
Qed.
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. intro; decompose records; eauto.
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.
+ simpl in *; cset_tac; firstorder.
+ 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_unique_commute `{OrderedType Y} (XL:list X) (VL:list Y) E D x y
: length XL = length VL
→ unique (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. reflexivity.
hnf; intros. lud. hnf in H2; simpl in ×.
dcr. exfalso. eapply H8. econstructor. eapply H5.
exploit (IHlength_eq H0 E {x1} x0 y0). simpl in *; intuition.
hnf; intros. eapply H9. econstructor 2; eauto.
exploit X0. cset_tac; reflexivity. rewrite X1. lud.
exploit (IHlength_eq H0 E {x1} x0 y0). simpl in *; intuition.
hnf; intros. eapply H8. econstructor 2; eauto.
exploit X0. cset_tac; reflexivity. rewrite X1. lud.
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.
inv H2. eapply agree_on_update_same. eapply H0; eauto.
eapply IHXL; eauto. rewrite minus_union; eauto.
rewrite add_union_singleton. rewrite (empty_union_2 (s:=∅)); eauto.
rewrite <- add_union_singleton; eauto.
eapply SetInterface.empty_1.
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; destruct Y´; eauto.
lud.
+ exfalso. eapply H1. simpl; cset_tac; intuition.
+ simpl in H1. assert (x ∉ of_list Z); eauto.
- cset_tac; intuition.
Qed.
Lemma update_with_list_agree_minus lv (E E´:X → Y) XL YL
: length XL = length YL
→ agree_on R lv E´ E
→ agree_on R (lv\of_list XL) (E´ [ XL <-- YL ]) E.
Proof.
intros. eapply length_length_eq in H1.
general induction H1; simpl. rewrite minus_empty. eassumption.
rewrite add_union_singleton. rewrite union_comm. rewrite <- minus_union.
eapply agree_on_update_dead.
cset_tac. intro; decompose records; eauto.
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_incl; 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. intro; decompose records; eauto.
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 *; isabsurd.
decide (z === x).
- ∃ 0, y, x; repeat split; eauto using get. lud.
- cset_tac; intuition.
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 destruct if; eqs; eauto.
exfalso. eapply H7. eapply H2.
exfalso. eapply H8. eapply H2.
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 × |- ×. exfalso; cset_tac; firstorder.
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).
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; intuition.
- destruct Z´; intuition. simpl.
eapply proper_update. eauto.
Qed.
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; intuition.
eapply IHZ; eauto. simpl in ×. cset_tac; intuition.
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; intuition.
eapply IHZ; eauto. cset_tac; intuition.
Qed.
Lemma lookup_set_update_not_in_Z´_not_in_Z {X} `{OrderedType X} {Y} `{OrderedType Y}
(f: X→ Y) `{Proper _ (_eq ==> _eq) f} x Z Z´
: length Z = length Z´
→ f [Z <-- Z´] x ∉ of_list Z´ → x ∉ of_list Z.
Proof.
intros. eapply length_length_eq in H2.
general induction H2; simpl in *; eauto.
- cset_tac; intuition.
- lud.
+ exfalso; cset_tac; intuition.
+ cset_tac; intuition; 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; firstorder.
eapply IHZ; eauto. intro. eapply H1. eapply add_2; eauto.
Qed.
Lemma update_with_list_lookup_set_incl {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) Z Z´ `{Proper _ (_eq ==> _eq) f} D
: length Z = length Z´
→ D ⊆ of_list Z
→ 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. cset_tac.
repeat rewrite lookup_set_spec; try (now intuition).
split; intros; cset_tac.
lud; intuition.
right. eauto.
destruct H3.
eexists x. intuition. lud. intuition.
destruct H3; dcr. eexists x0.
intuition. lud. exfalso. eapply H2. cset_tac.
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; isabsurd.
lud; eauto.
eapply IHZ. simpl in ×. cset_tac; intuition.
Qed.
Hint Resolve proper_update proper_update_with_list.
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; cset_tac.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
lud; cset_tac; eauto; intuition. eapply lookup_set_spec; eauto.
eexists x0; cset_tac; eauto.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
lud; cset_tac; eauto; intuition. eapply lookup_set_spec; eauto.
eexists x0; cset_tac; eauto. lud; intuition.
- eapply lookup_set_spec in H3; destruct H3; dcr; eauto.
- eauto.
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; cset_tac; eauto.
- eapply lookup_set_spec in H4; destruct H4; dcr; eauto.
rewrite H6 in H5.
eapply lookup_set_spec; eauto.
eexists x; cset_tac; intuition; eauto.
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 in H6; eauto.
- eapply lookup_set_spec in H4; destruct H4; dcr; eauto.
lud; cset_tac; eauto; intuition. eapply lookup_set_spec; eauto.
eexists x; cset_tac; eauto.
erewrite lookup_set_update_not_in_Z; eauto.
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´
→ unique 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. intro. eapply InA_in in H2. eauto.
+ exfalso; eapply H2; reflexivity.
Qed.