Commit e1df5b4b authored by Dan Frumin's avatar Dan Frumin

Show that early/late refinement (refinement in the other direction).

parent 69f331e5
...@@ -127,21 +127,27 @@ Section Refinement. ...@@ -127,21 +127,27 @@ Section Refinement.
rel_vals; eauto. rel_vals; eauto.
Qed. Qed.
Lemma refinement Γ ρ : Lemma prerefinement2 Γ x x' n ρ :
(spec_ctx ρ - (spec_ctx ρ - x ↦ᵢ (#nv n) - x' ↦ₛ (#nv n) -
Γ lateChoice log earlyChoice : TArrow (Tref TNat) TBool)%I. Γ earlyChoice #x log lateChoice #x' : TBool)%I.
Proof. Proof.
iIntros "#Hspec". iIntros "#Hspec Hx Hx'".
unfold lateChoice in *. unfold earlyChoice in *. unlock. unfold earlyChoice. unlock.
iApply bin_log_related_arrow; eauto. rel_rec_l.
iAlways. iIntros (Δ (l,l')) "Hxx'". simpl. rel_bind_l (rand #())%E.
iDestruct "Hxx'" as ([x x']) "[% #Hxx']". inversion H1; subst. simpl. iApply (rand_l with "Hspec"); eauto. simpl. iIntros (b).
replace (λ: "x", "x" <- Nat 0 ;; rand #())%E rel_rec_l.
with (of_val lateChoice); last first.
{ unfold lateChoice. unlock. reflexivity. } unfold lateChoice. unlock.
replace (λ: "x", (λ: "r", "x" <- Nat 0 ;; "r") (rand #()))%E rel_rec_r.
with (of_val earlyChoice); last first. rel_store_r. simpl.
{ unfold earlyChoice. unlock. reflexivity. } rel_rec_r.
Abort. rel_bind_r (rand #())%E.
iApply (rand_r b with "Hspec"); eauto. simpl.
rel_store_l. simpl.
rel_rec_l.
rel_vals; eauto.
Qed.
End Refinement. End Refinement.
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