Commit 3c5086b2 by Jacques-Henri Jourdan

### Get rid of useless IntoVal uses.

parent 6356ef03
 ... ... @@ -44,11 +44,10 @@ Global Instance join_handle_ne n l : Proof. solve_proper. Qed. (** The main proofs. *) Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) : IntoVal e f → {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}. Lemma spawn_spec (Ψ : val → iProp Σ) (f : val) : {{{ WP f #() {{ Ψ }} }}} spawn f {{{ l, RET #l; join_handle l Ψ }}}. Proof. iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=. wp_lam. iIntros (Φ) "Hf HΦ". rewrite /spawn /=. wp_lam. wp_alloc l as "Hl". iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". ... ...
 ... ... @@ -317,12 +317,12 @@ Proof. - iApply "HΦ". done. Qed. Lemma wp_resolve_proph e1 e2 p v w: IntoVal e1 (LitV (LitProphecy p)) → IntoVal e2 w → {{{ proph p v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}. Lemma wp_resolve_proph p v w: {{{ proph p v }}} ResolveProph (Val \$ LitV \$ LitProphecy p) (Val w) {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}. Proof. iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit; first by eauto. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!