From 224c374eb4460b577aa3e89cf65d42563b6dace6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Feb 2006 17:43:11 +0000 Subject: [PATCH] New tactics (badly) documented. --- helm/software/matita/help/C/sec_tactics.xml | 262 +++++++++++++++++++- 1 file changed, 252 insertions(+), 10 deletions(-) diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index fda93f0b3..caee727a4 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -346,7 +346,7 @@ Pre-conditions: - p must have type K1 t1 ... tn = K'1 t'1 ... t'm where K and K' must be different constructors of the same inductive type and each argument list can be empty if + p must have type K t1 ... tn = K' t'1 ... t'm where K and K' must be different constructors of the same inductive type and each argument list can be empty if its constructor takes no arguments. @@ -604,42 +604,258 @@ its constructor takes no arguments. generalize <pattern> [as <id>] generalize - The tactic generalize + generalize patt as H + + + + Pre-conditions: + + all the terms matched by patt must be + convertible and close in the context of the current sequent. + + + + Action: + + it closes the current sequent by applying a stronger + lemma that is proved using the new generated sequent. + + + + New sequents to prove: + + it opens a new sequent where the current sequent conclusion + G is generalized to + ∀x.G{x/t} where {x/t} + is a notation for the replacement with x of all + the occurrences of the term t matched by + patt. If patt matches no + subterm then t is defined as the + wanted part of the pattern. + + + + id id - The tactic id + absurd P + + + + Pre-conditions: + + none. + + + + Action: + + this identity tactic does nothing without failing. + + + + New sequents to prove: + + none. + + + + injection <term> injection - The tactic injection + injection p + + + + Pre-conditions: + + p must have type K t1 ... tn = K t'1 ... t'n where both argument lists are empty if +K takes no arguments. + + + + Action: + + it derives new hypotheses by injectivity of + K. + + + + New sequents to prove: + + the new sequent to prove is equal to the current sequent + with the additional hypotheses + t1=t'1 ... tn=t'n. + + + + intro [<ident>] intro - The tactic intro + intro H + + + + Pre-conditions: + + the conclusion of the sequent to prove must be an implication + or a universal quantification. + + + + Action: + + it applies the right introduction rule for implication, + closing the current sequent. + + + + New sequents to prove: + + it opens a new sequent to prove adding to the hypothesis + the antecedent of the implication and setting the conclusion + to the consequent of the implicaiton. The name of the new + hypothesis is H if provided; otherwise it + is automatically generated. + + + + intros <intros_spec> intros - The tactic intros + intros hyps + + + + Pre-conditions: + + If hyps specifies a number of hypotheses + to introduce, then the conclusion of the current sequent must + be formed by at least that number of imbricated implications + or universal quantifications. + + + + Action: + + it applies several times the right introduction rule for + implication, closing the current sequent. + + + + New sequents to prove: + + it opens a new sequent to prove adding a number of new + hypotheses equal to the number of new hypotheses requested. + If the user does not request a precise number of new hypotheses, + it adds as many hypotheses as possible. + The name of each new hypothesis is either popped from the + user provided list of names, or it is automatically generated when + the list is (or becomes) empty. + + + + inversion <term> inversion - The tactic inversion + inversion t + + + + Pre-conditions: + + the type of the term t must be an inductive + type or the application of an inductive type. + + + + Action: + + it proceeds by cases on t paying attention + to the constraints imposed by the actual "right arguments" + of the inductive type. + + + + New sequents to prove: + + it opens one new sequent to prove for each case in the + definition of the type of t. With respect to + a simple elimination, each new sequent has additional hypotheses + that states the equalities of the "right parameters" + of the inductive type with terms originally present in the + sequent to prove. + + + + lapply [depth=<int>] <term> [to <term list] [using <ident>] lapply - The tactic lapply + lapply ??? + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + left left - The tactic left + left + + + + Pre-conditions: + + the conclusion of the current sequent must be + an inductive type or the application of an inductive type. + + + + Action: + + equivalent to constructor 1. + + + + New sequents to prove: + + it opens a new sequent for each premise of the first + constructor of the inductive type that is the conclusion of the + current sequent. For more details, see the constructor tactic. + + + + letin <ident> ≝ <term> @@ -679,7 +895,33 @@ its constructor takes no arguments. right right - The tactic right + right + + + + Pre-conditions: + + the conclusion of the current sequent must be + an inductive type or the application of an inductive type with + at least two constructors. + + + + Action: + + equivalent to constructor 2. + + + + New sequents to prove: + + it opens a new sequent for each premise of the second + constructor of the inductive type that is the conclusion of the + current sequent. For more details, see the constructor tactic. + + + + ring -- 2.39.2