wp_tactics.v 5.68 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
(** 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. *)
59
60
               trans ( L   R)%I; first (apply sep_mono_l, later_intro; reflexivity);
               trans ( (L  R))%I; first (apply equiv_spec, later_sep; reflexivity );
61
62
63
64
               unlock; tac
      end
  in go.

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

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

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

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

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

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

141
Tactic Notation "wp" ">" tactic(tac) :=
142
143
144
  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
145
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
146
147

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