wp_tactics.v 7.49 KB
Newer Older
1
2
3
From heap_lang Require Export tactics substitution.
Import uPred.

4
(* TODO: The next few tactics are not wp-specific at all. They should move elsewhere. *)
5

6
7
8
9
Ltac revert_intros tac :=
  lazymatch goal with
  | |-  _, _ => let H := fresh in intro H; revert_intros tac; revert H
  | |- _ => tac
10
  end.
11

12
13
14
(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
    is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
    Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
15
16
Ltac u_strip_later :=
  let rec strip :=
17
      lazymatch goal with
18
      | |- (_  _)   _  =>
19
        etrans; last (eapply equiv_entails_sym, later_sep);
20
21
        apply sep_mono; strip
      | |- (_  _)   _  =>
22
        etrans; last (eapply equiv_entails_sym, later_and);
23
24
        apply sep_mono; strip
      | |- (_  _)   _  =>
25
        etrans; last (eapply equiv_entails_sym, later_or);
26
27
28
29
        apply sep_mono; strip
      | |-  _   _ => apply later_mono; reflexivity
      | |- _   _ => apply later_intro; reflexivity
      end
30
31
32
33
34
  in let rec shape_Q :=
    lazymatch goal with
    | |- _  (_  _) =>
      (* Force the later on the LHS to be top-level, matching laters
         below ★ on the RHS *)
35
      etrans; first (apply equiv_entails, later_sep; reflexivity);
36
37
38
      (* Match the arm recursively *)
      apply sep_mono; shape_Q
    | |- _  (_  _) =>
39
      etrans; first (apply equiv_entails, later_and; reflexivity);
40
41
      apply sep_mono; shape_Q
    | |- _  (_  _) =>
42
      etrans; first (apply equiv_entails, later_or; reflexivity);
43
44
45
46
47
48
      apply sep_mono; shape_Q
    | |- _   _ => apply later_mono; reflexivity
    (* We fail if we don't find laters in all branches. *)
    end
  in revert_intros ltac:(etrans; [|shape_Q];
                         etrans; last eapply later_mono; first solve [ strip ]).
49

Ralf Jung's avatar
Ralf Jung committed
50
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
51
    into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
Ralf Jung's avatar
Ralf Jung committed
52
    the moves all the assumptions back. *)
53
Ltac u_revert_all :=
Ralf Jung's avatar
Ralf Jung committed
54
  lazymatch goal with
55
  | |-  _, _ => let H := fresh in intro H; u_revert_all;
56
57
58
59
60
61
62
63
           (* TODO: Really, we should distinguish based on whether this is a
              dependent function type or not. Right now, we distinguish based
              on the sort of the argument, which is suboptimal. *)
           first [ apply (const_intro_impl _ _ _ H); clear H
                 | revert H; apply forall_elim']
  | |- ?C  _ => trans (True  C)%I;
           first (apply equiv_entails_sym, left_id, _; reflexivity);
           apply impl_elim_l'
Ralf Jung's avatar
Ralf Jung committed
64
65
  end.

66
67
68
(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
   It applies löb where all the Coq assumptions have been turned into logical
   assumptions, then moves all the Coq assumptions back out to the context,
Ralf Jung's avatar
Ralf Jung committed
69
   applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
70
71
   Coq assumption so that we end up with the same shape as where we started,
   but with an additional assumption ★-ed to the context *)
72
Ltac u_löb tac :=
73
  u_revert_all;
74
75
  (* Add a box *)
  etrans; last (eapply always_elim; reflexivity);
76
77
78
  (* We now have a goal for the form True ⊑ P, with the "original" conclusion
     being locked. *)
  apply löb_strong; etransitivity;
79
80
    first (apply equiv_entails, left_id, _; reflexivity);
  apply: always_intro;
81
82
  (* Now introduce again all the things that we reverted, and at the bottom,
     do the work *)
83
84
85
86
87
88
  let rec go :=
      lazymatch goal with
      | |- _  ( _, _) => apply forall_intro;
               let H := fresh in intro H; go; revert H
      | |- _  ( _  _) => apply impl_intro_l, const_elim_l;
               let H := fresh in intro H; go; revert H
89
90
91
92
93
94
      (* This is the "bottom" of the goal, where we see the impl introduced
         by u_revert_all as well as the ▷ from löb_strong and the □ we added. *)
      | |-   ?R  (?L  _) => apply impl_intro_l;
               trans (L    R)%I;
                 first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
               tac
95
96
97
      end
  in go.

98
99
100
101
102
103
104
105
106
107
108
(** wp-specific helper tactics *)
(* First try to productively strip off laters; if that fails, at least
   cosmetically get rid of laters in the conclusion. *)
Ltac wp_strip_later :=
  let rec go :=
    lazymatch goal with
    | |- _  (_  _) => apply sep_mono; go
    | |- _   _ => apply later_intro
    | |- _  _ => reflexivity
    end
  in revert_intros ltac:(first [ u_strip_later | etrans; [|go] ] ).
109
110
111
Ltac wp_bind K :=
  lazymatch eval hnf in K with
  | [] => idtac
112
  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
113
  end.
114
115
116
Ltac wp_finish :=
  let rec go :=
  match goal with
117
  | |- _   _ => etrans; [|apply later_mono; go; reflexivity]
118
  | |- _  wp _ _ _ =>
119
     etrans; [|eapply wp_value_pvs; reflexivity];
120
121
     (* sometimes, we will have to do a final view shift, so only apply
     wp_value if we obtain a consecutive wp *)
122
123
     try (eapply pvs_intro;
          match goal with |- _  wp _ _ _ => simpl | _ => fail end)
124
  | _ => idtac
125
  end in simpl; revert_intros go.
126

127
Tactic Notation "wp_rec" ">" :=
Ralf Jung's avatar
Ralf Jung committed
128
  u_löb ltac:((* Find the redex and apply wp_rec *)
129
              idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
130
               lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
131
132
133
               | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
                        match eval cbv in e' with
                        | App (Rec _ _ _) _ =>
134
135
                          wp_bind K; etrans; [|eapply wp_rec; reflexivity];
                          wp_finish
Ralf Jung's avatar
Ralf Jung committed
136
                        end)
137
138
               end).
Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
139

140
141
142
143
144
Tactic Notation "wp_lam" ">" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
    | App (Rec "" _ _) _ =>
145
       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
146
147
148
149
150
151
152
153
154
    end)
  end.
Tactic Notation "wp_lam" := wp_lam>; wp_strip_later.

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

155
Tactic Notation "wp_op" ">" :=
156
157
158
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
159
160
161
162
    | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
    | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
    | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
    | BinOp _ _ _ =>
163
       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
164
    | UnOp _ _ =>
165
       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
166
167
    end)
  end.
168
169
Tactic Notation "wp_op" := wp_op>; wp_strip_later.

170
Tactic Notation "wp_if" ">" :=
171
172
173
174
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
    | If _ _ _ =>
175
       wp_bind K;
176
       etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
177
178
    end)
  end.
179
Tactic Notation "wp_if" := wp_if>; wp_strip_later.
180

181
182
183
184
185
Tactic Notation "wp_focus" open_constr(efoc) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match e' with efoc => unify e' efoc; wp_bind K end)
  end.
186

187
Tactic Notation "wp" ">" tactic(tac) :=
188
189
190
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
  end.
Ralf Jung's avatar
Ralf Jung committed
191
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
192
193

(* In case the precondition does not match *)
194
195
Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).