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]).