X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=9ba73d991ad40a52f37a406a797906a330c0c858;hb=62d556ff7763f5d452661e127f6e77b351dfef1c;hp=a423f37c419e08dd60bb1e14b3a7e21f326c3569;hpb=f89e30b4f792260fe73c013aa18559bb2b85f3e4;p=helm.git diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index a423f37c4..9ba73d991 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -1,97 +1,585 @@ - + Tactics absurd <term> - The tactic absurd - - + absurd P + + + Pre-conditions: + + P must have type Prop. + + + + + Action: + + it closes the current sequent by eliminating an + absurd term. + + + + New sequents to prove: + + it opens two new sequents of conclusion P + and ¬P. + + + + apply <term> - The tactic apply + apply t + + + + Pre-conditions: + + t must have type + T1 → ... → + Tn → G + where G can be unified with the conclusion + of the current sequent. + + + + Action: + + 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. + + + + assumption - The tactic assumption + assumption + + + + Pre-conditions: + + 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. + + + + New sequents to prove: + + none + + + + auto [depth=<int>] [width=<int>] [paramodulation] [full] - The tactic auto + auto depth=d width=w paramodulation full + + + + Pre-conditions: + + 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 + signature of the current sequent are considered. The signature of + a sequent is ...TODO + + + + Action: + + it closes the current sequent by repeated application of + rewriting steps (unless paramodulation is + omitted), hypothesis and lemmas in the library. + + + + New sequents to prove: + + none + + + + clear <id> - The tactic clear + clear H + + + + Pre-conditions: + + H must be an hypothesis of the + current sequent to prove. + + + + Action: + + it hides the hypothesis H from the + current sequent. + + + + New sequents to prove: + + none + + + + clearbody <id> - The tactic clearbody + clearbody H + + + + Pre-conditions: + + H must be an hypothesis of the + current sequent to prove. + + + + Action: + + it hides the definiens of a definition in the current + sequent context. Thus the definition becomes an hypothesis. + + + + New sequents to prove: + + none. + + + + change <pattern> with <term> - The tactic change - - - compare <term> - The tactic compare + change patt with t + + + + Pre-conditions: + + each subterm matched by the pattern must be convertible + with the term t disambiguated in the context + of the matched subterm. + + + + 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: + + none. + + + + constructor <int> - The tactic constructor + constructor n + + + + Pre-conditions: + + the conclusion of the current sequent must be + an inductive type or the application of an inductive type. + + + + Action: + + 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 + that can not be inferred by unification. For more details, + see the apply tactic. + + + + contradiction - The tactic contradiction + contradiction + + + + Pre-conditions: + + there must be in the current context an hypothesis of type + False. + + + + Action: + + it closes the current sequent by applying an hypothesis of + type False. + + + + New sequents to prove: + + none + + + + cut <term> [as <id>] - The tactic cut - - - decide - The tactic decide equality + cut P as H + + + + Pre-conditions: + + P must have type Prop. + + + + Action: + + it closes the current sequent. + + + + New sequents to prove: + + 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 + hypotheses the hypotheses of the current sequent to prove. + + + + decompose [<ident list>] <ident> [<intros_spec>] - The tactic decompose + decompose ??? + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + discriminate <term> - The tactic discriminate + discriminate p + + + + 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 +its constructor takes no arguments. + + + + Action: + + it closes the current sequent by proving the absurdity of + p. + + + + New sequents to prove: + + none. + + + + elim <term> [using <term>] [<intros_spec>] - The tactic elim + elim t using th hyps + + + + Pre-conditions: + + t must inhabit an inductive type and + th must be an elimination principle for that + inductive type. If th is omitted the appropriate + standard elimination principle is chosen. + + + + Action: + + it proceeds by cases on the values of t, + according to the elimination principle th. + + + + + New sequents to prove: + + it opens one new sequent for each case. The names of + the new hypotheses are picked by hyps, if + provided. + + + + elimType <term> [using <term>] - The tactic elimType + elimType T using th + + + + Pre-conditions: + + T must be an inductive type. + + + + Action: + + TODO (severely bugged now). + + + + New sequents to prove: + + TODO + + + + exact <term> - The tactic exact + exact p + + + + Pre-conditions: + + the type of p must be convertible + with the conclusion of the current sequent. + + + + Action: + + it closes the current sequent using p. + + + + New sequents to prove: + + none. + + + + exists - The tactic exists + exists + + + + 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. + + + + fail - The tactic fail + fail + + + + Pre-conditions: + + none. + + + + Action: + + this tactic always fail. + + + + New sequents to prove: + + N.A. + + + + fold <reduction_kind> <term> <pattern> - The tactic fold + fold red t patt + + + + Pre-conditions: + + the pattern must not specify the wanted term. + + + + Action: + + 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 + t every occurrence of the normal form in the + matched subterm. + + + + New sequents to prove: + + none. + + + + fourier - The tactic fourier + fourier + + + + Pre-conditions: + + 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. + + + + Action: + + it closes the current sequent by applying the Fourier method. + + + + New sequents to prove: + + none. + + + + fwd <ident> [<ident list>] - The tactic fwd + fwd ...TODO + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + generalize <pattern> [as <id>] @@ -187,3 +675,4 @@ +