change AsVal to be easier to use (like IntoVal)

CHANGELOG.md

@@ -32,7 +32,8 @@ Changes in Coq:
   - `cmra_opM_assoc_L` → `cmra_op_opM_assoc_L`
   - `cmra_opM_assoc'` → `cmra_opM_opM_assoc`
 * `namespaces` has been moved to std++.
-* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`.
+* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
+  changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

theories/heap_lang/lifting.v

@@ -51,8 +51,8 @@ Local Hint Resolve to_of_val.
 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 :=
-  unfold IntoVal, AsVal in *; subst;
-  repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
+  unfold IntoVal in *;
+  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
   apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 
 Class AsRec (e : expr) (f x : binder) (erec : expr) :=
@@ -189,7 +189,7 @@ Lemma wp_cas_fail s E l q v' e1 v1 e2 :
   {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
-  iIntros (<- [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
+  iIntros (<- [v2 <-] ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
@@ -200,7 +200,7 @@ Lemma twp_cas_fail s E l q v' e1 v1 e2 :
   [[{ l ↦{q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
   [[{ RET LitV (LitBool false); l ↦{q} v' }]].
 Proof.
-  iIntros (<- [v2 <-%of_to_val] ? Φ) "Hl HΦ".
+  iIntros (<- [v2 <-] ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.

theories/heap_lang/tactics.v

@@ -138,18 +138,16 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 Lemma to_val_Some e v :
-  to_val e = Some v → heap_lang.to_val (to_expr e) = Some v.
+  to_val e = Some v → of_val v = W.to_expr e.
 Proof.
-  revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
-  - do 2 f_equal. apply proof_irrel.
-  - exfalso. unfold Closed in *; eauto using is_closed_correct.
+  revert v. induction e; intros; simplify_option_eq; try f_equal; auto using of_to_val.
 Qed.
 Lemma to_val_is_Some e :
-  is_Some (to_val e) → is_Some (heap_lang.to_val (to_expr e)).
+  is_Some (to_val e) → ∃ v, of_val v = to_expr e.
 Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
-Lemma expr_of_val e v :
-  to_val e = Some v → of_val v = W.to_expr e.
-Proof. intros ?. apply of_to_val, to_val_Some. done. Qed.
+Lemma to_val_is_Some' e :
+  is_Some (to_val e) → is_Some (heap_lang.to_val (to_expr e)).
+Proof. intros [v ?]%to_val_is_Some. exists v. rewrite -to_of_val. by f_equal. Qed.
 
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
@@ -205,7 +203,7 @@ Proof.
     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
   - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
     destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
-      naive_solver eauto using to_val_is_Some.
+      naive_solver eauto using to_val_is_Some'.
 Qed.
 End W.
 
@@ -221,14 +219,14 @@ Ltac solve_into_val :=
   match goal with
   | |- IntoVal ?e ?v =>
      let e' := W.of_expr e in change (of_val v = W.to_expr e');
-     apply W.expr_of_val; simpl; unfold W.to_expr; reflexivity
+     apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
   end.
 Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
 
 Ltac solve_as_val :=
   match goal with
   | |- AsVal ?e =>
-     let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
+     let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
 Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.

theories/program_logic/language.v

@@ -162,12 +162,12 @@ Section language.
   Class IntoVal (e : expr Λ) (v : val Λ) :=
     into_val : of_val v = e.
 
-  Class AsVal (e : expr Λ) := as_val : is_Some (to_val e).
+  Class AsVal (e : expr Λ) := as_val : ∃ v, of_val v = e.
   (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
   efficiently since no witness has to be computed. *)
   Global Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
   Proof.
     apply TCForall_Forall, Forall_fmap, Forall_true=> v.
-    rewrite /AsVal /= to_of_val; eauto.
+    rewrite /AsVal /=; eauto.
   Qed.
 End language.