From d74e871f5777052e02796f566e5d13a51c617289 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Fri, 2 Feb 2024 16:24:50 +0100
Subject: [PATCH] Some cleanup
---
theories/channel/multi_channel.v | 114 +++++++++-------------
theories/channel/multi_proto.v | 158 ++++++++++++-------------------
2 files changed, 103 insertions(+), 169 deletions(-)
diff --git a/theories/channel/multi_channel.v b/theories/channel/multi_channel.v
index aabf48d..2cf1f6d 100644
--- a/theories/channel/multi_channel.v
+++ b/theories/channel/multi_channel.v
@@ -148,9 +148,8 @@ Section channel.
Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
Proof.
rewrite iProto_pointsto_eq.
- iDestruct 1 as
- (γ γE l n i p ->) "(#IH & Hls & Hle & H◠& H◯ & Hown)".
- iIntros "Hle'". iExists γ, γE, l, n, i, p.
+ iDestruct 1 as (?????? ->) "(#IH & Hls & Hle & Hâ— & Hâ—¯ & Hown)".
+ iIntros "Hle'". iExists _,_,_,_,_,p'.
iSplit; [done|]. iFrame "#∗".
iApply (iProto_le_trans with "Hle Hle'").
Qed.
@@ -160,36 +159,28 @@ Section channel.
([∗ list] i ↦ _ ∈ replicate n x2, P i).
Proof.
iIntros "H".
- iInduction n as [|n] "IHn".
- { done. }
+ iInduction n as [|n] "IHn"; [done|].
replace (S n) with (n + 1) by lia.
- rewrite !replicate_add.
- simpl. iDestruct "H" as "[H1 H2]".
- iSplitL "H1".
- { by iApply "IHn". }
- simpl. rewrite !replicate_length. iFrame.
+ rewrite !replicate_add /=. iDestruct "H" as "[H1 H2]".
+ iSplitL "H1"; [by iApply "IHn"|]=> /=.
+ by rewrite !replicate_length.
Qed.
Lemma array_to_matrix_pre l n m v :
l ↦∗ replicate (n * m) v -∗
- [∗ list] i ↦ _ ∈ replicate n (),
- (l +ₗ i*m) ↦∗ replicate m v.
+ [∗ list] i ↦ _ ∈ replicate n (), (l +ₗ i*m) ↦∗ replicate m v.
Proof.
iIntros "Hl".
- iInduction n as [|n] "IHn".
- { done. }
+ iInduction n as [|n] "IHn"; [done|].
replace (S n) with (n + 1) by lia.
replace ((n + 1) * m) with (n * m + m) by lia.
- rewrite !replicate_add. simpl.
- rewrite array_app.
- iDestruct "Hl" as "[H1 H2]".
- iDestruct ("IHn" with "H1") as "H1".
- iFrame.
- simpl.
- rewrite Nat.add_0_r.
- rewrite !replicate_length.
+ rewrite !replicate_add /= array_app=> /=.
+ iDestruct "Hl" as "[Hl Hls]".
+ iDestruct ("IHn" with "Hl") as "Hl".
+ iFrame=> /=.
+ rewrite Nat.add_0_r !replicate_length.
replace (Z.of_nat (n * m)) with (Z.of_nat n * Z.of_nat m)%Z by lia.
- iFrame.
+ by iFrame.
Qed.
Lemma array_to_matrix l n v :
@@ -198,20 +189,17 @@ Section channel.
[∗ list] j ↦ _ ∈ replicate n (),
(l +ₗ pos n i j) ↦ v.
Proof.
- iIntros "H".
- iDestruct (array_to_matrix_pre with "H") as "H".
- iApply (big_sepL_impl with "H").
- iIntros "!>" (i ? HSome) "H".
- clear HSome.
- rewrite /array.
+ iIntros "Hl".
+ iDestruct (array_to_matrix_pre with "Hl") as "Hl".
+ iApply (big_sepL_impl with "Hl").
+ iIntros "!>" (i ? _) "Hl".
iApply big_sepL_replicate.
- iApply (big_sepL_impl with "H").
+ iApply (big_sepL_impl with "Hl").
iIntros "!>" (j ? HSome) "Hl".
- rewrite /pos.
rewrite Loc.add_assoc.
replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with
(Z.of_nat (i * n + j))%Z by lia.
- apply lookup_replicate in HSome as [-> _]. done.
+ by apply lookup_replicate in HSome as [-> _].
Qed.
(** ** Specifications of [send] and [recv] *)
@@ -234,49 +222,37 @@ Section channel.
own (γEs !!! i) (◯E (Next (ps !!! i))) ∗
iProto_own γ i (ps !!! i))%I with "[Hps']" as "H".
{ clear Hle.
- (* iInduction n as [|n] "IHn" forall (ps HSome Heq). *)
iInduction n as [|n] "IHn" forall (ps Hdom).
{ iExists []. iModIntro. simpl. done. }
- (* assert (n < S n) by lia. *)
- assert (is_Some (ps !! n)) as [p ?].
- { apply elem_of_dom.
- rewrite Hdom.
- apply elem_of_set_seq.
- lia. }
- iDestruct (big_sepM_delete _ _ n with "Hps'") as "[Hp Hps']".
- { done. }
+ assert (is_Some (ps !! n)) as [p HSome].
+ { apply elem_of_dom. rewrite Hdom. apply elem_of_set_seq. lia. }
+ iDestruct (big_sepM_delete _ _ n with "Hps'") as "[Hp Hps']"; [done|].
iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (γE) "[Hauth Hfrag]".
{ apply excl_auth_valid. }
iMod ("IHn" with "[] Hps'") as (γEs Hlen) "H".
{ iPureIntro.
- rewrite dom_delete_L. rewrite Hdom.
+ rewrite dom_delete_L Hdom.
replace (S n) with (n + 1) by lia.
- rewrite set_seq_add_L.
- simpl.
- rewrite right_id_L.
- rewrite difference_union_distr_l_L.
- rewrite difference_diag_L. rewrite right_id_L.
+ rewrite set_seq_add_L /= right_id_L difference_union_distr_l_L
+ difference_diag_L right_id_L.
assert (n ∉ (set_seq 0 n:gset _)); [|set_solver].
intros Hin%elem_of_set_seq. lia. }
iModIntro. iExists (γEs++[γE]).
replace (S n) with (n + 1) by lia.
- rewrite replicate_add.
- rewrite big_sepL_app.
- rewrite app_length.
- rewrite Hlen. iSplit; [done|].
- simpl.
+ rewrite replicate_add big_sepL_app app_length Hlen.
+ iSplit; [done|]=> /=.
iSplitL "H".
{ iApply (big_sepL_impl with "H").
iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
- assert (i < n).
- { by apply lookup_replicate_1 in HSome' as [? ?]. }
+ assert (i < n) as Hle.
+ { by apply lookup_replicate_1 in HSome' as [??]. }
assert (delete n ps !!! i = ps !!! i) as Heq'.
{ apply lookup_total_delete_ne. lia. }
rewrite Heq'. iFrame.
rewrite lookup_total_app_l; [|lia]. iFrame. }
- simpl. rewrite replicate_length. rewrite Nat.add_0_r.
+ rewrite replicate_length Nat.add_0_r.
rewrite list_lookup_total_middle; [|done].
- rewrite lookup_total_alt. rewrite H. simpl. iFrame. }
+ rewrite lookup_total_alt HSome. by iFrame. }
iMod "H" as (γEs Hlen) "H".
iAssert (|={⊤}=>
[∗ list] i ↦ _ ∈ replicate n (),
@@ -292,11 +268,8 @@ Section channel.
iApply big_sepL_fupd.
iApply (big_sepL_impl with "H1").
iIntros "!>" (j ? HSome'') "H1".
- iMod (own_alloc (Excl ())) as (γ') "Hγ'".
- { done. }
- iExists γ'.
- iApply inv_alloc.
- iLeft. iFrame. }
+ iMod (own_alloc (Excl ())) as (γ') "Hγ'"; [done|].
+ iExists γ'. iApply inv_alloc. iLeft. iFrame. }
iMod "IH" as "#IH".
iMod (inv_alloc with "Hps") as "#IHp".
iExists _,_,_,_.
@@ -319,16 +292,15 @@ Section channel.
{ apply lookup_replicate in HSome' as [_ Hle']. done. }
assert (j < n) as Hle''.
{ apply lookup_replicate in HSome'' as [_ Hle'']. done. }
- iDestruct (big_sepL_lookup _ _ i () with "IH") as "IH''".
- { rewrite lookup_replicate. done. }
- iDestruct (big_sepL_lookup _ _ j () with "IH''") as "IH'''".
- { rewrite lookup_replicate. done. }
- iFrame "#".
- iDestruct (big_sepL_lookup _ _ j () with "IH") as "H".
- { rewrite lookup_replicate. done. }
- iDestruct (big_sepL_lookup _ _ i () with "H") as "H'".
- { rewrite lookup_replicate. done. }
- iDestruct "IH'''" as (γ1) "?".
+ iDestruct (big_sepL_lookup _ _ i () with "IH") as "IH'";
+ [by rewrite lookup_replicate|].
+ iDestruct (big_sepL_lookup _ _ j () with "IH'") as "IH''";
+ [by rewrite lookup_replicate|].
+ iDestruct (big_sepL_lookup _ _ j () with "IH") as "H";
+ [by rewrite lookup_replicate|].
+ iDestruct (big_sepL_lookup _ _ i () with "H") as "H'";
+ [by rewrite lookup_replicate|].
+ iDestruct "IH''" as (γ1) "?".
iDestruct "H'" as (γ2) "?".
iExists _, _. iFrame "#".
Qed.
diff --git a/theories/channel/multi_proto.v b/theories/channel/multi_proto.v
index 90368e6..86f4505 100644
--- a/theories/channel/multi_proto.v
+++ b/theories/channel/multi_proto.v
@@ -510,23 +510,23 @@ Section proto.
End proto.
-Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate (END).
+Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
(ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ m1 m2,
- ((ps !!! i ≡ <(Send, j)> m1) -∗ (ps !!! j ≡ <(Recv, i)> m2) -∗
- ∀ v p1, iMsg_car m1 v (Next p1) -∗
- ∃ p2, iMsg_car m2 v (Next p2) ∗
- â–· (rec (<[i:=p1]>(<[j:=p2]>ps)))).
+ (ps !!! i ≡ <(Send, j)> m1) -∗
+ (ps !!! j ≡ <(Recv, i)> m2) -∗
+ ∀ v p1, iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗
+ â–· (rec (<[i:=p1]>(<[j:=p2]>ps))).
Definition valid_target {Σ V} (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
- ∀ a m, ((ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)âŒ).
+ ∀ a m, (ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)âŒ.
Definition iProto_consistent_pre {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
(ps : gmap nat (iProto Σ V)) : iProp Σ :=
- (∀ i j, valid_target ps i j) ∗
- (∀ i j, can_step rec ps i j).
+ (∀ i j, valid_target ps i j) ∗ (∀ i j, can_step rec ps i j).
Global Instance iProto_consistent_pre_ne {Σ V}
(rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
@@ -616,7 +616,6 @@ Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
(ps : gmap nat (iProto Σ V)) : iProp Σ :=
- (* own γ (◠∅). *)
own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$> ps) : gmap _ _)).
Definition iProto_ctx `{protoG Σ V}
@@ -669,21 +668,18 @@ Section proto.
Lemma iProto_le_send_inv i p1 m2 :
p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1,
(p1 ≡ <(Send,i)> m1) ∗
- ∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
+ ∀ v p2', iMsg_car m2 v (Next p2') -∗
+ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
Proof.
rewrite iProto_le_unfold.
iIntros "[[_ Heq]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]".
simplify_eq.
destruct a1 as [[]]; [|done].
- iDestruct "H" as (->) "H".
- iExists m1. iFrame.
- iIntros (v p2).
- iSpecialize ("Hm2" $! v (Next p2)).
- iRewrite "Hm2". iApply "H".
+ iDestruct "H" as (->) "H". iExists m1. iFrame "Hp1".
+ iIntros (v p2). iSpecialize ("Hm2" $! v (Next p2)). by iRewrite "Hm2".
Qed.
Lemma iProto_le_send_send_inv i m1 m2 v p2' :
@@ -699,8 +695,8 @@ Section proto.
Lemma iProto_le_recv_inv_l i m1 p2 :
(<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2,
(p2 ≡ <(Recv,i)> m2) ∗
- ∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
+ ∀ v p1', iMsg_car m1 v (Next p1') -∗
+ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
Proof.
rewrite iProto_le_unfold.
iIntros "[[Heq _]|H]".
@@ -709,18 +705,15 @@ Section proto.
rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]".
simplify_eq.
destruct a2 as [[]]; [done|].
- iDestruct "H" as (->) "H".
- iExists m2. iFrame.
- iIntros (v p1).
- iSpecialize ("Hm1" $! v (Next p1)).
- iRewrite "Hm1". iApply "H".
+ iDestruct "H" as (->) "H". iExists m2. iFrame "Hp2".
+ iIntros (v p1). iSpecialize ("Hm1" $! v (Next p1)). by iRewrite "Hm1".
Qed.
Lemma iProto_le_recv_inv_r i p1 m2 :
(p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1,
(p1 ≡ <(Recv,i)> m1) ∗
- ∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
+ ∀ v p1', iMsg_car m1 v (Next p1') -∗
+ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
Proof.
rewrite iProto_le_unfold.
iIntros "[[_ Heq]|H]".
@@ -759,12 +752,10 @@ Section proto.
destruct t1,t2; [|done|done|].
- rewrite iProto_message_equivI.
iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
- iDestruct "H" as (->) "H".
- iExists _. done.
+ iDestruct "H" as (->) "H". by iExists _.
- rewrite iProto_message_equivI.
iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
- iDestruct "H" as (->) "H".
- iExists _. done.
+ iDestruct "H" as (->) "H". by iExists _.
Qed.
Lemma iProto_le_msg_inv_r j a p1 m2 :
@@ -778,12 +769,10 @@ Section proto.
destruct t1,t2; [|done|done|].
- rewrite iProto_message_equivI.
iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
- iDestruct "H" as (->) "H".
- iExists _. done.
+ iDestruct "H" as (->) "H". by iExists _.
- rewrite iProto_message_equivI.
iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
- iDestruct "H" as (->) "H".
- iExists _. done.
+ iDestruct "H" as (->) "H". by iExists _.
Qed.
Lemma valid_target_le ps i p1 p2 :
@@ -798,7 +787,7 @@ Section proto.
iFrame "Hle".
iIntros (i' j' a m) "Hm".
destruct (decide (i = j')) as [->|Hneqj].
- { rewrite lookup_insert. done. }
+ { by rewrite lookup_insert. }
rewrite lookup_insert_ne; [|done].
destruct (decide (i = i')) as [->|Hneqi].
{ rewrite lookup_total_insert. iRewrite "H" in "Hm".
@@ -807,8 +796,7 @@ Section proto.
by iApply "Hprot". }
destruct Hmsg as (t & n & m & Hmsg).
setoid_rewrite Hmsg.
- iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq".
- iFrame.
+ iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle".
iIntros (i' j' a m') "Hm".
destruct (decide (i = j')) as [->|Hneqj].
{ rewrite lookup_insert. done. }
@@ -1020,7 +1008,8 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto].
iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
- iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. iApply iProto_le_recv.
+ iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
+ iApply iProto_le_recv.
iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
@@ -1123,9 +1112,7 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
ps !!! i ≡ (<(a, j)> m) -∗
⌜is_Some (ps !! j)âŒ.
Proof.
- rewrite iProto_consistent_unfold.
- iDestruct 1 as "[Htar _]".
- iApply "Htar".
+ rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]". iApply "Htar".
Qed.
Lemma iProto_consistent_step ps m1 m2 i j v p1 :
@@ -1153,13 +1140,10 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iDestruct (own_valid_2 with "H◠H◯") as "H✓".
rewrite gmap_view_both_validI.
iDestruct "H✓" as "[_ [H1 H2]]".
- rewrite lookup_total_alt.
- rewrite lookup_fmap.
+ rewrite lookup_total_alt lookup_fmap.
destruct (ps !! i); last first.
- { simpl. rewrite !option_equivI. done. }
- simpl.
- rewrite !option_equivI excl_equivI.
- by iNext.
+ { by rewrite !option_equivI. }
+ simpl. rewrite !option_equivI excl_equivI. by iNext.
Qed.
Lemma iProto_own_auth_update γ ps i p p' :
@@ -1184,19 +1168,13 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
{ apply gmap_view_auth_valid. }
iExists γ.
iInduction ps as [|i p ps Hin] "IH" using map_ind.
- { iModIntro. iFrame.
- by iApply big_sepM_empty. }
+ { iModIntro. iFrame. by iApply big_sepM_empty. }
iMod ("IH" with "Hauth") as "[Hauth Hfrags]".
rewrite big_sepM_insert; [|done]. iFrame "Hfrags".
iMod (own_update with "Hauth") as "[Hauth Hfrag]".
- { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))).
- - rewrite lookup_fmap. rewrite Hin. done.
- - done.
- - done. }
- iFrame.
- iModIntro.
- rewrite -fmap_insert.
- iFrame.
+ { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done].
+ by rewrite lookup_fmap Hin. }
+ iModIntro. rewrite -fmap_insert. iFrame.
iExists _. iFrame. iApply iProto_le_refl.
Qed.
@@ -1211,9 +1189,9 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
▷ iProto_consistent ps -∗
|==> ∃ γ, iProto_ctx γ (dom ps) ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p.
Proof.
- iIntros "Hconsistnet".
+ iIntros "Hconsistent".
iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
- iExists γ. iFrame. iExists _. iFrame. done.
+ iExists γ. iFrame. iExists _. by iFrame.
Qed.
Lemma own_prot_idx γ i j (p1 p2 : iProto Σ V) :
@@ -1224,7 +1202,7 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iIntros "Hown Hown'" (->).
iDestruct (own_valid_2 with "Hown Hown'") as "H".
rewrite uPred.cmra_valid_elim.
- iDestruct "H" as %H%gmap_view_frag_op_validN. by destruct H.
+ by iDestruct "H" as %[]%gmap_view_frag_op_validN.
Qed.
Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
@@ -1243,52 +1221,40 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj".
iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
iAssert (▷ (<[i:=<(Send, j)> m1]>ps !!! j ≡ pj))%I as "Hpj'".
- { rewrite lookup_total_insert_ne; done. }
-
+ { by rewrite lookup_total_insert_ne. }
iAssert (▷ (⌜is_Some (ps !! i)⌠∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]"
as "[Hi' Hile]".
- { iNext.
- iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#H".
- iFrame.
- iRewrite "H" in "Hpi".
- rewrite lookup_total_alt. simpl.
+ { iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq".
+ iFrame. iRewrite "Heq" in "Hpi". rewrite lookup_total_alt.
destruct (ps !! i); [done|].
- simpl. iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
+ iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
iAssert (▷ (⌜is_Some (ps !! j)⌠∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]"
as "[Hj' Hjle]".
- { iNext.
- iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#H".
- iFrame.
- iRewrite "H" in "Hpj".
- rewrite !lookup_total_alt. simpl.
+ { iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq".
+ iFrame. iRewrite "Heq" in "Hpj". rewrite !lookup_total_alt.
destruct (ps !! j); [done|].
- simpl. iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
+ iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent".
iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent".
iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent [] [] [Hm //]") as
(p2) "[Hm2 Hconsistent]".
{ rewrite lookup_total_insert_ne; [|done].
rewrite lookup_total_insert_ne; [|done].
- iNext. rewrite lookup_total_insert. done. }
+ by rewrite lookup_total_insert. }
{ rewrite lookup_total_insert_ne; [|done].
- iNext. rewrite lookup_total_insert. done. }
+ by rewrite lookup_total_insert. }
iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
- iIntros "!>!>". iExists p2. iFrame.
- iDestruct "Hi'" as %Hi.
- iDestruct "Hj'" as %Hj.
+ iIntros "!>!>". iExists p2. iFrame "Hm2".
+ iDestruct "Hi'" as %Hi. iDestruct "Hj'" as %Hj.
iSplitL "Hconsistent Hauth".
{ iExists (<[i:=p1]> (<[j:=p2]> ps)).
iSplit.
- { rewrite !dom_insert_lookup_L; [done|..].
- - done.
- - by rewrite lookup_insert_ne. }
+ { rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. }
iFrame. rewrite insert_insert.
rewrite insert_commute; [|done]. rewrite insert_insert.
- rewrite insert_commute; [|done]. done. }
- iSplitL "Hi".
- - iExists _. iFrame. iApply iProto_le_refl.
- - iExists _. iFrame. iApply iProto_le_refl.
+ by rewrite insert_commute; [|done]. }
+ iSplitL "Hi"; iExists _; iFrame; iApply iProto_le_refl.
Qed.
Lemma iProto_target γ ps_dom i a j m :
@@ -1300,20 +1266,16 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
rewrite /iProto_ctx /iProto_own.
iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]".
iDestruct "Hown" as (p') "[Hle Hown]".
- iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#H".
+ iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#Hi".
iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
iAssert (▷ (⌜is_Some (ps !! j)⌠∗ iProto_consistent ps))%I
- with "[Hps]" as "[H1 H2]".
- { iNext.
- iRewrite "Heq" in "H".
- iDestruct (iProto_consistent_target with "Hps H") as "#H'".
- iFrame. done. }
- iSplitL "H1".
- { iNext. iDestruct "H1" as %Heq.
- iPureIntro. simplify_eq. apply elem_of_dom. done. }
- iSplitL "Hauth H2".
- { iExists _. iFrame. done. }
- iExists _. iFrame.
+ with "[Hps]" as "[HSome Hps]".
+ { iNext. iRewrite "Heq" in "Hi".
+ iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
+ iSplitL "HSome".
+ { iNext. iDestruct "HSome" as %Heq.
+ iPureIntro. simplify_eq. by apply elem_of_dom. }
+ iSplitL "Hauth Hps"; iExists _; by iFrame.
Qed.
(* (** The instances below make it possible to use the tactics [iIntros], *)
--
GitLab