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

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

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
15
16
17
Ltac wp_strip_later :=
  let rec go :=
    lazymatch goal with
    | |- _  (_  _) => apply sep_mono; go
    | |- _   _ => apply later_intro
    | |- _  _ => reflexivity
    end
18
  in revert_intros ltac:(etrans; [|go]).
19

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
(** Assumes a goal of the shape P   Q.
    Will get rid of  in P below ,  and . *)
Ltac u_strip_later :=
  let rec strip :=
      match goal with
      | |- (_  _)   _  =>
        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
  in etrans; last eapply later_mono; first solve [ strip ].

Ralf Jung's avatar
Ralf Jung committed
39
40
41
(* 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? *)
42
Ltac u_lock_goal := revert_intros ltac:(apply uPred_lock_conclusion).
Ralf Jung's avatar
Ralf Jung committed
43
44
45
46

(** Transforms a goal of the form  ..., ?0...  ?1  ?2
    into True  ..., ?0...  ?1  ?2, applies tac, and
    the moves all the assumptions back. *)
47
Ltac u_revert_all :=
Ralf Jung's avatar
Ralf Jung committed
48
  lazymatch goal with
49
  | |-  _, _ => let H := fresh in intro H; u_revert_all;
Ralf Jung's avatar
Ralf Jung committed
50
51
52
53
54
55
56
57
58
59
                 (* 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 (rewrite [(True  C)%I]left_id; reflexivity);
                 apply wand_elim_l'
  end.

60
61
62
63
64
(** 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,
   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. *)
65
66
Ltac u_löb tac :=
  u_lock_goal; u_revert_all;
67
68
69
70
71
72
73
74
75
76
77
78
79
  (* 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);
  (* Now introduce again all the things that we reverted, and at the bottom, do the work *)
  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;
               (* TODO: Do sth. more robust than rewriting. *)
80
81
               trans ( L   R)%I; first (apply sep_mono_l, later_intro; reflexivity);
               trans ( (L  R))%I; first (apply equiv_spec, later_sep; reflexivity );
82
83
84
85
               unlock; tac
      end
  in go.

86
87
88
Ltac wp_bind K :=
  lazymatch eval hnf in K with
  | [] => idtac
89
  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
90
  end.
91
92
93
Ltac wp_finish :=
  let rec go :=
  match goal with
94
  | |- _   _ => etrans; [|apply later_mono; go; reflexivity]
95
  | |- _  wp _ _ _ =>
96
     etrans; [|eapply wp_value_pvs; reflexivity];
97
98
     (* sometimes, we will have to do a final view shift, so only apply
     wp_value if we obtain a consecutive wp *)
99
100
     try (eapply pvs_intro;
          match goal with |- _  wp _ _ _ => simpl | _ => fail end)
101
  | _ => idtac
102
  end in simpl; revert_intros go.
103

Ralf Jung's avatar
Ralf Jung committed
104
Tactic Notation "wp_rec" :=
105
  u_löb ltac:((* Find the redex and apply wp_rec *)
Ralf Jung's avatar
Ralf Jung committed
106
107
108
109
110
111
112
               match goal with
               | |- _  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)
               end;
113
               apply later_mono).
114

115
116
117
118
119
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 "" _ _) _ =>
120
       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
121
122
123
124
125
126
127
128
129
    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.

130
Tactic Notation "wp_op" ">" :=
131
132
133
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
134
135
136
137
    | 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 _ _ _ =>
138
       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
139
    | UnOp _ _ =>
140
       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
141
142
    end)
  end.
143
144
Tactic Notation "wp_op" := wp_op>; wp_strip_later.

145
Tactic Notation "wp_if" ">" :=
146
147
148
149
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
    | If _ _ _ =>
150
       wp_bind K;
151
       etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
152
153
    end)
  end.
154
Tactic Notation "wp_if" := wp_if>; wp_strip_later.
155

156
157
158
159
160
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.
161

162
Tactic Notation "wp" ">" tactic(tac) :=
163
164
165
  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
166
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
167
168

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