From dad6c7edd1e6ef2d443a2da1ce55b8439b0bc261 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 21 Nov 2016 19:38:23 +0100 Subject: [PATCH] Update to work with latest iris --- F_mu_ref/lang.v | 2 +- F_mu_ref/rules.v | 2 +- F_mu_ref/rules_binary.v | 22 ++++++++--------- F_mu_ref/soundness_binary.v | 2 +- F_mu_ref_conc/lang.v | 2 +- F_mu_ref_conc/rules.v | 2 +- F_mu_ref_conc/rules_binary.v | 42 ++++++++++++++++---------------- F_mu_ref_conc/soundness_binary.v | 2 +- README.md | 2 +- 9 files changed, 39 insertions(+), 39 deletions(-) diff --git a/F_mu_ref/lang.v b/F_mu_ref/lang.v index d030306..98ef4d1 100644 --- a/F_mu_ref/lang.v +++ b/F_mu_ref/lang.v @@ -245,4 +245,4 @@ Ltac solve_atomic := rewrite ?to_of_val; eapply mk_is_Some; fast_done. Hint Extern 0 (language.atomic _) => solve_atomic. -Hint Extern 0 (language.atomic _) => solve_atomic : atomic. +Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances. diff --git a/F_mu_ref/rules.v b/F_mu_ref/rules.v index b55980f..36fead0 100644 --- a/F_mu_ref/rules.v +++ b/F_mu_ref/rules.v @@ -96,7 +96,7 @@ Section lang_rules. l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1. Proof. destruct (decide (v1 = v2)) as [->|]. - { by rewrite heap_mapsto_op_eq pure_equiv // left_id. } + { by rewrite heap_mapsto_op_eq pure_True // left_id. } apply (anti_symm (⊢)); last by apply pure_elim_l. rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid. eapply pure_elim; [done|] => /=. diff --git a/F_mu_ref/rules_binary.v b/F_mu_ref/rules_binary.v index b43b39a..388ee58 100644 --- a/F_mu_ref/rules_binary.v +++ b/F_mu_ref/rules_binary.v @@ -63,10 +63,10 @@ Section cfg. Proof. iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto. iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e2 σ) "[Hown %]". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. subst. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, option_local_update, (exclusive_local_update _ (Excl (fill K e'))). } iFrame "Hj". iApply "Hclose". iNext. iExists (fill K e'), σ. @@ -80,10 +80,10 @@ Section cfg. iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto. iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]". destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom]. - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. subst. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, option_local_update, (exclusive_local_update _ (Excl (fill K (Loc l)))). } iMod (own_update with "Hown") as "[Hown Hl]". @@ -104,12 +104,12 @@ Section cfg. iIntros (?) "(#Hinv & Hj & Hl)". rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. subst. - iDestruct (own_valid_2 _ with "[$Hown $Hl]") + iDestruct (own_valid_2 _ with "Hown Hl") as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, option_local_update, (exclusive_local_update _ (Excl (fill K (of_val v)))). } iFrame "Hj Hl". iApply "Hclose". iNext. @@ -126,15 +126,15 @@ Section cfg. iIntros (??) "(#Hinv & Hj & Hl)". rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. subst. - iDestruct (own_valid_2 _ with "[$Hown $Hl]") + iDestruct (own_valid_2 _ with "Hown Hl") as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, option_local_update, (exclusive_local_update _ (Excl (fill K Unit))). } - iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]". + iMod (own_update_2 with "Hown Hl") as "[Hown Hl]". { eapply auth_update, prod_local_update_2, singleton_local_update, (exclusive_local_update _ (1%Qp, DecAgree v)); last done. by rewrite /to_heap lookup_fmap Hl. } diff --git a/F_mu_ref/soundness_binary.v b/F_mu_ref/soundness_binary.v index 022b55d..b54b256 100644 --- a/F_mu_ref/soundness_binary.v +++ b/F_mu_ref/soundness_binary.v @@ -31,7 +31,7 @@ Proof. iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e'' σ) "[Hown Hsteps]". iDestruct "Hsteps" as %Hsteps'. rewrite /tpool_mapsto /auth.auth_own /=. - iDestruct (own_valid_2 with "[$Hown $Hj]") as %Hvalid. + iDestruct (own_valid_2 with "Hown Hj") as %Hvalid. move: Hvalid=> /auth_valid_discrete_2 [/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst. iMod ("Hclose" with "[-]") as "_"; [iExists _, σ; auto|]. diff --git a/F_mu_ref_conc/lang.v b/F_mu_ref_conc/lang.v index dff9ecc..9038bdb 100644 --- a/F_mu_ref_conc/lang.v +++ b/F_mu_ref_conc/lang.v @@ -312,4 +312,4 @@ Ltac solve_atomic := rewrite ?to_of_val; eapply mk_is_Some; fast_done. Hint Extern 0 (language.atomic _) => solve_atomic. -Hint Extern 0 (language.atomic _) => solve_atomic : atomic. +Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances. diff --git a/F_mu_ref_conc/rules.v b/F_mu_ref_conc/rules.v index eb25dbf..352f5cf 100644 --- a/F_mu_ref_conc/rules.v +++ b/F_mu_ref_conc/rules.v @@ -96,7 +96,7 @@ Section lang_rules. l ↦ᵢ{q1} v1 ∗ l ↦ᵢ{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦ᵢ{q1+q2} v1. Proof. destruct (decide (v1 = v2)) as [->|]. - { by rewrite heap_mapsto_op_eq pure_equiv // left_id. } + { by rewrite heap_mapsto_op_eq pure_True // left_id. } apply (anti_symm (⊢)); last by apply pure_elim_l. rewrite heapI_mapsto_eq -auth_own_op auth_own_valid discrete_valid. eapply pure_elim; [done|] => /=. diff --git a/F_mu_ref_conc/rules_binary.v b/F_mu_ref_conc/rules_binary.v index 130d37d..27c8771 100644 --- a/F_mu_ref_conc/rules_binary.v +++ b/F_mu_ref_conc/rules_binary.v @@ -137,9 +137,9 @@ Section cfg. Proof. iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). } iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ. @@ -154,9 +154,9 @@ Section cfg. iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom]. - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (Loc l)))). } iMod (own_update with "Hown") as "[Hown Hl]". @@ -177,11 +177,11 @@ Section cfg. iIntros (?) "(#Hinv & Hj & Hl)". rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. - iDestruct (own_valid_2 _ with "[$Hown $Hl]") + iDestruct (own_valid_2 _ with "Hown Hl") as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (of_val v)))). } iFrame "Hj Hl". iApply "Hclose". iNext. @@ -198,14 +198,14 @@ Section cfg. iIntros (??) "(#Hinv & Hj & Hl)". rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2. - iDestruct (own_valid_2 _ with "[$Hown $Hl]") + iDestruct (own_valid_2 _ with "Hown Hl") as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K Unit))). } - iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]". + iMod (own_update_2 with "Hown Hl") as "[Hown Hl]". { eapply auth_update, prod_local_update_2, singleton_local_update, (exclusive_local_update _ (1%Qp, DecAgree v)); last done. by rewrite /to_heap lookup_fmap Hl. } @@ -223,11 +223,11 @@ Section cfg. iIntros (????) "(#Hinv & Hj & Hl)". rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. - iDestruct (own_valid_2 _ with "[$Hown $Hl]") + iDestruct (own_valid_2 _ with "Hown Hl") as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (#♭ false)))). } iFrame "Hj Hl". iApply "Hclose". iNext. @@ -244,14 +244,14 @@ Section cfg. iIntros (????) "(#Hinv & Hj & Hl)"; subst. rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2. - iDestruct (own_valid_2 _ with "[$Hown $Hl]") + iDestruct (own_valid_2 _ with "Hown Hl") as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (#♭ true)))). } - iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]". + iMod (own_update_2 with "Hown Hl") as "[Hown Hl]". { eapply auth_update, prod_local_update_2, singleton_local_update, (exclusive_local_update _ (1%Qp, DecAgree v2)); last done. by rewrite /to_heap lookup_fmap Hl. } @@ -321,13 +321,13 @@ Section cfg. Proof. iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". - iDestruct (own_valid_2 _ with "[$Hown $Hj]") + iDestruct (own_valid_2 _ with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. assert (j < length tp) by eauto using lookup_lt_Some. - iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K Unit))). } - iMod (own_update with "[$Hown]") as "[Hown Hfork]". + iMod (own_update with "Hown") as "[Hown Hfork]". { eapply auth_update_alloc, prod_local_update_1, (alloc_singleton_local_update _ (length tp) (Excl e)); last done. rewrite lookup_insert_ne ?tpool_lookup; last omega. diff --git a/F_mu_ref_conc/soundness_binary.v b/F_mu_ref_conc/soundness_binary.v index 15538d0..c540579 100644 --- a/F_mu_ref_conc/soundness_binary.v +++ b/F_mu_ref_conc/soundness_binary.v @@ -30,7 +30,7 @@ Proof. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]". iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'. rewrite /tpool_mapsto /auth.auth_own /=. - iDestruct (own_valid_2 with "[$Hown $Hj]") as %Hvalid. + iDestruct (own_valid_2 with "Hown Hj") as %Hvalid. move: Hvalid=> /auth_valid_discrete_2 [/prod_included [/tpool_singleton_included Hv2 _] _]. destruct tp as [|? tp']; simplify_eq/=. diff --git a/README.md b/README.md index 21a6e23..9fbc7a1 100644 --- a/README.md +++ b/README.md @@ -5,4 +5,4 @@ This version is known to compile with: - Coq 8.5pl2 - Ssreflect 1.6 - Autosubst 1.5 - - Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/2a7755f + - Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/a7e9167 \ No newline at end of file -- GitLab