From 08e8d55a7fddfc35d45a9d667ae86810711ba3cf Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sat, 15 Aug 2020 17:21:19 +0200
Subject: [PATCH] iAlways -> iModIntro
---
theories/examples/cell.v | 8 ++++----
theories/examples/namegen.v | 6 +++---
theories/examples/stack/refinement.v | 10 +++++-----
theories/examples/symbol.v | 16 ++++++++--------
theories/examples/ticket_lock.v | 8 ++++----
theories/examples/various.v | 14 +++++++-------
theories/experimental/hocap/counter.v | 6 +++---
theories/lib/Y.v | 12 ++++++------
theories/lib/counter.v | 10 +++++-----
theories/logic/derived.v | 4 ++--
theories/logic/proofmode/tactics.v | 4 ++--
theories/typing/contextual_refinement.v | 4 ++--
theories/typing/fundamental.v | 8 ++++----
theories/typing/soundness.v | 2 +-
14 files changed, 56 insertions(+), 56 deletions(-)
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index 97d00a9..ba72295 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -63,7 +63,7 @@ Section cell_refinement.
- (* New cell *)
rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (v1 v2) "/= #Hv".
+ iModIntro. iIntros (v1 v2) "/= #Hv".
rel_let_l. rel_let_r.
rel_alloc_r r as "Hr".
@@ -83,7 +83,7 @@ Section cell_refinement.
- (* Read cell *)
rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (v1 v2) "/=".
+ iModIntro. iIntros (v1 v2) "/=".
iDestruct 1 as (r1 r2 r3 l r) "[% [% #Hrs]]". simplify_eq.
repeat rel_pure_l.
rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk".
@@ -103,11 +103,11 @@ Section cell_refinement.
- (* Insert cell *)
rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (v1 v2) "/=".
+ iModIntro. iIntros (v1 v2) "/=".
iDestruct 1 as (r1 r2 r3 l r) "[% [% #Hrs]]". simplify_eq.
repeat rel_pure_l. repeat rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (v1 v2) "/= #Hv".
+ iModIntro. iIntros (v1 v2) "/= #Hv".
repeat rel_pure_l. repeat rel_pure_r.
rewrite /cellInt. iDestruct "Hrs" as (γlk N) "#Hlk".
rel_apply_l (refines_acquire_l with "Hlk"); first auto.
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 3dfe5cf..cc3f615 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -53,7 +53,7 @@ Section namegen_refinement.
- (* New name *)
rel_pure_l. rel_pure_r.
iApply refines_arrow.
- iAlways. iIntros (? ?) "/= _".
+ iModIntro. iIntros (? ?) "/= _".
rel_pure_l. rel_pure_r.
rel_alloc_l_atomic.
iInv N as (n L) "(HB & Hc & HL)" "Hcl".
@@ -85,11 +85,11 @@ Section namegen_refinement.
- (* Name comparison *)
rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (? ?) "/= #Hv".
+ iModIntro. iIntros (? ?) "/= #Hv".
iDestruct "Hv" as (l n) "(% & % & #Hln)". simplify_eq.
do 2 rel_pure_l. do 2 rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (? ?) "/= #Hv".
+ iModIntro. iIntros (? ?) "/= #Hv".
iDestruct "Hv" as (l' n') "(% & % & #Hl'n')". simplify_eq.
do 2 rel_pure_l. do 2 rel_pure_r.
iInv N as (m L) "(>HB & >Hc & HL)" "Hcl".
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index c2984a5..abefef6 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -168,11 +168,11 @@ Section proof.
⊢ REL FG_stack << CG_stack : ∀ A, ∃ B, (() → B) * (B → () + A) * (B → A → ()).
Proof.
unfold CG_stack, FG_stack.
- iApply refines_forall. iIntros (A). iAlways.
+ iApply refines_forall. iIntros (A). iModIntro.
iApply (refines_pack (stackInt A)).
repeat iApply refines_pair.
- unfold CG_new_stack, FG_new_stack.
- iApply refines_arrow_val. iAlways.
+ iApply refines_arrow_val. iModIntro.
iIntros (??) "_". repeat rel_pure_l. repeat rel_pure_r.
rel_alloc_l istk as "Hisk".
rel_alloc_l st as "Hst".
@@ -187,17 +187,17 @@ Section proof.
iExists _,_; eauto with iFrame. }
iModIntro. iExists _. eauto with iFrame.
- rel_pure_l. rel_pure_r. iApply refines_arrow_val.
- iAlways. iIntros (st1 st2) "Hst".
+ iModIntro. iIntros (st1 st2) "Hst".
rel_rec_l. rel_rec_r.
iDestruct "Hst" as (??) "#Hst". simplify_eq/=.
iApply (FG_CG_pop_refinement with "Hst").
solve_ndisj.
- rel_pure_l. rel_pure_r. iApply refines_arrow_val.
- iAlways. iIntros (st1 st2) "Hst".
+ iModIntro. iIntros (st1 st2) "Hst".
rel_rec_l. rel_rec_r.
iDestruct "Hst" as (??) "#Hst". simplify_eq/=.
rel_pure_l. rel_pure_r. iApply refines_arrow_val.
- iAlways. iIntros (x1 x2) "Hx".
+ iModIntro. iIntros (x1 x2) "Hx".
rel_rec_l. rel_rec_r.
iApply (FG_CG_push_refinement with "Hst Hx").
solve_ndisj.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 66262a4..41ce7c9 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -122,11 +122,11 @@ Section proof.
Proof.
unfold eqKey.
iApply refines_arrow_val.
- iAlways. iIntros (k1 k2) "/= #Hk".
+ iModIntro. iIntros (k1 k2) "/= #Hk".
iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
rel_let_l. rel_let_r. rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (k1 k2) "/= #Hk".
+ iModIntro. iIntros (k1 k2) "/= #Hk".
iDestruct "Hk" as (m) "(% & % & #Hm)"; simplify_eq.
rel_let_l. rel_let_r.
rel_op_l. rel_op_r. rel_values.
@@ -144,7 +144,7 @@ Section proof.
Proof.
iIntros "#Hinv".
iApply refines_arrow_val.
- iAlways. iIntros (k1 k2) "/= #Hk".
+ iModIntro. iIntros (k1 k2) "/= #Hk".
iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
rel_let_l. rel_let_r.
rel_load_l_atomic.
@@ -183,7 +183,7 @@ Section proof.
Proof.
iIntros "#Hinv".
iApply refines_arrow_val.
- iAlways. iIntros (k1 k2) "#Hk /=".
+ iModIntro. iIntros (k1 k2) "#Hk /=".
iDestruct "Hk" as (n) "(% & % & #Hn)"; simplify_eq.
repeat rel_pure_l. repeat rel_pure_r.
rel_load_l_atomic.
@@ -220,7 +220,7 @@ Section proof.
⊢ REL symbol1 << symbol2 : () → lrel_symbol.
Proof.
iApply refines_arrow_val.
- iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
+ iModIntro. iIntros (? ?) "[% %]"; simplify_eq/=.
rel_rec_l. rel_rec_r.
rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
@@ -243,7 +243,7 @@ Section proof.
(* Insert *)
- rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (? ?). iDestruct 1 as (n) "[% %]"; simplify_eq/=.
+ iModIntro. iIntros (? ?). iDestruct 1 as (n) "[% %]"; simplify_eq/=.
repeat rel_pure_l. repeat rel_pure_r.
rel_apply_l (refines_acquire_l with "Hl1").
iNext. iIntros "Hlk Htbl". repeat rel_pure_l.
@@ -299,7 +299,7 @@ Section proof.
⊢ REL symbol2 << symbol1 : () → lrel_symbol.
Proof.
iApply refines_arrow_val.
- iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
+ iModIntro. iIntros (? ?) "[% %]"; simplify_eq/=.
rel_rec_l. rel_rec_r.
rel_alloc_l size1 as "[Hs1 Hs1']"; repeat rel_pure_l.
rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
@@ -322,7 +322,7 @@ Section proof.
(* Insert *)
- rel_pure_l. rel_pure_r.
iApply refines_arrow_val.
- iAlways. iIntros (? ?). iDestruct 1 as (n) "[% %]"; simplify_eq/=.
+ iModIntro. iIntros (? ?). iDestruct 1 as (n) "[% %]"; simplify_eq/=.
repeat rel_pure_l. repeat rel_pure_r.
rel_apply_l (refines_acquire_l with "Hl1").
iNext. iIntros "Hlk Htbl". repeat rel_pure_l.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 4d82bdc..83aa92c 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -169,7 +169,7 @@ Section refinement.
rewrite /acquire.
repeat rel_pure_l.
rel_apply_l (FG_increment_atomic_l (fun n : nat => ∃ o : nat, lo ↦ #o ∗ issuedTickets γ n ∗ R o)%I P%I with "HP").
- iAlways.
+ iModIntro.
iPoseProof "H" as "H2".
iMod "H" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
iExists _; iFrame.
@@ -218,7 +218,7 @@ Section refinement.
(fun o => ∃ st, is_locked_r lk st ∗
if st then ticket γ o else True)%I
True%I γ); first done.
- iAlways.
+ iModIntro.
openI.
iModIntro. iExists _,_; iFrame.
iSplitL "Hbticket Hl'".
@@ -248,7 +248,7 @@ Section refinement.
iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
rel_rec_l. repeat rel_proj_l.
rel_apply_l (FG_increment_atomic_l (issuedTickets γ)%I True%I); first done.
- iAlways.
+ iModIntro.
openI.
iModIntro. iExists _; iFrame.
iSplit.
@@ -318,7 +318,7 @@ Section refinement.
∗ issuedTickets γ n ∗ is_locked_r lk st ∗
if st then ticket γ o else True)%I).
rel_apply_l (wkincr_atomic_l R True%I); first done.
- iAlways.
+ iModIntro.
openI.
iModIntro. iExists o; iFrame "Hlo".
rewrite {1}/R. iSplitR "Hcl".
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 1bae627..fbbf5d7 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -28,7 +28,7 @@ Section proofs.
repeat rel_pure_l.
iMod (inv_alloc (nroot.@"xinv") _ (x ↦ #1)%I with "Hx") as "#Hinv".
rel_pure_r. iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
rel_rec_l. rel_rec_r.
iApply (refines_seq with "[Hff]").
- iApply refines_app; eauto.
@@ -197,7 +197,7 @@ Section proofs.
iApply refines_pair.
- rel_pure_l. rel_pure_r.
iApply refines_arrow.
- iAlways. iIntros (f f') "Hf".
+ iModIntro. iIntros (f f') "Hf".
rel_let_l. rel_let_r.
rel_cmpxchg_l_atomic.
iInv i3n as (n) "(Hx & Hx' & >Hbb)" "Hcl".
@@ -254,7 +254,7 @@ Section proofs.
iFrame. iLeft. iFrame. }
rel_values. }
- rel_pure_l. rel_pure_r. iApply refines_arrow.
- iAlways. iIntros (u u') "_".
+ iModIntro. iIntros (u u') "_".
rel_let_l. rel_let_r.
rel_load_l_atomic.
iInv i3n as (n) "(>Hx & Hx' & >Hbb)" "Hcl".
@@ -331,7 +331,7 @@ Section proofs.
: (() → ()) → lrel_int.
Proof.
rel_pure_l. rel_pure_r. iApply refines_arrow; eauto.
- iAlways. iIntros (f1 f2) "Hf".
+ iModIntro. iIntros (f1 f2) "Hf".
rel_let_l. rel_let_r.
rel_alloc_l x as "Hx". repeat rel_pure_l.
rel_alloc_l y as "Hy". repeat rel_pure_l.
@@ -379,7 +379,7 @@ Section proofs.
{ iApply (refines_app with "Hg"). rel_values. }
rel_apply_l (FG_increment_atomic_l
(fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ nâŒ))%I True%I); first done.
- iAlways.
+ iModIntro.
iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht)]" "Hcl".
iModIntro.
- iExists n. iFrame "Hc1". iSplitL "Hc2 Ht".
@@ -450,7 +450,7 @@ Section proofs.
Proof.
iIntros "#Hinv #Hg".
iApply refines_arrow_val; auto.
- iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
+ iModIntro. iIntros (? ?) "[% %]". simplify_eq/=.
rel_seq_l. rel_seq_r.
iApply profiled_g; eauto.
Qed.
@@ -548,7 +548,7 @@ Section proofs.
rel_seq_l.
rel_apply_l (FG_increment_atomic_l
(fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ nâŒ))%I with "Ht'").
- iAlways.
+ iModIntro.
iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
iModIntro; last first.
{ iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z by lia.
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index ba83aad..0b9ea42 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -309,7 +309,7 @@ Section refinement.
Proof.
unfold FG_counter, CG_counter.
iApply refines_arrow_val.
- iAlways. iIntros (? ?) "_"; simplify_eq/=.
+ iModIntro. iIntros (? ?) "_"; simplify_eq/=.
rel_rec_l. rel_rec_r.
rel_apply_r refines_newlock_r; auto.
iIntros (lk) "Hlk".
@@ -329,10 +329,10 @@ Section refinement.
do 4 rel_pure_r. do 4 rel_pure_l.
iApply refines_pair .
- iApply refines_arrow_val.
- iAlways. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
+ iModIntro. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
iApply (incr_refinement with "HCnt Hinv").
- iApply refines_arrow_val.
- iAlways. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
+ iModIntro. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
iApply (read_refinement with "HCnt Hinv").
Qed.
diff --git a/theories/lib/Y.v b/theories/lib/Y.v
index bb23164..79d46d8 100644
--- a/theories/lib/Y.v
+++ b/theories/lib/Y.v
@@ -34,7 +34,7 @@ Section contents.
Proof.
unfold Y.
iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
rel_let_l. rel_let_r.
rel_pure_l. rel_pure_r.
rel_pure_l. rel_pure_r.
@@ -49,7 +49,7 @@ Section contents.
Proof.
unfold F.
iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
iLöb as "IH".
rel_let_l. rel_let_r.
iApply (refines_app with "Hff").
@@ -62,7 +62,7 @@ Section contents.
Proof.
unfold Y, Knot.
iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
rel_let_l. rel_let_r.
rel_pure_r. rel_pure_r.
rel_alloc_l z as "Hz". repeat rel_pure_l.
@@ -79,7 +79,7 @@ Section contents.
Proof.
unfold Y, Knot.
iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
rel_let_l. rel_let_r.
rel_pure_l. rel_pure_l.
rel_alloc_r z as "Hz". repeat rel_pure_r.
@@ -97,7 +97,7 @@ Section contents.
Proof.
unfold Y, F.
iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
rel_pure_r. rel_pure_r. rel_pure_r.
iLöb as "IH".
rel_let_l. rel_let_r.
@@ -110,7 +110,7 @@ Section contents.
Proof.
unfold Y, F.
iApply refines_arrow.
- iAlways. iIntros (f1 f2) "#Hff".
+ iModIntro. iIntros (f1 f2) "#Hff".
rel_pure_l. rel_pure_l. rel_pure_l.
iLöb as "IH".
rel_let_l. rel_let_r.
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index b35129a..9bdbd05 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -152,7 +152,7 @@ Section CG_Counter.
(FG_increment_atomic_l
(fun n => is_locked_r lk false ∗ cnt' ↦ₛ #n)%I
True%I); first done.
- iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro.
+ iModIntro. iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')".
iExists _; iFrame.
iSplit.
@@ -177,7 +177,7 @@ Section CG_Counter.
(counter_read_atomic_l
(fun n => is_locked_r lk false ∗ cnt' ↦ₛ #n)%I
True%I); first done.
- iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
+ iModIntro. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists n. iFrame "Hcnt Hcnt' Hl".
iSplit.
@@ -196,7 +196,7 @@ Section CG_Counter.
Proof.
unfold FG_counter, CG_counter.
iApply refines_arrow_val.
- iAlways. iIntros (? ?) "_"; simplify_eq/=.
+ iModIntro. iIntros (? ?) "_"; simplify_eq/=.
rel_rec_l. rel_rec_r.
rel_apply_r refines_newlock_r; auto.
iIntros (l) "Hl".
@@ -216,10 +216,10 @@ Section CG_Counter.
do 4 rel_pure_r. do 4 rel_pure_l.
iApply refines_pair .
- iApply refines_arrow_val.
- iAlways. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
+ iModIntro. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
iApply (FG_CG_increment_refinement with "Hinv").
- iApply refines_arrow_val.
- iAlways. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
+ iModIntro. iIntros (? ?) "_". rel_seq_l; rel_seq_r.
iApply (counter_read_refinement with "Hinv").
Qed.
End CG_Counter.
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 8b40823..6a93765 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -28,8 +28,8 @@ Section rules.
Proof.
iIntros "#H".
iApply refines_arrow_val; eauto.
- iAlways. iIntros (v1 v2) "#HA".
- iApply "H". iAlways.
+ iModIntro. iIntros (v1 v2) "#HA".
+ iApply "H". iModIntro.
by iApply refines_ret.
Qed.
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 54ea266..f0c6357 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -692,10 +692,10 @@ Ltac rel_arrow_val :=
rel_pures_l; rel_pures_r;
(iApply refines_arrow_val
|| fail "rel_arrow_val: cannot apply the closure rule");
- iAlways.
+ iModIntro.
Ltac rel_arrow :=
rel_pures_l; rel_pures_r;
(iApply refines_arrow
|| fail "rel_arrow: cannot apply the closure rule");
- iAlways.
+ iModIntro.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 3b2d943..eaa5ae1 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -329,7 +329,7 @@ Section bin_log_related_under_typed_ctx.
inversion Hx1; subst; simpl; iIntros "#Hrel";
iIntros (Δ).
+ iApply (bin_log_related_rec with "[-]"); auto.
- iAlways. iApply (IHK with "[Hrel]"); auto.
+ iModIntro. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_app with "[]").
iApply (IHK with "[Hrel]"); auto.
by iApply fundamental.
@@ -423,7 +423,7 @@ Section bin_log_related_under_typed_ctx.
+ iApply (bin_log_related_unfold with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tlam with "[]").
- iIntros (Ï„i). iAlways.
+ iIntros (Ï„i). iModIntro.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tapp' with "[]").
iApply (IHK with "[Hrel]"); auto.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 96abf5b..87eefa6 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -548,11 +548,11 @@ Section fundamental.
+ iApply bin_log_related_if;
by iApply fundamental.
+ iApply bin_log_related_rec.
- iAlways. by iApply fundamental.
+ iModIntro. by iApply fundamental.
+ iApply bin_log_related_app;
by iApply fundamental.
+ iApply bin_log_related_tlam.
- iIntros (A). iAlways. by iApply fundamental.
+ iIntros (A). iModIntro. by iApply fundamental.
+ iApply bin_log_related_tapp'; by iApply fundamental.
+ iApply bin_log_related_fold; by iApply fundamental.
+ iApply bin_log_related_unfold; by iApply fundamental.
@@ -577,7 +577,7 @@ Section fundamental.
repeat iSplit; eauto; by iApply fundamental_val.
+ iExists _,_. iRight.
repeat iSplit; eauto; by iApply fundamental_val.
- + iLöb as "IH". iAlways.
+ + iLöb as "IH". iModIntro.
iIntros (v1 v2) "#Hv".
pose (Γ := (<[f:=(τ1 → τ2)%ty]> (<[x:=τ1]> ∅)):stringmap type).
pose (γ := (binder_insert f ((rec: f x := e)%V,(rec: f x := e)%V)
@@ -590,7 +590,7 @@ Section fundamental.
iApply env_ltyped2_empty. }
rewrite /γ /=. rewrite !binder_insert_fmap !fmap_empty /=.
by rewrite !subst_map_binder_insert_2_empty.
- + iIntros (A). iAlways. iIntros (v1 v2) "_".
+ + iIntros (A). iModIntro. iIntros (v1 v2) "_".
rel_pures_l. rel_pures_r.
iPoseProof (fundamental (A::Δ) ∅ e τ $! ∅ with "[]") as "H"; eauto.
{ rewrite fmap_empty. iApply env_ltyped2_empty. }
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index c7613a1..0e821dd 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -66,7 +66,7 @@ Proof.
eapply (logrel_simul Σ); last by apply Hstep.
iIntros (? ?).
iApply (bin_log_related_under_typed_ctx with "[]"); eauto.
- iAlways. iIntros (?). iApply Hlog.
+ iModIntro. iIntros (?). iApply Hlog.
Qed.
Lemma refines_sound Σ `{relocPreG Σ} e e' τ :
--
GitLab