wp_tactics.v 4.54 KB
Newer Older
1
From iris.algebra Require Export upred_tactics.
2
From iris.heap_lang Require Export tactics derived.
3 4
Import uPred.

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

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

22 23 24 25 26 27
(* sometimes, we will have to do a final view shift, so only apply
pvs_intro if we obtain a consecutive wp *)
Ltac wp_strip_pvs :=
  lazymatch goal with
  | |- _  |={?E}=> _ =>
    etrans; [|apply pvs_intro];
28 29 30 31 32
    match goal with
    | |- _  wp E _ _ => simpl
    | |- _  |={E,_}=> _ => simpl
    | _ => fail
    end
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
  end.

35 36
Ltac wp_value_head := etrans; [|eapply wp_value_pvs; wp_done]; lazy beta.

37 38
Ltac wp_strip_later := idtac. (* a hook to be redefined later *)

39 40
Ltac wp_seq_head :=
  lazymatch goal with
41 42
  | |- _  wp ?E (Seq _ _) ?Q =>
    etrans; [|eapply wp_seq; wp_done]; wp_strip_later
43 44
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
45
Ltac wp_finish := intros_revert ltac:(
46 47 48 49 50 51
  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
52
  | |- _  |={_,_}=> _ => wp_strip_pvs
53
  end).
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55

Tactic Notation "wp_value" :=
56
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
58
    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
59
  | _ => fail "wp_value: not a wp"
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
  end.

62
Tactic Notation "wp_rec" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65
  lazymatch goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with App ?e1 _ =>
66 67
(* hnf does not reduce through an of_val *)
(*      match eval hnf in e1 with Rec _ _ _ => *)
68
    wp_bind_core K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
69 70 71
(*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
  | _ => fail "wp_rec: not a 'wp'"
  end.
72

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

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

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

101
Tactic Notation "wp_proj" :=
102
  lazymatch goal with
103
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
104
    match eval hnf in e' with
105 106
    | 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
107 108
    end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
  | _ => fail "wp_proj: not a 'wp'"
109 110
  end.

111
Tactic Notation "wp_if" :=
112
  lazymatch goal with
113
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
114 115
    match eval hnf in e' with
    | If _ _ _ =>
116
      wp_bind_core K;
117 118 119
      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'"
120
  end.
121

122
Tactic Notation "wp_match" :=
123
  lazymatch goal with
124
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
125 126
    match eval hnf in e' with
    | Case _ _ _ =>
127
      wp_bind_core K;
128 129 130 131
      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'"
132 133
  end.

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