wp_tactics.v 4.57 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.heap_lang Require Export tactics op_rules.
2 3
Import uPred.

4
(** wp-specific helper tactics *)
5
Ltac wp_bind_core K :=
6 7
  lazymatch eval hnf in K with
  | [] => idtac
8
  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
9
  end.
10

11
(* Solves side-conditions generated by the wp tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
12
Ltac wp_done :=
13 14
  match goal with
  | |- Closed _ _ => solve_closed
15
  | |- is_Some (to_val _) => solve_to_val
16 17 18 19
  | |- to_val _ = Some _ => solve_to_val
  | |- language.to_val _ = Some _ => solve_to_val
  | _ => fast_done
  end.
20

21
Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
22

23 24
Ltac wp_strip_later := idtac. (* a hook to be redefined later *)

25 26
Ltac wp_seq_head :=
  lazymatch goal with
27 28
  | |- _  wp ?E (Seq _ _) ?Q =>
    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
29 30
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
31
Ltac wp_finish := intros_revert ltac:(
32 33 34 35 36 37 38
  rewrite /= ?to_of_val;
  try wp_strip_later;
  repeat lazymatch goal with
  | |- _  wp ?E (Seq _ _) ?Q =>
     etrans; [|eapply wp_seq; wp_done]; wp_strip_later
  | |- _  wp ?E _ ?Q => wp_value_head
  end).
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40

Tactic Notation "wp_value" :=
41
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
43
    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
44
  | _ => fail "wp_value: not a wp"
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
  end.

47 48 49
Lemma of_val_unlock v e : of_val v = e  of_val (locked v) = e.
Proof. by unlock. Qed.

50 51
(* Applied to goals that are equalities of expressions. Will try to unlock the
   LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
52
Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
53

54
Tactic Notation "wp_rec" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56 57
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with App ?e1 _ =>
58 59
(* hnf does not reduce through an of_val *)
(*      match eval hnf in e1 with Rec _ _ _ => *)
60 61
    wp_bind_core K; etrans;
      [|eapply wp_rec; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
62 63 64
(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
  | _ => fail "wp_rec: not a 'wp'"
  end.
65

66
Tactic Notation "wp_lam" :=
67
  lazymatch goal with
68
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
69 70
    match eval hnf in e' with App ?e1 _ =>
(*    match eval hnf in e1 with Rec BAnon _ _ => *)
71 72
    wp_bind_core K; etrans;
      [|eapply wp_lam; [solve_of_val_unlock|wp_done..]]; simpl_subst; wp_finish
73 74
(*    end *) end) || fail "wp_lam: cannot find 'Lam' in" e
  | _ => fail "wp_lam: not a 'wp'"
75 76 77 78 79
  end.

Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_let.

80
Tactic Notation "wp_op" :=
81
  lazymatch goal with
82
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
Ralf Jung's avatar
Ralf Jung committed
83
    lazymatch eval hnf in e' with
84 85
    | BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
86 87
    | BinOp EqOp _ _ =>
       wp_bind_core K; eapply wp_eq; [wp_done|wp_done|wp_finish|wp_finish]
88
    | BinOp _ _ _ =>
89 90
       wp_bind_core K; etrans;
         [|eapply wp_bin_op; [wp_done|wp_done|try fast_done]]; wp_finish
91
    | UnOp _ _ =>
92 93
       wp_bind_core K; etrans;
         [|eapply wp_un_op; [wp_done|try fast_done]]; wp_finish
94 95
    end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
  | _ => fail "wp_op: not a 'wp'"
96
  end.
97

98
Tactic Notation "wp_proj" :=
99
  lazymatch goal with
100
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
101
    match eval hnf in e' with
102 103
    | Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
    | Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
104 105
    end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
  | _ => fail "wp_proj: not a 'wp'"
106 107
  end.

108
Tactic Notation "wp_if" :=
109
  lazymatch goal with
110
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
111 112
    match eval hnf in e' with
    | If _ _ _ =>
113
      wp_bind_core K;
114 115 116
      etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
    end) || fail "wp_if: cannot find 'If' in" e
  | _ => fail "wp_if: not a 'wp'"
117
  end.
118

119
Tactic Notation "wp_match" :=
120
  lazymatch goal with
121
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
122 123
    match eval hnf in e' with
    | Case _ _ _ =>
124
      wp_bind_core K;
125 126 127 128
      etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
      simpl_subst; wp_finish
    end) || fail "wp_match: cannot find 'Match' in" e
  | _ => fail "wp_match: not a 'wp'"
129 130
  end.

131
Tactic Notation "wp_bind" open_constr(efoc) :=
132
  lazymatch goal with
133
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
134
    match e' with
135 136 137
    | efoc => unify e' efoc; wp_bind_core K
    end) || fail "wp_bind: cannot find" efoc "in" e
  | _ => fail "wp_bind: not a 'wp'"
138
  end.