proofmode.v 3.54 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_awp_bind `{amonadG Σ} K Δ R Φ e f :
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
  envs_entails Δ (WP e {{ v, awp (f (of_val v)) R Φ }})%I 
  envs_entails Δ (awp (fill K e) R Φ).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_awp_bind. Qed.

Ltac awp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
  | _ => eapply (tac_awp_bind K); [simpl; reflexivity|lazy beta]
  end.

Tactic Notation "awp_apply" open_constr(lem) :=
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
    | |- envs_entails _ (awp ?e ?R ?Q) =>
      reshape_expr e ltac:(fun K e' =>
        awp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) ||
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "awp_apply: cannot apply" P
      end
    | _ => fail "awp_apply: not a 'awp'"
    end).

29
Lemma tac_awp_pure `{amonadG Σ} Δ Δ' 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 Δ Δ' 
Dan Frumin's avatar
Dan Frumin committed
34 35 36
  envs_entails Δ' (awp (fill K e2) R Φ) 
  envs_entails Δ (awp e R Φ).
Proof.
37 38
  rewrite envs_entails_eq=> -> ??? HΔ'.
  rewrite into_laterN_env_sound /=.
Dan Frumin's avatar
Dan Frumin committed
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
  rewrite HΔ' -awp_pure //.
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.

Tactic Notation "awp_pure" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
  | |- envs_entails _ (awp ?e ?R ?Q) =>
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
      eapply (tac_awp_pure _ _ _ _ _ (fill K e'));
      [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 71 72
      ])
    || fail "awp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
  | _ => fail "awp_pure: not an 'awp'"
  end.

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

Tactic Notation "awp_rec" :=
  let H := fresh in
  assert (H := AsRecV_recv_locked);
  awp_pure (App _ _);
  clear H.

Dan Frumin's avatar
Dan Frumin committed
85
Tactic Notation "awp_if" := awp_pure (If _ _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87
Tactic Notation "awp_if_true" := awp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "awp_if_false" := awp_pure (If (LitV (LitBool false)) _ _).
Dan Frumin's avatar
Dan Frumin committed
88 89 90 91 92 93 94 95 96
Tactic Notation "awp_unop" := awp_pure (UnOp _ _).
Tactic Notation "awp_binop" := awp_pure (BinOp _ _ _).
Tactic Notation "awp_op" := awp_unop || awp_binop.
Tactic Notation "awp_lam" := awp_rec.
Tactic Notation "awp_let" := awp_lam.
Tactic Notation "awp_seq" := awp_lam.
Tactic Notation "awp_proj" := awp_pure (Fst _) || awp_pure (Snd _).
Tactic Notation "awp_case" := awp_pure (Case _ _ _).
Tactic Notation "awp_match" := awp_case; awp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99
Tactic Notation "awp_inj" := awp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "awp_pair" := awp_pure (Pair _ _).
Tactic Notation "awp_closure" := awp_pure (Rec _ _ _).