From 3c9a0c4f87f57a85577315b978d6fcef6e52e24b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 7 Oct 2018 23:42:52 +0200
Subject: [PATCH] =?UTF-8?q?Weaken=20`PureExec=20=CF=86=20n=20e1=20e2`=20so?=
 =?UTF-8?q?=20that=20it=20can=20take=20`>=3D=20n`=20steps.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/heap_lang/lifting.v           |  4 +++-
 theories/program_logic/language.v      | 33 ++++++++++++++++++++++++--
 theories/program_logic/lifting.v       | 10 ++++++--
 theories/program_logic/total_lifting.v |  4 ++--
 4 files changed, 44 insertions(+), 7 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 52c3b33cd..efbd8ffa9 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -75,7 +75,9 @@ Proof. solve_atomic. Qed.
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
-  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
+  subst;
+  apply mk_pure_exec; intros ?;
+  apply nsteps_once, pure_head_step_pure_step;
     constructor; [solve_exec_safe | solve_exec_puredet].
 
 Class AsRecV (v : val) (f x : binder) (erec : expr) :=
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 8c50057f4..e75364098 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -142,7 +142,11 @@ Section language.
   (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
   succeeding when it did not actually do anything. *)
   Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
-    pure_exec : φ → nsteps pure_step n e1 e2.
+    pure_exec : φ → ∃ n', n ≤ n' ∧ nsteps pure_step n' e1 e2.
+  Lemma mk_pure_exec (φ : Prop) n e1 e2 :
+    (φ → nsteps pure_step n e1 e2) →
+    PureExec φ n e1 e2.
+  Proof. intros ??. exists n; eauto. Qed.
 
   Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
     pure_step e1 e2 →
@@ -165,7 +169,32 @@ Section language.
   Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
     PureExec φ n e1 e2 →
     PureExec φ n (K e1) (K e2).
-  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
+  Proof.
+    intros He ?. destruct He as (n'&?&?); eauto using pure_step_nsteps_ctx.
+  Qed.
+
+  Lemma pure_exec_mono (φ φ' : Prop) n n' e1 e2 :
+    (φ' → φ) → n' ≤ n → PureExec φ n e1 e2 → PureExec φ' n' e1 e2.
+  Proof. intros  ?? He ?. destruct He as (n''&?&?); eauto using Nat.le_trans. Qed.
+  Lemma pure_exec_mono_steps n n' φ e1 e2 :
+    n' ≤ n → PureExec φ n e1 e2 → PureExec φ n' e1 e2.
+  Proof. eauto using pure_exec_mono. Qed.
+
+  Lemma pure_exec_refl φ e : PureExec φ 0 e e.
+  Proof. intros _. exists 0. eauto using nsteps_O. Qed.
+  Lemma pure_exec_trans n1 n2 φ1 φ2 e1 e2 e3 :
+    PureExec φ1 n1 e1 e2 → PureExec φ2 n2 e2 e3 →
+    PureExec (φ1 ∧ φ2) (n1 + n2) e1 e3.
+  Proof.
+    intros He1 He2 [??]. destruct He1 as (n1'&?&?), He2 as (n2'&?&?);
+      eauto using Nat.add_le_mono, nsteps_trans.
+  Qed.
+  Lemma pure_exec_0_l n φ e1 e2 e3 :
+    PureExec True 0 e1 e2 → PureExec φ n e2 e3 → PureExec φ n e1 e3.
+  Proof.
+    intros. apply pure_exec_mono with (True ∧ φ) (0 + n);
+      eauto using pure_exec_trans.
+  Qed.
 
   (* This is a family of frequent assumptions for PureExec *)
   Class IntoVal (e : expr Λ) (v : val Λ) :=
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 637b6258e..c00630b8d 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -125,11 +125,17 @@ Qed.
 
 Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
+  E' ⊆ E →
   φ →
   Nat.iter n (λ P, |={E,E'}▷=> P) (WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
-  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iIntros (Hexec ? Hφ) "Hwp". specialize (Hexec Hφ) as (?&[n' ->]%nat_le_sum&Hexec).
+  iAssert (Nat.iter (n + n') (λ P, |={E,E'}▷=> P) (WP e2 @ s; E {{ v, Φ v }}))%I
+     with "[Hwp]" as "Hwp".
+  { clear Hexec. rewrite Nat.add_comm.
+    iInduction n' as [|n'] "IH"; simpl; first done.
+    iApply step_fupd_intro; first done. iNext. by iApply "IH". }
+  iInduction Hexec as [e|m e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
   iApply wp_lift_pure_det_step.
   - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
   - destruct s; naive_solver.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index c5aaca8fe..2577a5b14 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -73,8 +73,8 @@ Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
   φ →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
-  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ) as (n'&_&Hexec).
+  iInduction Hexec as [e|n' e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
   iApply twp_lift_pure_det_step; [done|naive_solver|].
   iModIntro. rewrite /= right_id. by iApply "IH".
 Qed.
-- 
GitLab