X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=0fabbbf7ca5f8a68167a62bcaa68334f59363eb3;hb=b2213b9fbc56461ef47b971686edbba82a9658bf;hp=779f95eb81153022a73692038f7a2a2137d5b539;hpb=bf455cb281797e01ea4e89086bee9fde115f6ee2;p=helm.git diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 779f95eb8..0fabbbf7c 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -1,14 +1,27 @@ - Tactics + Tactics + + + Quick reference card + + &tacticref; + + - absurd <term> + absurd absurd absurd P + + Synopsis: + + absurd &sterm; + + Pre-conditions: @@ -18,14 +31,14 @@ Action: - it closes the current sequent by eliminating an + It closes the current sequent by eliminating an absurd term. New sequents to prove: - it opens two new sequents of conclusion P + It opens two new sequents of conclusion P and ¬P. @@ -33,11 +46,17 @@ - apply <term> + apply apply apply t + + Synopsis: + + apply &sterm; + + Pre-conditions: @@ -51,13 +70,68 @@ Action: - it closes the current sequent by applying t to n implicit arguments (that become new sequents). + It closes the current sequent by applying t to n implicit arguments (that become new sequents). + + + + New sequents to prove: + + It opens a new sequent for each premise + Ti that is not + instantiated by unification. Ti is + the conclusion of the i-th new sequent to + prove. + + + + + + + applyS + applyS + applyS t auto_params + + + + Synopsis: + + applyS &sterm; &autoparams; + + + + Pre-conditions: + + t must have type + T1 → ... → + Tn → G. + + + + Action: + + applyS is useful when + apply fails because the current goal + and the conclusion of the applied theorems are extensionally + equivalent up to instantiation of metavariables, but cannot + be unified. E.g. the goal is P(n*O+m) and + the theorem to be applied proves ∀m.P(m+O). + + + It tries to automatically rewrite the current goal using + auto paramodulation + to make it unifiable with G. + Then it closes the current sequent by applying + t to n + implicit arguments (that become new sequents). + The auto_params parameters are passed + directly to auto paramodulation. + New sequents to prove: - it opens a new sequent for each premise + It opens a new sequent for each premise Ti that is not instantiated by unification. Ti is the conclusion of the i-th new sequent to @@ -73,49 +147,61 @@ assumption + + Synopsis: + + assumption + + Pre-conditions: - there must exist an hypothesis whose type can be unified with + There must exist an hypothesis whose type can be unified with the conclusion of the current sequent. Action: - it closes the current sequent exploiting an hypothesis. + It closes the current sequent exploiting an hypothesis. New sequents to prove: - none + None - auto [depth=<int>] [width=<int>] [paramodulation] [full] + auto auto - auto depth=d width=w paramodulation full + auto params + + Synopsis: + + auto &autoparams; + + Pre-conditions: - none, but the tactic may fail finding a proof if every + None, but the tactic may fail finding a proof if every proof is in the search space that is pruned away. Pruning is - controlled by d and w. + controlled by the optional params. Moreover, only lemmas whose type signature is a subset of the signature of the current sequent are considered. The signature of - a sequent is ...TODO + a sequent is ...&TODO; Action: - it closes the current sequent by repeated application of + It closes the current sequent by repeated application of rewriting steps (unless paramodulation is omitted), hypothesis and lemmas in the library. @@ -123,47 +209,118 @@ New sequents to prove: - none + None + + + + + + + cases + cases + + cases t hyps + + + + + Synopsis: + + + cases + &term; [([&id;]…)] + + + + + Pre-conditions: + + + t must inhabit an inductive type + + + + + Action: + + + It proceed by cases on t. The new generated + hypothesis in each branch are named according to + hyps. + + + + + New sequents to prove: + + One new sequent for each constructor of the type of + t. Each sequent has a new hypothesis for + each argument of the constructor. - clear <id> + clear clear - clear H + + clear H1 ... Hm + + + Synopsis: + + + clear + &id; [&id;…] + + + Pre-conditions: - H must be an hypothesis of the - current sequent to prove. + + + H1 ... Hm + must be hypotheses of the + current sequent to prove. + Action: - it hides the hypothesis H from the - current sequent. + + It hides the hypotheses + + H1 ... Hm + from the current sequent. + New sequents to prove: - none + None - clearbody <id> + clearbody clearbody clearbody H + + Synopsis: + + clearbody &id; + + Pre-conditions: @@ -174,29 +331,87 @@ Action: - it hides the definiens of a definition in the current + It hides the definiens of a definition in the current sequent context. Thus the definition becomes an hypothesis. New sequents to prove: - none. + None. + + + + + + + compose + compose + compose n t1 with t2 hyps + + + + Synopsis: + + compose [&nat;] &sterm; [with &sterm;] [&intros-spec;] + + + + Pre-conditions: + + + + + + Action: + + Composes t1 with t2 in every possible way + n times introducing generated terms + as if intros hyps was issued. + If t1:∀x:A.B[x] and + t2:∀x,y:A.B[x]→B[y]→C[x,y] it generates: + + + λx,y:A.t2 x y (t1 x) : ∀x,y:A.B[y]→C[x,y] + + + λx,y:A.λH:B[x].t2 x y H (t1 y) : ∀x,y:A.B[x]→C[x,y] + + + + + If t2 is omitted it composes + t1 + with every hypothesis that can be introduced. + n iterates the process. + + + + New sequents to prove: + + The same, but with more hypothesis eventually introduced + by the &intros-spec;. - change <pattern> with <term> + change change change patt with t + + Synopsis: + + change &pattern; with &sterm; + + Pre-conditions: - each subterm matched by the pattern must be convertible + Each subterm matched by the pattern must be convertible with the term t disambiguated in the context of the matched subterm. @@ -204,7 +419,7 @@ Action: - it replaces the subterms of the current sequent matched by + It replaces the subterms of the current sequent matched by patt with the new term t. For each subterm matched by the pattern, t is disambiguated in the context of the subterm. @@ -213,22 +428,28 @@ New sequents to prove: - none. + None. - constructor <int> + constructor constructor constructor n + + Synopsis: + + constructor &nat; + + Pre-conditions: - the conclusion of the current sequent must be + The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least n constructors. @@ -236,14 +457,14 @@ Action: - it applies the n-th constructor of the + It applies the n-th constructor of the inductive type of the conclusion of the current sequent. New sequents to prove: - it opens a new sequent for each premise of the constructor + It opens a new sequent for each premise of the constructor that can not be inferred by unification. For more details, see the apply tactic. @@ -257,35 +478,47 @@ contradiction + + Synopsis: + + contradiction + + Pre-conditions: - there must be in the current context an hypothesis of type + There must be in the current context an hypothesis of type False. Action: - it closes the current sequent by applying an hypothesis of + It closes the current sequent by applying an hypothesis of type False. New sequents to prove: - none + None - cut <term> [as <id>] + cut cut cut P as H + + Synopsis: + + cut &sterm; [as &id;] + + Pre-conditions: @@ -295,13 +528,13 @@ Action: - it closes the current sequent. + It closes the current sequent. New sequents to prove: - it opens two new sequents. The first one has an extra + It opens two new sequents. The first one has an extra hypothesis H:P. If H is omitted, the name of the hypothesis is automatically generated. The second sequent has conclusion P and @@ -312,67 +545,140 @@ - decompose [<ident list>] <ident> [<intros_spec>] + decompose decompose - decompose ??? + + decompose as H1 ... Hm + + + + + Synopsis: + + + decompose + [as &id;…] + + + + + Pre-conditions: + + None. + + + + Action: + + + For each each premise H of type + T in the current context where + T is a non-recursive inductive type without + right parameters and of sort Prop or CProp, the tactic runs + + elim H as H1 ... Hm + , clears H and runs itself + recursively on each new premise introduced by + elim in the opened sequents. + + + + + New sequents to prove: + + + The ones generated by all the elim tactics run. + + + + + + + + demodulate + demodulate + demodulate + + Synopsis: + + demodulate + + Pre-conditions: - TODO. + None. Action: - TODO. + &TODO; New sequents to prove: - TODO. + None. - - discriminate <term> - discriminate - discriminate p + + destruct + destruct + destruct p + + Synopsis: + + destruct &sterm; + + Pre-conditions: - 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. + p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type. Action: - it closes the current sequent by proving the absurdity of - p. + The tactic recursively compare the two sides of the equality + looking for different constructors in corresponding position. + If two of them are found, the tactic closes the current sequent + by proving the absurdity of p. Otherwise + it adds a new hypothesis for each leaf of the formula that + states the equality of the subformulae in the corresponding + positions on the two sides of the equality. + New sequents to prove: - none. + None. - elim <term> [using <term>] [<intros_spec>] + elim elim elim t using th hyps + + Synopsis: + + elim &sterm; [using &sterm;] &intros-spec; + + Pre-conditions: @@ -385,7 +691,7 @@ its constructor takes no arguments. Action: - it proceeds by cases on the values of t, + It proceeds by cases on the values of t, according to the elimination principle th. @@ -393,20 +699,29 @@ its constructor takes no arguments. New sequents to prove: - it opens one new sequent for each case. The names of + It opens one new sequent for each case. The names of the new hypotheses are picked by hyps, if - provided. + provided. If hyps specifies also a number of hypotheses that + is less than the number of new hypotheses for a new sequent, + then the exceeding hypothesis will be kept as implications in + the conclusion of the sequent. - elimType <term> [using <term>] + elimType elimType - elimType T using th + elimType T using th hyps + + Synopsis: + + elimType &sterm; [using &sterm;] &intros-spec; + + Pre-conditions: @@ -429,28 +744,34 @@ its constructor takes no arguments. - exact <term> + exact exact exact p + + Synopsis: + + exact &sterm; + + Pre-conditions: - the type of p must be convertible + The type of p must be convertible with the conclusion of the current sequent. Action: - it closes the current sequent using p. + It closes the current sequent using p. New sequents to prove: - none. + None. @@ -462,10 +783,16 @@ its constructor takes no arguments. exists + + Synopsis: + + exists + + Pre-conditions: - the conclusion of the current sequent must be + The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least one constructor. @@ -473,13 +800,13 @@ its constructor takes no arguments. Action: - equivalent to constructor 1. + Equivalent to constructor 1. New sequents to prove: - it opens a new sequent for each premise of the first + 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. @@ -488,21 +815,27 @@ its constructor takes no arguments. - fail - failt + fail + fail fail + + Synopsis: + + fail + + Pre-conditions: - none. + None. Action: - this tactic always fail. + This tactic always fail. @@ -515,21 +848,27 @@ its constructor takes no arguments. - fold <reduction_kind> <term> <pattern> + fold fold fold red t patt + + Synopsis: + + fold &reduction-kind; &sterm; &pattern; + + Pre-conditions: - the pattern must not specify the wanted term. + The pattern must not specify the wanted term. Action: - first of all it locates all the subterms matched by + First of all it locates all the subterms matched by patt. In the context of each matched subterm it disambiguates the term t and reduces it to its red normal form; then it replaces with @@ -540,7 +879,7 @@ its constructor takes no arguments. New sequents to prove: - none. + None. @@ -552,10 +891,16 @@ its constructor takes no arguments. fourier + + Synopsis: + + fourier + + Pre-conditions: - the conclusion of the current sequent must be a linear + The conclusion of the current sequent must be a linear inequation over real numbers taken from standard library of Coq. Moreover the inequations in the hypotheses must imply the inequation in the conclusion of the current sequent. @@ -564,69 +909,98 @@ its constructor takes no arguments. Action: - it closes the current sequent by applying the Fourier method. + It closes the current sequent by applying the Fourier method. New sequents to prove: - none. + None. - fwd <ident> [<ident list>] + fwd fwd - fwd ...TODO + fwd H as H0 ... Hn + + Synopsis: + + fwd &id; [as &id; [&id;]…] + + Pre-conditions: - TODO. + + The type of H must be the premise of a + forward simplification theorem. + Action: - TODO. + + This tactic is under development. + It simplifies the current context by removing + H using the following methods: + forward application (by lapply) of a suitable + simplification theorem, chosen automatically, of which the type + of H is a premise, + decomposition (by decompose), + rewriting (by rewrite). + H0 ... Hn + are passed to the tactics fwd invokes, as + names for the premise they introduce. + New sequents to prove: - TODO. + + The ones opened by the tactics fwd invokes. + - generalize <pattern> [as <id>] + generalize generalize generalize patt as H + + Synopsis: + + generalize &pattern; [as &id;] + + Pre-conditions: - all the terms matched by patt must be + 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 + 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 + 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 @@ -642,85 +1016,66 @@ its constructor takes no arguments. id id - absurd P + id - - Pre-conditions: - - none. - - - - Action: - - this identity tactic does nothing without failing. - - - - New sequents to prove: + + Synopsis: - none. + id - - - - - injection <term> - 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. + None. Action: - it derives new hypotheses by injectivity of - K. + This identity tactic does nothing without failing. 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. + None. - intro [<ident>] + intro intro intro H + + Synopsis: + + intro [&id;] + + Pre-conditions: - the conclusion of the sequent to prove must be an implication + The conclusion of the sequent to prove must be an implication or a universal quantification. Action: - it applies the right introduction rule for implication, + 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 + 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 @@ -731,11 +1086,17 @@ its constructor takes no arguments. - intros <intros_spec> + intros intros intros hyps + + Synopsis: + + intros &intros-spec; + + Pre-conditions: @@ -748,14 +1109,14 @@ its constructor takes no arguments. Action: - it applies several times the right introduction rule for + 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 + 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. @@ -768,22 +1129,28 @@ its constructor takes no arguments. - inversion <term> + inversion inversion inversion t + + Synopsis: + + inversion &sterm; + + Pre-conditions: - the type of the term t must be an inductive + 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 + It proceeds by cases on t paying attention to the constraints imposed by the actual "right arguments" of the inductive type. @@ -791,7 +1158,7 @@ its constructor takes no arguments. New sequents to prove: - it opens one new sequent to prove for each case in the + 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" @@ -803,27 +1170,70 @@ its constructor takes no arguments. - lapply [depth=<int>] <term> [to <term list] [using <ident>] + lapply lapply - lapply ??? + + lapply linear depth=d t + to t1, ..., tn as H + + + Synopsis: + + + lapply + [linear] + [depth=&nat;] + &sterm; + [to + &sterm; + [,&sterm;…] + ] + [as &id;] + + + Pre-conditions: - TODO. + + t must have at least d + independent premises and n must not be + greater than d. + Action: - TODO. + + Invokes letin H ≝ (t ? ... ?) + with enough ?'s to reach the + d-th independent premise of + t + (d is maximum if unspecified). + Then istantiates (by apply) with + t1, ..., tn + the ?'s corresponding to the first + n independent premises of + t. + Usually the other ?'s preceding the + n-th independent premise of + t are istantiated as a consequence. + If the linear flag is specified and if + t, t1, ..., tn + are (applications of) premises in the current context, they are + cleared. + New sequents to prove: - TODO. + + The ones opened by the tactics lapply invokes. + @@ -835,10 +1245,16 @@ its constructor takes no arguments. left + + Synopsis: + + left + + Pre-conditions: - the conclusion of the current sequent must be + The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least one constructor. @@ -846,13 +1262,13 @@ its constructor takes no arguments. Action: - equivalent to constructor 1. + Equivalent to constructor 1. New sequents to prove: - it opens a new sequent for each premise of the first + 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. @@ -861,111 +1277,102 @@ its constructor takes no arguments. - letin <ident> ≝ <term> + letin letin letin x ≝ t + + Synopsis: + + letin &id; ≝ &sterm; + + Pre-conditions: - none. + None. Action: - it adds to the context of the current sequent to prove a new + It adds to the context of the current sequent to prove a new definition x ≝ t. New sequents to prove: - none. + None. - normalize <pattern> + normalize normalize normalize patt - - Pre-conditions: + + Synopsis: - none. + normalize &pattern; - - Action: - - it replaces all the terms matched by patt - with their βδιζ-normal form. - - - - New sequents to prove: - - none. - - - - - - - paramodulation <pattern> - paramodulation - paramodulation patt - - Pre-conditions: - TODO. + None. Action: - TODO. + It replaces all the terms matched by patt + with their βδιζ-normal form. New sequents to prove: - TODO. + None. - reduce <pattern> + reduce reduce reduce patt + + Synopsis: + + reduce &pattern; + + Pre-conditions: - none. + None. Action: - it replaces all the terms matched by patt + It replaces all the terms matched by patt with their βδιζ-normal form. New sequents to prove: - none. + None. @@ -977,45 +1384,57 @@ its constructor takes no arguments. reflexivity + + Synopsis: + + reflexivity + + Pre-conditions: - the conclusion of the current sequent must be + The conclusion of the current sequent must be t=t for some term t Action: - it closes the current sequent by reflexivity + It closes the current sequent by reflexivity of equality. New sequents to prove: - none. + None. - replace <pattern> with <term> + replace change change patt with t + + Synopsis: + + replace &pattern; with &sterm; + + Pre-conditions: - none. + None. Action: - it replaces the subterms of the current sequent matched by + It replaces the subterms of the current sequent matched by patt with the new term t. For each subterm matched by the pattern, t is disambiguated in the context of the subterm. @@ -1024,7 +1443,7 @@ its constructor takes no arguments. New sequents to prove: - for each matched term t' it opens + For each matched term t' it opens a new sequent to prove whose conclusion is t'=t. @@ -1033,11 +1452,17 @@ its constructor takes no arguments. - rewrite {<|>} <term> <pattern> + rewrite rewrite rewrite dir p patt + + Synopsis: + + rewrite [<|>] &sterm; &pattern; + + Pre-conditions: @@ -1048,7 +1473,7 @@ its constructor takes no arguments. Action: - it looks in every term matched by patt + It looks in every term matched by patt for all the occurrences of the left hand side of the equality that p proves (resp. the right hand side if dir is @@ -1059,7 +1484,7 @@ its constructor takes no arguments. New sequents to prove: - it opens one new sequent for each hypothesis of the + It opens one new sequent for each hypothesis of the equality proved by p that is not closed by unification. @@ -1073,10 +1498,16 @@ its constructor takes no arguments. right + + Synopsis: + + right + + Pre-conditions: - the conclusion of the current sequent must be + The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least two constructors. @@ -1084,13 +1515,13 @@ its constructor takes no arguments. Action: - equivalent to constructor 2. + Equivalent to constructor 2. New sequents to prove: - it opens a new sequent for each premise of the second + 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. @@ -1104,10 +1535,16 @@ its constructor takes no arguments. ring + + Synopsis: + + ring + + Pre-conditions: - the conclusion of the current sequent must be an + The conclusion of the current sequent must be an equality over Coq's real numbers that can be proved using the ring properties of the real numbers only. @@ -1115,7 +1552,7 @@ its constructor takes no arguments. Action: - it closes the current sequent veryfying the equality by + It closes the current sequent veryfying the equality by means of computation (i.e. this is a reflexive tactic, implemented exploiting the "two level reasoning" technique). @@ -1123,35 +1560,41 @@ its constructor takes no arguments. New sequents to prove: - none. + None. - simplify <pattern> + simplify simplify simplify patt + + Synopsis: + + simplify &pattern; + + Pre-conditions: - none. + None. Action: - it replaces all the terms matched by patt + It replaces all the terms matched by patt with other convertible terms that are supposed to be simpler. New sequents to prove: - none. + None. @@ -1163,10 +1606,16 @@ its constructor takes no arguments. split + + Synopsis: + + split + + Pre-conditions: - the conclusion of the current sequent must be + The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least one constructor. @@ -1174,13 +1623,13 @@ its constructor takes no arguments. Action: - equivalent to constructor 1. + Equivalent to constructor 1. New sequents to prove: - it opens a new sequent for each premise of the first + 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. @@ -1188,6 +1637,46 @@ its constructor takes no arguments. + + + subst + subst + subst + + + + Synopsis: + + subst + + + + Pre-conditions: + + None. + + + + Action: + + For each premise of the form + H: x = t or H: t = x + where x is a local variable and + t does not depend on x, + the tactic rewrites H wherever + x appears clearing H and + x afterwards. + + + + New sequents to prove: + + The one opened by the applied tactics. + + + + + symmetry symmetry @@ -1195,50 +1684,62 @@ its constructor takes no arguments. symmetry + + Synopsis: + + symmetry + + Pre-conditions: - the conclusion of the current proof must be an equality. + The conclusion of the current proof must be an equality. Action: - it swaps the two sides of the equalityusing the symmetric + It swaps the two sides of the equalityusing the symmetric property. New sequents to prove: - none. + None. - transitivity <term> + transitivity transitivity transitivity t + + Synopsis: + + transitivity &sterm; + + Pre-conditions: - the conclusion of the current proof must be an equality. + The conclusion of the current proof must be an equality. Action: - it closes the current sequent by transitivity of the equality. + It closes the current sequent by transitivity of the equality. New sequents to prove: - it opens two new sequents l=t and + It opens two new sequents l=t and t=r where l and r are the left and right hand side of the equality in the conclusion of the current sequent to prove. @@ -1247,21 +1748,27 @@ the current sequent to prove. - unfold [<term>] <pattern> + unfold unfold unfold t patt + + Synopsis: + + unfold [&sterm;] &pattern; + + Pre-conditions: - none. + None. Action: - it finds all the occurrences of t + It finds all the occurrences of t (possibly applied to arguments) in the subterms matched by patt. Then it δ-expands each occurrence, also performing β-reduction of the obtained term. If @@ -1272,35 +1779,41 @@ the current sequent to prove. New sequents to prove: - none. + None. - whd <pattern> + whd whd whd patt + + Synopsis: + + whd &pattern; + + Pre-conditions: - none. + None. Action: - it replaces all the terms matched by patt + It replaces all the terms matched by patt with their βδιζ-weak-head normal form. New sequents to prove: - none. + None.