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