Commit 9331a371 authored by Robbert Krebbers's avatar Robbert Krebbers

Introduce notion of reducible, as in the appendix.

parent ae972c48
......@@ -15,7 +15,7 @@ Import uPred.
Lemma ht_lift_step E1 E2
(φ : iexpr Σ istate Σ option (iexpr Σ) Prop) P P' Q1 Q2 R e1 σ1 :
E1 E2 to_val e1 = None
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef)
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
(P >{E2,E1}> (ownP σ1 P') e2 σ2 ef,
( φ e2 σ2 ef ownP σ2 P') >{E1,E2}> (Q1 e2 σ2 ef Q2 e2 σ2 ef)
......@@ -45,7 +45,7 @@ Qed.
Lemma ht_lift_atomic E
(φ : iexpr Σ istate Σ option (iexpr Σ) Prop) P e1 σ1 :
atomic e1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef)
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
( e2 σ2 ef, {{ φ e2 σ2 ef P }} ef ?@ coPset_all {{ λ _, True }})
{{ ownP σ1 P }} e1 @ E {{ λ v, σ2 ef, ownP σ2 φ (of_val v) σ2 ef }}.
......@@ -71,7 +71,7 @@ Proof.
Qed.
Lemma ht_lift_pure_step E (φ : iexpr Σ option (iexpr Σ) Prop) P P' Q e1 :
to_val e1 = None
( σ1, e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef)
( σ1, reducible e1 σ1)
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
( e2 ef,
{{ φ e2 ef P }} e2 @ E {{ Q }}
......@@ -97,7 +97,7 @@ Qed.
Lemma ht_lift_pure_determistic_step E
(φ : iexpr Σ option (iexpr Σ) Prop) P P' Q e1 e2 ef :
to_val e1 = None
( σ1, prim_step e1 σ1 e2 σ1 ef)
( σ1, reducible e1 σ1)
( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' σ1 = σ2 e2 = e2' ef = ef')
({{ P }} e2 @ E {{ Q }} {{ P' }} ef ?@ coPset_all {{ λ _, True }})
{{ (P P') }} e1 @ E {{ Q }}.
......
......@@ -18,6 +18,11 @@ Class Language (E V St : Type) := {
Section language.
Context `{Language E V St}.
Definition reducible (e : E) (σ : St) :=
e' σ' ef, prim_step e σ e' σ' ef.
Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
Lemma atomic_of_val v : ¬atomic (of_val v).
Proof.
by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
......
......@@ -16,7 +16,7 @@ Transparent uPred_holds.
Lemma wp_lift_step E1 E2
(φ : iexpr Σ istate Σ option (iexpr Σ) Prop) Q e1 σ1 :
E1 E2 to_val e1 = None
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef)
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
pvs E2 E1 (ownP σ1 e2 σ2 ef, ( φ e2 σ2 ef ownP σ2) -
pvs E1 E2 (wp E2 e2 Q default True ef (flip (wp coPset_all) (λ _, True))))
......@@ -37,7 +37,7 @@ Proof.
Qed.
Lemma wp_lift_pure_step E (φ : iexpr Σ option (iexpr Σ) Prop) Q e1 :
to_val e1 = None
( σ1, e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef)
( σ1, reducible e1 σ1)
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
( e2 ef, φ e2 ef
wp E e2 Q default True ef (flip (wp coPset_all) (λ _, True)))
......
......@@ -9,7 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
Record wp_go {Σ} (E : coPset) (Q Qfork : iexpr Σ nat res' Σ Prop)
(k : nat) (rf : res' Σ) (e1 : iexpr Σ) (σ1 : istate Σ) := {
wf_safe : e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef;
wf_safe : reducible e1 σ1;
wp_step e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef
r2 r2',
......
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