proofmode.v 3.21 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris_c.c_translation Require Export monad.
Dan Frumin's avatar
Dan Frumin committed
5 6
From iris.proofmode Require Import coq_tactics.

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

31
Lemma tac_awp_pure `{amonadG Σ} Δ Δ' K e1 e2 e φ R Φ :
Dan Frumin's avatar
Dan Frumin committed
32 33 34 35 36 37 38
  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.