Commit 59d1cab3 authored by Dan Frumin's avatar Dan Frumin

More robust solve_closed tactic

Add a pre_solve_closed ltac that basically changes the goal from
`Closed X e` to `Closed ∅ e`. It is actually OK in practice.
parent 94ffe6ee
...@@ -238,7 +238,18 @@ Ltac solve_to_val := ...@@ -238,7 +238,18 @@ Ltac solve_to_val :=
end. end.
Hint Extern 0 (IntoVal _ _) => solve_to_val : typeclass_instances. Hint Extern 0 (IntoVal _ _) => solve_to_val : typeclass_instances.
(* TODO:
DF: this is also kind of a hack.
Basically, we canno't really solve goals of the form `Closed X e` for an abstract `X`.
`vm_compute` loops on goals like `bool_decide (x {[x]} X)`. *)
Ltac pre_solve_closed :=
lazymatch goal with
| [ |- Closed ?X ?e ] =>
apply (Closed_mono e X); [| apply empty_subseteq]
end.
Ltac solve_closed := Ltac solve_closed :=
pre_solve_closed;
match goal with match goal with
| [ |- Closed ?X ?e] => | [ |- Closed ?X ?e] =>
let e' := R.of_expr e in change (is_closed X (R.to_expr e')); let e' := R.of_expr e in change (is_closed X (R.to_expr e'));
......
...@@ -222,27 +222,6 @@ Section cell_refinement. ...@@ -222,27 +222,6 @@ Section cell_refinement.
Proof. Proof.
iIntros (Δ). iIntros (Δ).
unlock cell2 cell1 cellτ. unlock cell2 cell1 cellτ.
assert (Closed (dom _ Γ) (Pack
(λ: "x", (ref #false, ref "x", ref "x", newlock #()),
λ: "r",
let: "l" := Snd "r" in
acquire "l" ;;
let: "v" := if: ! (Fst (Fst (Fst "r"))) then
! (Snd (Fst "r")) else ! (Snd (Fst (Fst "r"))) in
release "l" ;; "v",
λ: "r" "x",
let: "l" := Snd "r" in
acquire "l" ;;
(if: ! (Fst (Fst (Fst "r")))
then Snd (Fst (Fst "r")) <- "x" ;;
Fst (Fst (Fst "r")) <- #false
else Snd (Fst "r") <- "x" ;; Fst (Fst (Fst "r")) <- #true) ;;
release "l"))%E).
{ apply Closed_mono with ; eauto.
set_solver. }
assert (Closed (dom _ Γ) (Pack (λ: "x", ref "x", λ: "r", ! "r", λ: "r" "x", "r" <- "x"))).
{ apply Closed_mono with ; eauto.
set_solver. }
iApply bin_log_related_tlam; auto. iApply bin_log_related_tlam; auto.
iIntros (R HR) "!#". iIntros (R HR) "!#".
iApply (bin_log_related_pack _ (cellR R)). iApply (bin_log_related_pack _ (cellR R)).
......
...@@ -368,12 +368,6 @@ Section refinement. ...@@ -368,12 +368,6 @@ Section refinement.
Proof. Proof.
iIntros (Δ). iIntros (Δ).
unlock CG_mkstack. unlock CG_mkstack.
assert (Closed (dom (gset string) Γ) (mk_stack #())).
{ eapply Closed_mono with ; eauto. set_solver. }
assert (Closed (dom (gset string) Γ) (let: "l" := ref #false in
let: "st" := ref Nile in
((CG_locked_pop "st") "l", (CG_locked_push "st") "l"))).
{ eapply Closed_mono with ; eauto. set_solver. }
rel_tlam_r. rel_tlam_r.
rel_alloc_r as l' "Hl'". rel_let_r. rel_alloc_r as l' "Hl'". rel_let_r.
rel_alloc_r as st' "Hst'". rel_let_r. rel_alloc_r as st' "Hst'". rel_let_r.
......
...@@ -19,7 +19,7 @@ Section Stack_refinement. ...@@ -19,7 +19,7 @@ Section Stack_refinement.
l' ↦ₛ #false)%I. l' ↦ₛ #false)%I.
Context `{stackG Σ}. Context `{stackG Σ}.
Definition sinv τi stk stk' l : iProp Σ := Definition sinv τi stk stk' l : iProp Σ :=
( (istk : loc) v h, (stack_owns h) ( (istk : loc) v h, (stack_owns h)
stk' ↦ₛ v stk' ↦ₛ v
stk ↦ᵢ (FoldV #istk) stk ↦ᵢ (FoldV #istk)
...@@ -68,7 +68,7 @@ Section Stack_refinement. ...@@ -68,7 +68,7 @@ Section Stack_refinement.
{ iNext. rewrite {2}/sinv. iExists _,_,_. { iNext. rewrite {2}/sinv. iExists _,_,_.
iFrame "Hoe Hst' Hst Hl". iFrame "Hoe Hst' Hst Hl".
rewrite (StackLink_unfold _ (# nstk, _)). rewrite (StackLink_unfold _ (# nstk, _)).
iExists _, _. iSplitR; auto. iExists _, _. iSplitR; auto.
iFrame "Hnstk". iFrame "Hnstk".
iRight. iExists _, _, _, _. auto. } iRight. iExists _, _, _, _. auto. }
rel_if_true_l. rel_if_true_l.
...@@ -248,7 +248,7 @@ replace ((rec: "pop" "st" <> := ...@@ -248,7 +248,7 @@ replace ((rec: "pop" "st" <> :=
rel_rec_r. rel_rec_r.
rel_load_l_atomic. rel_load_l_atomic.
iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose". iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]". iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
iExists _. iFrame "Histk_i". iExists _. iFrame "Histk_i".
iModIntro. iNext. iIntros "Histk_i /=". iModIntro. iNext. iIntros "Histk_i /=".
...@@ -277,7 +277,7 @@ replace ((rec: "pop" "st" <> := ...@@ -277,7 +277,7 @@ replace ((rec: "pop" "st" <> :=
rel_rec_l. rel_rec_l.
rel_snd_l. rel_snd_l.
rel_rec_l. rel_rec_l.
close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
simpl. simpl.
iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *) iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
+ iApply bin_log_related_arrow; eauto. + iApply bin_log_related_arrow; eauto.
...@@ -294,7 +294,7 @@ replace ((rec: "pop" "st" <> := ...@@ -294,7 +294,7 @@ replace ((rec: "pop" "st" <> :=
+ clear. + clear.
iClear "IH Histk HLK_tail HLK HLK'". iClear "IH Histk HLK_tail HLK HLK'".
iSpecialize ("Hff" $! (y1,y2) with "Hτ"). iSpecialize ("Hff" $! (y1,y2) with "Hτ").
iApply (related_ret with "[Hff]"). iApply (related_ret with "[Hff]").
done. done.
Qed. Qed.
...@@ -320,11 +320,6 @@ Section Full_refinement. ...@@ -320,11 +320,6 @@ Section Full_refinement.
(TArrow (TArrow (TVar 0) TUnit) TUnit)). (TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof. Proof.
unfold FG_stack. unfold CG_stack. unfold FG_stack. unfold CG_stack.
assert (Closed (dom _ Γ) ((λ: "st", FG_stack_body "st") (ref Fold (ref InjL #())))%E).
{ apply Closed_mono with ; last done. solve_closed. }
assert (Closed (dom _ Γ) ((λ: "l", (λ: "st", (CG_stack_body "st") "l") (ref Fold (InjL #()))) (ref #false))%E).
{ apply Closed_mono with ; last done. solve_closed. }
iApply bin_log_related_tlam; auto. iApply bin_log_related_tlam; auto.
iIntros (τi) "% !#". iIntros (τi) "% !#".
rel_alloc_r as l "Hl". rel_alloc_r as l "Hl".
......
...@@ -283,4 +283,5 @@ Section refinement. ...@@ -283,4 +283,5 @@ Section refinement.
iApply "Hpool". iExists _,_,_; iFrame. } iApply "Hpool". iExists _,_,_; iFrame. }
iApply bin_log_related_unit. iApply bin_log_related_unit.
Qed. 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