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

4
(* TODO: The next 5 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
20
21
22
23
24
25
26
27
28
29
      | |- (_  _)   _  =>
        etrans; last (eapply equiv_spec, later_sep);
        apply sep_mono; strip
      | |- (_  _)   _  =>
        etrans; last (eapply equiv_spec, later_and);
        apply sep_mono; strip
      | |- (_  _)   _  =>
        etrans; last (eapply equiv_spec, later_or);
        apply sep_mono; strip
      | |-  _   _ => apply later_mono; reflexivity
      | |- _   _ => apply later_intro; reflexivity
      end
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
  in let rec shape_Q :=
    lazymatch goal with
    | |- _  (_  _) =>
      (* Force the later on the LHS to be top-level, matching laters
         below  on the RHS *)
      etrans; first (apply equiv_spec; symmetry; apply later_sep; reflexivity);
      (* Match the arm recursively *)
      apply sep_mono; shape_Q
    | |- _  (_  _) =>
      etrans; first (apply equiv_spec; symmetry; apply later_and; reflexivity);
      apply sep_mono; shape_Q
    | |- _  (_  _) =>
      etrans; first (apply equiv_spec; symmetry; apply later_or; reflexivity);
      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
51
52
(* ssreflect-locks the part after the  *)
(* FIXME: I tried doing a lazymatch to only apply the tactic if the goal has shape ,
   bit the match is executed *before* doing the recursion... WTF? *)
53
Ltac u_lock_goal := revert_intros ltac:(apply uPred_lock_conclusion).
Ralf Jung's avatar
Ralf Jung committed
54
55
56
57

(** Transforms a goal of the form  ..., ?0...  ?1  ?2
    into True  ..., ?0...  ?1  ?2, applies tac, and
    the moves all the assumptions back. *)
58
Ltac u_revert_all :=
Ralf Jung's avatar
Ralf Jung committed
59
  lazymatch goal with
60
  | |-  _, _ => let H := fresh in intro H; u_revert_all;
61
62
63
64
65
             (* 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']
Ralf Jung's avatar
Ralf Jung committed
66
  | |- ?C  _ => trans (True  C)%I;
67
68
             first (rewrite [(True  C)%I]left_id; reflexivity);
             apply wand_elim_l'
Ralf Jung's avatar
Ralf Jung committed
69
70
  end.

71
72
73
(** 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,
74
75
76
77
   applies [tac ()] on the goal (now of the form _  _), and then reverts the
   Coq assumption so that we end up with the same shape as where we started.
   [tac] is a thunk because I found no other way to prevent Coq from expandig
   matches too early.*)
78
79
Ltac u_löb tac :=
  u_lock_goal; u_revert_all;
80
81
82
83
  (* We now have a goal for the form True  P, with the "original" conclusion
     being locked. *)
  apply löb_strong; etransitivity;
    first (apply equiv_spec; symmetry; apply (left_id _ _ _); reflexivity);
84
85
  (* Now introduce again all the things that we reverted, and at the bottom,
     do the work *)
86
87
88
89
90
91
92
  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
      | |-  ?R  (?L - locked _) => apply wand_intro_l;
93
               unlock; tac ()
94
95
96
      end
  in go.

97
98
99
100
101
102
103
104
105
106
107
(** 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] ] ).
108
109
110
Ltac wp_bind K :=
  lazymatch eval hnf in K with
  | [] => idtac
111
  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
112
  end.
113
114
115
Ltac wp_finish :=
  let rec go :=
  match goal with
116
  | |- _   _ => etrans; [|apply later_mono; go; reflexivity]
117
  | |- _  wp _ _ _ =>
118
     etrans; [|eapply wp_value_pvs; reflexivity];
119
120
     (* sometimes, we will have to do a final view shift, so only apply
     wp_value if we obtain a consecutive wp *)
121
122
     try (eapply pvs_intro;
          match goal with |- _  wp _ _ _ => simpl | _ => fail end)
123
  | _ => idtac
124
  end in simpl; revert_intros go.
125

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

137
138
139
140
141
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 "" _ _) _ =>
142
       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
143
144
145
146
147
148
149
150
151
    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.

152
Tactic Notation "wp_op" ">" :=
153
154
155
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
156
157
158
159
    | 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 _ _ _ =>
160
       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
161
    | UnOp _ _ =>
162
       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
163
164
    end)
  end.
165
166
Tactic Notation "wp_op" := wp_op>; wp_strip_later.

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

178
179
180
181
182
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.
183

184
Tactic Notation "wp" ">" tactic(tac) :=
185
186
187
  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
188
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
189
190

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