From 0360a2375e68f17c0379ab3551cd71696962a140 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Thu, 4 Aug 2022 15:16:24 +0200
Subject: [PATCH] Bumped Iris
---
theories/logrel/examples/choice_subtyping.v | 55 ++++++++-------------
theories/logrel/examples/mapper_list.v | 6 +--
theories/logrel/term_typing_judgment.v | 2 +-
3 files changed, 24 insertions(+), 39 deletions(-)
diff --git a/theories/logrel/examples/choice_subtyping.v b/theories/logrel/examples/choice_subtyping.v
index 09e72f7..8a45eb8 100644
--- a/theories/logrel/examples/choice_subtyping.v
+++ b/theories/logrel/examples/choice_subtyping.v
@@ -149,8 +149,7 @@ Section choice_example.
iIntros "#HRM #HSM #HRP #HSP #HR".
(** Weakening of select *)
iApply (lty_le_trans _ prot1).
- {
- iApply lty_le_branch.
+ { iApply lty_le_branch.
rewrite big_sepM2_insert=> //.
iSplit.
- iApply lty_le_recv; [iApply lty_le_refl | ].
@@ -158,22 +157,18 @@ Section choice_example.
rewrite (insert_commute _ 2%Z 3%Z) //.
rewrite (insert_commute _ 1%Z 3%Z) //.
by apply insert_subseteq.
- - rewrite big_sepM2_insert //. eauto.
- }
+ - rewrite big_sepM2_insert //. eauto. }
(** Swap recv/select *)
iApply (lty_le_trans _ prot2).
- {
- iApply lty_le_branch.
+ { iApply lty_le_branch.
rewrite big_sepM2_insert=> //.
iSplit.
- iApply lty_le_swap_recv_select.
- rewrite big_sepM2_insert=> //. iSplit=> //.
- iApply lty_le_swap_recv_select.
- }
+ iApply lty_le_swap_recv_select. }
(** Swap branch/select *)
iApply (lty_le_trans _ prot3).
- {
- iApply (lty_le_swap_branch_select
+ { iApply (lty_le_swap_branch_select
(<[1%Z:=
<[1%Z:=(<??> TY Sr; <!!> TY Srm; Tr)%lty]>
(<[2%Z:= (<??> TY Sr; <!!> TY Srp; Tr')%lty]>∅)]>
@@ -188,21 +183,17 @@ Section choice_example.
(<[2%Z:= (<??> TY Ss; <!!> TY Ssp; Ts')%lty]>∅)]>∅))
).
intros i j Ss1' Ss2' Hin1 Hin2.
- assert (i = 1%Z ∨ i = 2%Z).
- {
- destruct (decide (i = 1)). eauto.
+ assert (i = 1%Z ∨ i = 2%Z) as Hdisj1.
+ { destruct (decide (i = 1)). eauto.
destruct (decide (i = 2)). eauto.
rewrite lookup_insert_ne in Hin1=> //.
- rewrite lookup_insert_ne in Hin1=> //.
- }
- assert (j = 1%Z ∨ j = 2%Z).
- {
- destruct (decide (j = 1)). eauto.
+ rewrite lookup_insert_ne in Hin1=> //. }
+ assert (j = 1%Z ∨ j = 2%Z) as Hdisj2.
+ { destruct (decide (j = 1)). eauto.
destruct (decide (j = 2)). eauto.
rewrite lookup_insert_ne in Hin2=> //.
- rewrite lookup_insert_ne in Hin2=> //.
- }
- destruct H2 as [-> | ->] ,H1 as [-> | ->].
+ rewrite lookup_insert_ne in Hin2=> //. }
+ destruct Hdisj2 as [-> | ->], Hdisj1 as [-> | ->].
- rewrite lookup_insert in Hin1.
rewrite lookup_insert in Hin2.
inversion Hin1; inversion Hin2; eauto.
@@ -218,12 +209,10 @@ Section choice_example.
rewrite (insert_commute _ 1%Z 2%Z) in Hin2=> //.
rewrite lookup_insert in Hin1.
rewrite lookup_insert in Hin2.
- inversion Hin1; inversion Hin2; eauto.
- }
+ inversion Hin1; inversion Hin2; eauto. }
(** Swap recv/send *)
iApply (lty_le_trans _ prot4).
- {
- iApply lty_le_select.
+ { iApply lty_le_select.
rewrite big_sepM2_insert=> //. iSplit.
- iApply lty_le_branch. iIntros "!>".
rewrite big_sepM2_insert=> //. iSplit.
@@ -235,11 +224,9 @@ Section choice_example.
rewrite big_sepM2_insert=> //. iSplit.
+ iApply lty_le_swap_recv_send.
+ rewrite big_sepM2_insert=> //.
- iSplit=> //. iApply lty_le_swap_recv_send.
- }
+ iSplit=> //. iApply lty_le_swap_recv_send. }
iApply (lty_le_trans _ prot5).
- {
- iApply lty_le_select.
+ { iApply lty_le_select.
rewrite big_sepM2_insert=> //. iSplit.
- iApply lty_le_branch. iIntros "!>".
rewrite big_sepM2_insert=> //. iSplit.
@@ -252,19 +239,17 @@ Section choice_example.
+ iApply lty_le_send; [eauto|].
iApply lty_le_recv; eauto.
+ rewrite big_sepM2_insert=> //. iSplit=> //.
- iApply lty_le_send; eauto.
- }
+ iApply lty_le_send; eauto. }
(** Swap branch/send *)
iApply (lty_le_trans _ prot6).
- {
- iApply lty_le_select.
+ { iApply lty_le_select.
rewrite big_sepM2_insert=> //. iSplit.
- iApply (lty_le_swap_branch_send _
(<[1%Z:=(<??> TY Sr; Tr)%lty]> (<[2%Z:=(<??> TY Ss; Ts)%lty]> ∅))).
- rewrite big_sepM2_insert=> //. iSplit=> //.
iApply (lty_le_swap_branch_send _
- ((<[1%Z:=(<??> TY Sr'; Tr')%lty]> (<[2%Z:=(<??> TY Ss; Ts')%lty]> ∅)))).
- }
+ ((<[1%Z:=(<??> TY Sr'; Tr')%lty]>
+ (<[2%Z:=(<??> TY Ss; Ts')%lty]> ∅)))). }
(** Weaken branch *)
iApply lty_le_select.
rewrite big_sepM2_insert=> //. iSplit=> //.
diff --git a/theories/logrel/examples/mapper_list.v b/theories/logrel/examples/mapper_list.v
index cd7c109..c4c65fd 100644
--- a/theories/logrel/examples/mapper_list.v
+++ b/theories/logrel/examples/mapper_list.v
@@ -307,16 +307,16 @@ Section mapper_example.
Proof.
iIntros (Φ) "[Hl Hc] HΦ".
iLöb as "IH" forall (n Φ).
- destruct n.
+ destruct n as [|n].
{ wp_lam. wp_pures. iApply "HΦ". by iFrame. }
wp_lam. wp_recv (w) as "Hw". wp_pures.
rewrite Nat2Z.inj_succ.
replace (Z.succ (Z.of_nat (n)) - 1)%Z with (Z.of_nat (n)) by lia.
wp_smart_apply ("IH" with "Hl Hc").
- iIntros (ys) "(% & Hl & Hc)".
+ iIntros (ys) "(%Hlen & Hl & Hc)".
wp_smart_apply (lcons_spec with "[$Hl $Hw//]").
iIntros "Hl". iApply "HΦ". iFrame.
- iPureIntro. by rewrite H1.
+ iPureIntro. by rewrite Hlen.
Qed.
Lemma ltyped_mapper_client_ad_hoc Γ (A B : ltty Σ) :
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index d07bdcd..9075dff 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -96,7 +96,7 @@ Lemma ltyped_safety `{heapGpreS Σ} e σ es σ' e' :
rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
is_Some (to_val e') ∨ reducible e' σ'.
Proof.
- intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ??.
+ intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
destruct (Hty _) as (A & He). iIntros "_".
iDestruct (He $!∅ with "[]") as "He"; first by rewrite /ctx_ltyped.
iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
--
GitLab