Move out some PureExec assumptions into typeclasses

theories/heap_lang/lang.v

-From iris.program_logic Require Export ectx_language ectxi_language.
+From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
 From stdpp Require Export strings.
 From stdpp Require Import gmap.
@@ -109,6 +109,14 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 
+Class AsRec (e : expr) (f x : binder) (erec : expr) :=
+  as_rec : e = Rec f x erec.
+
+Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
+Instance AsRec_rec_locked_val v f x e :
+  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
+Proof. by unlock. Qed.
+
 (** The state: heaps of vals. *)
 Definition state := gmap loc val.
 
@@ -411,6 +419,9 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
 Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
+Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
+Proof. intros Hev; rewrite -(of_to_val e v Hev); apply is_closed_of_val. Qed.
+
 Lemma is_closed_subst X e x es :
   is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
 Proof.

theories/heap_lang/lifting.v

@@ -83,25 +83,24 @@ 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_pureexec :=
+  repeat lazymatch goal with
+  | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
+  | H: AsRec _ _ _ _ |- _ => rewrite H; clear H
+  end;
   apply hoist_pred_pureexec; intros; destruct_and?;
   apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
 
-Global Instance pure_rec f x erec e1 e2 v2 :
-  PureExec (to_val e2 = Some v2 ∧ e1 = Rec f x erec ∧ Closed (f :b: x :b: []) erec)
-           (App e1 e2)
-           (subst' x e2 (subst' f e1 erec)).
+Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
+    `{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
+  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
 Proof. solve_pureexec. Qed.
 
-Global Instance pure_unop op e v v' :
-  PureExec (to_val e = Some v ∧ un_op_eval op v = Some v')
-           (UnOp op e)
-           (of_val v').
+Global Instance pure_unop op e v v' `{!IntoVal e v} :
+  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
 Proof. solve_pureexec. Qed.
 
-Global Instance pure_binop op e1 e2 v1 v2 v' :
-  PureExec (to_val e1 = Some v1 ∧ to_val e2 = Some v2 ∧ bin_op_eval op v1 v2 = Some v')
-           (BinOp op e1 e2)
-           (of_val v').
+Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
+  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
 Proof. solve_pureexec. Qed.
 
 Global Instance pure_if_true e1 e2 :
@@ -112,24 +111,20 @@ Global Instance pure_if_false e1 e2 :
   PureExec True (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pureexec. Qed.
 
-Global Instance pure_fst e1 e2 v1 v2 :
-  PureExec (to_val e1 = Some v1 ∧ to_val e2 = Some v2)
-           (Fst (Pair e1 e2))
-           e1.
+Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+  PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pureexec. Qed.
 
-Global Instance pure_snd e1 e2 v1 v2 :
-  PureExec (to_val e1 = Some v1 ∧ to_val e2 = Some v2)
-           (Snd (Pair e1 e2))
-           e2.
+Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+  PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pureexec. Qed.
 
-Global Instance pure_case_inl e0 v e1 e2  :
-  PureExec (to_val e0 = Some v) (Case (InjL e0) e1 e2) (App e1 e0).
+Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
+  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
 Proof. solve_pureexec. Qed.
 
-Global Instance pure_case_inr e0 v e1 e2  :
-  PureExec (to_val e0 = Some v) (Case (InjR e0) e1 e2) (App e2 e0).
+Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
+  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
 Proof. solve_pureexec. Qed.
 
 (** Heap *)
@@ -209,5 +204,4 @@ Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
   is_Some (to_val e0) → Closed (x2 :b: []) e2 →
   ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
 Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
-
 End lifting.

theories/heap_lang/proofmode.v

@@ -24,20 +24,9 @@ Ltac wp_done :=
 
 Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl.
 
-Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
-Proof. by unlock. Qed.
-
-(* Applied to goals that are equalities of expressions. Will try to unlock the
-   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
-Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
-
 (* Solves side-conditions generated specifically by wp_pure *)
 Ltac wp_pure_done :=
-  split_and?;
-  lazymatch goal with
-  | |- of_val _ = _ => solve_of_val_unlock
-  | _ => wp_done
-  end.
+  split_and?; wp_done.
 
 Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →

theories/program_logic/language.v

@@ -105,4 +105,8 @@ Section language.
     (P → PureExec True e1 e2) →
     PureExec P e1 e2.
   Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
+
+  (* This is a family of frequent assumptions for PureExec *)
+  Class IntoVal (e : expr Λ) (v : val Λ) :=
+    into_val : to_val e = Some v.
 End language.