Commit ccec1584 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak gcd.

parent d22c6803
...@@ -20,60 +20,49 @@ Definition gcd : val := λ: "a" "b", ...@@ -20,60 +20,49 @@ Definition gcd : val := λ: "a" "b",
Section gcd_spec. Section gcd_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}. Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma gcd_spec (a b : Z) (l r: loc) R: Lemma gcd_spec (a b : Z) (l r: loc) R :
a >= 0 - b >= 0 - 0 a 0 b
l U #a - r U #b - l U #a - r U #b -
awp (gcd #l #r) R (λ v, v = #(Z.gcd a b)). awp (gcd #l #r) R (λ v, v = #(Z.gcd a b)).
Proof. Proof.
iIntros "% % Hl Hr". iIntros (??) "Hl Hr". do 2 awp_lam. iApply a_sequence_spec.
do 2 awp_lam. iApply a_sequence_spec. iApply (a_while_inv_spec ( x y : Z,
iApply (a_while_inv_spec 0 x 0 y Z.gcd x y = Z.gcd a b l U #x r U #y)%I with "[Hl Hr]").
( (x y: Z), l U #x r U #y - iExists a, b. eauto with iFrame.
x >= 0 y >= 0 Zgcd x y = Zgcd a b)%I - iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
with "[Hl Hr]").
- eauto with iFrame.
- iModIntro. iIntros "H". iDestruct "H" as (x y) "(Hl & Hr & % & % & %)".
iApply a_un_op_spec. iApply a_un_op_spec.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr". iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
assert (Hxy: x = y x < y y < x) by lia. assert (x = y x < y y < x) as [Hxy|[Hxy|Hxy]] by lia.
destruct Hxy as [Hxy|[Hxy|Hxy]].
+ iExists #true. simplify_eq /=. iSplit. + iExists #true. simplify_eq /=. iSplit.
{ rewrite/ bin_op_eval //=; case_bool_decide; eauto. } { rewrite/ bin_op_eval //=; case_bool_decide; eauto. }
iExists #false; iSplit; first done. iLeft; iSplit; first done. iExists #false; iSplit; first done. iLeft; iSplit; first done.
do 2 iModIntro. awp_seq. awp_load_ret l. iIntros. do 2 iModIntro. awp_seq. awp_load_ret l. iIntros.
rewrite- H5. iPureIntro. symmetry. rewrite Z.gcd_diag. by rewrite -Hgcd Z.gcd_diag Z.abs_eq.
rewrite Z.abs_eq; eauto with lia. + iExists #false. simplify_eq /=. iSplit.
+ iExists #false. simplify_eq /=. iSplit. { by rewrite /bin_op_eval //= bool_decide_false; last (intros [= ?]; lia). }
{ rewrite/ bin_op_eval //=. iExists #true; iSplit; first done. iRight; iSplit; first done.
case_bool_decide. inversion H6; subst. lia. eauto. }
iExists #true; iSplit; first done. iRight; iSplit; first done.
iApply a_if_spec. iApply a_if_spec.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr". iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
iExists #true; iSplit. iExists #true; iSplit.
{ rewrite/ bin_op_eval //=. case_bool_decide; eauto. } { by rewrite /bin_op_eval //= bool_decide_true. }
iLeft. iSplit; first done. awp_seq. iLeft. iSplit; first done. awp_seq.
iApply a_store_ret. iApply a_store_ret.
iApply (awp_bin_op_load_load with "[$Hr] [$Hl]"). iIntros "Hr Hl". iApply (awp_bin_op_load_load with "[$Hr] [$Hl]"). iIntros "Hr Hl".
iExists #(y - x); iSplit; first by eauto with lia. iExists #(y - x); iSplit; first by eauto with lia.
iExists #y. iFrame. iIntros "Hr". iModIntro. iExists #y. iIntros "{$Hr} Hr !>".
iExists x, (y-x). iFrame. iPureIntro. iExists x, (y-x). iFrame. rewrite -Hgcd Z.gcd_sub_diag_r. eauto with lia.
do 2 (split; first by lia). rewrite -H5; apply Z.gcd_sub_diag_r. + iExists #false. simplify_eq /=. iSplit.
+ iExists #false. simplify_eq /=. iSplit. { by rewrite/ bin_op_eval //= bool_decide_false; last (intros [= ?]; lia). }
{ rewrite/ bin_op_eval //=. iExists #true; iSplit; first done. iRight; iSplit; first done.
case_bool_decide. inversion H6; subst. lia. eauto. }
iExists #true; iSplit; first done. iRight; iSplit; first done.
iApply a_if_spec. iApply a_if_spec.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr". iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
iExists #false. iSplit. iExists #false. iSplit.
{ rewrite/ bin_op_eval //=. { by rewrite/ bin_op_eval //= bool_decide_false; last lia. }
case_bool_decide. inversion H6; subst. lia. eauto. }
iRight; iSplit; first done. awp_seq. iRight; iSplit; first done. awp_seq.
iApply a_store_ret. iApply a_store_ret.
iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr". iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
iExists #(x - y); iSplit; first by eauto with lia. iExists #(x - y); iSplit; first by eauto with lia.
iExists #x. iFrame. iIntros "Hl". iModIntro. iExists #x. iIntros "{$Hl} Hl !>". iExists (x - y), y. iFrame. iPureIntro.
iExists (x-y), y. iFrame. iPureIntro. rewrite -Hgcd Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. auto with lia.
do 2 (split; first by lia).
rewrite -H5 Z.gcd_comm (Z.gcd_comm x); apply Z.gcd_sub_diag_r.
Qed. Qed.
End gcd_spec. End gcd_spec.
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