From 389ee60e393386307867c73c77aab491d0ffa897 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Aug 2021 23:46:33 +0200
Subject: [PATCH] use Iris options file
---
theories/lang/adequacy.v | 2 +-
theories/lang/heap.v | 25 ++---
theories/lang/lang.v | 8 +-
theories/lang/lib/arc.v | 2 +-
theories/lang/lib/lock.v | 2 +-
theories/lang/lib/memcpy.v | 2 +-
theories/lang/lib/new_delete.v | 4 +-
theories/lang/lib/spawn.v | 2 +-
theories/lang/lib/swap.v | 2 +-
theories/lang/lib/tests.v | 2 +-
theories/lang/lifting.v | 2 +-
theories/lang/notation.v | 2 +-
theories/lang/proofmode.v | 2 +-
theories/lang/races.v | 33 ++++---
theories/lang/tactics.v | 2 +-
theories/lifetime/at_borrow.v | 14 +--
theories/lifetime/frac_borrow.v | 22 ++---
theories/lifetime/lifetime.v | 6 +-
theories/lifetime/lifetime_sig.v | 2 +-
theories/lifetime/meta.v | 2 +-
theories/lifetime/model/accessors.v | 99 +++++++++++--------
theories/lifetime/model/borrow.v | 2 +-
theories/lifetime/model/borrow_sep.v | 15 +--
theories/lifetime/model/creation.v | 2 +-
theories/lifetime/model/definitions.v | 2 +-
theories/lifetime/model/faking.v | 6 +-
theories/lifetime/model/primitive.v | 20 ++--
theories/lifetime/model/reborrow.v | 7 +-
theories/lifetime/na_borrow.v | 4 +-
theories/typing/base.v | 1 +
theories/typing/bool.v | 2 +-
theories/typing/borrow.v | 27 ++---
theories/typing/cont.v | 2 +-
theories/typing/cont_context.v | 2 +-
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/examples/lazy_lft.v | 2 +-
theories/typing/examples/nonlexical.v | 3 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/fixpoint.v | 2 +-
theories/typing/function.v | 2 +-
theories/typing/int.v | 2 +-
theories/typing/lft_contexts.v | 2 +-
theories/typing/lib/arc.v | 25 ++---
theories/typing/lib/brandedvec.v | 2 +-
theories/typing/lib/cell.v | 2 +-
theories/typing/lib/diverging_static.v | 2 +-
theories/typing/lib/fake_shared.v | 6 +-
theories/typing/lib/ghostcell.v | 2 +-
theories/typing/lib/join.v | 2 +-
theories/typing/lib/mutex/mutex.v | 2 +-
theories/typing/lib/mutex/mutexguard.v | 12 +--
theories/typing/lib/option.v | 2 +-
theories/typing/lib/panic.v | 2 +-
theories/typing/lib/rc/rc.v | 35 ++++---
theories/typing/lib/rc/weak.v | 7 +-
theories/typing/lib/refcell/ref.v | 34 +++----
theories/typing/lib/refcell/ref_code.v | 12 +--
theories/typing/lib/refcell/refcell.v | 27 ++---
theories/typing/lib/refcell/refcell_code.v | 18 ++--
theories/typing/lib/refcell/refmut.v | 38 +++----
theories/typing/lib/refcell/refmut_code.v | 40 ++++----
theories/typing/lib/rwlock/rwlock.v | 23 ++---
theories/typing/lib/rwlock/rwlock_code.v | 18 ++--
theories/typing/lib/rwlock/rwlockreadguard.v | 36 +++----
.../typing/lib/rwlock/rwlockreadguard_code.v | 13 +--
theories/typing/lib/rwlock/rwlockwriteguard.v | 32 +++---
.../typing/lib/rwlock/rwlockwriteguard_code.v | 28 +++---
theories/typing/lib/spawn.v | 2 +-
theories/typing/lib/swap.v | 2 +-
theories/typing/lib/take_mut.v | 2 +-
theories/typing/own.v | 16 +--
theories/typing/product.v | 20 ++--
theories/typing/product_split.v | 2 +-
theories/typing/programs.v | 8 +-
theories/typing/shr_bor.v | 4 +-
theories/typing/soundness.v | 12 +--
theories/typing/sum.v | 4 +-
theories/typing/type.v | 10 +-
theories/typing/type_context.v | 6 +-
theories/typing/type_sum.v | 14 +--
theories/typing/typing.v | 1 +
theories/typing/uninit.v | 2 +-
theories/typing/uniq_bor.v | 14 +--
theories/typing/util.v | 2 +-
86 files changed, 475 insertions(+), 416 deletions(-)
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 8ce55710..5f41bde0 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export adequacy weakestpre.
From iris.algebra Require Import auth.
From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Class lrustGpreS Σ := HeapGpreS {
lrustGpreS_irig :> invGpreS Σ;
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index f77770c1..2638b7c7 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -6,7 +6,7 @@ From iris.bi Require Import fractional.
From iris.base_logic Require Export lib.own.
From iris.proofmode Require Export proofmode.
From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Definition lock_stateR : cmra :=
@@ -42,7 +42,7 @@ Section definitions.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
heap_mapsto_st (RSt 0) l q v.
- Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
+ Definition heap_mapsto_aux : seal (@heap_mapsto_def). Proof. by eexists. Qed.
Definition heap_mapsto := unseal heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
seal_eq heap_mapsto_aux.
@@ -55,7 +55,7 @@ Section definitions.
Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
own heap_freeable_name (â—¯ {[ l.1 := (q, inter (l.2) n) ]}).
- Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
+ Definition heap_freeable_aux : seal (@heap_freeable_def). Proof. by eexists. Qed.
Definition heap_freeable := unseal heap_freeable_aux.
Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
seal_eq heap_freeable_aux.
@@ -122,7 +122,7 @@ Section heap.
Qed.
Global Instance heap_mapsto_as_fractional l q v:
AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
- Proof. split. done. apply _. Qed.
+ Proof. split; first done. apply _. Qed.
Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
Proof. rewrite /heap_mapsto_vec. apply _. Qed.
@@ -134,7 +134,7 @@ Section heap.
Qed.
Global Instance heap_mapsto_vec_as_fractional l q vl:
AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
- Proof. split. done. apply _. Qed.
+ Proof. split; first done. apply _. Qed.
Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
@@ -243,7 +243,7 @@ Section heap.
Qed.
Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
(∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
- Proof. split. done. apply _. Qed.
+ Proof. split; first done. apply _. Qed.
Lemma inter_lookup_Some i j (n : nat):
i ≤ j < i+n → inter i n !! j = Excl' ().
@@ -266,7 +266,7 @@ Section heap.
- by rewrite !inter_lookup_None; try lia.
Qed.
Lemma inter_valid i n : ✓ inter i n.
- Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
+ Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
Lemma heap_freeable_op_eq l q1 q2 n n' :
†{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
@@ -370,12 +370,13 @@ Section heap.
{ apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
- eauto using heap_freeable_rel_None.
- - split. done. apply inter_valid. }
+ - split; first done. apply inter_valid. }
iModIntro. iSplitL "Hvalσ HhF".
{ iExists _. iFrame. iPureIntro.
auto using heap_freeable_rel_init_mem. }
- rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
- iFrame. destruct (Z.to_nat n); done.
+ rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //; last first.
+ { destruct (Z.to_nat n); done. }
+ iFrame.
Qed.
Lemma heap_free_vs σ l vl :
@@ -437,7 +438,9 @@ Section heap.
[/Some_pair_included [_ Hincl] /to_agree_included->].
destruct ls as [|n], ls'' as [|n''],
Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
- by exists O. eauto. exists O. by rewrite Nat.add_0_r.
+ - by exists O.
+ - eauto.
+ - exists O. by rewrite Nat.add_0_r.
Qed.
Lemma heap_mapsto_lookup_1 σ l ls v :
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 43acbcd0..987e8749 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,7 +1,7 @@
From iris.program_logic Require Export language ectx_language ectxi_language.
From stdpp Require Export strings binders.
From stdpp Require Import gmap.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Open Scope Z_scope.
@@ -451,7 +451,7 @@ Lemma alloc_fresh n σ :
0 < n →
head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
Proof.
- intros l init Hn. apply AllocS. auto.
+ intros l init Hn. apply AllocS; first done.
- intros i. apply (is_fresh_block _ i).
Qed.
@@ -473,10 +473,10 @@ Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
Proof.
revert e X Y. fix FIX 1; intros e; destruct e=>X Y/=; try naive_solver.
- naive_solver set_solver.
- - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+ - rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
rename select (list expr) into el.
induction el=>/=; naive_solver.
- - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+ - rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
rename select (list expr) into el.
induction el=>/=; naive_solver.
Qed.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 734a2dbf..846d97bd 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import proofmode.
From iris.bi Require Import fractional.
From iris.algebra Require Import excl csum frac auth numbers.
From lrust.lang Require Import lang proofmode notation new_delete.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(* JH: while working on Arc, I think figured that the "weak count
locking" mechanism that Rust is using and that is verified below may
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 2ab7a9f3..e7987116 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Import excl.
From lrust.lang Require Import lang proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 3b70cb90..9edcaae8 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -1,6 +1,6 @@
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] :=
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 7f70f113..2b153350 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -1,6 +1,6 @@
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode memcpy.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition new : val :=
λ: ["n"],
@@ -24,7 +24,7 @@ Section specs.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- - wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst. iFrame.
+ - wp_if. wp_alloc l as "H↦" "H†"; first lia. iApply "HΦ". subst. iFrame.
Qed.
Lemma wp_delete E (n:Z) l vl :
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 66ad5d22..4dd4154c 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import proofmode.
From iris.algebra Require Import excl.
From lrust.lang Require Import proofmode notation.
From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition spawn : val :=
λ: ["f"],
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index e6997bbe..11f3cc45 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -1,6 +1,6 @@
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition swap : val :=
rec: "swap" ["p1";"p2";"len"] :=
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 7f6ebbaa..45a610eb 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -1,7 +1,7 @@
From iris.program_logic Require Import weakestpre.
From iris.proofmode Require Import proofmode.
From lrust.lang Require Import lang proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section tests.
Context `{!lrustGS Σ}.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 44f7f1cb..d337d48b 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From lrust.lang Require Export lang heap.
From lrust.lang Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Class lrustGS Σ := LRustGS {
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 53850236..de38f6cf 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -1,5 +1,5 @@
From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Coercion LitInt : Z >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index b38d166f..cd542a07 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Export proofmode.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting.
From lrust.lang Require Export tactics lifting.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
diff --git a/theories/lang/races.v b/theories/lang/races.v
index cb06828d..c247955c 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -1,7 +1,7 @@
From stdpp Require Import gmap.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
@@ -139,11 +139,11 @@ Proof.
assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! (l +ₗ i) = None).
{ clear. intros l n i Hi.
replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
- revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
+ revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi; first lia.
destruct (decide (i = 0)).
- subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
- replace i with (1+(i-1)) by lia.
- rewrite lookup_delete_ne -shift_loc_assoc ?IH //. lia.
+ rewrite lookup_delete_ne -shift_loc_assoc ?IH //; first lia.
destruct l; intros [=?]. lia. }
assert (FREE' : σ' !! l = None).
{ inversion Ha1; clear Ha1; inv_head_step. auto. }
@@ -163,8 +163,8 @@ Proof.
destruct (elem_of_list_split _ _ Hi) as (?&?&->).
eapply Hsafe; last by (apply: fill_not_val; subst).
- eapply rtc_l, rtc_l, rtc_refl.
- + eexists. econstructor. done. done. econstructor; done.
- + eexists. econstructor. done. done. econstructor; done.
+ + eexists. econstructor; [done..|]. econstructor; done.
+ + eexists. econstructor; [done..|]. econstructor; done.
- subst. set_solver+.
Qed.
@@ -180,7 +180,7 @@ Proof.
destruct (elem_of_list_split _ _ Hi) as (?&?&->).
eapply Hsafe; last by (apply: fill_not_val; subst).
- eapply rtc_l, rtc_refl.
- + eexists. econstructor. done. done. econstructor; done.
+ + eexists. econstructor; [done..|]. econstructor; done.
- subst. set_solver+.
Qed.
@@ -191,7 +191,7 @@ Theorem safe_nonracing el σ :
Proof.
intros Hsafe l a1 a2 (t1&?&t2&?&t3&->&(K1&e1&Ha1&->)&(K2&e2&Ha2&->)).
- assert (to_val e1 = None). by destruct Ha1.
+ assert (to_val e1 = None) by by destruct Ha1.
assert (Hrede1:head_reducible e1 σ).
{ eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
@@ -211,11 +211,13 @@ Proof.
{ destruct a1 as [a1 []]=>// _.
eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
fill_not_val=>//.
- by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
+ - by auto.
+ - abstract set_solver.
+ - by destruct Hstep1; inversion Ha1. }
assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
{ eapply (safe_step_not_reduce_to_stuck _ _ K1); first done; last done. set_solver+. }
- assert (to_val e2 = None). by destruct Ha2.
+ assert (to_val e2 = None) by by destruct Ha2.
assert (Hrede2:head_reducible e2 σ).
{ eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
@@ -235,7 +237,9 @@ Proof.
{ destruct a2 as [a2 []]=>// _.
eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
fill_not_val=>//.
- by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
+ - by auto.
+ - abstract set_solver.
+ - by destruct Hstep2; inversion Ha2. }
assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
{ eapply (safe_step_not_reduce_to_stuck _ _ K2); first done; last done. set_solver+. }
@@ -247,7 +251,7 @@ Proof.
abstract set_solver. }
assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
{ eapply (safe_not_reduce_to_stuck _ _ K2).
- - intros. eapply Hsafe. etrans; last done. done. done. done.
+ - intros. eapply Hsafe; [|done..]. etrans; last done. done.
- set_solver+. }
assert (Hσe1'1:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
@@ -262,7 +266,7 @@ Proof.
abstract set_solver. }
assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
{ eapply (safe_not_reduce_to_stuck _ _ K1).
- - intros. eapply Hsafe. etrans; last done. done. done. done.
+ - intros. eapply Hsafe; [|done..]. etrans; last done. done.
- set_solver+. }
assert (Hσe2'1:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
@@ -298,6 +302,7 @@ Corollary adequate_nonracing e1 t2 σ1 σ2 φ :
nonracing_threadpool t2 σ2.
Proof.
intros [_ Had] Hrtc. apply safe_nonracing. intros el' σ' e' ?? He'.
- edestruct (Had el' σ' e') as [He''|]; try done. etrans; eassumption.
- rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
+ edestruct (Had el' σ' e') as [He''|]; try done.
+ - etrans; eassumption.
+ - rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
Qed.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 27de5624..e92d7a55 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,6 +1,6 @@
From stdpp Require Import fin_maps.
From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 7fef53b3..020323fa 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import gmap auth frac.
From iris.proofmode Require Import proofmode.
From lrust.lifetime Require Export lifetime.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** Atomic persistent bors *)
(* TODO : update the TEX with the fact that we can choose the namespace. *)
@@ -34,7 +34,7 @@ Section atomic_bors.
Proof.
iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iFrame "#".
- iLeft. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
+ iLeft. iSplitR; first done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
Qed.
Lemma bor_share_lftN E κ :
@@ -42,7 +42,7 @@ Section atomic_bors.
Proof.
iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iFrame "#". subst.
- iRight. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
+ iRight. iSplitR; first done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
Qed.
Lemma at_bor_acc E κ :
@@ -52,12 +52,12 @@ Section atomic_bors.
Proof.
iIntros (??) "#LFT #HP". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
- iInv N as ">Hi" "Hclose". iMod (idx_bor_atomic_acc with "LFT Hidx Hi")
- as "[[HP Hclose']|[H†Hclose']]". solve_ndisj.
+ as "[[HP Hclose']|[H†Hclose']]"; first solve_ndisj.
+ iLeft. iFrame. iIntros "!>HP". iMod ("Hclose'" with "HP"). by iApply "Hclose".
+ iRight. iFrame. iIntros "!>". iMod "Hclose'". by iApply "Hclose".
- subst. rewrite difference_twice_L. iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
- iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
- iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H†Hclose]]". done.
+ iMod ("Hclose" with "[Hq'1]") as "_"; first solve_ndisj.
+ iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H†Hclose]]"; first done.
+ iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
+ iRight. iFrame. iIntros "!>". by iMod "Hclose".
Qed.
@@ -68,7 +68,7 @@ Section atomic_bors.
Proof.
iIntros (??) "#LFT #HP Hκ". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
- iInv N as ">Hi" "Hclose".
- iMod (idx_bor_acc with "LFT Hidx Hi Hκ") as "[$ Hclose']". solve_ndisj.
+ iMod (idx_bor_acc with "LFT Hidx Hi Hκ") as "[$ Hclose']"; first solve_ndisj.
iIntros "!> H". iMod ("Hclose'" with "H") as "[? $]". by iApply "Hclose".
- iMod (at_bor_acc with "LFT []") as "[[$ Hclose]|[H†_]]"; try done.
+ iExists i. auto.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 07561dde..bfa1faf1 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From iris.bi Require Import fractional.
From iris.algebra Require Import frac.
From lrust.lifetime Require Export at_borrow.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
@@ -41,17 +41,17 @@ Section frac_bor.
Lemma bor_fracture E κ :
↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
Proof.
- iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
- iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H†Hclose]]". done.
+ iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?"; first done.
+ iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H†Hclose]]"; first done.
- iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
iMod ("Hclose" with "[] [-]") as "Hφ"; last first.
{ iExists γ, κ'. iFrame "#". iApply (bor_share_lftN with "Hφ"); auto. }
{ iExists 1%Qp. iFrame. eauto. }
- iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
+ iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])"; first by subst.
iDestruct "Hκ" as (q'') "[_ Hκ]".
iDestruct (lft_tok_dead with "Hκ H†") as "[]".
- iMod "Hclose" as "_"; last first.
- iExists γ, κ. iSplitR. by iApply lft_incl_refl.
+ iExists γ, κ. iSplitR; first by iApply lft_incl_refl.
by iApply at_bor_fake_lftN.
Qed.
@@ -64,8 +64,8 @@ Section frac_bor.
iMod (at_bor_acc_lftN with "LFT Hshr") as "[[Hφ Hclose]|[H†Hclose]]"; try done.
- iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
- - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
- iApply fupd_mask_intro_subseteq. set_solver. done.
+ - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$"; first done.
+ iApply fupd_mask_intro_subseteq; first set_solver. done.
Qed.
Local Lemma frac_bor_trade1 γ κ' q :
@@ -120,7 +120,7 @@ Section frac_bor.
Proof.
iIntros (?) "#LFT #Hφ Hfrac Hκ". unfold frac_bor.
iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
- iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
+ iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]"; first done.
iMod (at_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
iDestruct (frac_bor_trade2 with "Hφ [$H $Hκ2]") as "[H Htrade]".
iDestruct "Htrade" as (q0 q1) "(>Hq & >Hκ2 & >Hown & Hqφ)".
@@ -137,7 +137,7 @@ Section frac_bor.
↑lftN ⊆ E →
lft_ctx -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
Proof.
- iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
+ iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"); first done.
iIntros "!>*". rewrite fractional. iSplit; auto.
Qed.
@@ -160,10 +160,10 @@ Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ κ' q:
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
- iIntros (q') "Hκ'".
- iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
+ iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]"; first done.
iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
- iIntros "H†'".
- iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
+ iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]"; first done.
iDestruct "H" as (q') "[>Hκ' _]".
iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
Qed.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index bfa1040c..27874643 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export lifetime_sig.
From lrust.lifetime.model Require definitions primitive accessors faking borrow
borrow_sep reborrow creation.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Module Export lifetime : lifetime_sig.
Definition lft := gmultiset positive.
@@ -190,7 +190,7 @@ Proof.
iMod (bor_create _ κ' with "LFT Hidx") as "[Hidx Hinh]"; first done.
iMod (idx_bor_unnest with "LFT Hbor Hidx") as "Hbor'"; first done.
iDestruct (bor_shorten with "[] Hbor'") as "$".
- { iApply lft_incl_glb. done. iApply lft_incl_refl. }
+ { iApply lft_incl_glb; first done. iApply lft_incl_refl. }
iIntros "!> H†". iMod ("Hinh" with "H†") as ">Hidx". auto with iFrame.
Qed.
@@ -210,7 +210,7 @@ Qed.
Lemma lft_incl_static κ : ⊢ κ ⊑ static.
Proof.
iApply lft_incl_intro. iIntros "!>". iSplitR.
- - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
+ - iIntros (q) "?". iExists 1%Qp. iSplitR; last by auto. by iApply lft_tok_static.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 345b819a..c179f0fa 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -3,7 +3,7 @@ From stdpp Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes.
From iris.bi Require Import fractional.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition lftN : namespace := nroot .@ "lft".
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index f5d8f12e..8a535061 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import dyn_reservation_map agree.
From iris.proofmode Require Import proofmode.
From lrust.lifetime Require Export lifetime.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** This module provides support for attaching metadata (specifically, a
[gname]) to a lifetime (as is required for types using branding). *)
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 49d61adb..971969f6 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export primitive.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic.lib Require Import boxes.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section accessors.
Context `{!invGS Σ, !lftGS Σ userE}.
@@ -21,11 +21,13 @@ Proof.
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_empty _ _ true with "Hslice Hbox") as "[$ Hbox]".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ { solve_ndisj. } { by rewrite lookup_fmap EQB. }
rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
- iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
- { eapply singleton_local_update. by rewrite lookup_fmap EQB.
- by apply (exclusive_local_update _ (1%Qp, to_agree (Bor_open q))). }
+ iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
+ { apply auth_update.
+ eapply singleton_local_update.
+ - by rewrite lookup_fmap EQB.
+ - by apply (exclusive_local_update _ (1%Qp, to_agree (Bor_open q))). }
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
iExists _. iFrame "∗".
rewrite -insert_delete_insert big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
@@ -43,11 +45,13 @@ Proof.
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_fill _ _ true with "Hslice HP Hbox") as "Hbox".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ { solve_ndisj. } { by rewrite lookup_fmap EQB. }
rewrite -(fmap_insert bor_filled _ _ Bor_in).
- iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
- { eapply singleton_local_update. by rewrite lookup_fmap EQB.
- by apply (exclusive_local_update _ (1%Qp, to_agree Bor_in)). }
+ iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
+ { apply auth_update.
+ eapply singleton_local_update.
+ - by rewrite lookup_fmap EQB.
+ - by apply (exclusive_local_update _ (1%Qp, to_agree Bor_in)). }
rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[>$ HB]".
iExists _. iFrame "Hbox Hown".
@@ -60,7 +64,7 @@ Lemma add_vs Pb Pb' P Q Pi κ :
Proof.
iIntros "#HEQ Hvs HvsQ". iApply (lft_vs_cons with "[-Hvs] Hvs").
iIntros "[HQ HPb'] #H†".
- iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". set_solver.
+ iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP"; first set_solver.
iModIntro. iNext. iRewrite "HEQ". iFrame.
Qed.
@@ -72,9 +76,10 @@ Lemma idx_bor_acc E q κ i P :
Proof.
unfold idx_bor. iIntros (HE) "#LFT [#Hle #Hs] Hbor Htok".
iDestruct "Hs" as (P') "[#HPP' Hs]".
- iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+ iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
- iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
+ iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'.
+ { by unfold idx_bor_own. }
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
@@ -93,8 +98,8 @@ Proof.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >Hdead_in]] Hclose'']".
+ rewrite lft_inv_alive_unfold.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
- iMod (bor_close_internal with "Hs Halive Hf HP") as "(Halive & $ & Htok)".
- solve_ndisj.
+ iMod (bor_close_internal with "Hs Halive Hf HP") as "(Halive & $ & Htok)";
+ first solve_ndisj.
iMod ("Hclose'" with "[-Htok Hclose]") as "_"; last by iApply "Hclose".
iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame.
@@ -103,7 +108,7 @@ Proof.
as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
- - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
+ - iMod (lft_dead_in_tok with "HA") as "[_ H†]"; first done.
iDestruct (lft_tok_dead with "Htok H†") as "[]".
Qed.
@@ -125,21 +130,24 @@ Proof.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
- iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]";
+ first solve_ndisj.
+ { by rewrite lookup_fmap EQB. }
iDestruct ("HPP'" with "HP'") as "$".
- iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>HP'". solve_ndisj.
+ iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>HP'"; first solve_ndisj.
iDestruct ("HPP'" with "HP'") as "HP".
- iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox".
- solve_ndisj. by rewrite lookup_insert. iFrame.
+ iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox";
+ first solve_ndisj.
+ { by rewrite lookup_insert. }
+ iFrame.
iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later.
iApply "Hclose''". iLeft. iFrame "%". iExists _, _. iFrame.
iExists _. iFrame.
rewrite insert_insert -(fmap_insert _ _ _ Bor_in) insert_id //.
- - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]". done.
+ - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
iMod ("Hclose'" with "[-Hbor]") as "_".
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
- + iMod (lft_incl_dead with "Hle H†"). done. iFrame.
+ + iMod (lft_incl_dead with "Hle H†"); first done. iFrame.
iApply fupd_mask_subseteq. solve_ndisj.
Qed.
@@ -153,15 +161,16 @@ Proof.
unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
iDestruct "Hs" as (P') "[#HPP' Hs]".
- iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+ iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
- iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
+ iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'.
+ { by unfold idx_bor_own. }
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
- iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_open_internal _ _ (κ'', s'') with "Hs Halive Hbor Htok")
- as "(Halive & Hbor & HP')". solve_ndisj.
+ as "(Halive & Hbor & HP')"; first solve_ndisj.
iDestruct ("HPP'" with "HP'") as "$".
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
@@ -177,8 +186,9 @@ Proof.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
- iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]";
+ first solve_ndisj.
+ { by rewrite lookup_fmap EQB. }
iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_empty _ _ true _ Q with "Hbox") as (j) "(% & #Hs' & Hbox)".
@@ -191,11 +201,12 @@ Proof.
-fmap_None -lookup_fmap fmap_delete //. }
rewrite own_bor_op. iDestruct "Hown" as "[Hown Hbor]".
iMod (bor_close_internal _ _ (_, _) with "Hs' [Hbox Hown HB] Hbor HQ")
- as "(Halive & Hbor & Htok)". solve_ndisj.
+ as "(Halive & Hbor & Htok)"; first solve_ndisj.
{ rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_open q'))
/lft_bor_alive. iExists _. iFrame "Hbox Hown".
- rewrite big_sepM_insert. by rewrite big_sepM_delete.
- by rewrite -fmap_None -lookup_fmap fmap_delete. }
+ rewrite big_sepM_insert.
+ - by rewrite big_sepM_delete.
+ - by rewrite -fmap_None -lookup_fmap fmap_delete. }
iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
@@ -207,7 +218,7 @@ Proof.
as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
- - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
+ - iMod (lft_dead_in_tok with "HA") as "[_ H†]"; first done.
iDestruct (lft_tok_dead with "Htok H†") as "[]".
Qed.
@@ -222,7 +233,8 @@ Proof.
iDestruct "Hbor" as (i) "((#Hle & #Hs) & Hbor)".
iDestruct "Hs" as (P') "[#HPP' Hs]".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
- iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
+ iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'.
+ { by unfold idx_bor_own. }
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
@@ -232,13 +244,15 @@ Proof.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
- iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
- solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
- iMod fupd_mask_subseteq as "Hclose"; last iIntros "!> %Q HvsQ HQ". solve_ndisj.
+ iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)";
+ first solve_ndisj.
+ { by rewrite lookup_fmap EQB. }
+ iDestruct ("HPP'" with "HP'") as "$".
+ iMod fupd_mask_subseteq as "Hclose"; last iIntros "!> %Q HvsQ HQ"; first solve_ndisj.
iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
- iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
- solve_ndisj.
+ iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)";
+ first solve_ndisj.
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
- apply delete_singleton_local_update, _.
@@ -253,12 +267,13 @@ Proof.
iLeft. iFrame "%". iExists _, _. iFrame. iNext.
rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
iExists _. iFrame "Hbox Hâ—".
- rewrite big_sepM_insert. by rewrite big_sepM_delete.
- by rewrite -fmap_None -lookup_fmap fmap_delete.
- - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]". done.
+ rewrite big_sepM_insert; last first.
+ { by rewrite -fmap_None -lookup_fmap fmap_delete. }
+ by rewrite big_sepM_delete.
+ - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
iMod ("Hclose'" with "[-Hbor]") as "_".
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
- + iMod (lft_incl_dead with "Hle H†") as "$". done.
- iApply fupd_mask_subseteq. solve_ndisj.
+ + iMod (lft_incl_dead with "Hle H†") as "$"; first done.
+ iApply fupd_mask_subseteq; first solve_ndisj.
Qed.
End accessors.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index ebfce718..56adf9af 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -3,7 +3,7 @@ From lrust.lifetime Require Export faking.
From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section borrow.
Context `{!invGS Σ, !lftGS Σ userE}.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 47dbef7d..227c668a 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -3,7 +3,7 @@ From lrust.lifetime Require Export faking reborrow.
From iris.algebra Require Import csum auth frac gmap agree.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section borrow.
Context `{!invGS Σ, !lftGS Σ userE}.
@@ -77,10 +77,10 @@ Lemma bor_combine E κ P Q :
Proof.
iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
- iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
- done. by apply gmultiset_disj_union_subseteq_l.
- iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
- done. by apply gmultiset_disj_union_subseteq_r.
+ iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1"; first solve_ndisj.
+ { by apply gmultiset_disj_union_subseteq_l. }
+ iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2"; first solve_ndisj.
+ { by apply gmultiset_disj_union_subseteq_r. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
iDestruct "Hslice1" as (P') "[#HPP' Hslice1]".
@@ -127,8 +127,9 @@ Proof.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox Hâ—".
rewrite !big_sepM_insert /=.
+ rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
- rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=.
- by iDestruct "HB" as "[_ $]". rewrite lookup_delete_ne //.
+ rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=; last first.
+ { rewrite lookup_delete_ne //. }
+ by iDestruct "HB" as "[_ $]".
+ rewrite -fmap_None -lookup_fmap !fmap_delete //.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 1bab34a2..8362e9af 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -3,7 +3,7 @@ From lrust.lifetime Require Import faking.
From iris.algebra Require Import csum auth frac gmap agree gset numbers.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section creation.
Context `{!invGS Σ, !lftGS Σ userE}.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 2fc9c8bd..f1f63cf0 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import csum auth frac gmap agree gset numbers.
From iris.base_logic.lib Require Import boxes.
From lrust.lifetime Require Export lifetime_sig.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Definition inhN : namespace := lftN .@ "inh".
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 861262c3..96c5f3c8 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export primitive.
From iris.algebra Require Import csum auth frac gmap agree gset numbers.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section faking.
Context `{!invGS Σ, !lftGS Σ userE}.
@@ -41,7 +41,9 @@ Proof.
- rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
iSplitL "Hbor"; last by iApply "Hinh".
rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !gset_to_gmap_empty.
- iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
+ iSplitL "Hbor".
+ + iExists γs. by iFrame.
+ + iApply box_alloc.
- rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
{ rewrite /lft_bor_alive. iExists ∅.
rewrite /to_borUR !fmap_empty big_sepM_empty.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index b7f6c4db..140b4d73 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset proofmode_classe
From iris.base_logic.lib Require Import boxes.
From iris.bi Require Import fractional.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Lemma lft_init `{!invGS Σ, !lftGpreS Σ} E userE :
@@ -67,7 +67,7 @@ Proof.
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
- iExists γs. iSplit. done. rewrite own_op; iFrame.
+ iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Global Instance own_bor_into_op κ x x1 x2 :
IsOp x x1 x2 → IntoSep (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
@@ -135,7 +135,7 @@ Proof.
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
- iExists γs. iSplit. done. rewrite own_op; iFrame.
+ iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Global Instance own_inh_into_op κ x x1 x2 :
IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
@@ -301,7 +301,7 @@ Proof.
Qed.
Global Instance lft_tok_as_fractional κ q :
AsFractional q.[κ] (λ q, q.[κ])%I q.
-Proof. split. done. apply _. Qed.
+Proof. split; first done. apply _. Qed.
Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
Proof.
intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
@@ -309,7 +309,7 @@ Proof.
Qed.
Global Instance idx_bor_own_as_fractional i q :
AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
-Proof. split. done. apply _. Qed.
+Proof. split; first done. apply _. Qed.
(** Lifetime inclusion *)
Lemma lft_incl_acc E κ κ' q :
@@ -377,7 +377,9 @@ Proof.
iExists qq. iFrame. iIntros "!> Hqq".
iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
- - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
+ - rewrite -lft_dead_or. iIntros "[H†|H†]".
+ + by iApply "H1†".
+ + by iApply "H2†".
Qed.
Lemma lft_intersect_mono κ1 κ1' κ2 κ2' :
@@ -394,14 +396,16 @@ Proof.
iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
iNext. iModIntro. iSplit; iIntros.
- by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
+ - by iApply "HPP'"; iApply "Hiff".
+ - by iApply "Hiff"; iApply "HPP'".
Qed.
Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
Proof.
unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
- by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
+ - by iApply "HPP'"; iApply "HP0P".
+ - by iApply "HP0P"; iApply "HPP'".
Qed.
Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 1c38d82a..d43ac391 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Import borrow accessors.
From iris.algebra Require Import csum auth frac gmap agree gset numbers.
From iris.base_logic.lib Require Import boxes.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section reborrow.
Context `{!invGS Σ, !lftGS Σ userE}.
@@ -120,8 +120,9 @@ Proof.
iDestruct "Halive" as (B) "(Hbox & >Hâ— & HB)".
iDestruct (own_bor_valid_2 with "Hâ— Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
- iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]";
+ first solve_ndisj.
+ { by rewrite lookup_fmap EQB. }
iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
iDestruct (own_bor_auth with "HI [Hidx]") as %HI; [by rewrite /idx_bor_own|].
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index cd77e700..144c079c 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,7 +1,7 @@
From lrust.lifetime Require Export lifetime.
From iris.base_logic.lib Require Export na_invariants.
From iris.proofmode Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition na_bor `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
(κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
@@ -45,7 +45,7 @@ Section na_bor.
iIntros (???) "#LFT#HP Hκ Hnaown".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
iMod (na_inv_acc with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
- iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
+ iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']"; first done.
iIntros "{$HP $Hnaown} !> HP Hnaown".
iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
Qed.
diff --git a/theories/typing/base.v b/theories/typing/base.v
index e5a84f36..4ba5c3d4 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,5 +1,6 @@
From stdpp Require Import namespaces.
From lrust.lang Require Export proofmode.
+From iris.prelude Require Import options.
(* Last, so that we make sure we shadow the defintion of delete for
sets coming from the prelude. *)
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 4e2dfb0b..d2bcfbe8 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section bool.
Context `{!typeGS Σ}.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 1988a5ea..da85d29a 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From lrust.lang Require Import proofmode.
From lrust.typing Require Export uniq_bor shr_bor own.
From lrust.typing Require Import lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
a separate file so make sure that own.v and uniq_bor.v can be compiled
@@ -16,10 +16,10 @@ Section borrow.
Proof.
iIntros (tid ??) "#LFT _ $ [H _]".
iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
- iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+ iMod (bor_create with "LFT Hmt") as "[Hbor Hext]"; first done.
iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
- iExists _. auto.
- - iExists _. iSplit. done. by iFrame.
+ - iExists _. iSplit; first done. by iFrame.
Qed.
Lemma tctx_share E L p κ ty :
@@ -69,7 +69,8 @@ Section borrow.
((p â—{κ} own_ptr n ty)::T).
Proof.
intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
- by apply tctx_borrow. by f_equiv.
+ - by apply tctx_borrow.
+ - by f_equiv.
Qed.
(* See the comment above [tctx_extract_hasty_share]. *)
@@ -91,13 +92,13 @@ Section borrow.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[|l|]|]) "_ Hown"; try done.
- iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
+ iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']"; first done.
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
- - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+ - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]"; first done.
+ iMod (bor_sep with "LFT Hbor") as "[_ Hbor]"; first done.
iMod ("Hclose" with "Htok") as "HL".
iDestruct ("HLclose" with "HL") as "$".
by rewrite tctx_interp_singleton tctx_hasty_val' //=.
@@ -124,7 +125,7 @@ Section borrow.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as (l') "#[H↦b #Hown]".
- iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+ iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']"; first done.
iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
@@ -152,11 +153,11 @@ Section borrow.
iDestruct (Hincl with "HL HE") as "%".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
- iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
- iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
+ iMod (bor_exists with "LFT Hown") as (vl) "Hbor"; first done.
+ iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]"; first done.
destruct vl as [|[[]|][]];
try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
- iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
+ iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']"; first done.
rewrite heap_mapsto_vec_singleton.
iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
iApply wp_fupd. wp_read.
@@ -165,7 +166,7 @@ Section borrow.
iDestruct ("HLclose" with "HL") as "$".
rewrite tctx_interp_singleton tctx_hasty_val' //.
iApply (bor_shorten with "[] Hbor").
- iApply lft_incl_glb. by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ iApply lft_incl_glb; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
Qed.
Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
@@ -186,7 +187,7 @@ Section borrow.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
iDestruct "Hshr" as (l') "[H↦ Hown]".
- iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+ iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']"; first done.
iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
{ iApply lft_incl_glb.
+ by iApply lft_incl_syn_sem.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index fb437c5d..068d1b66 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section typing.
Context `{!typeGS Σ}.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index cd3ca83b..58eb5376 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.lang Require Import notation.
From lrust.typing Require Import type lft_contexts type_context.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section cont_context_def.
Context `{!typeGS Σ}.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index a23415e6..8fd99719 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section get_x.
Context `{!typeGS Σ}.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index d4c2e6f5..c29bc528 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section init_prod.
Context `{!typeGS Σ}.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 1dbeee54..04618e96 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section lazy_lft.
Context `{!typeGS Σ}.
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 1592cc19..b29a8602 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -1,5 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing lib.option.
+From iris.prelude Require Import options.
(* Typing "problem case #3" from:
http://smallcultfollowing.com/babysteps/blog/2016/04/27/non-lexical-lifetimes-introduction/
@@ -74,7 +75,7 @@ Section non_lexical.
Lemma get_default_type :
typed_val get_default (fn(∀ m, ∅; &uniq{m} hashmap, K) → &uniq{m} V).
- Proof.
+ Proof using Type*.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (m Ï ret p). inv_vec p=>map key. simpl_subst.
iApply type_let; [iApply get_mut_type|solve_typing|].
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index b8c0b033..f7713129 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rebor.
Context `{!typeGS Σ}.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 1909c781..d73872b1 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section unbox.
Context `{!typeGS Σ}.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 01ffd0e5..4a151e02 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,6 +1,6 @@
From lrust.lang Require Import proofmode.
From lrust.typing Require Export lft_contexts type bool.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Section fixpoint_def.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9a7711fd..514d37fc 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From iris.algebra Require Import vector list.
From lrust.typing Require Export type.
From lrust.typing Require Import own programs cont.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section fn.
Context `{!typeGS Σ} {A : Type} {n : nat}.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 94771e2f..9b536cd2 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import bool programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section int.
Context `{!typeGS Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index f4383a45..fd97c826 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -3,7 +3,7 @@ From iris.bi Require Import fractional.
From lrust.lang Require Import proofmode.
From lrust.typing Require Export base.
From lrust.lifetime Require Import frac_borrow.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition elctx_elt : Type := lft * lft.
Notation elctx := (list elctx_elt).
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index c49af0d5..1c818641 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -5,7 +5,7 @@ From lrust.lang.lib Require Import memcpy arc.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition arcN := lrustN .@ "arc".
Definition arc_invN := arcN .@ "inv".
@@ -442,7 +442,7 @@ Section arc.
iMod ("Hclose2" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 #Hproto] !>".
iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & _)".
iDestruct "Hpersist" as "(_ & [Hshr|Hν†] & _)"; last first.
- { iMod (lft_incl_dead with "Hαν Hν†") as "Hα†". done.
+ { iMod (lft_incl_dead with "Hαν Hν†") as "Hα†"; first done.
iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
@@ -486,7 +486,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
- iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
+ iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro; first set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -529,7 +529,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
- iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
+ iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro; first set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -574,7 +574,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
- iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
+ iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro; first set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -618,7 +618,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
- iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
+ iMod fupd_mask_subseteq as "Hclose2"; last iModIntro; first set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -662,7 +662,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
- iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
+ iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro; first set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -709,7 +709,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
- iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
+ iMod fupd_mask_subseteq as "Hclose2"; last iModIntro; first set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
- (* Finish up the proof (sucess). *)
@@ -1048,7 +1048,7 @@ Section arc.
iApply type_jump; solve_typing.
- iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
- wp_apply wp_new=>//. lia. iIntros (l) "(H†& Hlvl) (#Hν & Hown & H†') !>".
+ wp_apply wp_new=>//; first lia. iIntros (l) "(H†& Hlvl) (#Hν & Hown & H†') !>".
rewrite -!lock Nat2Z.id.
wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
@@ -1089,7 +1089,7 @@ Section arc.
iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %Hsz.
iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
- wp_apply wp_new=>//. lia. iIntros (l') "(Hl'†& Hl')". wp_let. wp_op.
+ wp_apply wp_new=>//; first lia. iIntros (l') "(Hl'†& Hl')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
rewrite !heap_mapsto_vec_cons shift_loc_assoc.
iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
@@ -1112,7 +1112,10 @@ Section arc.
!tctx_hasty_val' //. unlock. iFrame. iRight.
iExists _, _, _. iFrame "∗#". }
iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
- iApply type_let. apply arc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+ iApply type_let.
+ { apply arc_drop_type. }
+ { solve_typing. }
+ iIntros (drop). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_assign; [solve_typing..|].
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 67af8d85..ef673b5a 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -4,7 +4,7 @@ From lrust.lang Require Import proofmode notation lib.new_delete.
From lrust.lifetime Require Import meta.
From lrust.typing Require Import typing.
From lrust.typing.lib Require Import option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition brandidx_stR := max_natUR.
Class brandidxG Σ := BrandedIdxG {
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 0e343ad8..7d200730 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -3,7 +3,7 @@ From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section cell.
Context `{!typeGS Σ}.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index d0a14ca1..a8cba7f1 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section diverging_static.
Context `{!typeGS Σ}.
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 9756ed20..54ab58f0 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section fake_shared.
Context `{!typeGS Σ}.
@@ -24,7 +24,7 @@ Section fake_shared.
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
{ iApply frac_bor_iff; last done. iIntros "!>!> *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
- iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro. set_solver.
+ iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro; first set_solver.
simpl. iApply ty_shr_mono; last done.
by iApply lft_incl_syn_sem. }
do 2 wp_seq.
@@ -55,7 +55,7 @@ Section fake_shared.
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
{ iApply frac_bor_iff; last done. iIntros "!>!> *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
- iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro. set_solver.
+ iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro; first set_solver.
simpl. iApply ty_shr_mono; last done.
by iApply lft_intersect_incl_l.
}
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 43660eb0..6a5dc438 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -4,7 +4,7 @@ From iris.bi Require Import lib.fractional.
From lrust.lang Require Import proofmode notation.
From lrust.lifetime Require Import meta.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition ghostcellN := lrustN .@ "ghostcell".
Definition ghosttokenN := lrustN .@ "ghosttoken".
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 05f87157..c0a81a94 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition joinN := lrustN .@ "join".
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f87a1467..9bf62cdd 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -4,7 +4,7 @@ From lrust.lang.lib Require Import memcpy lock.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition mutexN := lrustN .@ "mutex".
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 5aea0ab2..dc3ebf95 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -4,7 +4,7 @@ From lrust.lang.lib Require Import memcpy lock.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing util option mutex.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific
interface, like the one provided by lang.lib.lock.
@@ -58,7 +58,7 @@ Section mguard.
iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
(* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
goal, as does "iApply (lft_intersect_mono with ">")". *)
- iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ iNext. iApply lft_intersect_mono; first done. iApply lft_incl_refl.
Qed.
Next Obligation.
iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
@@ -66,10 +66,10 @@ Section mguard.
- by iApply frac_bor_shorten.
- iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ { iApply lft_intersect_mono; last done. iApply lft_incl_refl. }
+ iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
@@ -108,7 +108,7 @@ Section mguard.
iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done.
+ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 1cde437f..0ba57c40 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing lib.panic.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section option.
Context `{!typeGS Σ}.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 28b7991d..fdd142ef 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(* Minimal support for panic. Lambdarust does not support unwinding the
stack. Instead, we just end the current thread by not calling any
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e2c0374c..1c186f39 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -4,7 +4,7 @@ From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition rc_stR :=
prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
@@ -271,7 +271,7 @@ Section code.
}}}.
Proof.
iIntros (? Φ) "[Hna [(Hl1 & Hl2 & H†& Hown)|Hown]] HΦ".
- - wp_read. iApply "HΦ". iFrame "Hl1". iLeft. iSplit. done. iSplit.
+ - wp_read. iApply "HΦ". iFrame "Hl1". iLeft. iSplit; first done. iSplit.
+ iExists _. iFrame "Hl2". iLeft. iFrame. iSplit; first done.
iApply step_fupd_intro; auto.
+ iIntros "Hl1". iFrame. iApply step_fupd_intro; first done.
@@ -418,8 +418,9 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl.
+ - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >% & Hνtok & Hν†)".
wp_read. wp_let.
(* And closing it again. *)
@@ -477,8 +478,9 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl.
+ - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >% & Hνtok & Hν†)".
wp_read. wp_let.
(* And closing it again. *)
@@ -582,8 +584,9 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl.
+ - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >%Hq & Hνtok & Hν†)".
wp_read. wp_let. wp_op. rewrite shift_loc_0. wp_op. wp_write. wp_write.
(* And closing it again. *)
@@ -637,7 +640,7 @@ Section code.
iMod ("Hclose2" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 #Hproto] !>".
iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & _)".
iDestruct "Hpersist" as (ty') "(_ & _ & [Hshr|Hν†] & _)"; last first.
- { iMod (lft_incl_dead with "Hαν Hν†") as "Hα†". done.
+ { iMod (lft_incl_dead with "Hαν Hν†") as "Hα†"; first done.
iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
@@ -1040,7 +1043,7 @@ Section code.
iApply type_jump; solve_typing.
+ wp_op; case_bool_decide; first lia. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
- iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia. done.
+ iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia; first done.
rewrite -!lock Nat2Z.id.
iNext. iIntros (lr) "/= ([H†|%] & H↦lr) [Hty Hproto] !>"; last lia.
rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
@@ -1064,7 +1067,7 @@ Section code.
tctx_hasty_val' //. unlock. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
- - wp_apply wp_new; first lia. done.
+ - wp_apply wp_new; first lia; first done.
iIntros (lr) "/= ([H†|%] & H↦lr)"; last lia.
iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
@@ -1086,7 +1089,8 @@ Section code.
iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
{ iApply (Hclone _ [] $! _ 1%Qp with "LFT HE Hna").
- by rewrite /llctx_interp. by rewrite /tctx_interp. }
+ - by rewrite /llctx_interp.
+ - by rewrite /tctx_interp. }
clear clone Hclone. iIntros (clone) "(Hna & _ & Hclone)".
wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
@@ -1100,7 +1104,7 @@ Section code.
iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %Hsz.
iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
- wp_apply wp_new=>//. lia. iIntros (l') "(Hl'†& Hl')". wp_let. wp_op.
+ wp_apply wp_new=>//; first lia. iIntros (l') "(Hl'†& Hl')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
rewrite !heap_mapsto_vec_cons shift_loc_assoc.
iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
@@ -1123,7 +1127,10 @@ Section code.
!tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
- iApply type_let. apply rc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+ iApply type_let.
+ { apply rc_drop_type. }
+ { solve_typing. }
+ iIntros (drop). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_assign; [solve_typing..|].
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 5448deb7..c40204d5 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -5,7 +5,7 @@ From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
From lrust.typing.lib Require Export rc.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section weak.
Context `{!typeGS Σ, !rcG Σ}.
@@ -260,8 +260,9 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl.
+ - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hrcst)".
wp_read. wp_let. wp_op. wp_op. wp_write. wp_write.
(* And closing it again. *)
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index c8b40966..9d707fa6 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.refcell Require Import refcell.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition refcell_refN := refcellN .@ "ref".
@@ -39,26 +39,26 @@ Section ref.
Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+ iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
- iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
- iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
- iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
+ iMod (bor_exists with "LFT Hb") as (ν) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (q') "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (ty') "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hshr Hb]"; first done.
+ iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]"; first done.
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hinv Hb]"; first done.
+ iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hκν Hb]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. by rewrite Qp_mul_1_r. }
- iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
+ iMod (bor_na with "Hb") as "#Hb"; first done. eauto 20.
Qed.
Next Obligation.
iIntros (??????) "#? H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 58a897fa..88fa78bc 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.refcell Require Import refcell ref.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section ref_functions.
Context `{!typeGS Σ, !refcellG Σ}.
@@ -57,10 +57,10 @@ Section ref_functions.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
wp_op.
iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
+ iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]"; first done.
iMod (lctx_lft_alive_tok_noend α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
[solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]"; first done.
iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
@@ -116,7 +116,7 @@ Section ref_functions.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]=>//=.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]"; first done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -155,7 +155,7 @@ Section ref_functions.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
iDestruct "Hx" as (ν q γ β ty') "(_ & #Hαβ & #Hinv & Hν & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]"; first done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct (refcell_inv_reading_inv with "INV [$Hâ—¯]")
as (q' n) "(H↦lrc & >% & Hâ—â—¯ & H†& Hq' & Hshr)".
@@ -327,7 +327,7 @@ Section ref_functions.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
- iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]"; first done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct (refcell_inv_reading_inv with "INV Hγ")
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index b87dbc9d..e081d017 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition refcell_stR :=
optionUR (prodR (prodR
@@ -118,7 +118,7 @@ Section refcell.
Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]"; first done.
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
iDestruct "H" as "Hown".
iMod ("Hclose" $! ((∃ n:Z, l ↦ #n) ∗
@@ -128,34 +128,36 @@ Section refcell.
iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame. }
{ iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
iSplitL "Hn"; eauto with iFrame. }
- iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
- iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
+ iMod (bor_sep with "LFT H") as "[Hn Hvl]"; first done.
+ iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]"; first done.
iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
as "[$ HQ]"; last first.
{ iMod ("Hclose" with "[] HQ") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)". eauto.
- - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
+ - iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+ iExists κ, γ. iSplitR.
+ + by iApply lft_incl_refl.
+ + by iApply bor_na. }
clear dependent n. iDestruct "H" as ([|n|n]) "Hn"; try lia.
- iFrame. iMod (own_alloc (◠None)) as (γ) "Hst"; first by apply auth_auth_valid.
iExists γ, None. by iFrame.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first done.
iMod (own_alloc (◠(refcell_st_to_R $ Some (ν, false, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]"; first done.
{ iApply lft_intersect_incl_l. }
iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
- iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
+ iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]"; first done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn Hshr".
iSplitR "Htok2"; last by iExists _; iFrame; rewrite Qp_div_2.
iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
- iApply fupd_mask_mono; last iApply "Hh". set_solver+. rewrite -lft_dead_or. auto.
+ iApply fupd_mask_mono; last iApply "Hh"; first set_solver+. rewrite -lft_dead_or. auto.
- iMod (own_alloc (◠(refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
- { rewrite -step_fupd_intro. auto. set_solver+. }
+ { rewrite -step_fupd_intro; first auto. set_solver+. }
iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
iApply lft_tok_static.
Qed.
@@ -194,7 +196,8 @@ Section refcell.
- iIntros "!> %α %tid %l H". simpl.
iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
- by iApply "Hty1ty2". by iApply "Hty2ty1".
+ + by iApply "Hty1ty2".
+ + by iApply "Hty2ty1".
Qed.
Lemma refcell_mono' E L ty1 ty2 :
eqtype E L ty1 ty2 → subtype E L (refcell ty1) (refcell ty2).
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 6de85bb7..65c2dfb5 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -5,7 +5,7 @@ From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.refcell Require Import refcell ref refmut.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section refcell_functions.
Context `{!typeGS Σ, !refcellG Σ}.
@@ -154,7 +154,7 @@ Section refcell_functions.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]=>//=.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']"; first done.
iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose'')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- iMod ("Hclose''" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
@@ -190,15 +190,15 @@ Section refcell_functions.
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
iExists _. iFrame. rewrite -(assoc Qp_add) Qp_div_2 //.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first done.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
rewrite (right_id None). iExists _, _. iFrame "Htok1 Hreading".
iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". done.
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]"; first done.
{ iApply lft_intersect_incl_l. }
- iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
+ iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]"; first done. iFrame "Hshr".
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame "∗#".
iSplitR "Htok2".
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
@@ -218,7 +218,7 @@ Section refcell_functions.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. simpl. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
- iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -264,7 +264,7 @@ Section refcell_functions.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]=>//=.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']"; first done.
iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- wp_write. wp_apply wp_new; [done..|].
@@ -272,13 +272,13 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
destruct st as [[[[ν []] s] n]|]; try done.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first done.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc,
(op_local_update_discrete _ _ (refcell_st_to_R $ Some (ν, true, (1/2)%Qp, xH))). }
rewrite (right_id None).
iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]"; first done.
{ iApply lft_intersect_incl_l. }
iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh Htok1] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iNext. iSplitL "Hbh".
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index fd465bbd..b67458a4 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing util.
From lrust.typing.lib.refcell Require Import refcell.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section refmut.
Context `{!typeGS Σ, !refcellG Σ}.
@@ -40,22 +40,22 @@ Section refmut.
Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+ iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hαβ H]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
- iMod (bor_sep with "LFT H") as "[_ H]". done.
- iMod (bor_sep with "LFT H") as "[H _]". done.
- iMod (bor_fracture (λ q, (q' * q).[ν])%I with "LFT [H]") as "H". done.
+ iMod (bor_exists with "LFT Hb") as (ν) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (q') "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (ty') "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hb H]"; first done.
+ iMod (bor_sep with "LFT H") as "[Hαβ H]"; first done.
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
+ iMod (bor_sep with "LFT H") as "[_ H]"; first done.
+ iMod (bor_sep with "LFT H") as "[H _]"; first done.
+ iMod (bor_fracture (λ q, (q' * q).[ν])%I with "LFT [H]") as "H"; first done.
{ by rewrite Qp_mul_1_r. }
iDestruct (frac_bor_lft_incl with "LFT H") as "#Hκν". iClear "H".
iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
@@ -68,10 +68,10 @@ Section refmut.
- by iApply frac_bor_shorten.
- iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ { iApply lft_intersect_mono; last done. iApply lft_incl_refl. }
+ iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
@@ -106,7 +106,7 @@ Section refmut.
iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done.
- + iApply lft_intersect_mono. by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ + iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ by iApply "Hs".
Qed.
Global Instance refmut_mono_flip E L :
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 18eea9e8..c295c787 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.refcell Require Import refcell refmut.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section refmut_functions.
Context `{!typeGS Σ, !refcellG Σ}.
@@ -29,7 +29,7 @@ Section refmut_functions.
iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
[solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]"; first done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
[solve_typing..|].
@@ -64,27 +64,27 @@ Section refmut_functions.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
- iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
- iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+ iMod (bor_exists with "LFT Hx'") as (vl) "H"; first done.
+ iMod (bor_sep with "LFT H") as "[H↦ H]"; first done.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose')";
[solve_typing..|].
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]]; simpl;
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
- iMod (bor_exists with "LFT H") as (ν) "H". done.
- iMod (bor_exists with "LFT H") as (q) "H". done.
- iMod (bor_exists with "LFT H") as (γ) "H". done.
- iMod (bor_exists with "LFT H") as (δ) "H". done.
- iMod (bor_exists with "LFT H") as (ty') "H". done.
- iMod (bor_sep with "LFT H") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
- iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
- iMod (bor_sep with "LFT H") as "[_ H]". done.
- iMod (bor_sep with "LFT H") as "[H _]". done.
- iMod (bor_fracture (λ q', (q * q').[ν])%I with "LFT [H]") as "H". done.
+ iMod (bor_exists with "LFT H") as (ν) "H"; first done.
+ iMod (bor_exists with "LFT H") as (q) "H"; first done.
+ iMod (bor_exists with "LFT H") as (γ) "H"; first done.
+ iMod (bor_exists with "LFT H") as (δ) "H"; first done.
+ iMod (bor_exists with "LFT H") as (ty') "H"; first done.
+ iMod (bor_sep with "LFT H") as "[Hb H]"; first done.
+ iMod (bor_sep with "LFT H") as "[Hβδ H]"; first done.
+ iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]"; first done.
+ iMod (bor_sep with "LFT H") as "[_ H]"; first done.
+ iMod (bor_sep with "LFT H") as "[H _]"; first done.
+ iMod (bor_fracture (λ q', (q * q').[ν])%I with "LFT [H]") as "H"; first done.
{ by rewrite Qp_mul_1_r. }
iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
- rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
- iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+ rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]"; first done.
+ iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]"; first done.
wp_bind (!#lx')%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
@@ -124,7 +124,7 @@ Section refmut_functions.
iDestruct "Hx" as (ν q γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]"; first done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct "INV" as (st) "(H↦lrc & H◠& INV)". wp_read. wp_let. wp_op. wp_write.
iAssert (|={↑lftN ∪ lft_userE}[lft_userE]▷=> refcell_inv tid lrc γ β ty')%I
@@ -193,7 +193,7 @@ Section refmut_functions.
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν q γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
- wp_read. wp_let. wp_apply wp_new; first done. done.
+ wp_read. wp_let. wp_apply wp_new; [done..|].
iIntros (lx) "(H†& Hlx)". rewrite heap_mapsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
@@ -298,7 +298,7 @@ Section refmut_functions.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
- iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]"; first done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct "INV" as (st) "(Hlrc & Hâ— & Hst)".
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 7caefcf0..5df708e4 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import auth csum frac agree excl numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition rwlock_stR :=
optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
@@ -80,7 +80,7 @@ Section rwlock_inv.
iDestruct "H" as "($&$&H)"; destruct st as [[|[[agν ?]?]|]|]; try done;
last by iApply "Hb".
iDestruct "H" as (ν q') "(Hag & #Hend & Hh & ? & ? & ?)". iExists ν, q'.
- iFrame. iSplitR. done. iSplitL "Hh"; last by iApply "Hshr".
+ iFrame. iSplitR; first done. iSplitL "Hh"; last by iApply "Hshr".
iIntros "Hν". iApply "Hb". iApply ("Hh" with "Hν").
Qed.
@@ -128,7 +128,7 @@ Section rwlock.
Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]"; first done.
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
iDestruct "H" as "[>% Hown]".
iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ nâŒ) ∗
@@ -138,26 +138,26 @@ Section rwlock.
iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
{ iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
iSplitL "Hn"; [eauto|iExists _; iFrame]. }
- iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
- iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
+ iMod (bor_sep with "LFT H") as "[Hn Hvl]"; first done.
+ iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]"; first done.
iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid tid l γ κ ty)%I with "[> -Hclose]"
as "[$ HQ]"; last first.
{ iMod ("Hclose" with "[] HQ") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
- - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try done.
+ - iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+ iExists κ, γ. iSplitR; first by iApply lft_incl_refl. iApply bor_share; try done.
solve_ndisj. }
clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
- iFrame. iMod (own_alloc (◠None)) as (γ) "Hst"; first by apply auth_auth_valid.
iExists γ, None. by iFrame.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first done.
iMod (own_alloc (◠Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
- iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]"; first done.
{ iApply lft_intersect_incl_l. }
iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
- iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
+ iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]"; first done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Hshr}".
iSplitR; first by auto. iFrame "Htok2". iSplitR; first done.
@@ -202,7 +202,8 @@ Section rwlock.
- iIntros "!> %α %tid %l H". simpl.
iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
iApply at_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
- by iApply "Hty1ty2". by iApply "Hty2ty1".
+ + by iApply "Hty1ty2".
+ + by iApply "Hty2ty1".
Qed.
Lemma rwlock_mono' E L ty1 ty2 :
eqtype E L ty1 ty2 → subtype E L (rwlock ty1) (rwlock ty2).
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index c3e953d2..b2f06258 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -5,7 +5,7 @@ From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlock_functions.
Context `{!typeGS Σ, !rwlockG Σ}.
@@ -160,7 +160,7 @@ Section rwlock_functions.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']"; first done.
wp_bind (!ˢᶜ(LitV lx))%E.
iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & INV)". wp_read.
@@ -199,15 +199,15 @@ Section rwlock_functions.
iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first solve_ndisj.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite (right_id None). iExists _, _. iFrame "Htok1 Hreading".
iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
- iApply (fupd_mask_mono (↑lftN)). solve_ndisj.
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
+ iApply (fupd_mask_mono (↑lftN)); first solve_ndisj.
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]"; first solve_ndisj.
{ iApply lft_intersect_incl_l. }
- iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". solve_ndisj.
+ iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]"; first solve_ndisj.
iFrame "#". iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
rewrite Qp_div_2. iSplitL; last done.
@@ -231,7 +231,7 @@ Section rwlock_functions.
iSpecialize ("Hk" with "[]"); first solve_typing.
iApply ("Hk" $! [#] with "Hna HL").
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
- iExists _. iSplit. done. simpl. eauto.
+ iExists _. iSplit; first done. simpl. eauto.
Qed.
(* Acquiring a write lock. *)
@@ -267,7 +267,7 @@ Section rwlock_functions.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']"; first done.
wp_bind (CAS _ _ _).
iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st as [c|].
@@ -294,7 +294,7 @@ Section rwlock_functions.
#lx ◠rwlockwriteguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame. iExists _, _, _. iFrame "∗#". }
+ tctx_hasty_val' //. iFrame. iExists _, _, _. iFrame "∗#". }
iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 66605b0d..429772c2 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockreadguard.
Context `{!typeGS Σ, !rwlockG Σ}.
@@ -33,23 +33,23 @@ Section rwlockreadguard.
Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+ iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (tid_own) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
- iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
- iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
- iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
+ iMod (bor_exists with "LFT Hb") as (ν) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (q') "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (tid_own) "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hshr Hb]"; first done.
+ iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]"; first done.
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hinv Hb]"; first done.
+ iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hκν _]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. by rewrite Qp_mul_1_r. }
iExists _. iFrame "#". iApply ty_shr_mono; last done.
@@ -93,7 +93,9 @@ Section rwlockreadguard.
iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
+ iApply (at_bor_iff with "[] Hinv").
- iIntros "!> !>"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
+ iIntros "!> !>"; iSplit; iIntros "H".
+ * by iApply "Hty1ty2".
+ * by iApply "Hty2ty1".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
iFrame. iApply ty_shr_mono; last by iApply "Hs".
iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 1b553acc..279656a0 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockreadguard_functions.
Context `{!typeGS Σ, !rwlockG Σ}.
@@ -29,7 +29,7 @@ Section rwlockreadguard_functions.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]"; first done.
rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
@@ -74,7 +74,7 @@ Section rwlockreadguard_functions.
destruct x' as [[|lx'|]|]; try done. simpl.
iDestruct "Hx'" as (ν q γ β tid_own) "(Hx' & #Hαβ & #Hinv & Hν & H◯ & H†)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]"; first done.
wp_bind (!ˢᶜ#lx')%E.
iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st) "[H↦ INV]". wp_read.
@@ -102,7 +102,7 @@ Section rwlockreadguard_functions.
iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
iApply (own_update_2 with "Hâ— Hâ—¯"). apply auth_update_dealloc.
rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
- - iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
+ - iApply step_fupd_intro; first set_solver. iNext. iIntros "Hlx".
apply csum_included in Hle.
destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
[by subst|].
@@ -120,7 +120,7 @@ Section rwlockreadguard_functions.
{ rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
apply (cancel_local_update_unit (reading_st q ν)) , _. }
- iApply (wp_step_fupd with "INV"). set_solver.
+ iApply (wp_step_fupd with "INV"); first set_solver.
iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -132,7 +132,8 @@ Section rwlockreadguard_functions.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_jump; solve_typing.
+ iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
- iMod ("Hcloseβ" with "[Hlx H◠Hst]") as "Hβ". by iExists _; iFrame.
+ iMod ("Hcloseβ" with "[Hlx H◠Hst]") as "Hβ".
+ { by iExists _; iFrame. }
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iModIntro. wp_if.
iApply (type_type _ _ _ [ x ◠box (uninit 1); #lx' ◠rwlockreadguard α ty]
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 925a746f..801c4ab5 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import util typing.
From lrust.typing.lib.rwlock Require Import rwlock.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockwriteguard.
Context `{!typeGS Σ, !rwlockG Σ}.
@@ -34,21 +34,21 @@ Section rwlockwriteguard.
Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
+ iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (tid_shr) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+ iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
+ iMod (bor_exists with "LFT Hb") as (tid_shr) "Hb"; first done.
+ iMod (bor_sep with "LFT Hb") as "[Hb H]"; first done.
+ iMod (bor_sep with "LFT H") as "[Hαβ _]"; first done.
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
(* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
goal, as does "iApply (lft_intersect_mono with ">")". *)
- iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ iNext. iApply lft_intersect_mono; first done. iApply lft_incl_refl.
Qed.
Next Obligation.
iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
@@ -56,10 +56,10 @@ Section rwlockwriteguard.
- by iApply frac_bor_shorten.
- iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ { iApply lft_intersect_mono; last done. iApply lft_incl_refl. }
+ iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
@@ -93,7 +93,9 @@ Section rwlockwriteguard.
iExists vl; iFrame; by iApply "Ho".
+ iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
+ iApply at_bor_iff; try done.
- iIntros "!>!>"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
+ iIntros "!>!>"; iSplit; iIntros "H".
+ * by iApply "Hty1ty2".
+ * by iApply "Hty2ty1".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index ab0daec5..3c9ac622 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockwriteguard_functions.
Context `{!typeGS Σ, !rwlockG Σ}.
@@ -30,7 +30,7 @@ Section rwlockwriteguard_functions.
iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
[solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]"; first done.
rewrite heap_mapsto_vec_singleton.
iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
[solve_typing..|].
@@ -72,19 +72,19 @@ Section rwlockwriteguard_functions.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
- iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
- iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+ iMod (bor_exists with "LFT Hx'") as (vl) "H"; first done.
+ iMod (bor_sep with "LFT H") as "[H↦ H]"; first done.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
destruct vl as [|[[|l|]|][]];
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
rewrite heap_mapsto_vec_singleton.
- iMod (bor_exists with "LFT H") as (γ) "H". done.
- iMod (bor_exists with "LFT H") as (δ) "H". done.
- iMod (bor_exists with "LFT H") as (tid_shr) "H". done.
- iMod (bor_sep with "LFT H") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
- iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
- iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+ iMod (bor_exists with "LFT H") as (γ) "H"; first done.
+ iMod (bor_exists with "LFT H") as (δ) "H"; first done.
+ iMod (bor_exists with "LFT H") as (tid_shr) "H"; first done.
+ iMod (bor_sep with "LFT H") as "[Hb H]"; first done.
+ iMod (bor_sep with "LFT H") as "[Hβδ _]"; first done.
+ iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]"; first done.
+ iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]"; first done.
wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_op. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
@@ -93,8 +93,8 @@ Section rwlockwriteguard_functions.
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
- iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
- by iApply lft_incl_refl. }
+ - iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
+ - by iApply lft_incl_refl. }
iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -122,7 +122,7 @@ Section rwlockwriteguard_functions.
iDestruct "Hx'" as (γ β tid_own) "(Hx' & #Hαβ & #Hinv & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]"; first done.
wp_bind (#lx' <-ˢᶜ #0)%E.
iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st) "(H↦ & H◠& INV)". wp_write.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index b51fbaf5..64e558d4 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition spawnN := lrustN .@ "spawn".
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 30590962..92456d63 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.lang.lib Require Import swap.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section swap.
Context `{!typeGS Σ}.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 893f70ae..f2f4c05d 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -3,7 +3,7 @@ From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section code.
Context `{!typeGS Σ}.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index af3db712..20c253f3 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From lrust.lang.lib Require Import memcpy.
From lrust.typing Require Export type.
From lrust.typing Require Import util uninit type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section own.
Context `{!typeGS Σ}.
@@ -36,7 +36,9 @@ Section own.
destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
- by rewrite left_id shift_loc_0.
- by rewrite right_id Nat.add_0_r.
- - iSplit. by iIntros "[[]?]". by iIntros "[]".
+ - iSplit.
+ + by iIntros "[[]?]".
+ + by iIntros "[]".
- rewrite heap_freeable_op_eq. f_equiv.
by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
Qed.
@@ -78,7 +80,7 @@ Section own.
Next Obligation.
intros _ ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb #Hvs]".
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!> %F %q % Htok".
+ iExists l'. iSplit; first by iApply (frac_bor_shorten with "[]"). iIntros "!> %F %q % Htok".
iApply (step_fupd_mask_mono F _ (F∖↑shrN)); [solve_ndisj..|].
iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
@@ -99,7 +101,7 @@ Section own.
iApply "Ho".
- iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iFrame. iIntros "!>". iIntros (F' q) "% Htok".
- iMod ("Hvs" with "[%] Htok") as "Hvs'". done. iModIntro. iNext.
+ iMod ("Hvs" with "[%] Htok") as "Hvs'"; first done. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
@@ -322,7 +324,7 @@ Section typing.
{ (* TODO : simpl_subst should be able to do this. *)
unfold subst=>/=. repeat f_equal.
- by rewrite bool_decide_true.
- - eapply is_closed_subst. done. set_solver. }
+ - eapply is_closed_subst; first done. set_solver. }
iApply type_assign; [|solve_typing|by eapply write_own|solve_typing].
apply subst_is_closed; last done. apply is_closed_of_val.
Qed.
@@ -345,9 +347,9 @@ Section typing.
(xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
{ (* TODO : simpl_subst should be able to do this. *)
unfold subst=>/=. repeat f_equal.
- - eapply (is_closed_subst []). apply is_closed_of_val. set_solver.
+ - eapply (is_closed_subst []); last set_solver. apply is_closed_of_val.
- by rewrite bool_decide_true.
- - eapply is_closed_subst. done. set_solver. }
+ - eapply is_closed_subst; first done. set_solver. }
rewrite Nat2Z.id. iApply type_memcpy.
+ apply subst_is_closed; last done. apply is_closed_of_val.
+ solve_typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 82ec0d17..cea73ac8 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From iris.algebra Require Import list numbers.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section product.
Context `{!typeGS Σ}.
@@ -22,7 +22,7 @@ Section product.
Global Instance unit0_copy : Copy unit0.
Proof.
- split. by apply _. iIntros (????????) "_ _ Htok $".
+ split; first by apply _. iIntros (????????) "_ _ Htok $".
iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
iExists 1%Qp. iModIntro. iSplitR.
{ iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
@@ -96,7 +96,7 @@ Section product.
iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iModIntro.
- iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
- iExists _, _. iSplit. done. iSplitL "Hown1".
+ iExists _, _. iSplit; first done. iSplitL "Hown1".
+ by iApply "Ho1".
+ by iApply "Ho2".
- iIntros (???) "#[Hshr1 Hshr2]". iSplit.
@@ -128,7 +128,9 @@ Section product.
iDestruct (ty_size_eq with "H2") as "#>%".
iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
- - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
+ - iNext. iSplitL "H↦1 H1".
+ + iExists vl1. by iFrame.
+ + iExists vl2. by iFrame.
- iIntros "Htl [H1 H2]". iDestruct ("Htlclose" with "Htl") as "Htl".
iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
iDestruct (ty_size_eq with "H1") as "#>%".
@@ -136,8 +138,8 @@ Section product.
iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
rewrite !heap_mapsto_vec_op; [|congruence..].
iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
- iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]". by iExists _; iFrame.
- iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]". by iExists _; iFrame. done.
+ iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]"; first by iExists _; iFrame.
+ iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]"; last done. by iExists _; iFrame.
Qed.
Global Instance product2_send `{!Send ty1} `{!Send ty2} :
@@ -203,10 +205,10 @@ Section typing.
iSplit; first by rewrite /= assoc. iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
- iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit; first by rewrite assoc. iFrame. iExists _, _. by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
- iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit; first by rewrite -assoc. iFrame. iExists _, _. by iFrame.
- iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
by iFrame.
- iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
@@ -239,7 +241,7 @@ Section typing.
eqtype E L (Î (tyl1 ++ Î tyl2 :: tyl3)) (Î (tyl1 ++ tyl2 ++ tyl3)).
Proof.
unfold product. induction tyl1; simpl; last by f_equiv.
- induction tyl2. by rewrite left_id. by rewrite /= -assoc; f_equiv.
+ induction tyl2; first by rewrite left_id. by rewrite /= -assoc; f_equiv.
Qed.
Lemma prod_flatten_l E L tyl1 tyl2 :
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 0563f6a0..42e0a444 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
From lrust.typing Require Import shr_bor.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section product_split.
Context `{!typeGS Σ}.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index f0448ba9..c4692f28 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,6 +1,6 @@
From lrust.lang Require Import proofmode memcpy.
From lrust.typing Require Export type lft_contexts type_context cont_context.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section typing.
Context `{!typeGS Σ}.
@@ -70,7 +70,7 @@ Section typing.
∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌠∗ l ↦∗ vl ∗
(▷ l ↦∗: ty.(ty_own) tid ={F}=∗
llctx_interp_noend qmax L qL ∗ ty2.(ty_own) tid [v]))%I.
- Definition typed_write_aux : seal (@typed_write_def). by eexists. Qed.
+ Definition typed_write_aux : seal (@typed_write_def). Proof. by eexists. Qed.
Definition typed_write := typed_write_aux.(unseal).
Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
Global Arguments typed_write _ _ _%T _%T _%T.
@@ -91,7 +91,7 @@ Section typing.
∃ (l : loc) vl q, ⌜v = #l⌠∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
(l ↦∗{q} vl ={F}=∗ na_own tid F ∗
llctx_interp_noend qmax L qL ∗ ty2.(ty_own) tid [v]))%I.
- Definition typed_read_aux : seal (@typed_read_def). by eexists. Qed.
+ Definition typed_read_aux : seal (@typed_read_def). Proof. by eexists. Qed.
Definition typed_read := typed_read_aux.(unseal).
Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
Global Arguments typed_read _ _ _%T _%T _%T.
@@ -229,7 +229,7 @@ Section typing_rules.
⊢ typed_instruction_ty E L [p ◠ty] p ty.
Proof.
iIntros (??) "_ _ $$ [? _]".
- iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
+ iApply (wp_hasty with "[-]"); first done. iIntros (v) "_ Hv".
rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
Qed.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index cebbcef5..7d7a8967 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section shr_bor.
Context `{!typeGS Σ}.
@@ -78,7 +78,7 @@ Section typing.
iIntros (Hκκ' tid ??) "#LFT #HE HL [H _]". iDestruct (Hκκ' with "HL HE") as "%".
iFrame. rewrite /tctx_interp /=.
iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
- - iExists _. iSplit. done. iApply (ty_shr_mono with "[] Hshr").
+ - iExists _. iSplit; first done. iApply (ty_shr_mono with "[] Hshr").
by iApply lft_incl_syn_sem.
- iSplit=> //. iExists _. auto.
Qed.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index ebe28593..294469f0 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -4,8 +4,8 @@ From iris.proofmode Require Import proofmode.
From lrust.lang Require Import races adequacy proofmode notation.
From lrust.lifetime Require Import lifetime frac_borrow.
From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
-Set Default Proof Using "Type".
Class typeGpreS Σ := PreTypeG {
type_preG_lrustGS :> lrustGpreS Σ;
@@ -32,16 +32,16 @@ Section type_soundness.
Proof.
intros Hmain Hrtc.
cut (adequate NotStuck (main [exit_cont]%E) ∅ (λ _ _, True)).
- { split. by eapply adequate_nonracing.
+ { split; first by eapply adequate_nonracing.
intros. by eapply (adequate_not_stuck _ (main [exit_cont]%E)). }
apply: lrust_adequacy=>?. iIntros "_".
iMod (lft_init _ lft_userE) as (?) "#LFT"; [done|solve_ndisj|].
iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
wp_bind (of_val main). iApply (wp_wand with "[Htl]").
- iApply (Hmain Htype [] [] $! tid 1%Qp with "LFT [] Htl [] []").
- { by rewrite /elctx_interp big_sepL_nil. }
- { by rewrite /llctx_interp big_sepL_nil. }
- { by rewrite tctx_interp_nil. }
+ { iApply (Hmain Htype [] [] $! tid 1%Qp with "LFT [] Htl [] []").
+ - by rewrite /elctx_interp big_sepL_nil.
+ - by rewrite /llctx_interp big_sepL_nil.
+ - by rewrite tctx_interp_nil. }
clear Hrtc Hmain main. iIntros (main) "(Htl & _ & Hmain & _)".
iDestruct "Hmain" as (?) "[EQ Hmain]".
rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c124981f..a83b066e 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import list.
From iris.bi Require Import fractional.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section sum.
Context `{!typeGS Σ}.
@@ -178,7 +178,7 @@ Section sum.
Proof.
intros HFA. split.
- intros tid vl.
- cut (∀ i vl', Persistent (ty_own (nth i tyl emp0) tid vl')). by apply _.
+ cut (∀ i vl', Persistent (ty_own (nth i tyl emp0) tid vl')); first by apply _.
intros. apply @copy_persistent.
edestruct nth_in_or_default as [| ->]; [by eapply List.Forall_forall| ].
split; first by apply _. iIntros (????????) "? []".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index ea40b66f..2da15ced 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -4,7 +4,7 @@ From lrust.lang Require Export proofmode notation.
From lrust.lifetime Require Export frac_borrow.
From lrust.typing Require Export base.
From lrust.typing Require Import lft_contexts.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Class typeGS Σ := TypeG {
type_lrustGS :> lrustGS Σ;
@@ -216,7 +216,7 @@ Section ofe.
- (* TODO: automate this *)
repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
+ apply bi.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
- + apply bi.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
+ + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; first by apply Hty. by rewrite Hty.
+ apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+ apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
Qed.
@@ -251,7 +251,7 @@ Section ofe.
Global Instance ty_of_st_ne : NonExpansive ty_of_st.
Proof.
- intros n ?? EQ. constructor; try apply EQ. done.
+ intros n ?? EQ. constructor; try apply EQ; first done.
- simpl. intros; repeat f_equiv. apply EQ.
Qed.
Global Instance ty_of_st_proper : Proper ((≡) ==> (≡)) ty_of_st.
@@ -287,7 +287,7 @@ Section type_dist2.
Global Instance type_dist2_later_equivalence n :
Equivalence (type_dist2_later n).
- Proof. destruct n as [|n]. by split. apply type_dist2_equivalence. Qed.
+ Proof. destruct n as [|n]; first by split. apply type_dist2_equivalence. Qed.
(* The hierarchy of metrics:
dist n → type_dist2 n → dist_later n → type_dist2_later. *)
@@ -587,7 +587,7 @@ Section subtyping.
iDestruct (H12 with "HL") as "#H12".
iDestruct (H23 with "HL") as "#H23".
iClear "∗". iIntros "!> #HE".
- iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
+ iApply (type_incl_trans with "[#]"); first by iApply "H12". by iApply "H23".
Qed.
Lemma subtype_Forall2_llctx_noend E L tys1 tys2 qmax qL :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 2f9fe917..88b326d1 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Import type lft_contexts.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition path := expr.
Bind Scope expr_scope with path.
@@ -33,7 +33,7 @@ Section type_context.
Lemma eval_path_of_val (v : val) :
eval_path v = Some v.
- Proof. destruct v. done. simpl. rewrite (decide_True_pi _). done. Qed.
+ Proof. destruct v; first done. simpl. rewrite (decide_True_pi _). done. Qed.
Lemma wp_eval_path E p v :
eval_path p = Some v → ⊢ WP p @ E {{ v', ⌜v' = v⌠}}.
@@ -213,7 +213,7 @@ Section type_context.
Proof.
remember (p â— ty). induction 1 as [|???? IH]; subst.
- apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
- - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
+ - etrans; first by apply (tctx_incl_frame_l [_]), IH, reflexivity.
apply contains_tctx_incl, submseteq_swap.
Qed.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 1084b37d..368adcf4 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From lrust.lang Require Import memcpy.
From lrust.typing Require Import uninit uniq_bor shr_bor own sum.
From lrust.typing Require Import lft_contexts type_context programs product.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section case.
Context `{!typeGS Σ}.
@@ -67,8 +67,8 @@ Section case.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[|l|]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
- iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
- iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']". done.
+ iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first done.
+ iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']"; first done.
iDestruct "H↦" as (vl) "[H↦ Hown]".
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
iDestruct "EQlen" as %[=EQlen].
@@ -85,7 +85,7 @@ Section case.
iExists (#i::vl'2++vl''). iIntros "!>". iNext.
iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
- iFrame. iExists _, _, _. iSplit. by auto.
+ iFrame. iExists _, _, _. iSplit; first by auto.
rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
{ iExists vl'. iFrame. }
iMod ("Hclose" with "Htok") as "HL".
@@ -124,8 +124,8 @@ Section case.
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
iDestruct "Hp" as (i) "[#Hb Hshr]".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
- iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
- iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
+ iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first done.
+ iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']"; first done.
rewrite nth_lookup.
destruct (tyl !! i) as [ty|] eqn:EQty; last done.
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
@@ -203,7 +203,7 @@ Section case.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
rewrite typed_write_eq in Hw.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
- iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+ iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)"; first done.
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index bee83efc..e03975f5 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,3 +3,4 @@ From lrust.typing Require Export
lft_contexts type_context cont_context programs cont type
int bool own uniq_bor shr_bor uninit product sum fixpoint function
product_split borrow type_sum.
+From iris.prelude Require Import options.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 4b2c877e..d506d720 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
From lrust.typing Require Import product.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section uninit.
Context `{!typeGS Σ}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 9fe721a8..2b22b368 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import proofmode.
From lrust.lang Require Import heap.
From lrust.typing Require Export type.
From lrust.typing Require Import util lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section uniq_bor.
Context `{!typeGS Σ}.
@@ -32,8 +32,8 @@ Section uniq_bor.
Next Obligation.
intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
+ { iApply lft_intersect_mono; last done. iApply lft_incl_refl. }
+ iExists l'. iSplit; first by iApply (frac_bor_shorten with "[]").
iIntros "!> %F %q % Htok". iApply (step_fupd_mask_mono F _ (F∖↑shrN)); try solve_ndisj.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
@@ -81,7 +81,7 @@ Section uniq_bor.
Qed.
Global Instance uniq_mono_flip E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
- Proof. intros ??????. apply uniq_mono. done. by symmetry. Qed.
+ Proof. intros ??????. apply uniq_mono; first done. by symmetry. Qed.
Global Instance uniq_proper E L :
Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) uniq_bor.
Proof. intros ??[]; split; by apply uniq_mono. Qed.
@@ -131,7 +131,7 @@ Section typing.
iDestruct (lft_incl_syn_sem κ' κ H) as "Hκκ'".
iFrame. rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[% Hb]"; try done.
- iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
+ iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]"; first done. iModIntro.
iSplitL "Hb"; iExists _; auto.
Qed.
@@ -154,7 +154,7 @@ Section typing.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iIntros "!>".
iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
- iMod ("Hclose'" with "[H↦]") as "[$ Htok]". by iExists _; iFrame.
+ iMod ("Hclose'" with "[H↦]") as "[$ Htok]"; first by iExists _; iFrame.
by iMod ("Hclose" with "Htok") as "($ & $ & $)".
Qed.
@@ -168,7 +168,7 @@ Section typing.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
iDestruct "Hown" as ">%". iModIntro. iExists _, _. iSplit; first done.
iFrame. iIntros "Hown". iDestruct "Hown" as (vl') "[H↦ Hown]".
- iMod ("Hclose'" with "[H↦ Hown]") as "[$ Htok]". by iExists _; iFrame.
+ iMod ("Hclose'" with "[H↦ Hown]") as "[$ Htok]"; first by iExists _; iFrame.
by iMod ("Hclose" with "Htok") as "($ & $ & $)".
Qed.
End typing.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index e2489c01..bf8c3b7e 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import proofmode.
From lrust.typing Require Export type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section util.
Context `{!typeGS Σ}.
--
GitLab