(* 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. *)
From Coq Require Import Omega.
From Coq Require Export Psatz.
From prelude Require Export base.
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.
Hint Extern 1000 => omega : omega.
Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
be very bad, so use with care! *)
(** The tactic [intuition] expands to [intuition auto with *] by default. This
is rather efficient when having big hint databases, or expensive [Hint Extern]
declarations as the ones above. *)
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]
| eassumption
| 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.
(** Aliases for trans and etrans that are easier to type *)
Tactic Notation "trans" constr(A) := transitivity A.
Tactic Notation "etrans" := etransitivity.
(** 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?.
(** 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.
(** 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 *)
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.
(** The tactic [simplify_eq] repeatedly substitutes, discriminates,
and injects equalities, and tries to contradict impossible inequalities. *)
Tactic Notation "simplify_eq" := repeat
match goal with
| H : _ ≠ _ |- _ => by destruct H
| H : _ = _ → False |- _ => by destruct H
| H : ?x = _ |- _ => subst x
| H : _ = ?x |- _ => subst x
| H : _ = _ |- _ => discriminate H
| H : ?f _ = ?f _ |- _ => apply (inj f) in H
| H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H
(* 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
| 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.
Tactic Notation "simplify_eq" "/=" :=
repeat (progress csimpl in * || simplify_eq).
Tactic Notation "f_equal" "/=" := csimpl in *; f_equal.
Ltac setoid_subst_aux R x :=
match goal with
| H : R x ?y |- _ =>
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;
clear x H
end.
Ltac setoid_subst :=
repeat match goal with
| _ => progress simplify_eq/=
| 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
end.
(** f_equiv solves goals of the form "f _ = f _", for any relation and any
number of arguments, by looking for appropriate "Proper" instances.
If it cannot solve an equality, it will leave that to the user. *)
Ltac f_equiv :=
(* Deal with "pointwise_relation" *)
try lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
end;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
first [ reflexivity | assumption | symmetry; assumption |
match goal with
(* We support matches on both sides, *if* they concern the same
or provably equal variables.
TODO: We should support different variables, provided that we can
derive contradictions for the off-diagonal cases. *)
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
destruct x; f_equiv
| |- ?R (match ?x with _ => _ end) (match ?y with _ => _ end) =>
subst y; f_equiv
(* First assume that the arguments need the same relation as the result *)
| |- ?R (?f ?x) (?f _) =>
let H := fresh "Proper" in
assert (Proper (R ==> R) f) as H by (eapply _);
apply H; clear H; f_equiv
| |- ?R (?f ?x ?y) (?f _ _) =>
let H := fresh "Proper" in
assert (Proper (R ==> R ==> R) f) as H by (eapply _);
apply H; clear H; f_equiv
(* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *)
(* TODO: If some of the arguments are the same, we could also
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)
| |- ?R (?f ?x) (?f _) =>
let R1 := fresh "R" in let H := fresh "HProp" in
let T := type of x in evar (R1: relation T);
assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _);
subst R1; apply H; clear H; f_equiv
| |- ?R (?f ?x ?y) (?f _ _) =>
let R1 := fresh "R" in let R2 := fresh "R" in
let H := fresh "HProp" in
let T1 := type of x in evar (R1: relation T1);
let T2 := type of y in evar (R2: relation T2);
assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _);
subst R1 R2; apply H; clear H; f_equiv
(* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *)
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) =>
apply H; f_equiv
end | idtac (* Let the user solve this goal *)
].
(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
number of relations. All the actual work is done by f_equiv;
solve_proper just introduces the assumptions and unfolds the first
head symbol. *)
Ltac solve_proper :=
(* Introduce everything *)
intros;
repeat lazymatch goal with
| |- Proper _ _ => intros ???
| |- (_ ==> _)%signature _ _ => intros ???
end;
(* Unfold the head symbol, which is the one we are proving a new property about *)
lazymatch goal with
| |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
| |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
| |- ?R (?f _ _ _) (?f _ _ _) => unfold f
| |- ?R (?f _ _) (?f _ _) => unfold f
| |- ?R (?f _) (?f _) => unfold f
end;
solve [ f_equiv ].
(** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *)
Ltac intros_revert tac :=
lazymatch goal with
| |- ∀ _, _ => let H := fresh in intro H; intros_revert tac; revert H
| |- _ => tac
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.
(** The following tactic can be used to add support for patterns to tactic notation:
It will search for the first subterm of the goal matching [pat], and then call [tac]
with that subterm. *)
Ltac find_pat pat tac :=
match goal with |- context [?x] =>
unify pat x; tryif tac x then idtac else fail 2
end.
(** 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.
(** The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
creates any new evars. This trick is by Jonathan Leivent, see:
https://coq.inria.fr/bugs/show_bug.cgi?id=3872 *)
Ltac no_new_unsolved_evars tac := exact ltac:(tac).
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
| H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
(**i simplify and solve equalities *)
| |- _ => progress simplify_eq/=
(**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, _ => no_new_unsolved_evars ltac:(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;
no_new_unsolved_evars
ltac:(first [eapply H | efeed pose proof H]; clear H; go n')
end
end
end
in iter (fun n' => go n') (eval compute in (seq 1 6)).
Tactic Notation "naive_solver" := naive_solver eauto.