Merge branch 'ralf/into_val' into 'gen_proofmode'

change IntoVal so that it is easier to use in specs

See merge request FP/iris-coq!159

CHANGELOG.md

@@ -32,6 +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`, and
+  changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

theories/heap_lang/lib/atomic_heap.v

@@ -82,7 +82,7 @@ Section proof.
               (λ v (_:()), l ↦ w)%I
               (λ _ _, #()%V).
   Proof.
-    iIntros (<-%of_to_val Q Φ) "? AU". wp_let. wp_proj. wp_proj.
+    iIntros (<- Q Φ) "? AU". wp_let. wp_proj. wp_proj.
     iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
     wp_store. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
@@ -95,7 +95,7 @@ Section proof.
               (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
               (λ v _, #(if decide (v = w1) then true else false)%V).
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val Q Φ) "? AU". wp_let. repeat wp_proj.
+    iIntros (<- <- Q Φ) "? AU". wp_let. repeat wp_proj.
     iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
     destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".

theories/heap_lang/lib/par.v

@@ -21,13 +21,13 @@ Context `{!heapG Σ, !spawnG Σ}.
    brought together.  That is strictly stronger than first stripping a later
    and then merging them, as demonstrated by [tests/joining_existentials.v].
    This is why these are not Texan triples. *)
-Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ)
-    `{Hef : !IntoVal e (f1,f2)} :
+Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) :
+  IntoVal e (f1,f2) →
   WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
   (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP par e {{ Φ }}.
 Proof.
-  apply of_to_val in Hef as <-. iIntros "Hf1 Hf2 HΦ".
+  iIntros (<-) "Hf1 Hf2 HΦ".
   rewrite /par /=. wp_let. wp_proj.
   wp_apply (spawn_spec parN with "Hf1").
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).

theories/heap_lang/lib/spawn.v

@@ -44,10 +44,11 @@ Global Instance join_handle_ne n l :
 Proof. solve_proper. Qed.
 
 (** The main proofs. *)
-Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) `{Hef : !IntoVal e f} :
+Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
+  IntoVal e f →
   {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}.
 Proof.
-  apply of_to_val in Hef as <-. iIntros (Φ) "Hf HΦ". rewrite /spawn /=.
+  iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".

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) :=
@@ -125,7 +125,7 @@ Lemma wp_alloc s E e v :
   IntoVal e v →
   {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
@@ -135,7 +135,7 @@ Lemma twp_alloc s E e v :
   IntoVal e v →
   [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
-  iIntros (<-%of_to_val Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
   iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
@@ -165,7 +165,7 @@ Lemma wp_store s E l v' e v :
   IntoVal e v →
   {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) ">Hl HΦ".
+  iIntros (<- Φ) ">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.
@@ -176,7 +176,7 @@ Lemma twp_store s E l v' e v :
   IntoVal e v →
   [[{ l ↦ v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l ↦ v }]].
 Proof.
-  iIntros (<-%of_to_val Φ) "Hl HΦ".
+  iIntros (<- Φ) "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.
@@ -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 (<-%of_to_val [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 (<-%of_to_val [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.
@@ -212,7 +212,7 @@ Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
-  iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
+  iIntros (<- <- Φ) ">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.
@@ -224,7 +224,7 @@ Lemma twp_cas_suc s E l e1 v1 e2 v2 :
   [[{ l ↦ v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
   [[{ RET LitV (LitBool true); l ↦ v2 }]].
 Proof.
-  iIntros (<-%of_to_val <-%of_to_val Φ) "Hl HΦ".
+  iIntros (<- <- Φ) "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.
@@ -237,7 +237,7 @@ Lemma wp_faa s E l i1 e2 i2 :
   {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
   {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
 Proof.
-  iIntros (<-%of_to_val Φ) ">Hl HΦ".
+  iIntros (<- Φ) ">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.
@@ -249,7 +249,7 @@ Lemma twp_faa s E l i1 e2 i2 :
   [[{ l ↦ LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
   [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
 Proof.
-  iIntros (<-%of_to_val Φ) "Hl HΦ".
+  iIntros (<- Φ) "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,15 +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 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
@@ -202,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.
 
@@ -217,7 +218,7 @@ Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 Ltac solve_into_val :=
   match goal with
   | |- IntoVal ?e ?v =>
-     let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
+     let e' := W.of_expr e in change (of_val v = W.to_expr e');
      apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
   end.
 Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
@@ -225,7 +226,7 @@ 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

@@ -160,14 +160,14 @@ Section language.
 
   (* This is a family of frequent assumptions for PureExec *)
   Class IntoVal (e : expr Λ) (v : val Λ) :=
-    into_val : to_val e = Some v.
+    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.

theories/program_logic/lifting.v

@@ -94,7 +94,7 @@ Proof.
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
-  by iApply wp_value.
+  iApply wp_value; last done. by apply of_to_val.
 Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :

theories/program_logic/ownp.v

@@ -147,7 +147,7 @@ Section lifting.
     iNext; iIntros (e2 σ2 efs) "% Hσ".
     iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.
-    by iMod "Hclose"; iApply wp_value; auto using to_of_val.
+    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
   Qed.
 
   Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :

theories/program_logic/total_lifting.v

@@ -54,7 +54,7 @@ Proof.
   iIntros "!>" (e2 σ2 efs) "%". iMod "Hclose" as "_".
   iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
-  by iApply twp_value.
+  iApply twp_value; last done. by apply of_to_val.
 Qed.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :

theories/program_logic/total_weakestpre.v

@@ -213,14 +213,14 @@ Global Instance twp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (twp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
 
-Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }].
-Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value'. Qed.
+Lemma twp_value s E Φ e v : IntoVal e v → Φ v -∗ WP e @ s; E [{ Φ }].
+Proof. intros <-. by apply twp_value'. Qed.
 Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }].
 Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
-Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
-Proof. intros. rewrite -twp_fupd -twp_value //. Qed.
-Lemma twp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E [{ Φ }] ={E}=∗ Φ v.
-Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value_inv'. Qed.
+Lemma twp_value_fupd s E Φ e v : IntoVal e v → (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
+Proof. intros ?. rewrite -twp_fupd -twp_value //. Qed.
+Lemma twp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E [{ Φ }] ={E}=∗ Φ v.
+Proof. intros <-. by apply twp_value_inv'. Qed.
 
 Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }].
 Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.

theories/program_logic/weakestpre.v

@@ -175,15 +175,15 @@ Global Instance wp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
-Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; E {{ Φ }}.
-Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
+Lemma wp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }}.
+Proof. intros <-. by apply wp_value'. Qed.
 Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ s; E {{ Φ }}.
 Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
 Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
   (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
-Lemma wp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E {{ Φ }} ={E}=∗ Φ v.
-Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value_inv'. Qed.
+Lemma wp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E {{ Φ }} ={E}=∗ Φ v.
+Proof. intros <-. by apply wp_value_inv'. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.