tactics.v 14.1 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
(** This file collects general purpose tactics that are used throughout
4
the development. *)
5 6 7
From Coq Require Import Omega.
From Coq Require Export Psatz.
From stdpp Require Export base.
8

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12 13 14 15 16 17 18 19 20 21
Lemma f_equal_dep {A B} (f g :  x : A, B x) x : f = g  f x = g x.
Proof. intros ->; reflexivity. Qed.
Lemma f_equal_help {A B} (f g : A  B) x y : f = g  x = y  f x = g y.
Proof. intros -> ->; reflexivity. Qed.
Ltac f_equal :=
  let rec go :=
    match goal with
    | _ => reflexivity
    | _ => apply f_equal_help; [go|try reflexivity]
    | |- ?f ?x = ?g ?x => apply (f_equal_dep f g); go
    end in
  try go.

22 23 24 25 26
(** We declare hint databases [f_equal], [congruence] and [lia] and containing
solely the tactic corresponding to its name. These hint database are useful in
to be combined in combination with other hint database. *)
Hint Extern 998 (_ = _) => f_equal : f_equal.
Hint Extern 999 => congruence : congruence.
27
Hint Extern 1000 => lia : lia.
Ralf Jung's avatar
Ralf Jung committed
28
Hint Extern 1000 => omega : omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
be very bad, so use with care! *)
31 32 33

(** The tactic [intuition] expands to [intuition auto with *] by default. This
is rather efficient when having big hint databases, or expensive [Hint Extern]
Robbert Krebbers's avatar
Robbert Krebbers committed
34
declarations as the ones above. *)
35 36 37
Tactic Notation "intuition" := intuition auto.

(** A slightly modified version of Ssreflect's finishing tactic [done]. It
38 39 40 41
also performs [reflexivity] and uses symmetry of negated equalities. Compared
to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
unfolding setoid equalities. Note that this tactic performs much better than
Coq's [easy] tactic as it does not perform [inversion]. *)
42 43
Ltac done :=
  trivial; intros; solve
44 45 46
  [ repeat first
    [ solve [trivial]
    | solve [symmetry; trivial]
Robbert Krebbers's avatar
Robbert Krebbers committed
47
    | eassumption
48 49 50 51 52 53
    | reflexivity
    | discriminate
    | contradiction
    | solve [apply not_symmetry; trivial]
    | split ]
  | match goal with H : ¬_ |- _ => solve [destruct H; trivial] end ].
54 55 56
Tactic Notation "by" tactic(tac) :=
  tac; done.

57 58
(** Whereas the [split] tactic splits any inductive with one constructor, the
tactic [split_and] only splits a conjunction. *)
59
Ltac split_and := match goal with |- _  _ => split end.
60
Ltac split_ands := repeat split_and.
61
Ltac split_ands' := repeat (hnf; split_and).
62 63 64 65

(** The tactic [case_match] destructs an arbitrary match in the conclusion or
assumptions, and generates a corresponding equality. This tactic is best used
together with the [repeat] tactical. *)
66 67 68 69 70 71
Ltac case_match :=
  match goal with
  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?
  | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
  end.

72 73 74 75
(** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
the tactic [tac_fail]. *)
Tactic Notation "unless" constr(T) "by" tactic3(tac_fail) :=
  first [assert T by tac_fail; fail 1 | idtac].
76 77 78 79 80 81

(** The tactic [repeat_on_hyps tac] repeatedly applies [tac] in unspecified
order on all hypotheses until it cannot be applied to any hypothesis anymore. *)
Tactic Notation "repeat_on_hyps" tactic3(tac) :=
  repeat match goal with H : _ |- _ => progress tac H end.

82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
(** The tactic [clear dependent H1 ... Hn] clears the hypotheses [Hi] and
their dependencies. *)
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) :=
  clear dependent H1; clear dependent H2.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) :=
  clear dependent H1 H2; clear dependent H3.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) :=
  clear dependent H1 H2 H3; clear dependent H4.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4)
  hyp(H5) := clear dependent H1 H2 H3 H4; clear dependent H5.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
  hyp (H6) := clear dependent H1 H2 H3 H4 H5; clear dependent H6.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
  hyp (H6) hyp(H7) := clear dependent H1 H2 H3 H4 H5 H6; clear dependent H7.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
  hyp (H6) hyp(H7) hyp(H8) :=
  clear dependent H1 H2 H3 H4 H5 H6 H7; clear dependent H8.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
  hyp (H6) hyp(H7) hyp(H8) hyp(H9) :=
  clear dependent H1 H2 H3 H4 H5 H6 H7 H8; clear dependent H9.
Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
  hyp (H6) hyp(H7) hyp(H8) hyp(H9) hyp(H10) :=
  clear dependent H1 H2 H3 H4 H5 H6 H7 H8 H9; clear dependent H10.

(** The tactic [is_non_dependent H] determines whether the goal's conclusion or
107
hypotheses depend on [H]. *)
108 109 110 111 112 113 114
Tactic Notation "is_non_dependent" constr(H) :=
  match goal with
  | _ : context [ H ] |- _ => fail 1
  | |- context [ H ] => fail 1
  | _ => idtac
  end.

