(************************************************************************** * TLC: A library for Coq * * Library for locally nameless developments * **************************************************************************) Set Implicit Arguments. Require Import LibList. Require Export LibTactics LibProd LibLogic LibVar LibEnv. Open Scope fset_scope. Open Scope env_scope. (* ********************************************************************** *) (** ** Case analysis on variables and indices *) (** [case_if_eq E F] performs a case analysis to test whether [E = F] or [E <> F]. It is used to implement the following two tactics. *) Ltac case_if_eq_base E F H := destruct (classicT (E = F)) as [H|H]; [tryfalse; try subst E | tryfalse ]. Tactic Notation "case_if_eq" constr(E) constr(F) "as" ident(H) := case_if_eq_base E F H. Tactic Notation "case_if_eq" constr(E) constr(F) := let C := fresh "C" in case_if_eq E F as C. (** [case_nat] performs a case analysis to analyse a If-statement comparing two natural numbers for equality. The If-statement is searched for first in the hypotheses then it the goal. *) Ltac case_if_eq_nat := match goal with | H: context [classicT(?x = ?y :> nat)] |- _ => case_if_eq x y | |- context [classicT(?x = ?y :> nat)] => case_if_eq x y end. Tactic Notation "case_nat" := case_if_eq_nat. Tactic Notation "case_nat" "~" := case_nat; auto_tilde. Tactic Notation "case_nat" "*" := case_nat; auto_star. (** [case_var] performs a case analysis to analyse a If-statement comparing two variables for equality. The If-statement is searched for first in the hypotheses then it the goal. *) Ltac case_if_eq_var := match goal with | H: context [classicT(?x = ?y :> var)] |- _ => case_if_eq x y | |- context [classicT(?x = ?y :> var)] => case_if_eq x y end. Tactic Notation "case_var" := case_if_eq_var; try solve [ notin_false ]. Tactic Notation "case_var" "~" := case_var; auto_tilde. Tactic Notation "case_var" "*" := case_var; auto_star. (* ********************************************************************** *) (** ** Applying lemmas with quantification over cofinite sets *) (** [apply_fresh_base] tactic is a helper to build tactics that apply an inductive constructor whose first argument should be instantiated 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 instantiated, 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. (* ********************************************************************** *) (** * Applying lemma modulo a simple rewriting *) (** [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 like [do_rew] but it rewrites 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 like [do_rew] but rewrites as many times as possible *) 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. (* ********************************************************************** *) (** ** Tactics for applying lemmas on empty environments *) (** Tactic to apply an induction hypothesis modulo a rewrite of the associativity of the environment necessary to handle the inductive rules dealing with binders. [apply_ih_bind] is in fact just a syntactical sugar for [do_rew concat_assoc (eapply H)] which stands for [rewrite concat_assoc; eapply H; rewrite <- concat_assoc]. *) Tactic Notation "apply_ih_bind" constr(H) := do_rew concat_assoc (applys H). Tactic Notation "apply_ih_bind" "*" constr(H) := do_rew* concat_assoc (applys H). (** Similar as the above, except in the case where there is also a map function, so we need to use [concat_assoc_map_push] for rewriting. *) Tactic Notation "apply_ih_map_bind" constr(H) := do_rew concat_assoc_map_push (applys H); try solve [ rewrite concat_assoc; reflexivity ]. Tactic Notation "apply_ih_map_bind" "*" constr(H) := do_rew* concat_assoc_map_push (applys H); try solve [ rewrite concat_assoc; reflexivity ]. (** [clean_empty H] simplifies terms in H terms of the form [map f empty] and of the form [E & empty] *) Tactic Notation "clean_empty" hyp(H) := repeat (match type of H with context [map ?f empty] => rewrite (map_empty f) in H end); repeat (match type of H with context [?E & empty] => rewrite (concat_empty_r E) in H end). (** [apply_empty] applies a lemma of the form "forall E:env, P E" in the particular case where E is empty. The tricky step is the simplification of "P empty" before the "apply" tactic is called, and this is necessary for Coq to recognize that the lemma indeed applies. *) Ltac apply_empty_base H := let M := fresh "TEMP" in lets M: (@H empty); specializes_vars M; clean_empty M; first [ apply M | eapply M | applys M ]; clear M. Tactic Notation "apply_empty" constr(H) := apply_empty_base H. Tactic Notation "apply_empty" "~" constr(H) := apply_empty H; auto_tilde. Tactic Notation "apply_empty" "*" constr(H) := apply_empty H; auto_star. (* ********************************************************************** *) (** * Some results on lists *) (** We use [List.nth] instead of [LibList.nth] so that we can have control over the default value returned in case of invalid index *) Lemma list_map_nth : forall A (f : A -> A) (d : A) (l : list A) (n : nat), f d = d -> f (List.nth n l d) = List.nth n (LibList.map f l) d. Proof. induction l; introv E; destruct n; simpl; auto. Qed. (** Property over lists of given length *) Hint Constructors Forall. Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) := n = length L /\ Forall P L. Lemma list_for_n_concat : forall (A : Set) (P : A -> Prop) n1 n2 L1 L2, list_for_n P n1 L1 -> list_for_n P n2 L2 -> list_for_n P (n1+n2) (L1 ++ L2). Proof. unfold list_for_n. introv [? ?] [? ?]. split. rew_length~. apply* Forall_app. Qed. 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. (* ********************************************************************** *) (** * Misc *) (* Due to a parsing conflict between the syntax of tactics and the symbol [~:] which is used to write typing judgments in many developments, we need to rebind a few tactics in a slightly different way. *) Tactic Notation "forwards" "~:" constr(E) := forwards ~ : E. Tactic Notation "tests" "~:" constr(E) := tests ~ : E. |