Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

barrier/heap_lang.v

@@ -184,9 +184,6 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
      σ !! l = Some v1 →
      head_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None.
 
-Definition head_reducible e σ : Prop :=
-  ∃ e' σ' ef, head_step e σ e' σ' ef.
-
 (** Atomic expressions *)
 Definition atomic (e: expr) :=
   match e with
@@ -293,21 +290,6 @@ Proof.
   eauto using fill_item_inj, values_head_stuck, fill_not_val.
 Qed.
 
-Lemma prim_head_step e1 σ1 e2 σ2 ef :
-  head_reducible e1 σ1 →
-  prim_step e1 σ1 e2 σ2 ef →
-  head_step e1 σ1 e2 σ2 ef.
-Proof.
-  intros (e2'' & σ2'' & ef'' & Hstep'')  [K' e1' e2' Heq1 Heq2  Hstep].
-  assert (K' `prefix_of` []) as Hemp.
-  { eapply step_by_val; last first.
-    - eexact Hstep''.
-    - eapply values_head_stuck. eexact Hstep.
-    - done. }
-  destruct K'; last by (exfalso; eapply prefix_of_nil_not; eassumption).
-  by subst e1 e2.
-Qed.
-
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
   to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
@@ -339,11 +321,3 @@ Proof.
     exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
     econstructor; eauto.
 Qed.
-
-Lemma head_reducible_reducible e σ :
-  heap_lang.head_reducible e σ → reducible e σ.
-Proof.
-  intros H. destruct H; destruct_conjs.
-  do 3 eexists.
-  eapply heap_lang.Ectx_step with (K:=[]); last eassumption; done.
-Qed.

barrier/heap_lang_tactics.v

@@ -62,7 +62,6 @@ Ltac reshape_expr e tac :=
 
 Ltac do_step tac :=
   try match goal with |- language.reducible _ _ => eexists _, _, _ end;
-  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;
   match goal with
   | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
@@ -70,7 +69,4 @@ Ltac do_step tac :=
        eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
        first [apply alloc_fresh|econstructor];
        rewrite ?to_of_val; tac; fail
-  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
-       first [apply alloc_fresh|econstructor];
-       rewrite ?to_of_val; tac; fail
   end.

barrier/lifting.v

@@ -3,7 +3,6 @@ Require Export iris.weakestpre barrier.heap_lang_tactics.
 Import uPred.
 Import heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
-Local Hint Extern 0 (head_reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
 Context {Σ : iFunctor}.
@@ -24,7 +23,7 @@ Lemma wp_alloc_pst E σ e v Q :
 Proof.
   intros; set (φ e' σ' ef := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None
                                 ∧ ef = (None : option expr)).
-  rewrite -(wp_lift_step E E φ _ _  σ) // /φ; last (by intros; inv_step; eauto).
+  rewrite -(wp_lift_step E E φ _ _  σ) // /φ; last (by intros; inv_step; eauto); [].
   rewrite -pvs_intro. apply sep_mono, later_mono; first done.
   apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
   apply wand_intro_l.
@@ -34,26 +33,6 @@ Proof.
   by rewrite left_id wand_elim_r -wp_value'.
 Qed.
 
-Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
-  to_val e1 = None →
-  head_reducible e1 σ1 →
-  (∀ e' σ' ef, head_step e1 σ1 e' σ' ef → ef = None ∧ e' = of_val v2 ∧ σ' = σ2) →
-  (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2)) ⊑ wp E e1 Q.
-Proof.
-  intros He Hsafe Hstep.
-  rewrite -(wp_lift_step E E (λ e' σ' ef,
-    ef = None ∧ e' = of_val v2 ∧ σ' = σ2) _ e1 σ1) //;
-    eauto using prim_head_step, head_reducible_reducible.
-  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2'; apply forall_intro=>σ2'.
-  apply forall_intro=>ef; apply wand_intro_l.
-  rewrite always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> [-> ->]] /=.
-  rewrite -pvs_intro right_id -wp_value.
-  by rewrite wand_elim_r.
-Qed.
-
-
 Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
   (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
@@ -100,33 +79,19 @@ Proof.
   by rewrite -wp_value' //; apply const_intro.
 Qed.
 
-Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
-  to_val e1 = None →
-  (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ ef = None ∧ φ e2) →
-  (▷ ∀ e2, ■ φ e2 → wp E e2 Q) ⊑ wp E e1 Q.
-Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e' ef, ef = None ∧ φ e')) //=.
-  apply later_mono, forall_mono=>e2; apply forall_intro=>ef.
-  apply impl_intro_l, const_elim_l=>-[-> ?] /=.
-  by rewrite const_equiv // left_id right_id.
-Qed.
-
 Lemma wp_rec E ef e v Q :
   to_val e = Some v →
   ▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = ef.[Rec ef, e /])
