wp_tactics.v 7.22 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
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
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
Ralf Jung's avatar
Ralf Jung committed
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
             (* 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
61
  | |- ?C  _ => trans (True  C)%I;
62
63
             first (rewrite [(True  C)%I]left_id; reflexivity);
             apply wand_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
70
   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. *)
71
Ltac u_löb tac :=
72
  u_revert_all;
73
74
75
76
  (* 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);
77
78
  (* Now introduce again all the things that we reverted, and at the bottom,
     do the work *)
79
80
81
82
83
84
  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
Ralf Jung's avatar
Ralf Jung committed
85
      (* This is the "bottom" of the goal, where we see the wand introduced
86
87
         by u_revert_all as well as the ▷ from löb_strong. *)
      | |-  _  (_ - _) => apply wand_intro_l; tac
88
89
90
      end
  in go.

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

120
Tactic Notation "wp_rec" ">" :=
Ralf Jung's avatar
Ralf Jung committed
121
122
  u_löb ltac:((* Find the redex and apply wp_rec *)
              idtac; (* FIXME WTF without this, it matches the goal before executing u_löb ?!? *)
123
               lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
124
125
126
127
128
               | |- _  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)
129
130
               end).
Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
131

132
133
134
135
136
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 "" _ _) _ =>
137
       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
138
139
140
141
142
143
144
145
146
    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.

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

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

173
174
175
176
177
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.
178

179
Tactic Notation "wp" ">" tactic(tac) :=
180
181
182
  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
183
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
184
185

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