diff --git a/CHANGELOG.md b/CHANGELOG.md
index bcbf9837333308d2cf4c3862da06fe91f7aab3d4..75866d8b84af4a60a0bf93022d96163337ec1e70 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -184,6 +184,10 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   already at the top level).
 * The `wp_` tactics now preserve the possibility of doing a fancy update when
   the expression reduces to a value.
+* Move `IntoVal`, `AsVal`, `Atomic`, `AsRecV`, and `PureExec` instances to their
+  own file [heap_lang.class_instances](iris_heap_lang/class_instances.v).
+* Move `inv_head_step` tactic and `head_step` auto hints (now part of new hint
+  database `head_step`) to [heap_lang.tactics](iris_heap_lang/tactics.v).
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/_CoqProject b/_CoqProject
index 534926fad68657b80605451d958b577091e1cdb5..30b03d9dfcaf8c481dae9fcaa91cf34135045165 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -141,6 +141,7 @@ iris/proofmode/modality_instances.v
 
 iris_heap_lang/locations.v
 iris_heap_lang/lang.v
+iris_heap_lang/class_instances.v
 iris_heap_lang/metatheory.v
 iris_heap_lang/tactics.v
 iris_heap_lang/primitive_laws.v
diff --git a/iris_heap_lang/class_instances.v b/iris_heap_lang/class_instances.v
new file mode 100644
index 0000000000000000000000000000000000000000..6887a0acb70a2538dead50b6abe91c8af2f27c91
--- /dev/null
+++ b/iris_heap_lang/class_instances.v
@@ -0,0 +1,167 @@
+From iris.program_logic Require Export language.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import tactics notation.
+From iris.prelude Require Import options.
+
+Instance into_val_val v : IntoVal (Val v) v.
+Proof. done. Qed.
+Instance as_val_val v : AsVal (Val v).
+Proof. by eexists. Qed.
+
+(** * Instances of the [Atomic] class *)
+Section atomic.
+  Local Ltac solve_atomic :=
+    apply strongly_atomic_atomic, ectx_language_atomic;
+      [inversion 1; naive_solver
+      |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
+
+  Global Instance rec_atomic s f x e : Atomic s (Rec f x e).
+  Proof. solve_atomic. Qed.
+  Global Instance pair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
+  Proof. solve_atomic. Qed.
+  Global Instance injl_atomic s v : Atomic s (InjL (Val v)).
+  Proof. solve_atomic. Qed.
+  Global Instance injr_atomic s v : Atomic s (InjR (Val v)).
+  Proof. solve_atomic. Qed.
+  (** The instance below is a more general version of [Skip] *)
+  Global Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
+  Proof. destruct f, x; solve_atomic. Qed.
+  Global Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
+  Proof. solve_atomic. Qed.
+  Global Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
+  Proof. solve_atomic. Qed.
+  Global Instance if_true_atomic s v1 e2 :
+    Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
+  Proof. solve_atomic. Qed.
+  Global Instance if_false_atomic s e1 v2 :
+    Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
+  Proof. solve_atomic. Qed.
+  Global Instance fst_atomic s v : Atomic s (Fst (Val v)).
+  Proof. solve_atomic. Qed.
+  Global Instance snd_atomic s v : Atomic s (Snd (Val v)).
+  Proof. solve_atomic. Qed.
+
+  Global Instance fork_atomic s e : Atomic s (Fork e).
+  Proof. solve_atomic. Qed.
+
+  Global Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
+  Proof. solve_atomic. Qed.
+  Global Instance free_atomic s v : Atomic s (Free (Val v)).
+  Proof. solve_atomic. Qed.
+  Global Instance load_atomic s v : Atomic s (Load (Val v)).
+  Proof. solve_atomic. Qed.
+  Global Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
+  Proof. solve_atomic. Qed.
+  Global Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
+  Proof. solve_atomic. Qed.
+  Global Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
+  Proof. solve_atomic. Qed.
+
+  Global Instance new_proph_atomic s : Atomic s NewProph.
+  Proof. solve_atomic. Qed.
+  Global Instance resolve_atomic s e v1 v2 :
+    Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
+  Proof.
+    rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
+    simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
+    - subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
+    - rewrite fill_app. rewrite fill_app in Hfill.
+      assert (∀ v, Val v = fill Ks e1' → False) as fill_absurd.
+      { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
+        apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
+      destruct K; (inversion Hfill; clear Hfill; subst; try
+        match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
+      refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
+      + destruct s; intro Hs; simpl in *.
+        * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
+        * apply irreducible_resolve. by rewrite fill_app in Hs.
+      + econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
+  Qed.
+End atomic.
+
+(** * Instances of the [PureExec] class *)
+(** The behavior of the various [wp_] tactics with regard to lambda differs in
+the following way:
+
+- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
+- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.
+
+To realize this behavior, we define the class [AsRecV v f x erec], which takes a
+value [v] as its input, and turns it into a [RecV f x erec] via the instance
+[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
+[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
+not if [v] contains a lambda/rec that is hidden behind a definition.
+
+To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
+behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
+Class AsRecV (v : val) (f x : binder) (erec : expr) :=
+  as_recv : v = RecV f x erec.
+Global Hint Mode AsRecV ! - - - : typeclass_instances.
+Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
+Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
+  apply AsRecV_recv : typeclass_instances.
+
+Section pure_exec.
+  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;
+      constructor; [solve_exec_safe | solve_exec_puredet].
+
+  Global Instance pure_recc f x (erec : expr) :
+    PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
+  Proof. solve_pure_exec. Qed.
+  Global Instance pure_pairc (v1 v2 : val) :
+    PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
+  Proof. solve_pure_exec. Qed.
+  Global Instance pure_injlc (v : val) :
+    PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
+  Proof. solve_pure_exec. Qed.
+  Global Instance pure_injrc (v : val) :
+    PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
+    PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
+  Proof. unfold AsRecV in *. solve_pure_exec. Qed.
+
+  Global Instance pure_unop op v v' :
+    PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_binop op v1 v2 v' :
+    PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
+  Proof. solve_pure_exec. Qed.
+  (* Higher-priority instance for [EqOp]. *)
+  Global Instance pure_eqop v1 v2 :
+    PureExec (vals_compare_safe v1 v2) 1
+      (BinOp EqOp (Val v1) (Val v2))
+      (Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
+  Proof.
+    intros Hcompare.
+    cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
+    { intros. revert Hcompare. solve_pure_exec. }
+    rewrite /bin_op_eval /= decide_True //.
+  Qed.
+
+  Global Instance pure_if_true e1 e2 :
+    PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
+  Proof. solve_pure_exec. Qed.
+  Global Instance pure_if_false e1 e2 :
+    PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_fst v1 v2 :
+    PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
+  Proof. solve_pure_exec. Qed.
+  Global Instance pure_snd v1 v2 :
+    PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_case_inl v e1 e2 :
+    PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
+  Proof. solve_pure_exec. Qed.
+  Global Instance pure_case_inr v e1 e2 :
+    PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
+  Proof. solve_pure_exec. Qed.
+End pure_exec.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 194bca70de9cee08bfe0df482fedeee6a1154537..748262648f030c6e8039788db3b7bac1738ac7a5 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -1,14 +1,12 @@
 (** This file proves the basic laws of the HeapLang program logic by applying
 the Iris lifting lemmas. *)
 
-From stdpp Require Import fin_maps.
-From iris.algebra Require Import auth gmap.
 From iris.proofmode Require Import tactics.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
-From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Export class_instances.
 From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
 
@@ -59,187 +57,6 @@ Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
 Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
 
-(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
-[head_step]. The tactic will discharge head-reductions starting from values, and
-simplifies hypothesis related to conversions from and to values, and finite map
-operations. This tactic is slightly ad-hoc and tuned for proving our lifting
-lemmas. *)
-Ltac inv_head_step :=
-  repeat match goal with
-  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
-  | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | 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.
-
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
-Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
-
-(* [simpl apply] is too stupid, so we need extern hints here. *)
-Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
-Local Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : core.
-Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
-Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
-Local Hint Resolve to_of_val : core.
-
-Instance into_val_val v : IntoVal (Val v) v.
-Proof. done. Qed.
-Instance as_val_val v : AsVal (Val v).
-Proof. by eexists. Qed.
-
-Local Ltac solve_atomic :=
-  apply strongly_atomic_atomic, ectx_language_atomic;
-    [inversion 1; naive_solver
-    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
-
-Instance rec_atomic s f x e : Atomic s (Rec f x e).
-Proof. solve_atomic. Qed.
-Instance pair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
-Proof. solve_atomic. Qed.
-Instance injl_atomic s v : Atomic s (InjL (Val v)).
-Proof. solve_atomic. Qed.
-Instance injr_atomic s v : Atomic s (InjR (Val v)).
-Proof. solve_atomic. Qed.
-(** The instance below is a more general version of [Skip] *)
-Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
-Proof. destruct f, x; solve_atomic. Qed.
-Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
-Proof. solve_atomic. Qed.
-Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
-Proof. solve_atomic. Qed.
-Instance if_true_atomic s v1 e2 : Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
-Proof. solve_atomic. Qed.
-Instance if_false_atomic s e1 v2 : Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
-Proof. solve_atomic. Qed.
-Instance fst_atomic s v : Atomic s (Fst (Val v)).
-Proof. solve_atomic. Qed.
-Instance snd_atomic s v : Atomic s (Snd (Val v)).
-Proof. solve_atomic. Qed.
-
-Instance fork_atomic s e : Atomic s (Fork e).
-Proof. solve_atomic. Qed.
-
-Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
-Proof. solve_atomic. Qed.
-Instance free_atomic s v : Atomic s (Free (Val v)).
-Proof. solve_atomic. Qed.
-Instance load_atomic s v : Atomic s (Load (Val v)).
-Proof. solve_atomic. Qed.
-Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
-Proof. solve_atomic. Qed.
-Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
-Proof. solve_atomic. Qed.
-Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
-Proof. solve_atomic. Qed.
-
-Instance new_proph_atomic s : Atomic s NewProph.
-Proof. solve_atomic. Qed.
-Instance resolve_atomic s e v1 v2 :
-  Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
-Proof.
-  rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
-  simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
-  - subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
-  - rewrite fill_app. rewrite fill_app in Hfill.
-    assert (∀ v, Val v = fill Ks e1' → False) as fill_absurd.
-    { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
-      apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
-    destruct K; (inversion Hfill; clear Hfill; subst; try
-      match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
-    refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
-    + destruct s; intro Hs; simpl in *.
-      * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
-      * apply irreducible_resolve. by rewrite fill_app in Hs.
-    + econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
-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;
-    constructor; [solve_exec_safe | solve_exec_puredet].
-
-(** The behavior of the various [wp_] tactics with regard to lambda differs in
-the following way:
-
-- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
-- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.
-
-To realize this behavior, we define the class [AsRecV v f x erec], which takes a
-value [v] as its input, and turns it into a [RecV f x erec] via the instance
-[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
-[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
-not if [v] contains a lambda/rec that is hidden behind a definition.
-
-To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
-behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
-Class AsRecV (v : val) (f x : binder) (erec : expr) :=
-  as_recv : v = RecV f x erec.
-Global Hint Mode AsRecV ! - - - : typeclass_instances.
-Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
-Global Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
-  apply AsRecV_recv : typeclass_instances.
-
-Instance pure_recc f x (erec : expr) :
-  PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
-Proof. solve_pure_exec. Qed.
-Instance pure_pairc (v1 v2 : val) :
-  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
-Proof. solve_pure_exec. Qed.
-Instance pure_injlc (v : val) :
-  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
-Proof. solve_pure_exec. Qed.
-Instance pure_injrc (v : val) :
-  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
-  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
-Proof. unfold AsRecV in *. solve_pure_exec. Qed.
-
-Instance pure_unop op v v' :
-  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
-Proof. solve_pure_exec. Qed.
-
-Instance pure_binop op v1 v2 v' :
-  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
-Proof. solve_pure_exec. Qed.
-(* Higher-priority instance for [EqOp]. *)
-Instance pure_eqop v1 v2 :
-  PureExec (vals_compare_safe v1 v2) 1
-    (BinOp EqOp (Val v1) (Val v2))
-    (Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
-Proof.
-  intros Hcompare.
-  cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
-  { intros. revert Hcompare. solve_pure_exec. }
-  rewrite /bin_op_eval /= decide_True //.
-Qed.
-
-Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
-Proof. solve_pure_exec. Qed.
-
-Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
-Proof. solve_pure_exec. Qed.
-
-Instance pure_fst v1 v2 :
-  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_snd v1 v2 :
-  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_case_inl v e1 e2 :
-  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
-Proof. solve_pure_exec. Qed.
-
-Instance pure_case_inr v e1 e2 :
-  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
-Proof. solve_pure_exec. Qed.
-
 Section lifting.
 Context `{!heapG Σ}.
 Implicit Types P Q : iProp Σ.
@@ -268,15 +85,15 @@ Lemma wp_fork s E e Φ :
   ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
   iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
-  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
-  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
+  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto with head_step.
+  iIntros "!>" (v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
 Lemma twp_fork s E e Φ :
   WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
   iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
-  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
+  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
@@ -405,7 +222,7 @@ Lemma twp_allocN_seq s E v n :
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
+  iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (gen_heap_alloc_big _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
@@ -423,7 +240,7 @@ Lemma wp_allocN_seq s E v n :
       (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
-  iApply twp_allocN_seq; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
+  iApply twp_allocN_seq; [by auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_alloc s E v :
@@ -436,7 +253,7 @@ Lemma wp_alloc s E v :
   {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
-  iApply twp_alloc; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
+  iApply twp_alloc; [by auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_free s E l v :
@@ -444,25 +261,27 @@ Lemma twp_free s E l v :
   [[{ RET LitV LitUnit; True }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 Lemma wp_free s E l v :
   {{{ ▷ l ↦ v }}} Free (Val $ LitV (LitLoc l)) @ s; E
   {{{ RET LitV LitUnit; True }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
-  iApply (twp_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  iApply (twp_free with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_load s E l dq v :
   [[{ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{dq} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 Lemma wp_load s E l dq v :
@@ -477,17 +296,18 @@ Lemma twp_store s E l v' v :
   [[{ RET LitV LitUnit; l ↦ v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 Lemma wp_store s E l v' v :
   {{{ ▷ l ↦ v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
   {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
-  iApply (twp_store with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  iApply (twp_store with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
@@ -496,10 +316,11 @@ Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
   [[{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   rewrite bool_decide_false //.
-  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
+  iModIntro; iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
   v' ≠ v1 → vals_compare_safe v' v1 →
@@ -507,7 +328,7 @@ Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
   {{{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }}}.
 Proof.
   iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
-  iApply (twp_cmpxchg_fail with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  iApply (twp_cmpxchg_fail with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_cmpxchg_suc s E l v1 v2 v' :
@@ -516,11 +337,12 @@ Lemma twp_cmpxchg_suc s E l v1 v2 v' :
   [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   rewrite bool_decide_true //.
-  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
+  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 Lemma wp_cmpxchg_suc s E l v1 v2 v' :
   v' = v1 → vals_compare_safe v' v1 →
@@ -528,7 +350,7 @@ Lemma wp_cmpxchg_suc s E l v1 v2 v' :
   {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}.
 Proof.
   iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
-  iApply (twp_cmpxchg_suc with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  iApply (twp_cmpxchg_suc with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_faa s E l i1 i2 :
@@ -536,17 +358,18 @@ Lemma twp_faa s E l i1 i2 :
   [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ e2 σ2 efs Hstep); inv_head_step.
+  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. do 2 (iSplit; first done). iFrame. by iApply "HΦ".
 Qed.
 Lemma wp_faa s E l i1 i2 :
   {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
   {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
-  iApply (twp_faa with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
+  iApply (twp_faa with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma wp_new_proph s E :
@@ -555,10 +378,10 @@ Lemma wp_new_proph s E :
   {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
 Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
-  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
+  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto with head_step.
+  iIntros "!>" (v2 σ2 efs Hstep). inv_head_step.
   iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
-  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+  iModIntro; iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 (* In the following, strong atomicity is required due to the fact that [e] must
@@ -584,7 +407,7 @@ Lemma step_resolve e vp vt σ1 κ e2 σ2 efs :
 Proof.
   intros A [Ks e1' e2' Hfill -> step]. simpl in *.
   induction Ks as [|K Ks _] using rev_ind.
-  + simpl in *. subst. inversion step. by constructor.
+  + simpl in *. subst. inv_head_step. by constructor.
   + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
     - assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
         first by rewrite fill_app.
@@ -595,9 +418,9 @@ Proof.
       { apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
       destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
     - assert (to_val (fill Ks e1') = Some vp); first by rewrite -H1 //.
-      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
+      apply to_val_fill_some in H as [-> ->]. inv_head_step.
     - assert (to_val (fill Ks e1') = Some vt); first by rewrite -H2 //.
-      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
+      apply to_val_fill_some in H as [-> ->]. inv_head_step.
 Qed.
 
 Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
@@ -614,12 +437,12 @@ Proof.
   - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
     { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
     iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
-    inversion step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
-  - rewrite -app_assoc.
+    inv_head_step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
+  - rewrite -assoc.
     iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
     { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
     iIntros (e2 σ2 efs step). apply step_resolve in step; last done.
-    inversion step; simplify_list_eq.
+    inv_head_step; simplify_list_eq.
     iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe".
     { by eexists [] _ _. }
     iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
diff --git a/iris_heap_lang/tactics.v b/iris_heap_lang/tactics.v
index f29521e8bdcc89984aa381418a37298067e148f4..87484570cddcaebc27578a5cae06250708813981 100644
--- a/iris_heap_lang/tactics.v
+++ b/iris_heap_lang/tactics.v
@@ -1,3 +1,4 @@
+From stdpp Require Import fin_maps.
 From iris.heap_lang Require Export lang.
 From iris.prelude Require Import options.
 Import heap_lang.
@@ -52,3 +53,28 @@ Ltac reshape_expr e tac :=
     end
   in
   go (@nil ectx_item) (@nil (val * val)) e.
+
+(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
+[head_step]. The tactic will discharge head-reductions starting from values, and
+simplifies hypothesis related to conversions from and to values, and finite map
+operations. This tactic is slightly ad-hoc and tuned for proving our lifting
+lemmas. *)
+Ltac inv_head_step :=
+  repeat match goal with
+  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : head_step ?e _ _ _ _ _ |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
+     and should thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+
+Create HintDb head_step.
+Global Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : head_step.
+Global Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : head_step.
+
+(* [simpl apply] is too stupid, so we need extern hints here. *)
+Global Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : head_step.
+Global Hint Extern 0 (head_step (CmpXchg _ _ _) _ _ _ _ _) => eapply CmpXchgS : head_step.
+Global Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : head_step.
+Global Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : head_step.