proofmode.v 3.53 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
From iris.heap_lang Require Export proofmode notation.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris_c.c_translation Require Export monad.
Dan Frumin's avatar
Dan Frumin committed
3 4
From iris.proofmode Require Import coq_tactics.

5
Lemma tac_cwp_bind `{cmonadG Σ} K Δ R Φ e f :
Robbert Krebbers's avatar
Robbert Krebbers committed
6
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
7 8 9
  envs_entails Δ (WP e {{ v, cwp (f (of_val v)) R Φ }})%I 
  envs_entails Δ (cwp (fill K e) R Φ).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_cwp_bind. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11
Ltac cwp_bind_core K :=
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
  lazymatch eval hnf in K with
  | [] => idtac
14
  | _ => eapply (tac_cwp_bind K); [simpl; reflexivity|lazy beta]
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16
  end.

17
Tactic Notation "cwp_apply" open_constr(lem) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
20
    | |- envs_entails _ (cwp ?e ?R ?Q) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
21
      reshape_expr e ltac:(fun K e' =>
22
        cwp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) ||
Robbert Krebbers's avatar
Robbert Krebbers committed
23
      lazymatch iTypeOf H with
24
      | Some (_,?P) => fail "cwp_apply: cannot apply" P
Robbert Krebbers's avatar
Robbert Krebbers committed
25
      end
26
    | _ => fail "cwp_apply: not a 'cwp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28
    end).

29
Lemma tac_cwp_pure `{cmonadG Σ} Δ Δ' K e1 e2 e φ n R Φ :
Dan Frumin's avatar
Dan Frumin committed
30
  e = fill K e1 
31
  PureExec φ n e1 e2 
Dan Frumin's avatar
Dan Frumin committed
32
  φ 
33
  MaybeIntoLaterNEnvs n Δ Δ' 
34 35
  envs_entails Δ' (cwp (fill K e2) R Φ) 
  envs_entails Δ (cwp e R Φ).
Dan Frumin's avatar
Dan Frumin committed
36
Proof.
37 38
  rewrite envs_entails_eq=> -> ??? HΔ'.
  rewrite into_laterN_env_sound /=.
39
  rewrite HΔ' -cwp_pure //.
Dan Frumin's avatar
Dan Frumin committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
Qed.

Tactic Notation "tac_bind_helper" :=
  lazymatch goal with
  | |- fill ?K ?e = fill _ ?efoc =>
     reshape_expr e ltac:(fun K' e' =>
       unify e' efoc;
       let K'' := eval cbn[app] in (K' ++ K) in
       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
  | |- ?e = fill _ ?efoc =>
     reshape_expr e ltac:(fun K' e' =>
       unify e' efoc;
       replace e with (fill K' e') by (by rewrite ?fill_app))
  end; reflexivity.

55
Tactic Notation "cwp_pure" open_constr(efoc) :=
Dan Frumin's avatar
Dan Frumin committed
56 57
  iStartProof;
  lazymatch goal with
58
  | |- envs_entails _ (cwp ?e ?R ?Q) =>
Dan Frumin's avatar
Dan Frumin committed
59 60 61
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
62
      eapply (tac_cwp_pure _ _ _ _ _ (fill K e'));
Dan Frumin's avatar
Dan Frumin committed
63 64 65 66
      [tac_bind_helper                (* e = fill K e' *)
      |apply _                        (* PureExec *)
      |try fast_done                  (* The pure condition for PureExec *)
      |apply _                        (* IntoLaters *)
Robbert Krebbers's avatar
Robbert Krebbers committed
67
      |simpl
Dan Frumin's avatar
Dan Frumin committed
68
      ])
69 70
    || fail "cwp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
  | _ => fail "cwp_pure: not an 'cwp'"
Dan Frumin's avatar
Dan Frumin committed
71 72
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
73
(* See Iris for documentation on this tactic *)
74
Ltac cwp_pures :=
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  iStartProof;
76
  repeat (cwp_pure _; []). (* The `;[]` makes sure that no side-condition
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
                             magically spawns. *)

79
Tactic Notation "cwp_rec" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  let H := fresh in
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  assert (H := AsRecV_recv);
82
  cwp_pure (App _ _);
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
  clear H.

85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
Tactic Notation "cwp_if" := cwp_pure (If _ _ _).
Tactic Notation "cwp_if_true" := cwp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "cwp_if_false" := cwp_pure (If (LitV (LitBool false)) _ _).
Tactic Notation "cwp_unop" := cwp_pure (UnOp _ _).
Tactic Notation "cwp_binop" := cwp_pure (BinOp _ _ _).
Tactic Notation "cwp_op" := cwp_unop || cwp_binop.
Tactic Notation "cwp_lam" := cwp_rec.
Tactic Notation "cwp_let" := cwp_lam.
Tactic Notation "cwp_seq" := cwp_lam.
Tactic Notation "cwp_proj" := cwp_pure (Fst _) || cwp_pure (Snd _).
Tactic Notation "cwp_case" := cwp_pure (Case _ _ _).
Tactic Notation "cwp_match" := cwp_case; cwp_let.
Tactic Notation "cwp_inj" := cwp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "cwp_pair" := cwp_pure (Pair _ _).
Tactic Notation "cwp_closure" := cwp_pure (Rec _ _ _).