115 116
(** The tactic [var_eq x y] fails if [x] and [y] are unequal, and [var_neq]
does the converse. *)
117 118 119
Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.

120 121
(** The tactic [simplify_equality] repeatedly substitutes, discriminates,
and injects equalities, and tries to contradict impossible inequalities. *)
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
Ltac fold_classes :=
  repeat match goal with
  | |- appcontext [ ?F ] =>
    progress match type of F with
    | FMap _ =>
       change F with (@fmap _ F);
       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F)
    | MBind _ =>
       change F with (@mbind _ F);
       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F)
    | OMap _ =>
       change F with (@omap _ F);
       repeat change (@omap _ (@omap _ F)) with (@omap _ F)
    | Alter _ _ _ =>
       change F with (@alter _ _ _ F);
       repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F)
    end
  end.
140 141 142
Ltac fold_classes_hyps H :=
  repeat match type of H with
  | appcontext [ ?F ] =>
143 144
    progress match type of F with
    | FMap _ =>
145 146
       change F with (@fmap _ F) in H;
       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F) in H
147
    | MBind _ =>
148 149
       change F with (@mbind _ F) in H;
       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F) in H
150
    | OMap _ =>
151 152
       change F with (@omap _ F) in H;
       repeat change (@omap _ (@omap _ F)) with (@omap _ F) in H
153
    | Alter _ _ _ =>
154 155
       change F with (@alter _ _ _ F) in H;
       repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F) in H
156 157
    end
  end.
158 159
Tactic Notation "csimpl" "in" hyp(H) :=
  try (progress simpl in H; fold_classes_hyps H).
160
Tactic Notation "csimpl" := try (progress simpl; fold_classes).
161 162
Tactic Notation "csimpl" "in" "*" :=
  repeat_on_hyps (fun H => csimpl in H); csimpl.
163

164 165
Ltac simplify_equality := repeat
  match goal with
166 167 168 169
  | H : _  _ |- _ => by destruct H
  | H : _ = _  False |- _ => by destruct H
  | H : ?x = _ |- _ => subst x
  | H : _ = ?x |- _ => subst x
170
  | H : _ = _ |- _ => discriminate H
171 172
  | H : ?f _ = ?f _ |- _ => apply (inj f) in H
  | H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177 178 179 180
    (* before [injection] to circumvent bug #2939 in some situations *)
  | H : ?f _ = ?f _ |- _ => injection H as H
    (* first hyp will be named [H], subsequent hyps will be given fresh names *)
  | H : ?f _ _ = ?f _ _ |- _ => injection H as H
  | H : ?f _ _ _ = ?f _ _ _ |- _ => injection H as H
  | H : ?f _ _ _ _ = ?f _ _ _ _ |- _ => injection H as H
  | H : ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _ => injection H as H
  | H : ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _ => injection H as H
181
  | H : ?x = ?x |- _ => clear H
182 183 184 185
    (* unclear how to generalize the below *)
  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
    assert (y = x) by congruence; clear H2
  | H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence
186
  end.
187 188
Ltac simplify_equality' := repeat (progress csimpl in * || simplify_equality).
Ltac f_equal' := csimpl in *; f_equal.
189

Robbert Krebbers's avatar
Robbert Krebbers committed
190
Ltac setoid_subst_aux R x :=
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  | H : R x ?y |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197 198 199 200
     is_var x;
     try match y with x _ => fail 2 end;
     repeat match goal with
     | |- context [ x ] => setoid_rewrite H
     | H' : context [ x ] |- _ =>
        try match H' with H => fail 2 end;
        setoid_rewrite H in H'
     end;
201
     clear x H
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204 205
  end.
Ltac setoid_subst :=
  repeat match goal with
  | _ => progress simplify_equality'
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207
  | H : @equiv ?A ?e ?x _ |- _ => setoid_subst_aux (@equiv A e) x
  | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209
  end.

210 211 212 213
(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
runs [tac x] for each element [x] until [tac x] succeeds. If it does not
suceed for any element of the generated list, the whole tactic wil fail. *)
Tactic Notation "iter" tactic(tac) tactic(l) :=
214
  let rec go l :=
215
  match l with ?x :: ?l => tac x || go l end in go l.
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236

(** Given H : [A_1 → ... → A_n → B] (where each [A_i] is non-dependent), the
tactic [feed tac H tac_by] creates a subgoal for each [A_i] and calls [tac p]
with the generated proof [p] of [B]. *)
Tactic Notation "feed" tactic(tac) constr(H) :=
  let rec go H :=
  let T := type of H in
  lazymatch eval hnf in T with
  | ?T1  ?T2 =>
    (* Use a separate counter for fresh names to make it more likely that
    the generated name is "fresh" with respect to those generated before
    calling the [feed] tactic. In particular, this hack makes sure that
    tactics like [let H' := fresh in feed (fun p => pose proof p as H') H] do
    not break. *)
    let HT1 := fresh "feed" in assert T1 as HT1;
      [| go (H HT1); clear HT1 ]
  | ?T1 => tac H
  end in go H.

