Clean up heap_lang and remove some FIXMEs.

Notable changes:
* I am now using the same names for the fields of the language record and the
  instances in heap_lang. In order to deal with shadowing, I have put all
  definitions in heap_lang.v in a module.
* Instead of defining evaluation contexts recursively, these are now defined
  using lists. This way we can easily reuse operations on lists. For example,
  composition of evaluation contexts is just appending lists. Also, it allowed
  me to simplify the rather complicated proof of step_by_val as induction on
  the shape of contexts no longer results in a blow-up of the number of cases.
* Use better automation to prove all lemmas of heap_lang.
* I have introduced tactics to invert steps and to do steps. These tactics
  greatly helped simplifying boring parts of lifting lemmas.

_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.
+  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.
+  ▷ 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 :
   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 :
   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 →
+  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.
+  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.
+  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.
+  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) →
+  (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.
 End lifting.

barrier/sugar.v

 Require Export barrier.heap_lang barrier.lifting.
 Import uPred.
+Import heap_lang.
 
 (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
 Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
@@ -13,67 +14,52 @@ Definition Eq e1 e2 :=
 
 Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 
-Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
-Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
+Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
+Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
 
 Section suger.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+Implicit Types Q : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam E ef e v Q :
-  e2v e = Some v → ▷wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
+  to_val e = Some v → ▷ wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
 Proof.
   intros Hv. rewrite -wp_rec; last eassumption.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
      to talk to the Autosubst guys. *)
   by asimpl.
 Qed.
-
 Lemma wp_let e1 e2 E Q :
-  wp E e1 (λ v, ▷wp E (e2.[v2e v/]) Q) ⊑ wp E (Let e1 e2) Q.
+  wp E e1 (λ v, ▷wp E (e2.[of_val v/]) Q) ⊑ wp E (Let e1 e2) Q.
 Proof.
-  rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
-  rewrite -wp_lam //. by rewrite v2v.
+  rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
+  by rewrite -wp_lam //= to_of_val.
 Qed.
-
-Lemma wp_if_true e1 e2 E Q :
-  ▷wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
-Proof.
-  rewrite -wp_case_inl //. by asimpl.
-Qed.
-
-Lemma wp_if_false e1 e2 E Q :
-  ▷wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
-Proof.
-  rewrite -wp_case_inr //. by asimpl.
-Qed.
-
+Lemma wp_if_true e1 e2 E Q : ▷ wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
+Proof. rewrite -wp_case_inl //. by asimpl. Qed.
+Lemma wp_if_false e1 e2 E Q : ▷ wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
+Proof. rewrite -wp_case_inr //. by asimpl. Qed.
 Lemma wp_lt n1 n2 E P Q :
-  (n1 < n2 → P ⊑ ▷Q LitTrueV) →
-  (n1 ≥ n2 → P ⊑ ▷Q LitFalseV) →
+  (n1 < n2 → P ⊑ ▷ Q LitTrueV) →
+  (n1 ≥ n2 → P ⊑ ▷ Q LitFalseV) →
   P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HPlt HPge.
-  rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl.
-  apply wp_le; intros; [apply HPlt|apply HPge]; omega.
+  intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=.
+  auto using wp_le with lia.
 Qed.
-
 Lemma wp_eq n1 n2 E P Q :
-  (n1 = n2 → P ⊑ ▷Q LitTrueV) →
-  (n1 ≠ n2 → P ⊑ ▷Q LitFalseV) →
+  (n1 = n2 → P ⊑ ▷ Q LitTrueV) →
+  (n1 ≠ n2 → P ⊑ ▷ Q LitFalseV) →
   P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros HPeq HPne.
-  rewrite -wp_let -wp_value' // -later_intro. asimpl.
-  rewrite -wp_rec //. asimpl.
-  rewrite -(wp_bind (CaseCtx EmptyCtx _ _)) -later_intro.
-  apply wp_le; intros Hn12.
-  - asimpl. rewrite -wp_case_inl // -!later_intro. apply wp_le; intros Hn12'.
-    + apply HPeq; omega.
-    + apply HPne; omega.
-  - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //.
-    apply HPne; omega.
+  rewrite -wp_let -wp_value' // -later_intro; asimpl.
+  rewrite -wp_rec //; asimpl.
+  rewrite -(wp_bind [CaseCtx _ _]) -later_intro; asimpl.
+  apply wp_le; intros; asimpl.
+  * rewrite -wp_case_inl // -!later_intro. apply wp_le; auto with lia.
+  * rewrite -wp_case_inr // -later_intro -wp_value' //; auto with lia.
 Qed.
 End suger.

barrier/tests.v

 (** This file is essentially a bunch of testcases. *)
 Require Import modures.logic.
 Require Import barrier.lifting barrier.sugar.
+Import heap_lang.
 Import uPred.
 
 Module LangTests.
-  Definition add :=  Plus (LitNat 21) (LitNat 21).
+  Definition add := Plus (LitNat 21) (LitNat 21).
   Goal ∀ σ, prim_step add σ (LitNat 42) σ None.
-  Proof.
-    constructor.
-  Qed.
-
+  Proof. intros; do_step done. Qed.
   Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
   Definition rec_app := App rec (LitNat 0).
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
-  Proof.
-    move=>?. eapply BetaS.
-    reflexivity.
-  Qed.
-
+  Proof. intros; do_step done. Qed.
   Definition lam := Lam (Plus (Var 0) (LitNat 21)).
   Goal ∀ σ, prim_step (App lam (LitNat 21)) σ add σ None.
-  Proof.
-    move=>?. eapply BetaS. reflexivity.
-  Qed.
+  Proof. intros; do_step done. Qed.
 End LangTests.
 
 Module LiftingTests.
   Context {Σ : iFunctor}.
   Implicit Types P : iProp heap_lang Σ.
-  Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+  Implicit Types Q : val → iProp heap_lang Σ.
 
   (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
   Definition e3 := Load (Var 0).
@@ -42,26 +34,24 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
-    rewrite -(wp_bind (SeqCtx EmptyCtx (Load (Loc _)))).
-    rewrite -(wp_bind (StoreRCtx (LocV _) EmptyCtx)).
-    rewrite -(wp_bind (PlusLCtx EmptyCtx _)).
+    rewrite -(wp_bind [SeqCtx (Load (Loc _))]).
+    rewrite -(wp_bind [StoreRCtx (LocV _)]).
+    rewrite -(wp_bind [PlusLCtx _]).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
+    { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_plus -later_intro.
     rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. }
-    { reflexivity. }
+    { by rewrite lookup_insert. }
+    { done. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_lam // -later_intro. asimpl.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. }
+    { by rewrite lookup_insert. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     by apply const_intro.
   Qed.
 
-  Import Nat.
-
   Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
                                       (App f Sn1)
                                       n1.
@@ -85,10 +75,10 @@ Module LiftingTests.
     (* Go on. *)
     rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
     rewrite -wp_plus. asimpl.
-    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    rewrite -!later_intro. simpl.
+    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -!later_intro /=.
     apply wp_lt; intros Hn12.
-    - (* TODO RJ: It would be better if we could use wp_if_true here
+    * (* TODO RJ: It would be better if we could use wp_if_true here
          (and below). But we cannot, because the substitutions in there
          got already unfolded. *)
       rewrite -wp_case_inl //.
@@ -97,30 +87,29 @@ Module LiftingTests.
       eapply impl_elim; first by eapply and_elim_l. apply and_intro.
       + apply const_intro; omega.
       + by rewrite !and_elim_r.
-    - rewrite -wp_case_inr //.
+    * rewrite -wp_case_inr //.
       rewrite -!later_intro -wp_value' //.
       rewrite and_elim_r. apply const_elim_l=>Hle.
-      assert (Heq: n1 = pred n2) by omega. by subst n1.
+      by replace n1 with (pred n2) by lia.
   Qed.
 
   Lemma Pred_spec n E Q :
     ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
-    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    apply later_mono, wp_le; intros Hn.
+    rewrite -(wp_bind [CaseCtx _ _]).
+    apply later_mono, wp_le=> Hn.
     - rewrite -wp_case_inl //.
       rewrite -!later_intro -wp_value' //.
-      assert (Heq: n = 0) by omega. by subst n.
+      by replace n with 0 by lia.
     - rewrite -wp_case_inr //.
-      rewrite -!later_intro -FindPred_spec. apply and_intro.
-      + by apply const_intro; omega.
-      + done.
+      rewrite -!later_intro -FindPred_spec.
+      auto using and_intro, const_intro with lia.
   Qed.
 
   Goal ∀ E,
-    (True : iProp heap_lang Σ)
-    ⊑ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+    True ⊑ wp (Σ:=Σ) E
+      (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
   Proof.
     intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
     asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)

iris/hoare_lifting.v

@@ -55,7 +55,7 @@ Proof.
   rewrite -(ht_lift_step E E φ'  _ P
     (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I
     (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
-    try by (rewrite /φ'; eauto using atomic_not_value, atomic_step).
+    try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
   apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
   apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
   apply and_intro; [|apply and_intro; [|done]].

iris/language.v

@@ -11,7 +11,7 @@ Structure language := Language {
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
   values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None;
-  atomic_not_value e : atomic e → to_val e = None;
+  atomic_not_val e : atomic e → to_val e = None;
   atomic_step e1 σ1 e2 σ2 ef :
     atomic e1 →
     prim_step e1 σ1 e2 σ2 ef →
@@ -24,7 +24,7 @@ Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
 Arguments values_stuck {_} _ _ _ _ _ _.
-Arguments atomic_not_value {_} _ _.
+Arguments atomic_not_val {_} _ _.
 Arguments atomic_step {_} _ _ _ _ _ _ _.
 
 Canonical Structure istateC Σ := leibnizC (state Σ).
@@ -47,9 +47,7 @@ Section language.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
   Lemma atomic_of_val v : ¬atomic (of_val v).
-  Proof.
-    by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
-  Qed.
+  Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
   Global Instance: Injective (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
 End language.
@@ -59,12 +57,12 @@ Instance: Params (@fill) 3.
 Arguments fill {_ _ _} !_ _ / : simpl nomatch.
 
 Class CtxLanguage (Λ : language) (C : Type) `{Fill C (expr Λ)} := {
-  is_ctx_value K e :
+  fill_not_val K e :
     to_val e = None → to_val (fill K e) = None;
-  is_ctx_step_preserved K e1 σ1 e2 σ2 ef :
+  fill_step K e1 σ1 e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
     prim_step (fill K e1) σ1 (fill K e2) σ2 ef;
-  is_ctx_step K e1' σ1 e2 σ2 ef :
+  fill_step_inv K e1' σ1 e2 σ2 ef :
     to_val e1' = None → prim_step (fill K e1') σ1 e2 σ2 ef →
     ∃ e2', e2 = fill K e2' ∧ prim_step e1' σ1 e2' σ2 ef
 }.

iris/weakestpre.v

@@ -117,7 +117,7 @@ Qed.
 Lemma wp_atomic E1 E2 e Q :
   E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Q v))) ⊑ wp E1 e Q.
 Proof.
-  intros ? He r n ? Hvs; constructor; eauto using atomic_not_value.
+  intros ? He r n ? Hvs; constructor; eauto using atomic_not_val.
   intros rf k Ef σ1 ???.
   destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
   inversion Hwp as [|???? Hgo]; subst; [by destruct (atomic_of_val v)|].
@@ -165,13 +165,13 @@ Lemma wp_bind `{CtxLanguage Λ C} E K e Q :
   wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
 Proof.
   intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?.
-  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using is_ctx_value.
+  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using fill_not_val.
   intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split.
   { destruct Hsafe as (e2&σ2&ef&?).
-    by exists (fill K e2), σ2, ef; apply is_ctx_step_preserved. }
+    by exists (fill K e2), σ2, ef; apply fill_step. }
   intros e2 σ2 ef ?.
-  destruct (is_ctx_step K e σ1 e2 σ2 ef) as (e2'&->&?); auto.
+  destruct (fill_step_inv K e σ1 e2 σ2 ef) as (e2'&->&?); auto.
   destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
   exists r2, r2'; split_ands; try eapply IH; eauto.
 Qed.