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

4
5
6
7
Ltac revert_intros tac :=
  lazymatch goal with
  | |-  _, _ => let H := fresh in intro H; revert_intros tac; revert H
  | |- _ => tac
8
  end.
9
10
11
12
13
14
15
Ltac wp_strip_later :=
  let rec go :=
    lazymatch goal with
    | |- _  (_  _) => apply sep_mono; go
    | |- _   _ => apply later_intro
    | |- _  _ => reflexivity
    end
16
  in revert_intros ltac:(etrans; [|go]).
17

Ralf Jung's avatar
Ralf Jung committed
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
(* 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? *)
Ltac uLock_goal := revert_intros ltac:(apply uPred_lock_conclusion).

(** Transforms a goal of the form  ..., ?0...  ?1  ?2
    into True  ..., ?0...  ?1  ?2, applies tac, and
    the moves all the assumptions back. *)
Ltac uRevert_all :=
  lazymatch goal with
  | |-  _, _ => let H := fresh in intro H; uRevert_all;
                 (* 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.

39
40
41
Ltac wp_bind K :=
  lazymatch eval hnf in K with
  | [] => idtac
42
  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
43
  end.
44
45
46
Ltac wp_finish :=
  let rec go :=
  match goal with
47
  | |- _   _ => etrans; [|apply later_mono; go; reflexivity]
48
  | |- _  wp _ _ _ =>
49
     etrans; [|eapply wp_value_pvs; reflexivity];
50
51
     (* sometimes, we will have to do a final view shift, so only apply
     wp_value if we obtain a consecutive wp *)
52
53
     try (eapply pvs_intro;
          match goal with |- _  wp _ _ _ => simpl | _ => fail end)
54
  | _ => idtac
55
  end in simpl; revert_intros go.
56

Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
Tactic Notation "wp_rec" :=
  uLock_goal; uRevert_all;
  (* 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 _ _ _)); [];
  (* 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. *)
               trans ( (L  R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
               unlock;
               (* Find the redex and apply wp_rec *)
               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;
               apply later_mono
      end
  in go.
85

86
87
88
89
90
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 "" _ _) _ =>
91
       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
92
93
94
95
96
97
98
99
100
    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.

101
Tactic Notation "wp_op" ">" :=
102
103
104
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
105
106
107
108
    | 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 _ _ _ =>
109
       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
110
    | UnOp _ _ =>
111
       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
112
113
    end)
  end.
114
115
Tactic Notation "wp_op" := wp_op>; wp_strip_later.

116
Tactic Notation "wp_if" ">" :=
117
118
119
120
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
    | If _ _ _ =>
121
       wp_bind K;
122
       etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
123
124
    end)
  end.
125
Tactic Notation "wp_if" := wp_if>; wp_strip_later.
126

127
128
129
130
131
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.
132

133
Tactic Notation "wp" ">" tactic(tac) :=
134
135
136
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
  end.
137
Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
138
139

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