X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=4bba23eb6e22c887d99171a63f6776f76dfdf4b5;hb=bfcb2bf3391de8f0c4de9b8d35ea44ddc71a4291;hp=caee727a4ab52835465a31ce12574a0086a42b98;hpb=224c374eb4460b577aa3e89cf65d42563b6dace6;p=helm.git diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index caee727a4..4bba23eb6 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -18,14 +18,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. @@ -51,13 +51,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 @@ -76,20 +76,20 @@ 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 @@ -104,7 +104,7 @@ 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 @@ -115,7 +115,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. @@ -123,7 +123,7 @@ New sequents to prove: - none + None @@ -145,14 +145,14 @@ Action: - it hides the hypothesis H from the + It hides the hypothesis H from the current sequent. New sequents to prove: - none + None @@ -174,14 +174,14 @@ 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. @@ -196,7 +196,7 @@ 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 +204,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,7 +213,7 @@ New sequents to prove: - none. + None. @@ -228,21 +228,22 @@ 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. @@ -259,21 +260,21 @@ 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 @@ -294,13 +295,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 @@ -353,14 +354,14 @@ 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. @@ -384,7 +385,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. @@ -392,18 +393,21 @@ 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 <term> [using <term>] [<intros_spec>] elimType - elimType T using th + elimType T using th hyps @@ -436,20 +440,20 @@ its constructor takes no arguments. 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. @@ -464,20 +468,21 @@ its constructor takes no arguments. 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. @@ -494,13 +499,13 @@ its constructor takes no arguments. Pre-conditions: - none. + None. Action: - this tactic always fail. + This tactic always fail. @@ -521,13 +526,13 @@ its constructor takes no arguments. 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 @@ -538,7 +543,7 @@ its constructor takes no arguments. New sequents to prove: - none. + None. @@ -553,7 +558,7 @@ its constructor takes no arguments. 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. @@ -562,13 +567,13 @@ 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. @@ -610,21 +615,21 @@ its constructor takes no arguments. 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 @@ -640,25 +645,25 @@ its constructor takes no arguments. id id - absurd P + id Pre-conditions: - none. + None. Action: - this identity tactic does nothing without failing. + This identity tactic does nothing without failing. New sequents to prove: - none. + None. @@ -680,14 +685,14 @@ its constructor takes no arguments. Action: - it derives new hypotheses by injectivity of + It derives new hypotheses by injectivity of K. New sequents to prove: - the new sequent to prove is equal to the current sequent + The new sequent to prove is equal to the current sequent with the additional hypotheses t1=t'1 ... tn=t'n. @@ -704,21 +709,21 @@ its constructor takes no arguments. 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 @@ -746,14 +751,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. @@ -774,14 +779,14 @@ its constructor takes no arguments. 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. @@ -789,7 +794,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" @@ -836,20 +841,21 @@ its constructor takes no arguments. 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. @@ -860,37 +866,209 @@ its constructor takes no arguments. letin <ident> ≝ <term> letin - The tactic letin + letin x ≝ t + + + + 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 <pattern> normalize - The tactic normalize + normalize patt + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with their βδιζ-normal form. + + + + New sequents to prove: + + None. + + + + paramodulation <pattern> paramodulation - The tactic paramodulation + paramodulation patt + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + reduce <pattern> reduce - The tactic reduce + reduce patt + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with their βδιζ-normal form. + + + + New sequents to prove: + + None. + + + + reflexivity reflexivity - The tactic reflexivity + 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> - replace - The tactic replace + change + change patt with t + + + + 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> rewrite - The tactic rewrite + rewrite dir p patt + + + + 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 @@ -901,7 +1079,7 @@ its constructor takes no arguments. 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. @@ -909,13 +1087,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. @@ -926,37 +1104,210 @@ its constructor takes no arguments. ring ring - The tactic ring + 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> simplify - The tactic simplify + simplify patt + + + + 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 split - The tactic split + 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 + + + + 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> transitivity - The tactic transitivity + transitivity t + + + + 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> unfold - The tactic unfold + unfold t patt + + + + 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> whd - The tactic whd + whd patt + + + + Pre-conditions: + + None. + + + + Action: + + It replaces all the terms matched by patt + with their βδιζ-weak-head normal form. + + + + New sequents to prove: + + None. + + + +