Commit ea4d95cb authored by Léon Gondelman's avatar Léon Gondelman

factorial proved using invariant-based awp-rule

parent 0fa4f300
......@@ -142,12 +142,12 @@ Section proofs.
Qed.
Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
(I - awp c R (λ v, (v = #false U (Φ #()))
(v = #true (awp b R (λ _, U I))))%I) -
I -
(I - awp c R (λ v, (v = #false U (Φ #()))
(v = #true (awp b R (λ _, U I))))%I) -
awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
Proof.
iIntros "#Hinv Hi". iLöb as "IH".
iIntros "Hi #Hinv". iLöb as "IH".
iApply a_while_spec. iNext.
iApply a_if_spec.
iSpecialize ("Hinv" with "Hi"). iApply (awp_wand with "Hinv").
......
......@@ -101,4 +101,47 @@ Section factorial_spec.
awp_load_ret r #(fact n).
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret #1 r "Hr".
iApply awp_bind. awp_alloc_ret #0 c "Hc".
iApply a_sequence_spec. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k <= n c U #k r U #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc]").
+ awp_load_ret c #k.
+ awp_ret_value.
+ iIntros (v1 v2) "[% Hc] %"; subst.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
case_bool_decide.
* iRight. iSplit; eauto.
iApply a_sequence_spec.
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_ret with "[Hr Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #(fact k) r U #(fact k))%I
(λ v, v = #(k + 1) c U #(k+1))%I with "[Hr] [Hc]").
** awp_load_ret r #(fact k).
** awp_load_ret c #(k + 1).
** iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
rewrite /bin_op_eval /=.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
{ rewrite Nat.add_1_r /fact. lia. }
iExists #(fact (k+1)); repeat (iSplit; eauto).
iExists #(fact k). iFrame. iIntros "Hr". iModIntro.
assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
iExists (k+1)%nat. eauto with iFrame lia.
* iLeft. iSplit; eauto. do 2 iModIntro. awp_seq.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r #(fact n).
Qed.
End factorial_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