(** The tactic [efeed tac H] is similar to [feed], but it also instantiates
dependent premises of [H] with evars. *)
237
Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) :=
238 239 240 241 242
  let rec go H :=
  let T := type of H in
  lazymatch eval hnf in T with
  | ?T1  ?T2 =>
    let HT1 := fresh "feed" in assert T1 as HT1;
243
      [bytac | go (H HT1); clear HT1 ]
244 245 246 247 248 249
  | ?T1  _ =>
    let e := fresh "feed" in evar (e:T1);
    let e' := eval unfold e in e in
    clear e; go (H e')
  | ?T1 => tac H
  end in go H.
250 251
Tactic Notation "efeed" constr(H) "using" tactic3(tac) :=
  efeed H using tac by idtac.
252 253 254 255 256 257 258 259 260

(** The following variants of [pose proof], [specialize], [inversion], and
[destruct], use the [feed] tactic before invoking the actual tactic. *)
Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
  feed (fun p => pose proof p as H') H.
Tactic Notation "feed" "pose" "proof" constr(H) :=
  feed (fun p => pose proof p) H.

Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
261
  efeed H using (fun p => pose proof p as H').
262
Tactic Notation "efeed" "pose" "proof" constr(H) :=
263
  efeed H using (fun p => pose proof p).
264 265 266 267

Tactic Notation "feed" "specialize" hyp(H) :=
  feed (fun p => specialize p) H.
Tactic Notation "efeed" "specialize" hyp(H) :=
268
  efeed H using (fun p => specialize p).
269 270 271 272 273 274 275 276 277 278 279 280

Tactic Notation "feed" "inversion" constr(H) :=
  feed (fun p => let H':=fresh in pose proof p as H'; inversion H') H.
Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
  feed (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP) H.

Tactic Notation "feed" "destruct" constr(H) :=
  feed (fun p => let H':=fresh in pose proof p as H'; destruct H') H.
Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
  feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.

(** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
281 282 283 284
particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on collections. The [naive_solver] tactic implements an
ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
mechanism. The tactic suffers from the following limitations:
285
- It might leave unresolved evars as Ltac provides no way to detect that.
286 287
- To avoid the tactic becoming too slow, we allow a universally quantified
  hypothesis to be instantiated only once during each search path.
288 289 290
- It does not perform backtracking on instantiation of universally quantified
  assumptions.

291 292 293 294
We use a counter to make the search breath first. Breath first search ensures
that a minimal number of hypotheses is instantiated, and thus reduced the
posibility that an evar remains unresolved.

295 296 297
Despite these limitations, it works much better than Coq's [firstorder] tactic
for the purposes of this development. This tactic either fails or proves the
goal. *)
298 299 300 301
Lemma forall_and_distr (A : Type) (P Q : A  Prop) :
  ( x, P x  Q x)  ( x, P x)  ( x, Q x).
Proof. firstorder. Qed.

302 303
Tactic Notation "naive_solver" tactic(tac) :=
  unfold iff, not in *;
304 305
  repeat match goal with
  | H : context [ _, _  _ ] |- _ =>
306
    repeat setoid_rewrite forall_and_distr in H; revert H
307
  end;
308
  let rec go n :=
309 310 311 312 313 314 315
  repeat match goal with
  (**i intros *)
  | |-  _, _ => intro
  (**i simplification of assumptions *)
  | H : False |- _ => destruct H
  | H : _  _ |- _ => destruct H
  | H :  _, _  |- _ => destruct H
Robbert Krebbers's avatar
Robbert Krebbers committed
316
  | H : ?P  ?Q, H2 : ?P |- _ => specialize (H H2)
317
  (**i simplify and solve equalities *)
318
  | |- _ => progress simplify_equality'
319
  (**i solve the goal *)
320 321 322 323 324 325
  | |- _ =>
    solve
    [ eassumption
    | symmetry; eassumption
    | apply not_symmetry; eassumption
    | reflexivity ]
326 327 328 329 330 331
  (**i operations that generate more subgoals *)
  | |- _  _ => split
  | H : _  _ |- _ => destruct H
  (**i solve the goal using the user supplied tactic *)
  | |- _ => solve [tac]
  end;
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
  (**i use recursion to enable backtracking on the following clauses. *)
  match goal with
  (**i instantiation of the conclusion *)
  | |-  x, _ => eexists; go n
  | |- _  _ => first [left; go n | right; go n]
  | _ =>
    (**i instantiations of assumptions. *)
    lazymatch n with
    | S ?n' =>
      (**i we give priority to assumptions that fit on the conclusion. *)
      match goal with 
      | H : _  _ |- _ =>
        is_non_dependent H;
        eapply H; clear H; go n'
      | H : _  _ |- _ =>
        is_non_dependent H;
        try (eapply H; fail 2);
        efeed pose proof H; clear H; go n'
      end
    end
  end
  in iter (fun n' => go n') (eval compute in (seq 0 6)).
354
Tactic Notation "naive_solver" := naive_solver eauto.