Lifting lemmas do no longer have in hypothsesis that the expression is not a value.

This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.

CHANGELOG.md

@@ -5,6 +5,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 ## Iris 3.0
 
+# Lifting lemmas do no longer take as hypothesis the fact the the
+  considered expression is not a value. This is deduced from the fact that
+  it is reducible.
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre

heap_lang/lifting.v

@@ -61,8 +61,8 @@ Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto 10.
-  intros; inv_head_step; eauto 10.
+  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto.
+  intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_store_pst E σ l v v' Φ :
@@ -89,7 +89,7 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
   ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
-    (<[l:=v2]>σ)); eauto 10.
+    (<[l:=v2]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 

program_logic/ectx_lifting.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ}.
+Context `{irisG (ectx_lang expr) Σ} `{Inhabited state}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
@@ -17,27 +17,25 @@ Lemma wp_ectx_bind {E e} K Φ :
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_lift_head_step E Φ e1 :
-  to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ★ ▷ ownP σ1 ★
     ▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ★ ownP σ2
           ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E); try done.
+  iIntros "H". iApply (wp_lift_step E); try done.
   iVs "H" as (σ1) "(%&Hσ1&Hwp)". iVsIntro. iExists σ1.
   iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
   iApply "Hwp". by eauto.
 Qed.
 
 Lemma wp_lift_pure_head_step E Φ e1 :
-  to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (▷ ∀ e2 efs σ, ■ head_step e1 σ e2 σ efs →
     WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
+  iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
   iIntros (????). iApply "H". eauto.
 Qed.
 
@@ -75,7 +73,6 @@ Proof.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
-  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 = efs') →
   ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})

program_logic/lifting.v

@@ -12,29 +12,32 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma wp_lift_step E Φ e1 :
-  to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ★ ▷ ownP σ1 ★
     ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ★ ownP σ2
           ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
-  iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
-  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
-  iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
-  iApply "H"; eauto.
+  iIntros "H". rewrite wp_unfold /wp_pre.
+  destruct (to_val e1) as [v|] eqn:EQe1.
+  - iLeft. iExists v. iSplit. done. iVs "H" as (σ1) "[% _]".
+    by erewrite reducible_not_val in EQe1.
+  - iRight; iSplit; eauto.
+    iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
+    iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
+    iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
+    iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
+    iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_pure_step E Φ e1 :
-  to_val e1 = None →
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs →
     WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
+  iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
+  { iPureIntro. eapply reducible_not_val, (Hsafe inhabitant). }
   iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
   iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
@@ -49,8 +52,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
     (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (Hatomic ?) "[Hσ H]".
-  iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
+  iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
   iApply pvs_intro'; [set_solver|iIntros "Hclose"].
   iExists σ1. iFrame "Hσ"; iSplit; eauto.
   iNext; iIntros (e2 σ2 efs) "[% Hσ]".
@@ -73,14 +75,13 @@ Proof.
   edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
 Qed.
 
-Lemma wp_lift_pure_det_step {E Φ} e1 e2 efs :
-  to_val e1 = None →
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
+  iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
   by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.