diff options
| -rw-r--r-- | CHANGES | 11 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 58 |
2 files changed, 69 insertions, 0 deletions
@@ -9,6 +9,17 @@ Tactic Language - Second-order pattern-matching now working in Ltac "match" clauses (syntax for second-order unification variable is "@?X"). - Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer) +- The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]" + is extended so that at most one expr_i may have the form "expr .." + or just "..". Also, n can be different from the number of subgoals + generated by expr_0. In this case, the value of expr (or idtac in + case of just "..") is applied to the intermediate subgoals to make + the number of tactics equal to the number of subgoals. + +Tactics + +- New tactics [apply -> term], [apply <- term], [apply -> term in + ident], [apply <- term in ident] for applying equivalences (iff). Changes from V8.1gamma to V8.1 ============================== diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 78e35b11d..f45b541bc 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -68,3 +68,61 @@ Ltac remembertac x a := (set (x:=a) in *; assert (H: x=a) by reflexivity; clearbody x). Tactic Notation "remember" constr(c) "as" ident(x) := remembertac x c. + +(** Tactics for applying equivalences. + +The following code provides tactics "apply -> t", "apply <- t", +"apply -> t in H" and "apply <- t in H". Here t is a term whose type +consists of nested dependent and nondependent products with an +equivalence A <-> B as the conclusion. The tactics with "->" in their +names apply A -> B while those with "<-" in the name apply B -> A. *) + +(* The idea of the tactics is to first provide a term in the context +whose type is the implication (in one of the directions), and then +apply it. The first idea is to produce a statement "forall ..., A -> +B" (call this type T) and then do "assert (H : T)" for a fresh H. +Thus, T can be proved from the original equivalence and then used to +perform the application. However, currently in Ltac it is difficult +to produce such T from the original formula. + +Therefore, we first pose the original equivalence as H. If the type of +H is a dependent product, we create an existential variable and apply +H to this variable. If the type of H has the form C -> D, then we do a +cut on C. Once we eliminate all products, we split (i.e., destruct) +the conjunction into two parts and apply the relevant one. *) + +Ltac find_equiv H := +let T := type of H in +lazymatch T with +| ?A -> ?B => + let H1 := fresh in + let H2 := fresh in + cut A; + [intro H1; pose proof (H H1) as H2; clear H H1; + rename H2 into H; find_equiv H | + clear H] +| forall x : ?t, _ => + let a := fresh "a" with + H1 := fresh "H" in + evar (a : t); pose proof (H a) as H1; unfold a in H1; + clear a; clear H; rename H1 into H; find_equiv H +| ?A <-> ?B => idtac +| _ => fail "The given statement does not seem to end with an equivalence" +end. + +Ltac bapply lemma todo := +let H := fresh in + pose proof lemma as H; + find_equiv H; [todo H; clear H | .. ]. + +Tactic Notation "apply" "->" constr(lemma) := +bapply lemma ltac:(fun H => destruct H as [H _]; apply H). + +Tactic Notation "apply" "<-" constr(lemma) := +bapply lemma ltac:(fun H => destruct H as [_ H]; apply H). + +Tactic Notation "apply" "->" constr(lemma) "in" ident(J) := +bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J). + +Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) := +bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J). |