Commit 05f79935 authored by Dan Frumin's avatar Dan Frumin

Fix all the examples

parent 87523047
......@@ -416,19 +416,28 @@ Section proofs.
- awp_pures. iApply awp_ret. by iApply wp_value.
Qed.
Lemma a_whileV_inv_spec I R Φ c e :
I -
(I - AWP c @ R {{ v, (v = #false U (Φ #()))
(v = #true U (AWP e @ R {{ _, U I }})) }}) -
AWP whileV (c) { e } @ R {{ Φ }}.
Proof.
iIntros "HI #Hinv". iLöb as "IH".
iApply a_whileV_spec. iNext.
iSpecialize ("Hinv" with "HI"). iApply (awp_wand with "Hinv").
iIntros (v) "[[-> H]|[-> H]] /="; first by auto.
iLeft. iSplit; first done. iModIntro.
iApply (awp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
Qed.
Lemma a_while_inv_spec I R Φ c e :
I -
(I - AWP c @ R {{ v, (v = #false U (Φ #()))
(v = #true U (AWP e @ R {{ _, U I }})) }}) -
AWP while (c) { e } @ R {{ Φ }}.
Proof.
iIntros "HI #Hinv". iApply a_while_spec. iLöb as "IH".
iApply a_whileV_spec. iNext.
iSpecialize ("Hinv" with "HI"). iApply (awp_wand with "Hinv").
iIntros (v) "[[-> H]|[-> H]] /="; first by auto.
iLeft. iSplit; first done. iModIntro.
iApply (awp_wand with "H"); iIntros (_) "HI !>". by iApply "IH".
Qed.
Proof.
iIntros "HI #Hinv". iApply a_while_spec. by iApply (a_whileV_inv_spec with "HI Hinv").
Qed.
Lemma a_call_spec R Ψ Φ (f : val) ea :
AWP ea @ R {{ Ψ }} -
......
......@@ -6,12 +6,12 @@ Definition incr : val := λ: "l",
Definition factorial_body : val := λ: "n" "c" "r",
while (∗ᶜ (a_ret "c") < (a_ret "n"))
{ incr "c" ;
{ (call (incr, a_ret "c")) ;
a_ret "r" = ((∗ᶜ (a_ret "r")) * (∗ᶜ (a_ret "c"))) }.
Definition factorial : val := λ: "n",
"r" ←ᶜ a_alloc 1 1;;
"k" ←ᶜ a_alloc 1 0;;
"r" ←ᶜ a_alloc 1 1;
"k" ←ᶜ a_alloc 1 0;
factorial_body "n" "k" "r" ;
∗ᶜ(a_ret "r").
......@@ -22,7 +22,8 @@ Section factorial_spec.
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
AWP incr (cloc_to_val l) @ R {{ Φ }}.
Proof.
iIntros "Hl HΦ". awp_lam. vcg_solver. auto.
iIntros "Hl HΦ". awp_lam. vcg.
rewrite !Z.add_0_l Z.add_comm. eauto.
Qed.
Lemma factorial_body_spec (n k : nat) (c r: cloc) R :
......@@ -32,18 +33,19 @@ Section factorial_spec.
Proof.
iIntros "(Hk & Hc & Hr)". awp_lam. awp_pures.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_whileV_spec. iNext.
vcg_solver. rewrite Qp_half_half. iIntros "Hr Hc".
vcg. iIntros "Hr Hc".
case_bool_decide.
+ iLeft. iSplit; eauto.
iApply a_sequence_spec'.
iApply (incr_spec with "Hc"). iIntros "Hc".
iModIntro. vcg_solver. iIntros "Hc Hr".
iModIntro. vcg.
iIntros "Hc Hr". iIntros "!> HR". iExists R. iFrame.
iApply (incr_spec with "Hc"). iIntros "Hc $".
vcg_continue. iIntros "Hc Hr".
iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
+ iRight. iSplit; eauto. iApply a_seq_spec. iModIntro.
assert ((fact k) * (S k) = fact (S k)) as ->.
{ rewrite /fact. lia. }
iApply ("IH" $! n (S k) with "[] Hc Hr").
{ iPureIntro. lia. }
+ iRight. iSplit; eauto. iModIntro.
iDestruct "Hk" as %Hk.
assert (k = n) as -> by lia. by iFrame.
Qed.
......@@ -51,40 +53,13 @@ Section factorial_spec.
Lemma factorial_spec (n: nat) R :
AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof.
awp_lam.
vcg_solver.
iIntros (r) "[Hr _]". vcg_continue. iIntros "Hr".
iIntros (c) "[Hc _]". vcg_continue. iIntros "Hr Hc".
awp_lam. vcg.
iIntros (r) "? ?".
iIntros (c) "? ?".
iIntros "Hr Hc".
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". vcg_continue. iModIntro. eauto.
- iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame.
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
vcg_solver.
iIntros (r) "[Hr _]". vcg_continue. iIntros "Hr".
iIntros (c) "[Hc _]". vcg_continue. iIntros "Hr Hc".
do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
vcg_solver. iIntros "Hr Hc".
case_bool_decide.
+ iRight. iSplit; eauto.
iNext. iApply a_sequence_spec'. rewrite Qp_half_half.
iApply (incr_spec with "Hc").
iIntros "Hc". iModIntro. vcg_solver.
iIntros "Hc Hr". iModIntro.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
vcg_continue. eauto.
Qed.
End factorial_spec.
......@@ -2,7 +2,9 @@ From iris_c.vcgen Require Import proofmode.
Local Open Scope Z_scope.
(* TODO: Notation, get rid of parenthesis around the while loop *)
Definition gcd : val := λ: "a" "b",
Definition gcd : val := λ: "x",
"a" ←ᶜ a_ret (Fst "x");
"b" ←ᶜ a_ret (Snd "x");
(while (∗ᶜ(a_ret "a") != ∗ᶜ(a_ret "b")) {
if (∗ᶜ(a_ret "a") < ∗ᶜ(a_ret "b")) {
(a_ret "b") = ∗ᶜ(a_ret "b") - ∗ᶜ(a_ret "a")
......@@ -19,29 +21,28 @@ Section gcd_spec.
Lemma gcd_spec (a b : Z) (l r: cloc) R :
0 a 0 b
l C #a - r C #b -
awp (gcd (cloc_to_val l) (cloc_to_val r)) R (λ v, v = #(Z.gcd a b)).
awp (gcd (cloc_to_val l, cloc_to_val r)%V) R (λ v, v = #(Z.gcd a b)).
Proof.
iIntros (??) "Hl Hr". unfold gcd. do 2 awp_lam.
(* vcg_solver. *)
(* iIntros "Hr Hl". *)
iApply a_sequence_spec'.
iApply (a_while_inv_spec ( x y : Z,
iIntros (??) "Hl Hr". unfold gcd. awp_lam.
vcg. iIntros "Hl Hr".
iApply (a_whileV_inv_spec ( x y : Z,
0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[Hl Hr]").
- iExists a, b. eauto with iFrame.
- iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
vcg_solver.
vcg.
iIntros "Hr Hl /=".
case_bool_decide; simpl; [ iLeft | iRight ];
iSplit; eauto.
+ repeat iModIntro. vcg_solver.
rewrite Qp_half_half. simplify_eq/=.
+ repeat iModIntro. vcg_continue. simplify_eq/=.
rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame.
+ iNext. iApply a_if_spec'.
vcg_solver. rewrite !Qp_half_half.
+ iModIntro.
iApply a_if_spec. vcg.
iIntros "Hl Hr /=".
case_bool_decide; simpl; [ iLeft | iRight ];
(iSplit; first done);
vcg_solver;
eauto 400 with iFrame.
(iSplit; first done); iModIntro.
* vcg. iIntros "Hl Hr". iModIntro. iExists x, (y - x); iFrame.
iPureIntro. rewrite Z.gcd_sub_diag_r. lia.
* vcg. iIntros "Hl Hr". iModIntro. iExists (x-y), y; iFrame.
iPureIntro. rewrite Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. lia.
Qed.
End gcd_spec.
......@@ -41,7 +41,7 @@ Section tests_vcg.
intros ?. iStartProof.
vcg. iExists (n). repeat iSplit; eauto.
{ iPureIntro. lia. }
iIntros (l) "Hl". assert ( m, n = S m) as [k ->]. exists (pred n). lia.
iIntros (l) "? Hl". assert ( m, n = S m) as [k ->]. exists (pred n). lia.
iDestruct "Hl" as "[Hl Hls]". (* TODO: this looks ridiculous *)
vcg_continue. eauto 42 with 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