fact.v 3.3 KB
Newer Older
1 2
From iris_c.vcgen Require Import vcg_solver.
Local Open Scope Z_scope.
3 4

Definition incr : val := λ: "l",
5
  (a_ret "l") = (∗ᶜ (a_ret "l") + 1).
6 7

Definition factorial_body : val := λ: "n" "c" "r",
8
  while (∗ᶜ (a_ret "c") < (a_ret "n"))
9 10
         { incr "c" ;
           a_ret "r" = ((∗ᶜ (a_ret "r")) * (∗ᶜ (a_ret "c"))) }.
11 12

Definition factorial : val := λ: "n",
13 14 15 16
  "r" ←ᶜ a_alloc 1 1;;
  "k" ←ᶜ a_alloc 1 0;;
  factorial_body "n" "k" "r" ;
  ∗ᶜ(a_ret "r").
17 18 19 20

Section factorial_spec.
  Context `{amonadG Σ}.

21
  Lemma incr_spec (l : cloc) (n : Z) R Φ :
22
    l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
23
    AWP incr (cloc_to_val l) @ R {{ Φ }}.
24
  Proof.
Dan Frumin's avatar
Dan Frumin committed
25
    iIntros "Hl HΦ". awp_lam. vcg_solver. auto.
Dan Frumin's avatar
Dan Frumin committed
26
  Qed.
27

28
  Lemma factorial_body_spec (n k : nat) (c r: cloc) R :
29
    (k  n  c C[ULvl] #k  r C #(fact k)) -
30 31
    AWP factorial_body #n (cloc_to_val c) (cloc_to_val r) @ R
        {{ _, c C #n  r C #(fact n) }}.
32 33
  Proof.
    iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
34
    iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext.
Dan Frumin's avatar
Dan Frumin committed
35
    vcg_solver. rewrite Qp_half_half. iIntros "Hr Hc".
36
    case_bool_decide.
37
    + iLeft. iSplit; eauto.
38
      iApply a_sequence_spec'.
39 40
      iApply (incr_spec with "Hc"). iIntros "Hc".
      iModIntro. vcg_solver. iIntros "Hc Hr".
Dan Frumin's avatar
Dan Frumin committed
41
      iModIntro.
42 43
      assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
      { rewrite Nat.add_1_r /fact. lia. }
44
      assert (Z_of_nat' (k + 1)%nat = (k + 1)) as <- by lia.
45 46
      iApply ("IH" $! n (k+1)%nat with "[] Hc Hr"). iPureIntro. lia.
    + iRight. iSplit; eauto.  iApply a_seq_spec. iModIntro.
47 48
      iDestruct "Hk" as %Hk.
      assert (k = n) as -> by lia. by iFrame.
49 50 51
  Qed.

  Lemma factorial_spec (n: nat) R :
52
    AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
53 54
  Proof.
    awp_lam.
55
    vcg_solver.
Dan Frumin's avatar
Dan Frumin committed
56 57
    iIntros (r) "[Hr _]". vcg_continue. iIntros "Hr".
    iIntros (c) "[Hc _]". vcg_continue. iIntros "Hr Hc".
58 59
    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.
60
    - iIntros (?) "[Hc Hr]". vcg_continue. iModIntro. eauto.
61 62 63 64 65 66
  Qed.

  Lemma factorial_spec_with_inv (n: nat) R :
    awp (factorial #n) R (λ v, v = #(fact n))%I.
  Proof.
    awp_lam.
67
    vcg_solver.
Dan Frumin's avatar
Dan Frumin committed
68 69
    iIntros (r) "[Hr _]". vcg_continue. iIntros "Hr".
    iIntros (c) "[Hc _]". vcg_continue. iIntros "Hr Hc".
70
    do 3 awp_lam.
71
    iApply (a_while_inv_spec
72
      (k:nat, k  n  c C #k  r C #(fact k))%I with "[Hr Hc]").
73 74
    - iExists O. eauto with iFrame lia.
    - iModIntro. iIntros "H".  iDestruct "H" as (k) "(H & Hc & Hr)".
Dan Frumin's avatar
Dan Frumin committed
75
      vcg_solver. iIntros "Hr Hc".
76 77
      case_bool_decide.
      + iRight. iSplit; eauto.
78
        iNext. iApply a_sequence_spec'. rewrite Qp_half_half.
79
        iApply (incr_spec with "Hc").
Dan Frumin's avatar
Dan Frumin committed
80
        iIntros "Hc". iModIntro. vcg_solver.
81 82 83 84 85
        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.
86
      + iLeft. iSplit; eauto. iModIntro.
87
        iRevert "H". iIntros "%". assert (k = n) as -> by lia.
88
        vcg_continue. eauto.
89 90
  Qed.
End factorial_spec.