tactics.v 15 KB
 Robbert Krebbers committed Nov 11, 2015 1 2 3 4 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects general purpose tactics that are used throughout the development. *) `````` Robbert Krebbers committed Feb 13, 2016 5 6 7 ``````From Coq Require Import Omega. From Coq Require Export Psatz. From prelude Require Export base. `````` Robbert Krebbers committed Nov 11, 2015 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 `````` 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. (** 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. Hint Extern 1000 => lia : lia. `````` Ralf Jung committed Feb 02, 2016 28 ``````Hint Extern 1000 => omega : omega. `````` Robbert Krebbers committed Feb 08, 2016 29 30 ``````Hint Extern 1001 => progress subst : subst. (** backtracking on this one will be very bad, so use with care! *) `````` Robbert Krebbers committed Nov 11, 2015 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 committed Feb 08, 2016 34 ``````declarations as the ones above. *) `````` Robbert Krebbers committed Nov 11, 2015 35 36 37 38 39 40 41 42 43 44 45 46 ``````Tactic Notation "intuition" := intuition auto. (** A slightly modified version of Ssreflect's finishing tactic [done]. It 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]. *) Ltac done := trivial; intros; solve [ repeat first [ solve [trivial] | solve [symmetry; trivial] `````` Robbert Krebbers committed Feb 14, 2016 47 `````` | eassumption `````` Robbert Krebbers committed Nov 11, 2015 48 49 50 51 52 53 54 55 56 `````` | reflexivity | discriminate | contradiction | solve [apply not_symmetry; trivial] | split ] | match goal with H : ¬_ |- _ => solve [destruct H; trivial] end ]. Tactic Notation "by" tactic(tac) := tac; done. `````` Ralf Jung committed Feb 20, 2016 57 58 59 60 ``````(** Aliases for trans and etrans that are easier to type *) Tactic Notation "trans" constr(A) := transitivity A. Tactic Notation "etrans" := etransitivity. `````` Robbert Krebbers committed Feb 19, 2016 61 62 63 64 65 66 67 68 69 70 71 72 73 74 ``````(** Tactics for splitting conjunctions: - [split_and] : split the goal if is syntactically of the shape [_ ∧ _] - [split_ands?] : split the goal repeatedly (perhaps zero times) while it is of the shape [_ ∧ _]. - [split_ands!] : works similarly, but at least one split should succeed. In order to do so, it will head normalize the goal first to possibly expose a conjunction. Note that [split_and] differs from [split] by only splitting conjunctions. The [split] tactic splits any inductive with one constructor. *) Tactic Notation "split_and" := match goal with |- _ ∧ _ => split end. Tactic Notation "split_and" "?" := repeat split_and. Tactic Notation "split_and" "!" := hnf; split_and; split_and?. `````` Robbert Krebbers committed Nov 11, 2015 75 76 77 78 79 80 81 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 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 `````` (** 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. *) Ltac case_match := match goal with | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:? | |- context [ match ?x with _ => _ end ] => destruct x eqn:? end. (** 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]. (** 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. (** 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 hypotheses depend on [H]. *) Tactic Notation "is_non_dependent" constr(H) := match goal with | _ : context [ H ] |- _ => fail 1 | |- context [ H ] => fail 1 | _ => idtac end. (** The tactic [var_eq x y] fails if [x] and [y] are unequal, and [var_neq] does the converse. *) 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. `````` Robbert Krebbers committed Feb 17, 2016 133 134 135 136 137 138 139 ``````(** Operational type class projections in recursive calls are not folded back appropriately by [simpl]. The tactic [csimpl] uses the [fold_classes] tactics to refold recursive calls of [fmap], [mbind], [omap] and [alter]. A self-contained example explaining the problem can be found in the following Coq-club message: https://sympa.inria.fr/sympa/arc/coq-club/2012-10/msg00147.html *) `````` Robbert Krebbers committed Nov 11, 2015 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 ``````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. Ltac fold_classes_hyps H := repeat match type of H with | appcontext [ ?F ] => progress match type of F with | FMap _ => change F with (@fmap _ F) in H; repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F) in H | MBind _ => change F with (@mbind _ F) in H; repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F) in H | OMap _ => change F with (@omap _ F) in H; repeat change (@omap _ (@omap _ F)) with (@omap _ F) in H | Alter _ _ _ => change F with (@alter _ _ _ F) in H; repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F) in H end end. Tactic Notation "csimpl" "in" hyp(H) := try (progress simpl in H; fold_classes_hyps H). Tactic Notation "csimpl" := try (progress simpl; fold_classes). Tactic Notation "csimpl" "in" "*" := repeat_on_hyps (fun H => csimpl in H); csimpl. `````` Robbert Krebbers committed Feb 17, 2016 182 ``````(** The tactic [simplify_eq] repeatedly substitutes, discriminates, `````` Robbert Krebbers committed Feb 17, 2016 183 184 ``````and injects equalities, and tries to contradict impossible inequalities. *) Tactic Notation "simplify_eq" := repeat `````` Robbert Krebbers committed Nov 11, 2015 185 186 187 188 189 190 `````` match goal with | H : _ ≠ _ |- _ => by destruct H | H : _ = _ → False |- _ => by destruct H | H : ?x = _ |- _ => subst x | H : _ = ?x |- _ => subst x | H : _ = _ |- _ => discriminate H `````` Robbert Krebbers committed Feb 11, 2016 191 192 `````` | H : ?f _ = ?f _ |- _ => apply (inj f) in H | H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H `````` Robbert Krebbers committed Feb 17, 2016 193 194 195 196 197 198 199 200 `````` (* 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 `````` Robbert Krebbers committed Nov 11, 2015 201 202 203 204 205 206 `````` | H : ?x = ?x |- _ => clear H (* 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 end. `````` Robbert Krebbers committed Feb 17, 2016 207 208 209 ``````Tactic Notation "simplify_eq" "/=" := repeat (progress csimpl in * || simplify_eq). Tactic Notation "f_equal" "/=" := csimpl in *; f_equal. `````` Robbert Krebbers committed Nov 11, 2015 210 `````` `````` Robbert Krebbers committed Nov 17, 2015 211 ``````Ltac setoid_subst_aux R x := `````` Robbert Krebbers committed Nov 11, 2015 212 `````` match goal with `````` Robbert Krebbers committed Nov 17, 2015 213 `````` | H : R x ?y |- _ => `````` Robbert Krebbers committed Nov 11, 2015 214 215 216 217 218 219 220 221 `````` 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; `````` Robbert Krebbers committed Jan 18, 2016 222 `````` clear x H `````` Robbert Krebbers committed Nov 11, 2015 223 224 225 `````` end. Ltac setoid_subst := repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 226 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Jan 16, 2016 227 228 `````` | 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 committed Nov 11, 2015 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 `````` end. (** 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) := let rec go l := match l with ?x :: ?l => tac x || go l end in go l. (** 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. *) Tactic Notation "efeed" constr(H) "using" tactic3(tac) "by" tactic3 (bytac) := 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; [bytac | go (H HT1); clear HT1 ] | ?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. Tactic Notation "efeed" constr(H) "using" tactic3(tac) := efeed H using tac by idtac. (** 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') := efeed H using (fun p => pose proof p as H'). Tactic Notation "efeed" "pose" "proof" constr(H) := efeed H using (fun p => pose proof p). Tactic Notation "feed" "specialize" hyp(H) := feed (fun p => specialize p) H. Tactic Notation "efeed" "specialize" hyp(H) := efeed H using (fun p => specialize p). 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 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: - It might leave unresolved evars as Ltac provides no way to detect that. - To avoid the tactic becoming too slow, we allow a universally quantified hypothesis to be instantiated only once during each search path. - It does not perform backtracking on instantiation of universally quantified assumptions. 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. 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. *) Lemma forall_and_distr (A : Type) (P Q : A → Prop) : (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x). Proof. firstorder. Qed. Tactic Notation "naive_solver" tactic(tac) := unfold iff, not in *; repeat match goal with | H : context [∀ _, _ ∧ _ ] |- _ => repeat setoid_rewrite forall_and_distr in H; revert H end; let rec go n := repeat match goal with (**i intros *) | |- ∀ _, _ => intro (**i simplification of assumptions *) | H : False |- _ => destruct H | H : _ ∧ _ |- _ => destruct H | H : ∃ _, _ |- _ => destruct H `````` Robbert Krebbers committed Jan 12, 2016 337 `````` | H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2) `````` Robbert Krebbers committed Nov 11, 2015 338 `````` (**i simplify and solve equalities *) `````` Robbert Krebbers committed Feb 17, 2016 339 `````` | |- _ => progress simplify_eq/= `````` Robbert Krebbers committed Nov 11, 2015 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 `````` (**i solve the goal *) | |- _ => solve [ eassumption | symmetry; eassumption | apply not_symmetry; eassumption | reflexivity ] (**i operations that generate more subgoals *) | |- _ ∧ _ => split | H : _ ∨ _ |- _ => destruct H (**i solve the goal using the user supplied tactic *) | |- _ => solve [tac] end; (**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)). Tactic Notation "naive_solver" := naive_solver eauto.``````