Commit 60001769 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 3f33781f
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2019-07-05.0.d392b7a6") | (= "dev") } "coq-iris" { (= "dev.2019-08-13.5.c1d6ef7f") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -80,7 +80,7 @@ Section proof. ...@@ -80,7 +80,7 @@ Section proof.
Proof. Proof.
rewrite /bag_contents. apply bi.wand_intro_r. rewrite /bag_contents. apply bi.wand_intro_r.
rewrite -own_op own_valid uPred.discrete_valid. rewrite -own_op own_valid uPred.discrete_valid.
f_equiv=> /=. rewrite pair_op. f_equiv=> /=. rewrite -pair_op.
by intros [_ ?%agree_op_invL']. by intros [_ ?%agree_op_invL'].
Qed. Qed.
...@@ -90,7 +90,7 @@ Section proof. ...@@ -90,7 +90,7 @@ Section proof.
iIntros "[Hb1 Hb2]". iIntros "[Hb1 Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-. iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (own_update_2 with "Hb1 Hb2") as "Hb". iMod (own_update_2 with "Hb1 Hb2") as "Hb".
{ rewrite pair_op frac_op'. { rewrite -pair_op frac_op'.
assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2. assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
by apply (cmra_update_exclusive (1%Qp, to_agree Y)). } by apply (cmra_update_exclusive (1%Qp, to_agree Y)). }
iDestruct "Hb" as "[Hb1 Hb2]". iDestruct "Hb" as "[Hb1 Hb2]".
......
...@@ -32,7 +32,7 @@ Qed. ...@@ -32,7 +32,7 @@ Qed.
Global Instance SET_RES_fractional `{saG Σ} γ v : Fractional (fun q => SET_RES γ q v)%I. Global Instance SET_RES_fractional `{saG Σ} γ v : Fractional (fun q => SET_RES γ q v)%I.
Proof. Proof.
intros p q. rewrite /SET_RES. intros p q. rewrite /SET_RES.
rewrite -own_op Cinr_op Cinl_op pair_op agree_idemp. f_equiv. rewrite -own_op -Cinr_op -Cinl_op -pair_op agree_idemp. f_equiv.
Qed. Qed.
Global Instance SET_RES_as_fractional `{saG Σ} γ q v: Global Instance SET_RES_as_fractional `{saG Σ} γ q v:
AsFractional (SET_RES γ q v) (fun q => SET_RES γ q v)%I q. AsFractional (SET_RES γ q v) (fun q => SET_RES γ q v)%I q.
...@@ -65,7 +65,7 @@ Lemma SET_RES_agree `{saG Σ} (γ: gname) (q q': Qp) (v w: val) : ...@@ -65,7 +65,7 @@ Lemma SET_RES_agree `{saG Σ} (γ: gname) (q q': Qp) (v w: val) :
Proof. Proof.
iIntros "Hs1 Hs2". iIntros "Hs1 Hs2".
iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo. iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
iPureIntro. rewrite Cinr_op Cinl_op pair_op in Hfoo. iPureIntro. rewrite -Cinr_op -Cinl_op -pair_op in Hfoo.
by destruct Hfoo as [_ ?%agree_op_invL']. by destruct Hfoo as [_ ?%agree_op_invL'].
Qed. Qed.
Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) : Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) :
...@@ -73,7 +73,7 @@ Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) : ...@@ -73,7 +73,7 @@ Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) :
Proof. Proof.
iIntros "Hs1 Hs2". iIntros "Hs1 Hs2".
iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo. iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
iPureIntro. rewrite Cinr_op Cinr_op in Hfoo. iPureIntro. rewrite -Cinr_op -Cinr_op in Hfoo.
by apply agree_op_invL'. by apply agree_op_invL'.
Qed. Qed.
Lemma INIT_SET_RES `{saG Σ} (v: val) γ : Lemma INIT_SET_RES `{saG Σ} (v: val) γ :
......
...@@ -109,7 +109,7 @@ Section proof. ...@@ -109,7 +109,7 @@ Section proof.
Proof. Proof.
rewrite /bag_contents. apply bi.wand_intro_r. rewrite /bag_contents. apply bi.wand_intro_r.
rewrite -own_op own_valid uPred.discrete_valid. rewrite -own_op own_valid uPred.discrete_valid.
f_equiv=> /=. rewrite pair_op. f_equiv=> /=. rewrite -pair_op.
by intros [_ ?%agree_op_invL']. by intros [_ ?%agree_op_invL'].
Qed. Qed.
...@@ -119,7 +119,7 @@ Section proof. ...@@ -119,7 +119,7 @@ Section proof.
iIntros "[Hb1 Hb2]". iIntros "[Hb1 Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-. iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iMod (own_update_2 with "Hb1 Hb2") as "Hb". iMod (own_update_2 with "Hb1 Hb2") as "Hb".
{ rewrite pair_op frac_op'. { rewrite -pair_op frac_op'.
assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2. assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
by apply (cmra_update_exclusive (1%Qp, to_agree Y)). } by apply (cmra_update_exclusive (1%Qp, to_agree Y)). }
iDestruct "Hb" as "[Hb1 Hb2]". iDestruct "Hb" as "[Hb1 Hb2]".
......
...@@ -49,7 +49,7 @@ Section atomic_sync. ...@@ -49,7 +49,7 @@ Section atomic_sync.
Proof. Proof.
iIntros (Hsync g0 ϕ ret) "Hϕ Hret". iIntros (Hsync g0 ϕ ret) "Hϕ Hret".
iMod (own_alloc (((1 / 2)%Qp, to_agree g0) ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]". iMod (own_alloc (((1 / 2)%Qp, to_agree g0) ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]".
{ by rewrite pair_op agree_idemp. } { by rewrite -pair_op agree_idemp. }
iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[Hg1 Hϕ]")=>//. iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
{ iExists g0. by iFrame. } { iExists g0. by iFrame. }
iNext. iIntros (s) "#Hsyncer". iApply "Hret". iNext. iIntros (s) "#Hsyncer". iApply "Hret".
...@@ -77,7 +77,7 @@ Section atomic_sync. ...@@ -77,7 +77,7 @@ Section atomic_sync.
iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ((1 / 2)%Qp, to_agree g')))%I iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ((1 / 2)%Qp, to_agree g')))%I
with "[Hg]" as ">[Hg1 Hg2]". with "[Hg]" as ">[Hg1 Hg2]".
{ iApply own_update; last by iAssumption. { iApply own_update; last by iAssumption.
apply cmra_update_exclusive. by rewrite pair_op agree_idemp. } apply cmra_update_exclusive. by rewrite -pair_op agree_idemp. }
iMod ("Hvs2" with "[Hg1 Hβ]"). iMod ("Hvs2" with "[Hg1 Hβ]").
{ iExists g'. iFrame. } { iExists g'. iFrame. }
iModIntro. iSplitL "Hg2 Hϕ'"; last done. iModIntro. iSplitL "Hg2 Hϕ'"; last done.
......
...@@ -11,11 +11,11 @@ Import uPred. ...@@ -11,11 +11,11 @@ Import uPred.
Section lemmas. Section lemmas.
Lemma pair_l_frac_op' (p q: Qp) (g g': val): Lemma pair_l_frac_op' (p q: Qp) (g g': val):
((p + q)%Qp, to_agree g') ~~> (((p, to_agree g') (q, to_agree g'))). ((p + q)%Qp, to_agree g') ~~> (((p, to_agree g') (q, to_agree g'))).
Proof. by rewrite pair_op agree_idemp frac_op'. Qed. Proof. by rewrite -pair_op agree_idemp frac_op'. Qed.
Lemma pair_l_frac_op_1' (g g': val): Lemma pair_l_frac_op_1' (g g': val):
(1%Qp, to_agree g') ~~> (((1/2)%Qp, to_agree g') ((1/2)%Qp, to_agree g')). (1%Qp, to_agree g') ~~> (((1/2)%Qp, to_agree g') ((1/2)%Qp, to_agree g')).
Proof. by rewrite pair_op agree_idemp frac_op' Qp_div_2. Qed. Proof. by rewrite -pair_op agree_idemp frac_op' Qp_div_2. Qed.
End lemmas. End lemmas.
......
...@@ -19,7 +19,7 @@ Proof. induction n as [|n IH]; [ done | by rewrite /= -IH ]. Qed. ...@@ -19,7 +19,7 @@ Proof. induction n as [|n IH]; [ done | by rewrite /= -IH ]. Qed.
Lemma map_imap_id {A} (m : gmap nat A) : Lemma map_imap_id {A} (m : gmap nat A) :
map_imap (λ _ e, Some e) m = m. map_imap (λ _ e, Some e) m = m.
Proof. Proof.
apply map_eq. intros i. rewrite lookup_imap. by destruct (m !! i). apply map_eq. intros i. rewrite map_lookup_imap. by destruct (m !! i).
Qed. Qed.
Lemma map_imap_insert {A B} (f : nat A option B) (i : nat) (v : A) (m : gmap nat A) : Lemma map_imap_insert {A B} (f : nat A option B) (i : nat) (v : A) (m : gmap nat A) :
...@@ -29,18 +29,18 @@ Lemma map_imap_insert {A B} (f : nat → A → option B) (i : nat) (v : A) (m : ...@@ -29,18 +29,18 @@ Lemma map_imap_insert {A B} (f : nat → A → option B) (i : nat) (v : A) (m :
end. end.
Proof. Proof.
destruct (f i v) as [w|] eqn:Hw. destruct (f i v) as [w|] eqn:Hw.
- apply map_eq. intros k. rewrite lookup_imap. - apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i]. destruct (decide (k = i)) as [->|Hk_not_i].
+ by rewrite lookup_insert lookup_insert /=. + by rewrite lookup_insert lookup_insert /=.
+ rewrite lookup_insert_ne; last done. + rewrite lookup_insert_ne; last done.
rewrite lookup_insert_ne; last done. rewrite lookup_insert_ne; last done.
by rewrite lookup_imap. by rewrite map_lookup_imap.
- apply map_eq. intros k. rewrite lookup_imap. - apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i]. destruct (decide (k = i)) as [->|Hk_not_i].
+ by rewrite lookup_insert lookup_delete /=. + by rewrite lookup_insert lookup_delete /=.
+ rewrite lookup_insert_ne; last done. + rewrite lookup_insert_ne; last done.
rewrite lookup_delete_ne; last done. rewrite lookup_delete_ne; last done.
by rewrite lookup_imap. by rewrite map_lookup_imap.
Qed. Qed.
Lemma map_imap_ext {A B} (f1 f2 : nat A option B) (m1 m2 : gmap nat A) : Lemma map_imap_ext {A B} (f1 f2 : nat A option B) (m1 m2 : gmap nat A) :
...@@ -49,7 +49,7 @@ Lemma map_imap_ext {A B} (f1 f2 : nat → A → option B) (m1 m2 : gmap nat A) : ...@@ -49,7 +49,7 @@ Lemma map_imap_ext {A B} (f1 f2 : nat → A → option B) (m1 m2 : gmap nat A) :
map_imap f1 m1 = map_imap f2 m2. map_imap f1 m1 = map_imap f2 m2.
Proof. Proof.
intros Hdom HExt. apply map_eq. intros i. intros Hdom HExt. apply map_eq. intros i.
rewrite lookup_imap lookup_imap. rewrite map_lookup_imap map_lookup_imap.
destruct (m1 !! i) as [v1|] eqn:Hi1. destruct (m1 !! i) as [v1|] eqn:Hi1.
+ specialize (HExt i v1 Hi1). + specialize (HExt i v1 Hi1).
destruct (m2 !! i); by inversion HExt. destruct (m2 !! i); by inversion HExt.
...@@ -606,7 +606,7 @@ Lemma shot_not_equiv_not_shot' e : shot ≢ not_shot ⋅ e. ...@@ -606,7 +606,7 @@ Lemma shot_not_equiv_not_shot' e : shot ≢ not_shot ⋅ e.
Proof. Proof.
intros H. rewrite /shot /not_shot in H. intros H. rewrite /shot /not_shot in H.
destruct e as [e|]; first destruct e. destruct e as [e|]; first destruct e.
- rewrite -Some_op Cinl_op in H. - rewrite -Some_op -Cinl_op in H.
inversion H as [x y Habsurd|]; inversion Habsurd. inversion H as [x y Habsurd|]; inversion Habsurd.
- rewrite -Some_op in H. compute in H. - rewrite -Some_op in H. compute in H.
inversion H as [x y HAbsurd|]. inversion HAbsurd. inversion H as [x y HAbsurd|]. inversion HAbsurd.
...@@ -1421,7 +1421,7 @@ Qed. ...@@ -1421,7 +1421,7 @@ Qed.
Lemma map_imap_helped_nil slots : map_imap (helped []) slots = slots. Lemma map_imap_helped_nil slots : map_imap (helped []) slots = slots.
Proof. Proof.
apply map_eq. intros i. rewrite lookup_imap. apply map_eq. intros i. rewrite map_lookup_imap.
destruct (slots !! i) as [d|] eqn:HEq. destruct (slots !! i) as [d|] eqn:HEq.
- rewrite /helped /= HEq. by destruct (state_of d). - rewrite /helped /= HEq. by destruct (state_of d).
- by rewrite /= HEq. - by rewrite /= HEq.
...@@ -1445,7 +1445,7 @@ Proof. ...@@ -1445,7 +1445,7 @@ Proof.
{ simpl in HND. apply NoDup_cons in HND as (HND & _). { simpl in HND. apply NoDup_cons in HND as (HND & _).
apply not_elem_of_app in HND as (_ & HND). apply not_elem_of_app in HND as (_ & HND).
by apply not_elem_of_cons in HND as (HND & _). } by apply not_elem_of_cons in HND as (HND & _). }
rewrite /get_value lookup_imap lookup_insert_ne; last done. rewrite /get_value map_lookup_imap lookup_insert_ne; last done.
destruct (slots !! pref_hd) as [[[lp sp] wp]|]; last done. destruct (slots !! pref_hd) as [[[lp sp] wp]|]; last done.
destruct sp; try done. rewrite /= /helped /=. destruct sp; try done. rewrite /= /helped /=.
rewrite decide_False; first done. rewrite decide_False; first done.
...@@ -1470,7 +1470,7 @@ Proof. ...@@ -1470,7 +1470,7 @@ Proof.
destruct (slots !! p) destruct (slots !! p)
as [[[lp sp] wp]|] eqn:Hslots_p; [ f_equal | by inversion Hcomm ]. as [[[lp sp] wp]|] eqn:Hslots_p; [ f_equal | by inversion Hcomm ].
- rewrite /= map_imap_insert /helped /= /get_value. - rewrite /= map_imap_insert /helped /= /get_value.
rewrite lookup_insert_ne; last done. rewrite lookup_imap Hslots_p /=. rewrite lookup_insert_ne; last done. rewrite map_lookup_imap Hslots_p /=.
destruct sp; try done. rewrite decide_True; [ done | by set_solver ]. destruct sp; try done. rewrite decide_True; [ done | by set_solver ].
- rewrite -IH; first last; try done. - rewrite -IH; first last; try done.
{ apply NoDup_app in HND as (HND1 & HND2 & HND3). { apply NoDup_app in HND as (HND1 & HND2 & HND3).
...@@ -1482,7 +1482,7 @@ Proof. ...@@ -1482,7 +1482,7 @@ Proof.
apply NoDup_cons in HND3_2 as (HND3_2_1 & HND3_2_2). done. } apply NoDup_cons in HND3_2 as (HND3_2_1 & HND3_2_2). done. }
{ intros k Hk. by apply Hvalid_2, elem_of_list_further, Hk. } { intros k Hk. by apply Hvalid_2, elem_of_list_further, Hk. }
apply map_ext_in. intros k Hk. apply map_ext_in. intros k Hk.
rewrite /get_value lookup_imap lookup_imap. rewrite /get_value map_lookup_imap map_lookup_imap.
assert (i k) as Hi_not_k. assert (i k) as Hi_not_k.
{ intros ->. apply NoDup_app in HND as (_ & _ & HND). { intros ->. apply NoDup_app in HND as (_ & _ & HND).
apply NoDup_cons in HND as (HND & _). apply NoDup_cons in HND as (HND & _).
...@@ -1547,9 +1547,9 @@ Proof. ...@@ -1547,9 +1547,9 @@ Proof.
assert (map_imap (helped ps) (<[n:=(l, Help γ, w)]> slots) assert (map_imap (helped ps) (<[n:=(l, Help γ, w)]> slots)
= map_imap (helped (n :: ps)) slots) as ->. = map_imap (helped (n :: ps)) slots) as ->.
{ apply map_eq. intros i. destruct (decide (i = n)) as [->|Hi_not_n]. { apply map_eq. intros i. destruct (decide (i = n)) as [->|Hi_not_n].
- rewrite lookup_imap lookup_imap /= lookup_insert Hn /=. - rewrite map_lookup_imap map_lookup_imap /= lookup_insert Hn /=.
rewrite /helped /=. rewrite decide_True; first done. set_solver. rewrite /helped /=. rewrite decide_True; first done. set_solver.
- rewrite lookup_imap lookup_imap /= lookup_insert_ne; last done. - rewrite map_lookup_imap map_lookup_imap /= lookup_insert_ne; last done.
destruct (slots !! i) as [[[li si] wi]|]; last done. simpl. destruct (slots !! i) as [[[li si] wi]|]; last done. simpl.
rewrite /helped /=. destruct si; try done. rewrite /helped /=. destruct si; try done.
destruct (decide (i n :: ps)). destruct (decide (i n :: ps)).
...@@ -2012,7 +2012,7 @@ Proof. ...@@ -2012,7 +2012,7 @@ Proof.
iFrame. iSplitL "Hℓ_ar". iFrame. iSplitL "Hℓ_ar".
{ assert (array_content sz slots deqs = array_content sz new_slots deqs) as ->; last done. { assert (array_content sz slots deqs = array_content sz new_slots deqs) as ->; last done.
apply array_content_ext. intros k Hk. rewrite /new_slots /array_get. apply array_content_ext. intros k Hk. rewrite /new_slots /array_get.
rewrite lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i]. rewrite map_lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i].
- by rewrite lookup_insert Hb_valid1 /helped /= decide_False. - by rewrite lookup_insert Hb_valid1 /helped /= decide_False.
- rewrite lookup_insert_ne; last done. - rewrite lookup_insert_ne; last done.
destruct (slots !! k) as [[[dl ds] dw]|]; last done. destruct (slots !! k) as [[[dl ds] dw]|]; last done.
...@@ -2024,7 +2024,7 @@ Proof. ...@@ -2024,7 +2024,7 @@ Proof.
{ rewrite -app_nil_end /new_pref /elts map_app map_cons. { rewrite -app_nil_end /new_pref /elts map_app map_cons.
rewrite [in get_value new_slots deqs i]/get_value. rewrite [in get_value new_slots deqs i]/get_value.
rewrite [in new_slots !! i]/new_slots. rewrite [in new_slots !! i]/new_slots.
rewrite lookup_imap lookup_insert /= -app_assoc cons_middle. rewrite map_lookup_imap lookup_insert /= -app_assoc cons_middle.
assert (NoDup (pref ++ i :: b_pendings)) as HND. assert (NoDup (pref ++ i :: b_pendings)) as HND.
{ apply NoDup_app in Hpvs_ND as (HND & _ & _). { apply NoDup_app in Hpvs_ND as (HND & _ & _).
rewrite cons_middle app_assoc. rewrite cons_middle app_assoc.
...@@ -2038,7 +2038,7 @@ Proof. ...@@ -2038,7 +2038,7 @@ Proof.
- done. - done.
- intros k Hk. by apply Hpref in Hk as (H1 & H2 & _). } - intros k Hk. by apply Hpref in Hk as (H1 & H2 & _). }
iPureIntro. repeat split_and; try done. iPureIntro. repeat split_and; try done.
- intros k. rewrite /new_slots lookup_imap. split; intros Hk. - intros k. rewrite /new_slots map_lookup_imap. split; intros Hk.
+ destruct (decide (k = i)) as [->|Hk_not_i]. + destruct (decide (k = i)) as [->|Hk_not_i].
* rewrite lookup_insert /helped /=. by eexists. * rewrite lookup_insert /helped /=. by eexists.
* rewrite lookup_insert_ne; last done. * rewrite lookup_insert_ne; last done.
...@@ -2049,7 +2049,7 @@ Proof. ...@@ -2049,7 +2049,7 @@ Proof.
assert (k < back `min` sz)%nat as H; last by lia. assert (k < back `min` sz)%nat as H; last by lia.
apply Hslots. destruct (slots !! k) as [d|]; first by exists d. apply Hslots. destruct (slots !! k) as [d|]; first by exists d.
by inversion Hk. by inversion Hk.
- intros k. rewrite /new_slots lookup_imap. - intros k. rewrite /new_slots map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i]; destruct (decide (k = i)) as [->|Hk_not_i];
first by rewrite lookup_insert /helped /=. first by rewrite lookup_insert /helped /=.
rewrite lookup_insert_ne; last done. split; intros Hk. rewrite lookup_insert_ne; last done. split; intros Hk.
...@@ -2069,19 +2069,19 @@ Proof. ...@@ -2069,19 +2069,19 @@ Proof.
{ apply Hpref in Hk as (H1 & H2). split; last done. { apply Hpref in Hk as (H1 & H2). split; last done.
rewrite map_imap_insert /=. destruct (decide (k = i)) as [->|Hk_not_i]. rewrite map_imap_insert /=. destruct (decide (k = i)) as [->|Hk_not_i].
- by rewrite lookup_insert. - by rewrite lookup_insert.
- rewrite lookup_insert_ne; last done. rewrite lookup_imap. - rewrite lookup_insert_ne; last done. rewrite map_lookup_imap.
destruct (slots !! k) as [[[dl ds] dw]|]; last by inversion H1. destruct (slots !! k) as [[[dl ds] dw]|]; last by inversion H1.
rewrite /= /helped. destruct ds as [dγ|dγ|]; try done. } rewrite /= /helped. destruct ds as [dγ|dγ|]; try done. }
apply elem_of_cons in Hk as [Hk|Hk]. apply elem_of_cons in Hk as [Hk|Hk].
{ subst k. split; last done. by rewrite map_imap_insert /= lookup_insert. } { subst k. split; last done. by rewrite map_imap_insert /= lookup_insert. }
apply Hb_valid2 in Hk as Hb_valid2_k. split. apply Hb_valid2 in Hk as Hb_valid2_k. split.
+ rewrite lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i]. + rewrite map_lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i].
* by rewrite lookup_insert /=. * by rewrite lookup_insert /=.
* rewrite lookup_insert_ne; last done. * rewrite lookup_insert_ne; last done.
destruct (slots !! k) as [[[kl ks] kw]|]; last by inversion Hb_valid2_k. destruct (slots !! k) as [[[kl ks] kw]|]; last by inversion Hb_valid2_k.
rewrite /= /helped. destruct ks; try done. by rewrite /= decide_True. rewrite /= /helped. destruct ks; try done. by rewrite /= decide_True.
+ apply Hstate in Hb_valid2_k. apply Hstate in Hb_valid2_k. done. + apply Hstate in Hb_valid2_k. apply Hstate in Hb_valid2_k. done.
- intros k Hk. subst new_slots. rewrite /array_get lookup_imap. - intros k Hk. subst new_slots. rewrite /array_get map_lookup_imap.
assert (k i) as Hk_not_i. { intros ->. apply Hi_not_in_deq, Hk. } assert (k i) as Hk_not_i. { intros ->. apply Hi_not_in_deq, Hk. }
rewrite lookup_insert_ne; last done. apply Hdeqs in Hk as (H1 & H2 & H3). rewrite lookup_insert_ne; last done. apply Hdeqs in Hk as (H1 & H2 & H3).
destruct (slots !! k) as [[[lk sk] wk]|] eqn:HEq; last by inversion H1. destruct (slots !! k) as [[[lk sk] wk]|] eqn:HEq; last by inversion H1.
...@@ -2103,12 +2103,12 @@ Proof. ...@@ -2103,12 +2103,12 @@ Proof.
+ assert (b.1 i) as Hb1_not_i. + assert (b.1 i) as Hb1_not_i.
{ intros HEq. apply NoDup_cons in HND as [HND1 HND2]. apply HND1. { intros HEq. apply NoDup_cons in HND as [HND1 HND2]. apply HND1.
rewrite -HEq. apply elem_of_app. by right. } rewrite -HEq. apply elem_of_app. by right. }
rewrite lookup_insert_ne; last done. by rewrite lookup_imap H1. rewrite lookup_insert_ne; last done. by rewrite map_lookup_imap H1.
+ intros j Hj. assert (j i) as Hj_not_i. + intros j Hj. assert (j i) as Hj_not_i.
{ intros HEq. apply NoDup_cons in HND as [HND1 HND2]. apply HND1. { intros HEq. apply NoDup_cons in HND as [HND1 HND2]. apply HND1.
rewrite -HEq. apply elem_of_app. right. rewrite -HEq. apply elem_of_app. right.
apply (flatten_blocks_mem2 _ _ Hk _ Hj). } apply (flatten_blocks_mem2 _ _ Hk _ Hj). }
rewrite lookup_insert_ne; last done. rewrite lookup_imap. rewrite lookup_insert_ne; last done. rewrite map_lookup_imap.
apply H2 in Hj as Hcomm. apply H2 in Hj as Hcomm.
destruct (slots !! j) as [[[lj sj] wj]|]; last by inversion Hj. destruct (slots !! j) as [[[lj sj] wj]|]; last by inversion Hj.
rewrite /= /helped. destruct sj; try done. simpl. rewrite /= /helped. destruct sj; try done. simpl.
......
...@@ -123,7 +123,7 @@ Definition of_graph_empty (g : graph loc) : ...@@ -123,7 +123,7 @@ Definition of_graph_empty (g : graph loc) :
of_graph g = fmap (λ x, (false, x)) g. of_graph g = fmap (λ x, (false, x)) g.
Proof. Proof.
apply: map_eq => i. apply: map_eq => i.
rewrite lookup_imap /of_graph_elem lookup_fmap lookup_omap //. rewrite map_lookup_imap /of_graph_elem lookup_fmap lookup_omap //.
Qed. Qed.
Lemma of_graph_dom_eq g G : Lemma of_graph_dom_eq g G :
...@@ -133,7 +133,7 @@ Proof. ...@@ -133,7 +133,7 @@ Proof.
intros HGvl. rewrite Gmon_graph_dom // => Hd. apply map_eq => i. intros HGvl. rewrite Gmon_graph_dom // => Hd. apply map_eq => i.
assert (Hd' : i dom (gset _) g i dom (gset _) G) by (by rewrite Hd). assert (Hd' : i dom (gset _) g i dom (gset _) G) by (by rewrite Hd).
revert Hd'; clear Hd. specialize (HGvl i); revert HGvl. revert Hd'; clear Hd. specialize (HGvl i); revert HGvl.
rewrite /of_graph /of_graph_elem /Gmon_graph lookup_imap lookup_fmap rewrite /of_graph /of_graph_elem /Gmon_graph map_lookup_imap lookup_fmap
lookup_omap ?elem_of_dom. lookup_omap ?elem_of_dom.
case _ : (g !! i); case _ : (G !! i) => [[]|] /=; inversion 1; eauto; case _ : (g !! i); case _ : (G !! i) => [[]|] /=; inversion 1; eauto;
intros [? ?]; intros [? ?];
...@@ -231,7 +231,7 @@ Proof. intros H. by rewrite lookup_op lookup_singleton_ne //= left_id_L. Qed. ...@@ -231,7 +231,7 @@ Proof. intros H. by rewrite lookup_op lookup_singleton_ne //= left_id_L. Qed.
Lemma of_graph_dom g G : dom (gset loc) (of_graph g G) = dom (gset _) g. Lemma of_graph_dom g G : dom (gset loc) (of_graph g G) = dom (gset _) g.
Proof. Proof.
apply elem_of_equiv_L=>i. apply elem_of_equiv_L=>i.
rewrite ?elem_of_dom lookup_imap /of_graph_elem lookup_omap. rewrite ?elem_of_dom map_lookup_imap /of_graph_elem lookup_omap.
case _ : (g !! i) => [x|]; case _ : (G !! i) => [[]|] //=; split; case _ : (g !! i) => [x|]; case _ : (G !! i) => [[]|] //=; split;
intros [? Hcn]; inversion Hcn; eauto. intros [? Hcn]; inversion Hcn; eauto.
Qed. Qed.
...@@ -239,7 +239,7 @@ Qed. ...@@ -239,7 +239,7 @@ Qed.
Lemma in_dom_of_graph (g : graph loc) (G : Gmon) x (b : bool) v : Lemma in_dom_of_graph (g : graph loc) (G : Gmon) x (b : bool) v :
G of_graph g G !! x = Some (b, v) b x dom (gset _) G. G of_graph g G !! x = Some (b, v) b x dom (gset _) G.
Proof. Proof.
rewrite /of_graph /of_graph_elem lookup_imap lookup_omap elem_of_dom. rewrite /of_graph /of_graph_elem map_lookup_imap lookup_omap elem_of_dom.
intros Hvl; specialize (Hvl x); revert Hvl; intros Hvl; specialize (Hvl x); revert Hvl;
case _ : (g !! x) => [?|]; case _ : (G !! x) => [[] ?|] //=; case _ : (g !! x) => [?|]; case _ : (G !! x) => [[] ?|] //=;
intros Hvl; inversion Hvl; try (inversion 1; subst); split; intros Hvl; inversion Hvl; try (inversion 1; subst); split;
...@@ -256,14 +256,14 @@ Lemma mark_update_lookup (g : graph loc) (G : Gmon) x v : ...@@ -256,14 +256,14 @@ Lemma mark_update_lookup (g : graph loc) (G : Gmon) x v :
((x [] v) G) of_graph g ((x [] v) G) !! x = Some (true, v). ((x [] v) G) of_graph g ((x [] v) G) !! x = Some (true, v).
Proof. Proof.
rewrite elem_of_dom /is_Some. intros [w H1] H2. rewrite elem_of_dom /is_Some. intros [w H1] H2.
rewrite /of_graph /of_graph_elem lookup_imap H1 lookup_omap; simpl. rewrite /of_graph /of_graph_elem map_lookup_imap H1 lookup_omap; simpl.
rewrite mark_update_lookup_base; trivial. rewrite mark_update_lookup_base; trivial.
Qed. Qed.
Lemma mark_update_lookup_ne (g : graph loc) (G : Gmon) x i v : Lemma mark_update_lookup_ne (g : graph loc) (G : Gmon) x i v :
i x of_graph g ((x [] v) G) !! i = (of_graph g G) !! i. i x of_graph g ((x [] v) G) !! i = (of_graph g G) !! i.
Proof. Proof.
intros H. rewrite /of_graph /of_graph_elem ?lookup_imap ?lookup_omap; simpl. intros H. rewrite /of_graph /of_graph_elem ?map_lookup_imap ?lookup_omap; simpl.
rewrite mark_update_lookup_ne_base //=. rewrite mark_update_lookup_ne_base //=.
Qed. Qed.
...@@ -419,7 +419,7 @@ Lemma delete_marked g G x w : ...@@ -419,7 +419,7 @@ Lemma delete_marked g G x w :
Proof. Proof.
apply: map_eq => i. destruct (decide (i = x)). apply: map_eq => i. destruct (decide (i = x)).
- subst; by rewrite ?lookup_delete. - subst; by rewrite ?lookup_delete.
- rewrite ?lookup_delete_ne //= /of_graph /of_graph_elem ?lookup_imap - rewrite ?lookup_delete_ne //= /of_graph /of_graph_elem ?map_lookup_imap
?lookup_omap; case _ : (g !! i) => [v|] //=. ?lookup_omap; case _ : (g !! i) => [v|] //=.
by rewrite lookup_op lookup_singleton_ne //= left_id_L. by rewrite lookup_op lookup_singleton_ne //= left_id_L.
Qed. Qed.
...@@ -705,7 +705,7 @@ Qed. ...@@ -705,7 +705,7 @@ Qed.
Lemma of_graph_unmarked (g : graph loc) (G : Gmon) x v : Lemma of_graph_unmarked (g : graph loc) (G : Gmon) x v :
of_graph g G !! x = Some (false, v) g !! x = Some v. of_graph g G !! x = Some (false, v) g !! x = Some v.
Proof. Proof.
rewrite lookup_imap /of_graph_elem lookup_omap. rewrite map_lookup_imap /of_graph_elem lookup_omap.
case _ : (g !! x); case _ : (G !! x) => [[]|]; by inversion 1. case _ : (g !! x); case _ : (G !! x) => [[]|]; by inversion 1.
Qed. Qed.
Lemma get_lr_disj (G G' : Gmon) i : (G G') Lemma get_lr_disj (G G' : Gmon) i : (G G')
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment