From 259f1414221ceab817091162614e7e8b621dfc85 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 3 May 2023 21:50:13 +0200 Subject: [PATCH] update dependencies --- coq-iris-examples.opam | 2 +- theories/concurrent_stacks/concurrent_stack4.v | 2 +- theories/hocap/cg_bag.v | 2 +- theories/hocap/concurrent_runners.v | 4 ++-- theories/hocap/fg_bag.v | 4 ++-- theories/hocap/lib/oneshot.v | 2 +- theories/logatom/counter_with_backup/counter_proof.v | 6 +++--- theories/logatom/herlihy_wing_queue/hwq.v | 2 +- theories/logrel/F_mu_ref_conc/binary/context_refinement.v | 2 +- theories/logrel/F_mu_ref_conc/binary/rules.v | 4 ++-- 10 files changed, 15 insertions(+), 15 deletions(-) diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam index a8a9b317..672c50b7 100644 --- a/coq-iris-examples.opam +++ b/coq-iris-examples.opam @@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git" synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything" depends: [ - "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") } + "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") } "coq-autosubst" { = "dev" } ] diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v index b1ff313f..8e4a9f14 100644 --- a/theories/concurrent_stacks/concurrent_stack4.v +++ b/theories/concurrent_stacks/concurrent_stack4.v @@ -364,7 +364,7 @@ Section proofs. Proof. iIntros (Φ) "(Hstack & Hupd) HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)". - iDestruct (bi.and_mono_r with "Hupd") as "Hupd"; first apply inner_mask_promote. + iDestruct (bi.and_mono_r with "Hupd") as "Hupd"; first by iApply inner_mask_promote. iDestruct (bi.and_mono_l _ _ (∀ (v : val) (xs : list val), _)%I with "Hupd") as "Hupd". { iIntros "Hupdcons". iIntros (v xs). iSpecialize ("Hupdcons" $! v xs). iApply (inner_mask_promote with "Hupdcons"). } iLöb as "IH". diff --git a/theories/hocap/cg_bag.v b/theories/hocap/cg_bag.v index 85c7070c..426acc7c 100644 --- a/theories/hocap/cg_bag.v +++ b/theories/hocap/cg_bag.v @@ -77,7 +77,7 @@ Section proof. Lemma bag_contents_agree γb X Y : bag_contents γb X -∗ bag_contents γb Y -∗ ⌜X = YâŒ. Proof. - rewrite /bag_contents. apply bi.wand_intro_r. + rewrite /bag_contents. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_op own_valid uPred.discrete_valid. f_equiv=> /=. rewrite -pair_op. by intros [_ ?%to_agree_op_inv_L]. diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v index acf475bc..62d5f2f8 100644 --- a/theories/hocap/concurrent_runners.v +++ b/theories/hocap/concurrent_runners.v @@ -79,13 +79,13 @@ Qed. Lemma INIT_SET_RES `{saG Σ} (v: val) γ : INIT γ 1%Qp ==∗ SET_RES γ 1%Qp v. Proof. - apply own_update. + apply bi.entails_wand, own_update. by apply cmra_update_exclusive. Qed. Lemma SET_RES_FIN `{saG Σ} (v w: val) γ : SET_RES γ 1%Qp v ==∗ FIN γ w. Proof. - apply own_update. + apply bi.entails_wand, own_update. by apply cmra_update_exclusive. Qed. diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v index a3ea7b8a..a15aee83 100644 --- a/theories/hocap/fg_bag.v +++ b/theories/hocap/fg_bag.v @@ -60,7 +60,7 @@ Section proof. | _, _ => False end%I. - Lemma is_list_duplicate hd xs : is_list hd xs -∗ is_list hd xs ∗ is_list hd xs. + Lemma is_list_duplicate hd xs : is_list hd xs ⊢ is_list hd xs ∗ is_list hd xs. Proof. iInduction xs as [ | x xs ] "IH" forall (hd); simpl; eauto. destruct hd; last by auto. @@ -98,7 +98,7 @@ Section proof. Lemma bag_contents_agree γb X Y : bag_contents γb X -∗ bag_contents γb Y -∗ ⌜X = YâŒ. Proof. - rewrite /bag_contents. apply bi.wand_intro_r. + rewrite /bag_contents. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_op own_valid uPred.discrete_valid. f_equiv=> /=. rewrite -pair_op. by intros [_ ?%to_agree_op_inv_L]. diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v index dc4a5df8..3cc02aea 100644 --- a/theories/hocap/lib/oneshot.v +++ b/theories/hocap/lib/oneshot.v @@ -18,7 +18,7 @@ Lemma new_pending `{oneshotG Σ} : ⊢ |==> ∃ γ, pending γ 1%Qp. Proof. by apply own_alloc. Qed. Lemma shoot `{oneshotG Σ} (v: val) γ : pending γ 1%Qp ==∗ shot γ v. Proof. - apply own_update. + apply bi.entails_wand, own_update. by apply cmra_update_exclusive. Qed. Lemma shot_not_pending `{oneshotG Σ} γ v q : diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v index a8b52a1a..42761fb7 100644 --- a/theories/logatom/counter_with_backup/counter_proof.v +++ b/theories/logatom/counter_with_backup/counter_proof.v @@ -530,7 +530,7 @@ Section counter_proof. (** *** Proof of [get] *) Lemma get_spec γs (c : val) : - is_counter γs c ⊢ <<< ∀∀ (n : nat), value γs n >>> (get c) @ ↑N <<< value γs n, RET #n>>>. + is_counter γs c -∗ <<< ∀∀ (n : nat), value γs n >>> (get c) @ ↑N <<< value γs n, RET #n>>>. Proof. iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex]. iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)". @@ -568,7 +568,7 @@ Section counter_proof. (** *** Proof of [get_backup] *) Lemma get_backup_spec γs (c: val) : - is_counter γs c ⊢ <<< ∀∀ (n: nat), value γs n >>> (get_backup c) @ ↑N <<< value γs n, RET #n>>>. + is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (get_backup c) @ ↑N <<< value γs n, RET #n>>>. Proof. iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex]. iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)". @@ -589,7 +589,7 @@ Section counter_proof. (** *** Proof of [increment] *) Lemma increment_spec γs (c: val) : - is_counter γs c ⊢ <<< ∀∀ (n: nat), value γs n >>> (increment c) @ ↑N <<< value γs (n + 1), RET #n>>>. + is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (increment c) @ ↑N <<< value γs (n + 1), RET #n>>>. Proof. iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex]. iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)". diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v index 5348b47c..caee2fbc 100644 --- a/theories/logatom/herlihy_wing_queue/hwq.v +++ b/theories/logatom/herlihy_wing_queue/hwq.v @@ -254,7 +254,7 @@ Lemma new_no_contra : ⊢ |==> ∃ γc, no_contra γc. Proof. by apply own_alloc. Qed. Lemma to_contra i1 i2 γc : no_contra γc ==∗ contra γc i1 i2. -Proof. apply own_update. by apply cmra_update_exclusive. Qed. +Proof. apply bi.entails_wand, own_update. by apply cmra_update_exclusive. Qed. Lemma contra_not_no_contra i1 i2 γc : no_contra γc -∗ contra γc i1 i2 -∗ False. diff --git a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v index 5fa6f185..89eb137c 100644 --- a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v +++ b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v @@ -242,7 +242,7 @@ Section bin_log_related_under_typed_ctx. Proof. revert Γ Ï„ Γ' Ï„' e e'. induction K as [|k K IHK]=> Γ Ï„ Γ' Ï„' e e' H1 H2; simpl. - { inversion_clear 1; trivial. } + { inversion_clear 1; auto. } inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. iIntros "#H". iPoseProof (IHK with "H") as "H'"; [done|done|done|]. diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v index 929d354a..21685ff1 100644 --- a/theories/logrel/F_mu_ref_conc/binary/rules.v +++ b/theories/logrel/F_mu_ref_conc/binary/rules.v @@ -165,7 +165,7 @@ Section cfg. Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2âŒ. Proof. - apply wand_intro_r. + apply entails_wand, wand_intro_r. rewrite /heapS_mapsto -own_op own_valid uPred.discrete_valid. f_equiv. rewrite auth_frag_op_valid -pair_op singleton_op -pair_op. rewrite pair_valid singleton_valid pair_valid to_agree_op_valid_L. @@ -180,7 +180,7 @@ Section cfg. Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q. Proof. rewrite /heapS_mapsto own_valid !discrete_valid auth_frag_valid. - by apply pure_mono=> -[_] /singleton_valid [??]. + by apply entails_wand, pure_mono=> -[_] /singleton_valid [??]. Qed. Lemma mapstoS_valid_2 l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ✓ (q1 + q2)%Qp. -- GitLab