Commit 0e4b3598 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 98f58353 c399acaf
......@@ -36,10 +36,8 @@ Proof.
iIntros "[HP HΦ]". iFrame "HP". iNext.
iIntros {v2 σ2 ef} "[% HP]".
(* FIXME: I should not have to refer to "H0". *)
destruct H0 as (l & -> & ? & -> & ?).
rewrite -(of_to_val (Loc l) (LocV l)) // in H0.
apply of_val_inj in H0 as ->.
simpl. iSplitL; last done. iApply "HΦ" {l}. iSplit; done.
destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
iSplit; last done. iApply "HΦ"; by iSplit.
Qed.
Lemma wp_load_pst E σ l v Φ :
......
......@@ -46,6 +46,8 @@ Section language.
prim_step e1 σ1 e2 σ2 ef
step ρ1 ρ2.
Lemma of_to_val_flip v e : of_val v = e to_val e = Some v.
Proof. intros <-. by rewrite to_of_val. Qed.
Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
Lemma atomic_of_val v : ¬atomic (of_val v).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment