Library Metatheory_Tactics
We define notations for the equality of variables (our free variables)
and for the equality of naturals (our bound variables represented using
de Bruijn indices).
Notation "x == y" := (eq_var_dec x y) (at level 67).
Notation "i === j" := (Peano_dec.eq_nat_dec i j) (at level 67).
Tactic for comparing two bound or free variables.
Ltac case_nat_base :=
let destr x y := destruct (x === y); [try subst x | idtac] in
match goal with
| H: context [?x === ?y] |- _ => destr x y
| |- context [?x === ?y] => destr x y
end.
Tactic Notation "case_nat" :=
case_nat_base;
try solve [ match goal with H: ?x <> ?x |- _ =>
false_goal; apply H; reflexivity end ].
Tactic Notation "case_nat" "~" := case_nat; auto_tilde.
Tactic Notation "case_nat" "*" := case_nat; auto_star.
Ltac case_var_base :=
let destr x y := destruct (x == y); [try subst x | idtac] in
match goal with
| H: context [?x == ?y] |- _ => destr x y
| |- context [?x == ?y] => destr x y
end.
Tactic Notation "case_var" :=
case_var_base; try solve [ notin_false ].
Tactic Notation "case_var" "~" := case_var; auto_tilde.
Tactic Notation "case_var" "*" := case_var; auto_star.
gather_vars_for_type T F return the union of all the finite sets
of variables F x where x is a variable from the context such that
F x type checks. In other words x has to be of the type of the
argument of F. The resulting union of sets does not contain any
duplicated item. This tactic is an extreme piece of hacking necessary
because the tactic language does not support a "fold" operation on
the context.
Ltac gather_vars_with F :=
let rec gather V :=
match goal with
| H: ?S |- _ =>
let FH := constr:(F H) in
match V with
| {} => gather FH
| context [FH] => fail 1
| _ => gather (FH \u V)
end
| _ => V
end in
let L := gather {} in eval simpl in L.
beautify_fset V assumes that V is built as a union of finite
sets and return the same set cleaned up: empty sets are removed and
items are laid out in a nicely parenthesized way
Ltac beautify_fset V :=
let rec go Acc E :=
match E with
| ?E1 \u ?E2 => let Acc1 := go Acc E1 in
go Acc1 E2
| {} => Acc
| ?E1 => match Acc with
| {} => E1
| _ => constr:(Acc \u E1)
end
end
in go {} V.
pick_fresh_gen L Y expects L to be a finite set of variables
and adds to the context a variable with name Y and a proof that
Y is fresh for L.
Ltac pick_fresh_gen L Y :=
let Fr := fresh "Fr" in
let L := beautify_fset L in
(destruct (var_fresh L) as [Y Fr]).
pick_fresh_gens L n Y expects L to be a finite set of variables
and adds to the context a list of variables with name Y and a proof
that Y is of length n and contains variable fresh for L and
distinct from one another.
Ltac pick_freshes_gen L n Y :=
let Fr := fresh "Fr" in
let L := beautify_fset L in
(destruct (var_freshes L n) as [Y Fr]).
apply_fresh_base tactic is a helper to build tactics that apply an
inductive constructor whose first argument should be instanciated
by the set of names already used in the context. Those names should
be returned by the gather tactic given in argument. For each premise
of the inductive rule starting with an universal quantification of names
outside the set of names instanciated, a subgoal with be generated by
the application of the rule, and in those subgoal we introduce the name
quantified as well as its proof of freshness.
Ltac apply_fresh_base_simple lemma gather :=
let L0 := gather in let L := beautify_fset L0 in
first [apply (@lemma L) | eapply (@lemma L)].
Ltac intros_fresh x :=
first [
let Fr := fresh "Fr" x in
intros x Fr
| let x2 :=
match goal with |- forall _:?T, _ =>
match T with
| var => fresh "y"
| vars => fresh "ys"
| list var => fresh "ys"
| _ => fresh "y"
end end in
let Fr := fresh "Fr" x2 in
intros x2 Fr ].
Ltac apply_fresh_base lemma gather var_name :=
apply_fresh_base_simple lemma gather;
try (match goal with
| |- forall _:_, _ \notin _ -> _ => intros_fresh var_name
| |- forall _:_, fresh _ _ _ -> _ => intros_fresh var_name
end).
exists_fresh_gen G y Fry picks a variable y fresh from
the current context. Fry is the name of the freshness
hypothesis, and G is the local tactic gather_vars.
Ltac exists_fresh_gen G y Fry :=
let L := G in exists L; intros y Fry.
do_rew is used to perform the sequence:
rewrite the goal, execute a tactic, rewrite the goal back
Tactic Notation "do_rew" constr(E) tactic(T) :=
rewrite <- E; T; try rewrite E.
Tactic Notation "do_rew" "<-" constr(E) tactic(T) :=
rewrite E; T; try rewrite <- E.
Tactic Notation "do_rew" "*" constr(E) tactic(T) :=
rewrite <- E; T; auto*; try rewrite* E.
Tactic Notation "do_rew" "*" "<-" constr(E) tactic(T) :=
rewrite E; T; auto*; try rewrite* <- E.
do_rew_2 is the same as do_rew but it does rewrite twice
Tactic Notation "do_rew_2" constr(E) tactic(T) :=
do 2 rewrite <- E; T; try do 2 rewrite E.
Tactic Notation "do_rew_2" "<-" constr(E) tactic(T) :=
do 2 rewrite E; T; try do 2 rewrite <- E.
do_rew_all is the same as do_rew but it does rewrite twice
Tactic Notation "do_rew_all" constr(E) tactic(T) :=
rewrite_all <- E; T; try rewrite_all E.
Tactic Notation "do_rew_all" "<-" constr(E) tactic(T) :=
rewrite_all E; T; try rewrite_all <- E.
Inductive list_forall (A : Set) (P : A -> Prop) : list A -> Prop :=
| list_forall_nil : list_forall P nil
| list_forall_cons : forall L x, list_forall P L -> P x -> list_forall P (x::L).
Hint Constructors list_forall.
Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) :=
n = length L /\ list_forall P L.
Hint Extern 1 (?n = length ?xs) =>
match goal with H: list_for_n _ ?n ?xs |- _ =>
apply (proj1 H) end.
Hint Extern 1 (length ?xs = ?n) =>
match goal with H: list_for_n _ ?n ?xs |- _ =>
apply (sym_eq (proj1 H)) end.
inst_notin H y as H' expects H to be of the form
forall x, x \notin L, P x and creates an hypothesis H'
of type P y. It tries to prove the subgoal y \notin L
by auto. This tactic is very useful to apply induction
hypotheses given in the cases with binders.
Tactic Notation "inst_notin" constr(lemma) constr(var)
"as" ident(hyp_name) :=
let go L := let Fr := fresh in assert (Fr : var \notin L);
[ notin_solve | lets hyp_name: (@lemma var Fr); clear Fr ] in
match type of lemma with
forall _, _ \notin ?L -> _ => go L end.
Tactic Notation "inst_notin" "~" constr(lemma) constr(var)
"as" ident(hyp_name) :=
inst_notin lemma var as hyp_name; auto_tilde.
Tactic Notation "inst_notin" "*" constr(lemma) constr(var)
"as" ident(hyp_name) :=
inst_notin lemma var as hyp_name; auto_star.
Ltac fresh_simpl_to_notin_in_context :=
repeat (match goal with H: fresh _ _ _ |- _ =>
progress (simpl in H; destructs H) end).
Ltac contradictions :=
assert False; [ try discriminate | contradiction ].
Ltac notin_solve :=
fresh_simpl_to_notin_in_context;
notin_simpl; notin_solve_one.
Ltac notin_contradiction :=
match goal with H: ?x \notin ?E |- _ =>
match E with context[x] =>
let K := fresh in assert (K : x \notin {{x}});
[ notin_solve_one
| contradictions; apply (notin_same K) ]
end
end.
Ltac simpl_subset :=
try rewrite union_empty_r ; try rewrite union_empty_l ; try apply subset_refl ; try apply subset_empty_l ;
try apply subset_union_weak_l ; try apply subset_union_weak_r.