proofmode.v 3.27 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris_c.lib Require Import locking_heap mset flock.
From iris_c.c_translation Require Export monad lifting.
From iris.proofmode Require Import coq_tactics.

Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
Lemma tac_awp_bind `{locking_heapG Σ, heapG Σ, flockG Σ} K Δ R Φ e f :
  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).

Dan Frumin's avatar
Dan Frumin committed
31 32 33 34 35 36 37 38
Lemma tac_awp_pure `{locking_heapG Σ, heapG Σ, flockG Σ} Δ Δ' K e1 e2 e φ R Φ :
  e = fill K e1 
  PureExec φ e1 e2 
  φ 
  MaybeIntoLaterNEnvs 1 Δ Δ' 
  envs_entails Δ' (awp (fill K e2) R Φ) 
  envs_entails Δ (awp e R Φ).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  rewrite envs_entails_eq=> -> ??? HΔ'. rewrite into_laterN_env_sound /=.
Dan Frumin's avatar
Dan Frumin committed
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
  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 *)
      |simpl_subst
      ])
    || fail "awp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
  | _ => fail "awp_pure: not an 'awp'"
  end.

Tactic Notation "awp_if" := awp_pure (If _ _ _).
Tactic Notation "awp_if_true" := awp_pure (If (Lit (LitBool true)) _ _).
Tactic Notation "awp_if_false" := awp_pure (If (Lit (LitBool false)) _ _).
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_rec" := awp_pure (App _ _).
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.