From f7af5b3f891f217be492222253354e00b346d13c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 29 Oct 2018 17:49:08 +0100
Subject: [PATCH] Remove non-fork versions of pure lifting lemmas.

---
 theories/heap_lang/lifting.v                | 12 ++++----
 theories/program_logic/ectx_lifting.v       | 28 +----------------
 theories/program_logic/lifting.v            | 34 ---------------------
 theories/program_logic/ownp.v               | 28 +++--------------
 theories/program_logic/total_ectx_lifting.v | 21 -------------
 theories/program_logic/total_lifting.v      | 32 -------------------
 theories/program_logic/weakestpre.v         |  3 --
 7 files changed, 11 insertions(+), 147 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 505b93895..2a39566e8 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -162,17 +162,17 @@ Implicit Types σ : state.
 Lemma wp_fork s E e Φ :
   ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
-  iIntros "He HΦ".
-  iApply wp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
-  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
+  iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
+  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
 Lemma twp_fork s E e Φ :
   WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
-  iIntros "He HΦ".
-  iApply twp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
-  iIntros "!> /= {$He}". by iApply twp_value.
+  iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
+  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
 (** Heap *)
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index d878c0a8e..1ef64166e 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -54,20 +54,6 @@ Proof.
   iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
 Qed.
 
-Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
-  state_interp_fork_indep →
-  (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
-  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
-  ⊢ WP e1 @ s; E {{ Φ }}.
-Proof using Hinh.
-  iIntros (???) "H". iApply wp_lift_pure_step; [done| |by eauto|].
-  { by destruct s; auto. }
-  iApply (step_fupd_wand with "H"); iIntros "H".
-  iIntros (?????). iApply "H"; eauto.
-Qed.
-
 Lemma wp_lift_pure_head_stuck E Φ e :
   to_val e = None →
   sub_redexes_are_values e →
@@ -140,18 +126,6 @@ Proof.
   iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
 Qed.
 
-Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
-  state_interp_fork_indep →
-  (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
-  ⊢ WP e1 @ s; E {{ Φ }}.
-Proof using Hinh.
-  intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
-  destruct s; by auto.
-Qed.
-
 Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
@@ -167,7 +141,7 @@ Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧  σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
   ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 2c885e962..197a9c824 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -53,26 +53,6 @@ Proof.
   iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
 Qed.
 
-Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
-  state_interp_fork_indep →
-  (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-  (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
-  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
-  ⊢ WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (Hfork Hsafe Hstep) "H". iApply wp_lift_step.
-  { specialize (Hsafe inhabitant). destruct s; last done.
-      by eapply reducible_not_val. }
-  iIntros (σ1 κ κs n) "Hσ". iMod "H".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
-  { iPureIntro. destruct s; done. }
-  iNext. iIntros (e2 σ2 efs Hstep').
-  destruct (Hstep κ σ1 e2 σ2 efs); auto; subst; clear Hstep.
-  iMod "Hclose" as "_". iMod "H". iModIntro.
-  rewrite (Hfork _ _ _ n). iFrame "Hσ". iApply "H"; auto.
-Qed.
-
 Lemma wp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2 ∧ efs = []) →
@@ -140,20 +120,6 @@ Proof.
   by iApply "H".
 Qed.
 
-Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
-  state_interp_fork_indep →
-  (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
-    κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
-  ⊢ WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
-  { by naive_solver. }
-  iApply (step_fupd_wand with "H"); iIntros "H".
-  by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
-Qed.
-
 Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E E' Φ} e1 e2 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 4f12f1e48..d6611437d 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -189,22 +189,12 @@ Section lifting.
     iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
   Qed.
 
-  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
-    (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-    ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
-    ⊢ WP e1 @ s; E {{ Φ }}.
-  Proof.
-    iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
-    naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
-  Qed.
-
   Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) // ?big_sepL_nil ?right_id; eauto.
+    intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //; eauto.
   Qed.
 End lifting.
 
@@ -289,22 +279,12 @@ Section ectx_lifting.
     by destruct s; eauto using reducible_not_val.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
-    (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-    ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
-    ⊢ WP e1 @ s; E {{ Φ }}.
-  Proof using Hinh.
-    iIntros (??) "H"; iApply wp_lift_pure_det_step; try by eauto.
-    by destruct s; eauto using reducible_not_val.
-  Qed.
-
   Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs' = []) →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
-    iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
+    iIntros (??) "H"; iApply wp_lift_pure_det_step_no_fork; try by eauto.
     by destruct s; eauto using reducible_not_val.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index c26cc5acf..5dcdc380a 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -31,18 +31,6 @@ Proof.
   iApply "H". by eauto.
 Qed.
 
-Lemma twp_lift_pure_head_step {s E Φ} e1 :
-  state_interp_fork_indep →
-  (∀ σ1, head_reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
-  (|={E}=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
-  ⊢ WP e1 @ s; E [{ Φ }].
-Proof using Hinh.
-  iIntros (???) ">H". iApply twp_lift_pure_step; eauto.
-  iIntros "!>" (?????). iApply "H"; eauto.
-Qed.
-
 Lemma twp_lift_pure_head_step_no_fork {s E Φ} e1 :
   (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2 ∧ efs = []) →
@@ -83,15 +71,6 @@ Proof.
   iMod ("H" with "[# //]") as "(-> & -> & ? & $) /=". by iFrame.
 Qed.
 
-Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
-  state_interp_fork_indep →
-  (∀ σ1, head_reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
-  ⊢ WP e1 @ s; E [{ Φ }].
-Proof using Hinh. eauto 20 using twp_lift_pure_det_step. Qed.
-
 Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible_no_obs e1 σ1) →
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index 12ec53f16..2e22a7291 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -25,26 +25,7 @@ Lemma twp_lift_step s E Φ e1 :
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
-
 (** Derived lifting lemmas. *)
-Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
-  state_interp_fork_indep →
-  (∀ σ1, reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
-  (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
-    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
-  ⊢ WP e1 @ s; E [{ Φ }].
-Proof.
-  iIntros (Hfork Hsafe Hstep) "H". iApply twp_lift_step.
-  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
-  iIntros (σ1 κs n) "Hσ". iMod "H".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
-  iSplit; [by destruct s|]. iIntros (κ e2 σ2 efs Hstep').
-  destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
-  iMod "Hclose" as "_". iModIntro. iSplit; first done. rewrite (Hfork _ _ _ n).
-  iFrame "Hσ". iApply "H"; auto.
-Qed.
-
 Lemma twp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E Φ e1 :
   (∀ σ1, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2 ∧ efs = []) →
@@ -84,19 +65,6 @@ Proof.
   iApply twp_value; last done. by apply of_to_val.
 Qed.
 
-Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
-  state_interp_fork_indep →
-  (∀ σ1, reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
-    κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
-  ⊢ WP e1 @ s; E [{ Φ }].
-Proof.
-  iIntros (?? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
-  { by naive_solver. }
-  by iIntros "!>" (κ e' efs' σ (->&_&->&->)%Hpuredet).
-Qed.
-
 Lemma twp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
   (∀ σ1, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index c2437fb8a..4d71c1a4b 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -13,9 +13,6 @@ Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG {
 Notation irisG Λ Σ := (irisG' (state Λ) (observation Λ) Σ).
 Global Opaque iris_invG.
 
-Definition state_interp_fork_indep `{irisG Λ Σ} :=
-  ∀ σ κs n n', state_interp σ κs n = state_interp σ κs n'.
-
 Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
-- 
GitLab