X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=712ce837a524ec2cd360fc94ad45f12e04fdf5e2;hb=80916272b252d42c86967e087c8840fa584ef278;hp=03842a70904647081e5335656fc3b39534c5316f;hpb=a3e2307340205d6a9651d90a5342cfdd232138dd;p=helm.git diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 03842a709..712ce837a 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -1,13 +1,27 @@ - Tactics + Tactics + + + Quick reference card + + &tacticref; + + - absurd <term> + absurd + absurd absurd P + + Synopsis: + + absurd &sterm; + + Pre-conditions: @@ -17,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. @@ -32,10 +46,17 @@ - apply <term> + apply + apply apply t + + Synopsis: + + apply &sterm; + + Pre-conditions: @@ -49,13 +70,13 @@ 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 + 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 @@ -67,40 +88,54 @@ assumption + assumption 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 + + Synopsis: + + auto [depth=&nat;] [width=&nat;] [paramodulation] [full] + + 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. Moreover, only lemmas whose type signature is a subset of the @@ -111,7 +146,7 @@ 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. @@ -119,17 +154,24 @@ New sequents to prove: - none + None - clear <id> + clear + clear clear H + + Synopsis: + + clear &id; + + Pre-conditions: @@ -140,24 +182,31 @@ Action: - it hides the hypothesis H from the + It hides the hypothesis H from the current sequent. New sequents to prove: - none + None - clearbody <id> + clearbody + clearbody clearbody H + + Synopsis: + + clearbody &id; + + Pre-conditions: @@ -168,28 +217,35 @@ 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. - 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. @@ -197,7 +253,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. @@ -206,35 +262,43 @@ 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 - an inductive type or the application of an inductive type. + The conclusion of the current sequent must be + an inductive type or the application of an inductive type with + at least n constructors. 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. @@ -244,37 +308,51 @@ contradiction + contradiction 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: @@ -284,13 +362,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 @@ -301,64 +379,132 @@ - decompose [<ident list>] <ident> [<intros_spec>] - decompose ??? + decompose + decompose + + decompose (T1 ... Tn) H hips + + + Synopsis: + + decompose &id; [&id;]… &intros-spec; + + Pre-conditions: - TODO. + + H must inhabit one inductive type among + + T1 ... Tn + + and the types of a predefined list. + Action: - TODO. + + Runs elim H hyps, clears H and tries to run + itself recursively on each new identifier introduced by + elim in the opened sequents. + New sequents to prove: - TODO. + + The ones generated by all the elim tactics run. + + + + + + + + demodulation + demodulation + demodulation patt + + + + Synopsis: + + demodulation &pattern; + + + + Pre-conditions: + + None. + + + + Action: + + &TODO; + + + + New sequents to prove: + + None. - discriminate <term> + discriminate + discriminate discriminate p + + Synopsis: + + discriminate &sterm; + + 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. Action: - it closes the current sequent by proving the absurdity of + It closes the current sequent by proving the absurdity of p. 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: @@ -371,7 +517,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. @@ -379,19 +525,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 T using th + elimType + elimType + elimType T using th hyps + + Synopsis: + + elimType &sterm; [using &sterm;] &intros-spec; + + Pre-conditions: @@ -414,27 +570,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. @@ -442,26 +605,34 @@ its constructor takes no arguments. exists + exists exists + + Synopsis: + + exists + + Pre-conditions: - the conclusion of the current sequent must be - an inductive type or the application of an inductive type. + The conclusion of the current sequent must be + an inductive type or the application of an inductive type + with at least one constructor. 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. @@ -470,20 +641,27 @@ its constructor takes no arguments. - fail + fail + fail fail + + Synopsis: + + fail + + Pre-conditions: - none. + None. Action: - this tactic always fail. + This tactic always fail. @@ -496,20 +674,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 @@ -520,7 +705,7 @@ its constructor takes no arguments. New sequents to prove: - none. + None. @@ -528,13 +713,20 @@ its constructor takes no arguments. fourier + fourier 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. @@ -543,23 +735,30 @@ 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 + + Synopsis: + + fwd &id; [([&id;]…)] + + Pre-conditions: @@ -582,96 +781,848 @@ its constructor takes no arguments. - generalize <pattern> [as <id>] - The tactic generalize + generalize + generalize + generalize patt as H + + + + Synopsis: + + generalize &pattern; [as &id;] + + + + 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 - The tactic id + id + id + + + + Synopsis: + + id + + + + Pre-conditions: + + None. + + + + Action: + + This identity tactic does nothing without failing. + + + + New sequents to prove: + + None. + + + + - injection <term> - The tactic injection + injection + injection + injection p + + + + Synopsis: + + injection &sterm; + + + + 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>] - The tactic intro + intro + intro + intro H + + + + Synopsis: + + intro [&id;] + + + + 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> - The tactic intros + intros + intros + intros hyps + + + + Synopsis: + + intros &intros-spec; + + + + 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. + + + + - intros <term> - The tactic intros + inversion + inversion + inversion t + + + + Synopsis: + + inversion &sterm; + + + + 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>] - The tactic lapply + lapply + lapply + + lapply depth=d t + to t1, ..., tn as H + + + + + Synopsis: + + lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]…] [as &id;] + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + left - The tactic left - - - letin <ident> ≝ <term> - The tactic letin - - - normalize <pattern> - The tactic normalize - - - paramodulation <pattern> - The tactic paramodulation - - - reduce <pattern> - The tactic reduce - + left + left + + + + Synopsis: + + left + + + + Pre-conditions: + + The conclusion of the current sequent must be + an inductive type or the application of an inductive type + with at least one constructor. + + + + 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 + letin + letin x ≝ t + + + + Synopsis: + + letin &id; ≝ &sterm; + + + + Pre-conditions: + + None. + + + + Action: + + It adds to the context of the current sequent to prove a new + definition x ≝ t. + + + + New sequents to prove: + + None. + + + + + + + normalize + normalize + normalize patt + + + + Synopsis: + + normalize &pattern; + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with their βδιζ-normal form. + + + + New sequents to prove: + + None. + + + + + + + paramodulation + paramodulation + paramodulation patt + + + + Synopsis: + + paramodulation &pattern; + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + + + + reduce + reduce + reduce patt + + + + Synopsis: + + reduce &pattern; + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with their βδιζ-normal form. + + + + New sequents to prove: + + None. + + + + + reflexivity - The tactic reflexivity + reflexivity + reflexivity + + + + Synopsis: + + reflexivity + + + + Pre-conditions: + + The conclusion of the current sequent must be + t=t for some term t + + + + Action: + + It closes the current sequent by reflexivity + of equality. + + + + New sequents to prove: + + None. + + + + - replace <pattern> with <term> - The tactic replace + replace + change + change patt with t + + + + Synopsis: + + replace &pattern; with &sterm; + + + + Pre-conditions: + + None. + + + + Action: + + 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. + + + + New sequents to prove: + + For each matched term t' it opens + a new sequent to prove whose conclusion is + t'=t. + + + + - rewrite {<|>} <term> <pattern> - The tactic rewrite + rewrite + rewrite + rewrite dir p patt + + + + Synopsis: + + rewrite [<|>] &sterm; &pattern; + + + + Pre-conditions: + + p must be the proof of an equality, + possibly under some hypotheses. + + + + Action: + + 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 + <). Every occurence found is replaced with + the opposite side of the equality. + + + + New sequents to prove: + + It opens one new sequent for each hypothesis of the + equality proved by p that is not closed + by unification. + + + + right - The tactic right + right + right + + + + Synopsis: + + 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 - The tactic ring + ring + ring + + + + Synopsis: + + ring + + + + Pre-conditions: + + 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. + + + + Action: + + 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). + + + + New sequents to prove: + + None. + + + + - simplify <pattern> - The tactic simplify + simplify + simplify + simplify patt + + + + Synopsis: + + simplify &pattern; + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with other convertible terms that are supposed to be simpler. + + + + New sequents to prove: + + None. + + + + split - The tactic split + split + split + + + + Synopsis: + + split + + + + Pre-conditions: + + The conclusion of the current sequent must be + an inductive type or the application of an inductive type with + at least one constructor. + + + + 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. + + + + symmetry + symmetry The tactic symmetry + symmetry + + + + Synopsis: + + symmetry + + + + Pre-conditions: + + The conclusion of the current proof must be an equality. + + + + Action: + + It swaps the two sides of the equalityusing the symmetric + property. + + + + New sequents to prove: + + None. + + + + - transitivity <term> - The tactic transitivity + transitivity + transitivity + transitivity t + + + + Synopsis: + + transitivity &sterm; + + + + Pre-conditions: + + The conclusion of the current proof must be an equality. + + + + Action: + + It closes the current sequent by transitivity of the equality. + + + + New sequents to prove: + + 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. + + + + - unfold [<term>] <pattern> - The tactic unfold + unfold + unfold + unfold t patt + + + + Synopsis: + + unfold [&sterm;] &pattern; + + + + Pre-conditions: + + None. + + + + Action: + + 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 + t is omitted it defaults to each + subterm matched by patt. + + + + New sequents to prove: + + None. + + + + - whd <pattern> - The tactic whd + whd + whd + whd patt + + + + Synopsis: + + whd &pattern; + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with their βδιζ-weak-head normal form. + + + + New sequents to prove: + + None. + + + +