fact.v 8.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Import
     soundness_binary rules rules_binary.
From iris.program_logic Require Import adequacy.

Definition fact : expr :=
  Rec (If (BinOp Eq (Var 1) (#n 0))
          (#n 1)
          (BinOp Mult (Var 1) (App (Var 0) (BinOp Sub (Var 1) (#n 1))))).

Lemma fact_typed : []  fact : TArrow TNat TNat.
Proof. repeat econstructor. Qed.

Definition fact_acc_body : expr :=
  Rec (Lam
         (If (BinOp Eq (Var 2) (#n 0))
             (Var 0)
             (LetIn
                (BinOp Mult (Var 2) (Var 0))
                (LetIn
                   (BinOp Sub (Var 3) (#n 1))
                   (App (App (Var 3) (Var 0)) (Var 1))
                )
             )
         )
      ).

Lemma fact_acc_body_typed : []  fact_acc_body : TArrow TNat (TArrow TNat TNat).
Proof. repeat econstructor. Qed.

Lemma fact_acc_body_subst f : fact_acc_body.[f] = fact_acc_body.
Proof. by asimpl. Qed.

Hint Rewrite fact_acc_body_subst : autosubst.

Lemma fact_acc_body_unfold :
  fact_acc_body =
  Rec (Lam
         (If (BinOp Eq (Var 2) (#n 0))
             (Var 0)
             (LetIn
                (BinOp Mult (Var 2) (Var 0))
                (LetIn
                   (BinOp Sub (Var 3) (#n 1))
                   (App (App (Var 3) (Var 0)) (Var 1))
                )
             )
         )
      ).
Proof. trivial. Qed.

52
Typeclasses Opaque fact_acc_body.
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
Global Opaque fact_acc_body.

Definition fact_acc : expr :=
  Lam (App (App fact_acc_body (Var 0)) (#n 1)).

Lemma fact_acc_typed : []  fact_acc : TArrow TNat TNat.
Proof.
  repeat econstructor.
  apply (closed_context_weakening [_] []); eauto.
  apply fact_acc_body_typed.
Qed.

Section fact_equiv.
  Context `{heapIG Σ, cfgSG Σ}.

  Lemma fact_fact_acc_refinement :
    []  fact log fact_acc : (TArrow TNat TNat).
  Proof.
71
    iIntros (? vs _) "[#HE HΔ]".
72 73 74 75 76 77 78 79 80 81
    iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
    iClear "HΔ". simpl.
    iIntros (j K) "Hj"; simpl.
    iApply wp_value; iExists (LamV _); iFrame.
    rewrite /= -/fact.
    iAlways. iIntros ([? ?] [n [? ?]]); simpl in *; simplify_eq; simpl.
    clear j K.
    iIntros (j K) "Hj"; simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
    asimpl.
82 83 84
    iApply (wp_mono _ _ _ (λ v,  m, j  fill K (#n (1 * m))  v = #nv m))%I.
    { iIntros (?). iDestruct 1 as (m) "[Hm %]"; subst.
      iExists (#nv _); iFrame; eauto. }
85 86 87 88 89
    generalize 1 as l => l.
    iInduction n as [|n] "IH" forall (l).
    - iApply wp_pure_step_later; auto.
      iNext; simpl; asimpl.
      rewrite fact_acc_body_unfold.
90
      iMod (do_step_pure _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
91 92 93 94 95 96 97
      rewrite -fact_acc_body_unfold.
      simpl; asimpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      iApply (wp_bind (fill [IfCtx _ _])).
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iApply wp_value. simpl.
98
      iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
99 100 101 102 103
      simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      iApply wp_value.
104
      iExists 1. replace (l * 1) with l by lia.
105 106 107 108
      auto.
    - iApply wp_pure_step_later; auto.
      iNext; simpl; asimpl.
      rewrite fact_acc_body_unfold.
109
      iMod (do_step_pure _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
110 111 112 113 114 115 116
      rewrite -fact_acc_body_unfold.
      simpl; asimpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      iApply (wp_bind (fill [IfCtx _ _])).
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iApply wp_value. simpl.
117
      iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
118 119 120 121 122 123 124 125 126
      simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      asimpl.
      iApply (wp_bind (fill [BinOpRCtx _ (#nv _)])).
      iApply (wp_bind (fill [AppRCtx (RecV _)])).
      iApply wp_pure_step_later; auto.
      iNext; simpl; iApply wp_value; simpl.
127
      iMod (do_step_pure _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
128 129 130
      simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      asimpl.
131
      iMod (do_step_pure _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
132 133 134 135 136
      simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      asimpl.
      replace (n -0) with n by lia.
      iApply wp_wand_r; iSplitL; first iApply ("IH" with "[Hj]"); eauto.
137
      iIntros (v). iDestruct 1 as (m) "[H %]"; simplify_eq.
138 139
      iApply wp_pure_step_later; auto.
      iNext; simpl; iApply wp_value.
140 141
      iExists ((S n) * m); simpl.
      replace (l * (m + n * m)) with ((l + n * l) * m)
142 143 144 145 146 147 148
        by lia.
      iFrame; auto.
  Qed.

  Lemma fact_acc_fact_refinement :
    []  fact_acc log fact : (TArrow TNat TNat).
  Proof.
149
    iIntros (? vs _) "[#HE HΔ]".
150 151 152 153 154 155 156 157 158 159
    iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
    iClear "HΔ". simpl.
    iIntros (j K) "Hj"; simpl.
    iApply wp_value; iExists (RecV _); iFrame.
    iAlways. iIntros ([? ?] [n [? ?]]); simpl in *; simplify_eq; simpl.
    clear j K.
    iIntros (j K) "Hj"; simpl.
    iApply wp_pure_step_later; auto.
    iNext; asimpl.
    rewrite -/fact.
160 161 162 163
    iApply (wp_mono _ _ _ (λ v,  m, j  fill K (#n m)  v = #nv (1 * m)))%I.
    { iIntros (?). iDestruct 1 as (m) "[? %]"; simplify_eq.
      replace (1 * m) with m by lia.
      iExists (#nv _); iFrame; eauto. }
164 165 166 167 168 169 170 171 172 173 174 175
    generalize 1 as l => l.
    iInduction n as [|n] "IH" forall (K l).
    - rewrite fact_acc_body_unfold.
      iApply (wp_bind (fill [AppLCtx _])).
      iApply wp_pure_step_later; auto.
      rewrite -fact_acc_body_unfold.
      iNext; simpl; asimpl.
      iApply wp_value; simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl; asimpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      simpl; asimpl.
176
      iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
177 178 179 180 181 182 183 184
      iApply (wp_bind (fill [IfCtx _ _])).
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iApply wp_value. simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iApply wp_value.
185
      iExists 1.
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
      replace (l * 1) with l by lia; auto.
    - rewrite {2}fact_acc_body_unfold.
      iApply (wp_bind (fill [AppLCtx _])).
      iApply wp_pure_step_later; auto.
      rewrite -fact_acc_body_unfold.
      iNext; simpl; asimpl.
      iApply wp_value; simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl; asimpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      simpl.
      iApply (wp_bind (fill [IfCtx _ _])).
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iApply wp_value. simpl.
201
      iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
202 203 204 205
      simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
206
      iMod (do_step_pure _ _ (AppRCtx (RecV _):: BinOpRCtx _ (#nv _) :: _)
207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
              with "[$Hj]") as "Hj"; eauto.
      simpl.
      iApply (wp_bind (fill [LetInCtx _])).
      iApply wp_pure_step_later; auto.
      iNext; simpl; iApply wp_value; simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl. asimpl.
      iApply (wp_bind (fill [LetInCtx _])).
      iApply wp_pure_step_later; auto.
      iNext; simpl; iApply wp_value; simpl.
      iApply wp_pure_step_later; auto.
      iNext; simpl. asimpl.
      replace (n -0) with n by lia.
      iApply wp_fupd.
      iApply wp_wand_r; iSplitL;
        first iApply ("IH" $! (BinOpRCtx _ (#nv _) :: K) with "[$Hj]"); eauto.
223
      iIntros (v). iDestruct 1 as (m) "[Hj %]"; simplify_eq.
224 225 226
      simpl.
      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
      simpl.
227 228 229
      iModIntro.
      iExists (S n * m).
      iFrame.
230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
      eauto with lia.
  Qed.

End fact_equiv.

Theorem fact_ctx_equiv :
  []  fact ctx fact_acc : (TArrow TNat TNat) 
  []  fact_acc ctx fact : (TArrow TNat TNat).
Proof.
  set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (auth.authR cfgUR)]).
  set (HG := soundness_unary.HeapPreIG Σ _ _).
  split.
  - eapply (binary_soundness Σ _); auto using fact_acc_typed, fact_typed.
    intros; apply fact_fact_acc_refinement.
  -  eapply (binary_soundness Σ _); auto using fact_acc_typed, fact_typed.
    intros; apply fact_acc_fact_refinement.
Qed.