Commit 5d15373a authored by Dan Frumin's avatar Dan Frumin
Browse files

More work on tp_ tactics

- All tp_ tactics work without explicit modalities in the goal;
- All tp_ tactics simplify the ghost thread pool points-to;
- Proof term size improvements
parent c32e111d
......@@ -125,7 +125,7 @@ Section rules.
tp_pures i. tp_store i.
tp_pures j.
tp_rec j.
tp_pures j. iApply fupd_wp. tp_load j. tp_normalise j.
tp_pures j. iApply fupd_wp. tp_load j.
tp_pures j.
iModIntro. wp_pures. iExists (v2, w2)%V. eauto.
Qed.
......@@ -160,10 +160,10 @@ Section rules.
iApply (wp_wand with "He2"). iIntros (w1).
iDestruct 1 as (w2) "[Hj Hw]".
iSimpl in "Hi". iSimpl in "Hj".
tp_pure i _. iSimpl in "Hi".
tp_pure i _.
tp_store i.
tp_pures j. tp_rec j.
tp_load j. tp_normalise j.
tp_load j.
tp_pures j.
iModIntro. iExists _. iFrame.
Qed.
......@@ -227,6 +227,6 @@ Section rules.
tp_pures i. tp_store i.
tp_pures j.
rewrite /spawn.join. tp_pures j.
tp_load j. iSimpl in "Hj". tp_pures j. eauto with iFrame.
tp_load j. tp_pures j. eauto with iFrame.
Qed.
End rules.
......@@ -459,10 +459,10 @@ Section refinement.
iApply refines_spec_ctx. iIntros "#Hρ".
iApply fupd_refines.
(* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
tp_cmpxchg_suc j. iSimpl in "Hj".
tp_cmpxchg_suc j.
tp_pures j. tp_rec j. tp_pures j.
tp_load j. tp_normalise j. tp_pures j.
tp_store j. tp_normalise j. tp_pures j.
tp_load j. tp_pures j.
tp_store j. tp_pures j.
tp_rec j. tp_store j.
iSpecialize ("Hoff" with "Hj").
iSpecialize ("HN" with "Hoff").
......
This diff is collapsed.
......@@ -15,7 +15,7 @@ Lemma test1 E1 j K (l : loc) (n : nat) :
={E1}= l ↦ₛ #(n+1) j fill K #().
Proof.
iIntros (?) "#? Hj Hl".
tp_load j. tp_normalise j.
tp_load j.
tp_pures j.
tp_store j. by iFrame.
Qed.
......@@ -29,9 +29,9 @@ Lemma test2 E1 j K (l : loc) (n : nat) :
={E1}= l ↦ₛ #(n*2) j fill K #true.
Proof.
iIntros (?) "#? Hj Hl".
tp_cmpxchg_fail j. tp_normalise j.
tp_cmpxchg_fail j.
tp_pures j.
tp_cmpxchg_suc j. tp_normalise j.
tp_cmpxchg_suc j.
tp_pures j. by iFrame.
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