-    Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
-  by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /]) //=;
+    last by intros; inv_step; eauto.
 Qed.
 
 Lemma wp_plus E n1 n2 Q :
   ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
-  rewrite -(wp_lift_pure_step E (λ e', e' = LitNat (n1 + n2))) //=;
+  rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2))) //=;
     last by intros; inv_step; eauto.
-  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
 
@@ -134,9 +99,8 @@ Lemma wp_le_true E n1 n2 Q :
   n1 ≤ n2 →
   ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = LitTrue)) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue) //=;
     last by intros; inv_step; eauto with lia.
-  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
 
@@ -144,9 +108,8 @@ Lemma wp_le_false E n1 n2 Q :
   n1 > n2 →
   ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = LitFalse)) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse) //=;
     last by intros; inv_step; eauto with lia.
-  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
 
@@ -154,9 +117,8 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e1)) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Fst _) e1) //=;
     last by intros; inv_step; eauto.
-  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
 
@@ -164,9 +126,8 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e2)) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Snd _) e2) //=;
     last by intros; inv_step; eauto.
-  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
 
@@ -174,18 +135,16 @@ Lemma wp_case_inl E e0 v0 e1 e2 Q :
   to_val e0 = Some v0 →
   ▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e1.[e0/]) _
-    (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
-  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/]) //=;
+    last by intros; inv_step; eauto.
 Qed.
 
 Lemma wp_case_inr E e0 v0 e1 e2 Q :
   to_val e0 = Some v0 →
   ▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_step E (λ e', e' = e2.[e0/]) _
-    (Case (InjR e0) e1 e2)) //=; last by intros; inv_step; eauto.
-  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/]) //=;
+    last by intros; inv_step; eauto.
 Qed.
 
 (** Some derived stateless axioms *)

iris/lifting.v

 Require Export iris.weakestpre.
 Require Import iris.wsat.
+Import uPred.
+
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
@@ -36,6 +38,7 @@ Proof.
   { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
   by exists r1', r2'; split_ands; [| |by intros ? ->].
 Qed.
+
 Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
@@ -50,4 +53,36 @@ Proof.
   destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto; [by destruct k|].
   exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
 Qed.
+
+(** Derived lifting lemmas. *)
+Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
+  to_val e1 = None →
+  reducible e1 σ1 →
+  (∀ e' σ' ef, prim_step e1 σ1 e' σ' ef → ef = None ∧ e' = of_val v2 ∧ σ' = σ2) →
+  (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2)) ⊑ wp E e1 Q.
+Proof.
+  intros He Hsafe Hstep.
+  rewrite -(wp_lift_step E E (λ e' σ' ef,
+    ef = None ∧ e' = of_val v2 ∧ σ' = σ2) _ e1 σ1) //; [].
+  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2'; apply forall_intro=>σ2'.
+  apply forall_intro=>ef; apply wand_intro_l.
+  rewrite always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> [-> ->]] /=.
+  rewrite -pvs_intro right_id -wp_value.
+  by rewrite wand_elim_r.
+Qed.
+
+Lemma wp_lift_pure_det_step {E Q} e1 e2 :
+  to_val e1 = None →
+  (∀ σ1, reducible e1 σ1) →
+  (∀ σ1 e' σ' ef, prim_step e1 σ1 e' σ' ef → σ1 = σ' ∧ ef = None ∧ e' = e2) →
+  (▷ wp E e2 Q) ⊑ wp E e1 Q.
+Proof.
+  intros. rewrite -(wp_lift_pure_step E (λ e' ef, ef = None ∧ e' = e2) _ e1) //=.
+  apply later_mono, forall_intro=>e'; apply forall_intro=>ef.
+  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
+  by rewrite right_id.
+Qed.
+
 End lifting.