rules.v 12.2 KB
Newer Older
1 2
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
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 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
From iris.program_logic Require Import hoare.

Section prim.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Import uPred.
Lemma test P Q :
  (P  (Q  P))%I.
Proof.
  iIntros "HP". apply impl_intro_r.
  rewrite and_elim_l. 
  change (envs_entails (Envs Enil (Esnoc Enil "HP" P)) P).
  iFrame.
Qed.
Lemma exist_impl {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a) - (( a, Φ a)   a, Ψ a).
Proof.
  apply impl_intro_r.
  iIntros "HΦ".
  rewrite and_exist_l.
  iDestruct "HΦ" as (a) "HΦ".
  iExists a. rewrite (and_mono_l ( a0 : A, Φ a0  Ψ a0) _ (Φ a  Ψ a)).
  - by rewrite impl_elim_l.
  - iIntros "H". iApply "H".
Qed.
(* Lemma forall_wand {A} (Φ Ψ : A  uPred M) : *)
(*   ( a, Φ a - Ψ a) - ( a, Φ a) -  a, Ψ a. *)
(* Proof. *)
(*   iIntros "HΦ Ha" (a). *)
(*   by iApply "HΦ". *)
(* Qed. *)
Lemma and_impl (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
  (Φ1  Ψ1) - 
  (Φ2  Ψ2) -
  (Φ1  Φ2)  (Ψ1  Ψ2).
Proof.
  apply wand_intro_l.
  apply impl_intro_r.
  rewrite sep_and.
  rewrite assoc. rewrite -(assoc uPred_and _ _ Φ1).
  rewrite impl_elim_l. rewrite (comm uPred_and _ Ψ1).
  rewrite -assoc. rewrite impl_elim_l. done.
Qed.
Lemma wand_wand (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
  (Ψ1 - Φ1) - 
  (Φ2 - Ψ2) -
  (Φ1 - Φ2) - (Ψ1 - Ψ2).
Proof.
  iIntros "HΦ1 HΦ2 HΦ HΨ".
  iApply "HΦ2". iApply "HΦ". by iApply "HΦ1".
Qed.
Lemma sep_wand (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
  (Φ1 - Ψ1) - 
  (Φ2 - Ψ2) -
  (Φ1  Φ2) - (Ψ1  Ψ2).
Proof.
  iIntros "HΦ1 HΦ2 [HΦ HΦ']".
  iSplitL "HΦ HΦ1".
  - by iApply "HΦ1". 
  - by iApply "HΦ2".
Qed.
Lemma or_wand (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
  (Φ1 - Ψ1) - 
  (Φ2 - Ψ2) -
  (Φ1  Φ2) - (Ψ1  Ψ2).
Proof.
  iIntros "HΦ1 HΦ2 [HΦ | HΦ]".
  - iLeft. by iApply "HΦ1". 
  - iRight. by iApply "HΦ2".
Qed.
End prim.

Section derived.
Context `{irisG F_mu_ref_conc_lang Σ}.
Implicit Types Φ Ψ : iProp Σ.

Lemma fupd_wand (E : coPset) Φ Ψ :
  (Φ - Ψ) - 
  (|={E}=> Φ) - (|={E}=> Ψ).
Proof.
  iIntros "HΦ". iMod 1 as "HΦ'".
  iModIntro. by iApply "HΦ".
Qed.
Lemma wp_wand_flipped E e (Φ Ψ : val  iProp Σ) :
  ( v, Φ v - Ψ v) - 
  WP e @ E {{ Φ }} - WP e @ E {{ Ψ }}.
Proof.
  iIntros "H1 H2". iApply (wp_wand with "H2 H1").
Qed.
End derived.
95 96 97

Section test.
  Context `{logrelG Σ}.
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
  Notation D := (prodC valC valC -n> iProp Σ).
  Import uPred.

  (* HACK: move somewhere else *)
  Ltac auto_equiv :=
    (* Deal with "pointwise_relation" *)
    repeat lazymatch goal with
           | |- pointwise_relation _ _ _ _ => intros ?
           end;
    (* Normalize away equalities. *)
    repeat match goal with
           | H : _ {_} _ |-  _ => apply (discrete_iff _ _) in H
           | _ => progress simplify_eq
           end;
    (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
    try (f_equiv; fast_done || auto_equiv).

  Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).

  Program Definition interp_arrow_alt
          (interp1 : listC D -n> D) (τ2 : type) : listC D -n> D :=
    λne Δ ww,
    (  vv, interp1 Δ vv 
             {,;Δ;}  (App (of_val (ww.1)) (of_val (vv.1)))
                         log
                            (App (of_val (ww.2)) (of_val (vv.2))) : τ2)%I.
  Solve Obligations with solve_proper.
  Next Obligation.
    intros τ2 interp n.
    intros Δ1 Δ2 HΔ.
    intros [v1 v2]. simpl.
    auto_equiv.
    by apply bin_log_related_ne.
  Qed.

  (* ALSO holds for vv : expr * expr *)
  Lemma interp_expr_wat τ2 Δ (vv ww : prodC valC valC) ρ :
    spec_ctx ρ -
    ({Δ; }  (App (vv.1) (ww.1)) log (App (vv.2) (ww.2)) : τ2) 
     τ2 ⟧ₑ Δ ((vv.1) (ww.1), (vv.2) (ww.2)).
  Proof.
    iIntros "#Hspec H /=".
    rewrite bin_log_related_eq /bin_log_related_def.
    iIntros (j K) "Hj /=".
    iSpecialize ("H" $!  ρ with "Hspec []").
    { iAlways. by iApply interp_env_nil. }
    rewrite /interp_expr /=.
    iSpecialize ("H" $! j K).
    rewrite /env_subst !fmap_empty !subst_p_empty.
    iMod ("H" with "Hj"). done.
  Qed.

  Lemma interp_arrow_interp_alt τ1 τ2 Δ vv ρ :
    spec_ctx ρ -
    (interp   (TArrow τ1 τ2) Δ vv - interp_arrow_alt (interp   τ1) τ2 Δ vv).
  Proof.
    iIntros "#Hs /= #Hvv". iAlways.
    iIntros (ww) "Hww".
    iApply (related_ret ).
    by iApply "Hvv".
  Qed.
  Lemma interp_arrow_alt_interp τ1 τ2 Δ vv ρ :
    spec_ctx ρ -
    (interp_arrow_alt (interp   τ1) τ2 Δ vv - interp   (TArrow τ1 τ2) Δ vv).
  Proof.
    iIntros "#Hs /= #Hvv". iAlways.
    iIntros (ww) "Hww".
    iApply (interp_expr_wat with "Hs").
    by iApply "Hvv".
  Qed.

  Fixpoint interp_alt (τ : type) : listC D -n> D :=
    match τ return _ with
    | TUnit => interp_unit
    | TNat => interp_nat
    | TBool => interp_bool
    | TProd τ1 τ2 => interp_prod (interp_alt τ1) (interp_alt τ2)
    | TSum τ1 τ2 => interp_sum (interp_alt τ1) (interp_alt τ2)
    | TArrow τ1 τ2 =>
      interp_arrow_alt (interp_alt τ1) τ2
    | TVar x => ctx_lookup x
    | TForall τ' => interp_forall   (interp_alt τ')
    | TExists τ' => interp_exists (interp_alt τ')
    | TRec τ' => interp_rec (interp_alt τ')
    | Tref τ' => interp_ref (interp_alt τ')
    end.

  Global Instance interp_alt_persistent τ Δ vv :
    Persistent (interp_alt τ Δ vv).
  Proof.
    revert vv Δ; induction τ=> vv Δ; simpl; try apply _.
    rewrite /Persistent /interp_rec fixpoint_unfold /interp_rec1 /=. eauto.
  Qed.
    
  Ltac mononess :=
    repeat match goal with
    (* | |- envs_entails _ (( _: _, _) - ( _: _, _)) => *)
    (*   iApply exist_wand; iIntros (?) *)
    (* | |- envs_entails _ (( _: _, _) - ( _: _, _)) => *)
    (*   iApply forall_wand; iIntros (?) *)
    (* | |- envs_entails _ ((_  _) - (_  _)) => iApply and_wand *)
    | |- envs_entails _ ((_  _) - (_  _)) => iApply or_wand
    (* | |- envs_entails _ ((_  _) - (_  _)) => iApply impl_wand' *)
    | |- envs_entails _ ((_ - _) - (_ - _)) => iApply wand_wand
    | |- envs_entails _ ((WP _ @ _ {{ _ }}) - (WP _ @ _ {{ _ }})) =>
      iApply wp_wand_flipped; iIntros (?)
    | |- envs_entails _ (( _) - ( _)) => iApply later_wand; iNext
    | |- envs_entails _ (( _)%I - ( _)%I) => iApply persistently_wand
    | |- envs_entails _ ((|={_}=> _ ) - (|={_}=> _ )) => iApply fupd_wand
    | |- envs_entails _ ((_  _) - (_  _)) => iApply sep_wand
    (* | |- (inv _ _)%I  (inv _ _)%I => apply (contractive_proper _) *)
    end.

  Local Ltac solve_clause :=
    first
      [ iDestruct ("IH" $! _ _) as "[IH' _]";
        iApply "IH'"
      | iDestruct ("IH1" $! _ _) as "[IH' _]";
        iApply "IH'"
      | iDestruct ("IH" $! _ _) as "[_ IH']";
        iApply "IH'"
      | iDestruct ("IH1" $! _ _) as "[_ IH']";
        iApply "IH'" ].

  (* TODO: Something like Proper  and ==>  but inside Iris*)
  Lemma interp_interp_alt τ Δ vv ρ :
    spec_ctx ρ - (interp   τ Δ vv  interp_alt τ Δ vv).
  Proof.
    iIntros "#Hspec".
    iInduction (τ) as [] "IH" forall (vv Δ); simpl; eauto.
    - iSplit.
      iApply exist_impl; iIntros (?).
      iApply exist_impl; iIntros (?).
      iApply and_impl; eauto.
      iApply and_impl; eauto.
      iDestruct ("IH" $! a Δ) as "[IH'' IH']". done.
      admit.
    - iSplitL; mononess; eauto; solve_clause.
    - iSplitL.
      { mononess. iAlways.
        mononess. rewrite !impl_wand.
        mononess. solve_clause.
        rewrite bin_log_related_eq /bin_log_related_def.
        iIntros "HZ" (? ?) "? #Hg".
        rewrite /env_subst !Closed_subst_p_id.
        iApply "HZ". }
      { mononess. iAlways.
        mononess. rewrite !impl_wand.
        mononess. solve_clause.
        iApply (interp_expr_wat with "Hspec"). }
    - iSplitL; mononess; eauto.
      iLöb as "FP".
      rewrite {2}fixpoint_unfold.
      rewrite {2}(fixpoint_unfold (interp_rec1 (interp_alt τ) Δ)).
      rewrite /interp_rec1 /=.
      mononess; eauto.
      admit. (* This is very annoying, our IH is not strong enough to deal with this *)
    - iSplitL; mononess; eauto; solve_clause.
    - iSplitL.
      { repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto).
        rewrite /interp_expr.
        repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto). 
        solve_clause. }
      { repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto).
        rewrite /interp_expr.
        repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto). 
        solve_clause. }
    - iSplitL; mononess; eauto; solve_clause.
    - iSplitL; mononess; eauto.
      admit. admit. (* THIS IS NOT TRUE *)
  Admitted.

  (* Notation "〚 τ 〛" := (interp_alt τ). *)

  Lemma bin_log_related_arrow_val_alt Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
    e = (rec: f x := eb)%E 
    e' = (rec: f' x' := eb')%E 
    Closed  e 
    Closed  e' 
    ( v1 v2, interp_alt τ Δ (v1, v2) -
      {Δ;Γ}  App e (of_val v1) log App e' (of_val v2) : τ') -
    {E;Δ;Γ}  e log e' : TArrow τ τ'.
  Proof.
    iIntros (????) "#H".
    subst e e'.
    rewrite bin_log_related_eq.
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
    cbn-[subst_p].
    iModIntro.
    rewrite {2}/env_subst Closed_subst_p_id.
    iApply wp_value.
    { rewrite /IntoVal. simpl. erewrite decide_left. done. }
    rewrite /env_subst Closed_subst_p_id.
    iExists (RecV f' x' eb').
    iFrame "Hj". iAlways. iIntros ([v1 v2]) "Hvv".
    iAssert (interp_alt τ Δ (v1, v2)) with "[Hvv]" as "Hvv".
    { by iApply interp_interp_alt. }
    iSpecialize ("H" $! v1 v2 with "Hvv Hs []").
    { iAlways. iApply "HΓ". }
    assert (Closed  ((rec: f x := eb) v1)).
    { unfold Closed in *. simpl.
      intros. split_and?; auto. apply of_val_closed. }
    assert (Closed  ((rec: f' x' := eb') v2)).
    { unfold Closed in *. simpl.
      intros. split_and?; auto. apply of_val_closed. }
    rewrite /env_subst. rewrite !Closed_subst_p_id. done.
  Qed.

  Lemma bin_log_related_val_alt Δ Γ E e e' τ v v' :
    to_val e = Some v 
    to_val e' = Some v' 
    (|={E}=> interp_alt τ Δ (v, v'))  {E;Δ;Γ}  e log e' : τ.
  Proof.
    iIntros (He He') "Hτ".
    iMod "Hτ" as "Hτ".
    apply bin_log_related_spec_ctx.
    iDestruct 1 as (ρ) "#Hρ".
    rewrite -(related_ret ).
    iApply (interp_ret ); eauto.
    by iApply interp_interp_alt.
  Qed.
319

320 321 322
  (*****************************************************)
  (* TODO: interesting fact?
   bin_log_related_arrow_val can be proved using bin_log_related_arrow
323 324 325 326 327 328 329 330 331 332
   specifically, at some point we can update
   {Δ; Γ}  v1 log v2 : τ
   to
    τ  Δ (v1, v2') for some value v2'
   *)
  Lemma bin_log_related_arrow_val Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
    e = (rec: f x := eb)%E 
    e' = (rec: f' x' := eb')%E 
    Closed  e 
    Closed  e' 
333
    ( v1 v2, interp_alt τ Δ (v1, v2) -
334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
      {Δ;Γ}  App e (of_val v1) log App e' (of_val v2) : τ') -
    {E;Δ;Γ}  e log e' : TArrow τ τ'.
  Proof.
    iIntros (????) "#H".
    iApply bin_log_related_arrow; eauto. iAlways.
    iIntros (v1 v2) "#Hvv".
    rewrite bin_log_related_eq.
    iIntros (ρ vvs) "#Hspec #HΓ". simpl.
    rewrite /env_subst. rewrite !Closed_subst_p_id.
    rewrite /interp_expr.
    iIntros (j K) "Hj /=".
    subst.
    tp_bind j v2.
    iSpecialize ("Hvv" $! ρ vvs with "Hspec [HΓ]"); auto.
    iSpecialize ("Hvv" $! j (AppRCtx (RecV f' x' eb') :: K)).
    simpl. rewrite /env_subst !Closed_subst_p_id.
    iMod ("Hvv" with "Hj") as "Hvv".
    iMod (wp_value_inv with "Hvv") as (v') "[Hj Hvv]".
    iSpecialize ("H" with "Hvv Hspec [HΓ]"); auto.
    replace (rec: f x := eb)%E with (of_val (rec: f x := eb)) by (unlock;reflexivity).
    replace (rec: f' x' := eb')%E with (of_val (rec: f' x' := eb')) by (unlock;reflexivity).
    rewrite /env_subst /= !Closed_subst_p_id.
    iSpecialize ("H" with "Hj").
    done.
  Qed.
End test.