wp_tactics.v 5.59 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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(** 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. *)
Ltac uLöb tac :=
  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 _ _ _); 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. *)
               trans ( (L  R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
               unlock; tac
      end
  in go.

64
65
66
Ltac wp_bind K :=
  lazymatch eval hnf in K with
  | [] => idtac
67
  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
68
  end.
69
70
71
Ltac wp_finish :=
  let rec go :=
  match goal with
72
  | |- _   _ => etrans; [|apply later_mono; go; reflexivity]
73
  | |- _  wp _ _ _ =>
74
     etrans; [|eapply wp_value_pvs; reflexivity];
75
76
     (* sometimes, we will have to do a final view shift, so only apply
     wp_value if we obtain a consecutive wp *)
77
78
     try (eapply pvs_intro;
          match goal with |- _  wp _ _ _ => simpl | _ => fail end)
79
  | _ => idtac
80
  end in simpl; revert_intros go.
81

Ralf Jung's avatar
Ralf Jung committed
82
Tactic Notation "wp_rec" :=
83
  uLöb ltac:((* Find the redex and apply wp_rec *)
Ralf Jung's avatar
Ralf Jung committed
84
85
86
87
88
89
90
               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;
91
               apply later_mono).
92

93
94
95
96
97
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 "" _ _) _ =>
98
       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
99
100
101
102
103
104
105
106
107
    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.

108
Tactic Notation "wp_op" ">" :=
109
110
111
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
112
113
114
115
    | 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 _ _ _ =>
116
       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
117
    | UnOp _ _ =>
118
       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
119
120
    end)
  end.
121
122
Tactic Notation "wp_op" := wp_op>; wp_strip_later.

123
Tactic Notation "wp_if" ">" :=
124
125
126
127
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval cbv in e' with
    | If _ _ _ =>
128
       wp_bind K;
129
       etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
130
131
    end)
  end.
132
Tactic Notation "wp_if" := wp_if>; wp_strip_later.
133

134
135
136
137
138
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.
139

140
Tactic Notation "wp" ">" tactic(tac) :=
141
142
143
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
  end.
144
Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
145
146

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