Commit 6c8c4c60 authored by Dan Frumin's avatar Dan Frumin

Strengthen the bin_log_related_arrow rule

parent aefd864f
......@@ -12,17 +12,13 @@ Section contents.
{,;Δ;Γ} Y log Y : TArrow (TArrow A A) A.
Proof.
unlock Y. simpl.
iApply bin_log_related_arrow_val; eauto.
Typeclasses Opaque interp. (* TODO *)
iApply bin_log_related_arrow; eauto.
iAlways. iIntros (f1 f2) "#Hff".
rel_let_l. rel_let_r.
iLöb as "IH".
rel_let_l. rel_let_r.
iApply bin_log_related_app.
- iApply (related_ret ).
iApply (interp_ret ); eauto using to_of_val.
simpl. iApply "Hff".
- iApply "IH".
iApply (bin_log_related_app with "Hff").
by iApply "IH".
Qed.
End contents.
......
......@@ -143,7 +143,7 @@ Section refinement.
- (* Allocating a new lock *)
unlock newlock lock.newlock.
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "/= [% %]". simplify_eq.
iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
rel_let_l. rel_let_r.
rel_alloc_r as l' "Hl'".
rel_alloc_l as lo "Hlo".
......
......@@ -67,14 +67,14 @@ Section properties.
f2 = (rec: f' x' := eb')%E
Closed f1
Closed f2
( (v1 v2 : val), {,;Δ;Γ} v1 log v2 : τ -
( (v1 v2 : val), ({,;Δ;Γ} v1 log v2 : τ) -
{,;Δ;Γ} f1 v1 log f2 v2 : τ') -
{E,E;Δ;Γ} f1 log f2 : TArrow τ τ'.
Proof.
iIntros (????) "#H".
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (v1 v2) "Hvv".
iApply "H".
iAlways. iIntros (v1 v2) "#Hvv".
iApply "H". iAlways.
iApply (related_ret ).
by iApply interp_ret.
Qed.
......
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