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

_CoqProject

@@ -64,6 +64,7 @@ iris/language.v
 iris/functor.v
 iris/tests.v
 barrier/heap_lang.v
+barrier/heap_lang_tactics.v
 barrier/lifting.v
 barrier/sugar.v
 barrier/tests.v

barrier/heap_lang_tactics.v

+Require Export barrier.heap_lang.
+Require Import prelude.fin_maps.
+Import heap_lang.
+
+Ltac inv_step :=
+  repeat match goal with
+  | _ => progress simplify_map_equality' (* simplify memory stuff *)
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
+  | H : prim_step _ _ _ _ _ |- _ => destruct H; subst
+  | H : _ = fill ?K ?e |- _ =>
+     destruct K as [|[]];
+     simpl in H; first [subst e|discriminate H|injection' H]
+     (* ensure that we make progress for each subgoal *)
+  | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
+    apply values_head_stuck, (fill_not_val K) in H;
+    by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
+  | H : head_step ?e _ _ _ _ |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if e is a variable
+     and can thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+
+Ltac reshape_expr e tac :=
+  let rec go K e :=
+  match e with
+  | _ => tac (reverse K) e
+  | App ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
+     end
+  | Plus ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (PlusRCtx v1 :: K) e2 | _ => go (PlusLCtx e2 :: K) e1
+     end
+  | Le ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (LeRCtx v1 :: K) e2 | _ => go (LeLCtx e2 :: K) e1
+     end
+  | Pair ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
+     end
+  | Fst ?e => go (FstCtx :: K) e
+  | Snd ?e => go (SndCtx :: K) e
+  | InjL ?e => go (InjLCtx :: K) e
+  | InjR ?e => go (InjRCtx :: K) e
+  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
+  | Alloc ?e => go (AllocCtx :: K) e
+  | Load ?e => go (LoadCtx :: K) e
+  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1 || go (StoreRCtx e1 :: K) e2
+  | Cas ?e0 ?e1 ?e2 =>
+     lazymatch e0 with
+     | of_val ?v0 =>
+        lazymatch e1 with
+        | of_val ?v1 => go (CasRCtx v0 v1 :: K) e2
+        | _ => go (CasMCtx v0 e2 :: K) e1
+        end
+     | _ => go (CasLCtx e1 e2 :: K) e0
+     end
+  end in go (@nil ectx_item) e.
+
+Ltac do_step tac :=
+  try match goal with |- reducible _ _ => eexists _, _, _ end;
+  simpl;
+  match goal with
+  | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+     reshape_expr e1 ltac:(fun K e1' =>
+       eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
+       first [apply alloc_fresh|econstructor];
+       rewrite ?to_of_val; tac; fail
+  end.

barrier/lifting.v

 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.heap_lang.
+Require Export iris.weakestpre barrier.heap_lang_tactics.
 Import uPred.
+Import heap_lang.
+Local Hint Extern 0 (reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+Implicit Types Q : val → iProp heap_lang Σ.
+Implicit Types K : ectx.
 
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
-  wp E e (λ v, wp E (fill K (v2e v)) Q) ⊑ wp E (fill K e) Q.
-Proof. apply (wp_bind (K:=fill K)), fill_is_ctx. Qed.
+  wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
+Proof. apply wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-
 Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
   reducible e1 σ1 →
@@ -23,303 +25,176 @@ Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
   ⊑ wp E2 e1 Q.
 Proof.
   intros ? He Hsafe Hstep.
-  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
-  etransitivity; last eapply wp_lift_step with (σ2 := σ1)
-    (φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first.
-  - intros e2 σ2 ef Hstep'%prim_ectx_step; last done.
-    by apply Hstep.
-  - destruct Hsafe as (e' & σ' & ? & ?).
-    do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); eassumption.
-  - done.
-  - eassumption.
-  - apply pvs_mono. apply sep_mono; first done.
-    apply later_mono. apply forall_mono=>e2. apply forall_mono=>σ2.
-    apply forall_intro=>ef. apply wand_intro_l.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ.
-    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
-    apply pvs_mono. rewrite right_id. done.
+  rewrite -(wp_lift_step E1 E2 (λ e' σ' ef, ef = None ∧ φ e' σ') _ _ σ1) //.
+  apply pvs_mono, sep_mono, later_mono; first done.
+  apply forall_mono=>e2; apply forall_mono=>σ2.
+  apply forall_intro=>ef; apply wand_intro_l.
+  rewrite always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ?] /=.
+  by rewrite const_equiv // left_id wand_elim_r right_id.
 Qed.
 
 (* TODO RJ: Figure out some better way to make the
    postcondition a predicate over a *location* *)
 Lemma wp_alloc_pst E σ e v Q :
-  e2v e = Some v →
-  (ownP σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
+  to_val e = Some v →
+  (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
-  intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None);
-    last first.
-  - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done.
-    rewrite Hv in Hvl. inversion_clear Hvl.
-    eexists; split_ands; done.
-  - set (l := fresh $ dom (gset loc) σ).
-    exists (Loc l), ((<[l:=v]>)σ), None. eapply AllocS; first done.
-    apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [l [-> [-> Hl]]].
-    rewrite (forall_elim l). eapply const_intro_l; first eexact Hl.
-    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
-    rewrite -wp_value'; done.
+  intros; set (φ e' σ' := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+  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 wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[l [-> [-> ?]]].
+  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
-  (ownP σ ★ ▷(ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
+  (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
 Proof.
-  intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
-  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}.
-    rewrite Hlookup. case=>->. done.
-  - do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value.
+  intros; rewrite -(wp_lift_step E E (λ e' σ', e' = of_val v ∧ σ' = σ)) //;
+    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 wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value.
 Qed.
-
 Lemma wp_store_pst E σ l e v v' Q :
-  e2v e = Some v →
-  σ !! l = Some v' →
-  (ownP σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
+  to_val e = Some v → σ !! l = Some v' →
+  (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
-  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}.
-    rewrite Hvl in Hv. inversion_clear Hv. done.
-  - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros.
+  rewrite -(wp_lift_step E E (λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ)) //;
+    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 wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  σ !! l = Some v' → v' <> v1 →
-  (ownP σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
+  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
+  (ownP σ ★ ▷ (ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitFalse ∧ σ' = σ) (E1:=E); auto; last first.
-  - by inversion_clear 1; simplify_map_equality.
-  - do 3 eexists; econstructor; eauto.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2'. apply forall_intro=>σ2'.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros; rewrite -(wp_lift_step E E (λ e' σ', e' = LitFalse ∧ σ' = σ)) //;
+    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 wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  σ !! l = Some v1 →
-  (ownP σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
+  to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
+  (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first.
-  - intros e2' σ2' ef Hstep. move:H. inversion_clear Hstep=>H.
-    (* FIXME this rewriting is rather ugly. *)
-    + exfalso. rewrite H in Hlookup. case:Hlookup=>?; subst vl.
-      rewrite Hvl in Hv1. case:Hv1=>?; subst v1. done.
-    + rewrite H in Hlookup. case:Hlookup=>?; subst v1.
-      rewrite Hl in Hv2. case:Hv2=>?; subst v2. done.
-  - do 3 eexists. eapply CasSucS; eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2'. apply forall_intro=>σ2'.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros.
+  rewrite -(wp_lift_step E E (λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ)) //;
+    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 wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-
 Lemma wp_fork E e :
-  ▷ wp coPset_all e (λ _, True : iProp heap_lang Σ)
-  ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
+  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
-    last first.
-  - intros σ1 e2 σ2 ef Hstep%prim_ectx_step; last first.
-    { do 3 eexists. eapply ForkS. }
-    inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); [].
-    eapply ForkS.
-  - reflexivity.
-  - apply later_mono.
-    apply forall_intro=>e2; apply forall_intro=>ef.
-    apply impl_intro_l, const_elim_l=>-[-> ->] /=; apply sep_intro_True_l; auto.
-    by rewrite -wp_value' //; apply const_intro.
+  rewrite -(wp_lift_pure_step E (λ e' ef, e' = LitUnit ∧ ef = Some e)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2; apply forall_intro=>ef.
+  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
+  apply sep_intro_True_l; last done.
+  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 He Hsafe Hstep.
-  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ0 := λ e' ef, ef = None ∧ φ e'); last first.
-  - intros σ1 e2 σ2 ef Hstep'%prim_ectx_step; last done.
-    by apply Hstep.
-  - intros σ1. destruct (Hsafe σ1) as (e' & σ' & ? & ?).
-    do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); eassumption.
-  - done.
-  - apply later_mono. apply forall_mono=>e2. apply forall_intro=>ef.
-    apply impl_intro_l. apply const_elim_l; move=>[-> Hφ].
-    eapply const_intro_l; first eexact Hφ. rewrite impl_elim_r.
-    rewrite right_id. done.
+  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 :
-  e2v e = Some v →
-  ▷wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
+  to_val e = Some v →
+  ▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = ef.[Rec ef, e /]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. eapply BetaS; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->. done.
+  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=>->.
 Qed.
-
-Lemma wp_plus n1 n2 E Q :
-  ▷Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
+Lemma wp_plus E n1 n2 Q :
+  ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = LitNat (n1 + n2)); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  rewrite -(wp_lift_pure_step E (λ e', e' = 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.
-
-Lemma wp_le_true n1 n2 E Q :
+Lemma wp_le_true E n1 n2 Q :
   n1 ≤ n2 →
-  ▷Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros Hle. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = LitTrue); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; first done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = 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.
-
-Lemma wp_le_false n1 n2 E Q :
+Lemma wp_le_false E n1 n2 Q :
   n1 > n2 →
-  ▷Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros Hle. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = LitFalse); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = 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.
-
-Lemma wp_fst e1 v1 e2 v2 E Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
+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 Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e1); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last eassumption; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = 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.
-
-Lemma wp_snd e1 v1 e2 v2 E Q :
-  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  ▷Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
+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 Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e2); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last eassumption; done.
+  intros; rewrite -(wp_lift_pure_step E (λ e', e' = 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.
-
-Lemma wp_case_inl e0 v0 e1 e2 E Q :
-  e2v e0 = Some v0 →
-  ▷wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
+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 Hv0. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e1.[e0/]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e1'. apply impl_intro_l.
-    by apply const_elim_l=>->.
+  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=>->.
 Qed.
-
-Lemma wp_case_inr e0 v0 e1 e2 E Q :
-  e2v e0 = Some v0 →
-  ▷wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
+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 Hv0. etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e2.[e0/]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    by apply const_elim_l=>->.
+  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=>->.
 Qed.
 
 (** Some derived stateless axioms *)
-
-Lemma wp_le n1 n2 E P Q :
-  (n1 ≤ n2 → P ⊑ ▷Q LitTrueV) →
-  (n1 > n2 → P ⊑ ▷Q LitFalseV) →
+Lemma wp_le E n1 n2 P Q :
+  (n1 ≤ n2 → P ⊑ ▷ Q LitTrueV) →
+  (n1 > n2 → P ⊑ ▷ Q LitFalseV) →
   P ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HPle HPgt.
-  assert (Decision (n1 ≤ n2)) as Hn12 by apply _.
-  destruct Hn12 as [Hle|Hgt].
-  - rewrite -wp_le_true; auto.
-  - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
+  intros; destruct (decide (n1 ≤ n2)).
+  * rewrite -wp_le_true; auto.
+  * rewrite -wp_le_false; auto with lia.
 Qed.