Commit 0abc7f0f authored by Robbert Krebbers's avatar Robbert Krebbers

Convert some tests to Texan triples.

parent 752371c8
......@@ -26,12 +26,12 @@ Definition rev : val :=
"rev" "tmp2" "hd"
end.
Lemma rev_acc_wp hd acc xs ys (Φ : val iProp Σ) :
is_list hd xs - is_list acc ys -
( w, is_list w (reverse xs ++ ys) - Φ w) -
WP rev hd acc {{ Φ }}.
Lemma rev_acc_wp hd acc xs ys :
{{{ is_list hd xs is_list acc ys }}}
rev hd acc
{{{ w, RET w; is_list w (reverse xs ++ ys) }}}.
Proof.
iIntros "Hxs Hys HΦ".
iIntros (Φ) "[Hxs Hys] HΦ".
iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ".
......@@ -39,15 +39,14 @@ Proof.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. }
iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
iNext. iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Qed.
Lemma rev_wp hd xs (Φ : val iProp Σ) :
is_list hd xs - ( w, is_list w (reverse xs) - Φ w) -
WP rev hd (InjL #()) {{ Φ }}.
Lemma rev_wp hd xs :
{{{ is_list hd xs }}} rev hd (InjL #()) {{{ w, RET w; is_list w (reverse xs) }}}.
Proof.
iIntros "Hxs HΦ".
iApply (rev_acc_wp hd NONEV xs [] with "Hxs [%]")=> //.
iIntros (w). rewrite right_id_L. iApply "HΦ".
iIntros (Φ) "Hxs HΦ".
iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
iNext; iIntros (w). rewrite right_id_L. iApply "HΦ".
Qed.
End list_reverse.
......@@ -34,32 +34,33 @@ Definition sum' : val := λ: "t",
sum_loop "t" "l";;
!"l".
Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val iProp Σ) :
l #n - is_tree v t - (l #(sum t + n) - is_tree v t - Φ #()) -
WP sum_loop v #l {{ Φ }}.
Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
{{{ l #n is_tree v t }}}
sum_loop v #l
{{{ RET #(); l #(sum t + n) is_tree v t }}}.
Proof.
iIntros "Hl Ht HΦ".
iIntros (Φ) "[Hl Ht] HΦ".
iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
destruct t as [n'|tl tr]; simpl in *.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "Hl").
by iApply ("HΦ" with "[$Hl]").
- iDestruct "Ht" as (ll lr vl vr) "(% & Hll & Htl & Hlr & Htr)"; subst.
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "Hl Htl".
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htr"). iIntros "Hl Htr".
iApply ("HΦ" with "[Hl]").
wp_apply ("IH" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
iExists ll, lr, vl, vr. by iFrame.
Qed.
Lemma sum_wp `{!heapG Σ} v t Φ :
is_tree v t - (is_tree v t - Φ #(sum t)) - WP sum' v {{ Φ }}.
Lemma sum_wp `{!heapG Σ} v t :
{{{ is_tree v t }}} sum' v {{{ RET #(sum t); is_tree v t }}}.
Proof.
iIntros "Ht HΦ". rewrite /sum' /=.
iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
wp_let. wp_alloc l as "Hl". wp_let.
wp_apply (sum_loop_wp with "Hl Ht").
wp_apply (sum_loop_wp with "[$Hl $Ht]").
rewrite Z.add_0_r.
iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
iIntros "[Hl Ht]". wp_seq. wp_load. by iApply "HΦ".
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