Commit c61b7c2a authored by Dan Frumin's avatar Dan Frumin

Add `solve_closed` to the global hint db

parent d13b876d
......@@ -99,16 +99,15 @@ Section CG_Counter.
iApply bin_log_related_wp_l.
wp_bind (FG_increment #x).
unfold FG_increment. unlock.
iApply wp_rec; eauto.
solve_closed. (* TODO: why is it not being solved automatically? *)
iApply wp_rec; eauto.
iNext. simpl.
iApply wp_value; eauto. simpl. by rewrite decide_left.
iApply wp_rec; eauto. solve_closed. (* TODO: same comment here *)
iApply wp_rec; eauto.
iNext. simpl.
wp_bind (Load (Loc x)).
iApply (wp_load with "[Hx]"); auto. iNext.
iIntros "Hx".
iApply wp_rec; eauto. solve_closed. (* TODO: same comment here *)
iApply wp_rec; eauto.
iNext. simpl.
wp_bind (BinOp _ _ _).
iApply (wp_nat_binop). iNext. iModIntro. simpl.
......
......@@ -29,13 +29,13 @@ Section Refinement.
Proof.
iStartProof.
unfold rand. unlock.
iApply wp_rec; eauto. solve_closed. iNext. simpl.
iApply wp_rec; eauto. iNext. simpl.
wp_bind (Alloc _). iApply wp_alloc; auto. iNext. iIntros (y) "Hy".
iMod (inv_alloc choiceN _ (y ↦ᵢ (#v false) y ↦ᵢ (#v true))%I with "[Hy]") as "#Hinv"; eauto.
iApply wp_rec; eauto. solve_closed. iNext. simpl.
iApply wp_rec; eauto. iNext. simpl.
wp_bind (Fork _). iApply wp_fork. iNext.
iSplitL.
- iModIntro. iApply wp_rec; eauto. solve_closed. iNext; simpl.
- iModIntro. iApply wp_rec; eauto. iNext; simpl.
iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_load with "Hy"); eauto; iNext;
iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
- iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_store with "Hy"); eauto; iNext;
......
......@@ -252,6 +252,7 @@ Ltac solve_closed :=
eapply R.is_closed_correct; vm_compute; exact I
end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Hint Extern 0 (Closed _ _) => solve_closed.
Ltac simpl_subst :=
cbn[subst'];
......
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