X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=cc0043724f57c33fa32f0e7bec60dfff326c8098;hb=cc16727f34114cee287e6a81b80f68657c656725;hp=b4e3cb3a9a20d8e7a890fcff67813e95e2d6ce8b;hpb=4041b420beef86580438e1f021d4bd674f16bb71;p=helm.git diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index b4e3cb3a9..cc0043724 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -4,7 +4,7 @@ Tactics - absurd <term> + <emphasis role="bold">absurd</emphasis> &sterm; absurd absurd P @@ -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. @@ -33,7 +33,7 @@ - apply <term> + <emphasis role="bold">apply</emphasis> &sterm; apply apply t @@ -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 @@ -68,7 +68,7 @@ - assumption + <emphasis role="bold">assumption</emphasis> assumption assumption @@ -76,27 +76,27 @@ 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] + <emphasis role="bold">auto</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] [<emphasis role="bold">width=</emphasis>&nat;] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>] auto auto depth=d width=w paramodulation full @@ -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,14 +123,14 @@ New sequents to prove: - none + None - clear <id> + <emphasis role="bold">clear</emphasis> &id; clear clear H @@ -145,21 +145,21 @@ 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> + <emphasis role="bold">clearbody</emphasis> &id; clearbody clearbody H @@ -174,21 +174,21 @@ 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> + <emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm; change change patt with t @@ -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,14 +213,14 @@ New sequents to prove: - none. + None. - constructor <int> + <emphasis role="bold">constructor</emphasis> &nat; constructor constructor n @@ -228,7 +228,7 @@ 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 +236,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. @@ -252,7 +252,7 @@ - contradiction + <emphasis role="bold">contradiction</emphasis> contradiction contradiction @@ -260,28 +260,28 @@ 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>] + <emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;] cut cut P as H @@ -295,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 @@ -312,34 +312,75 @@ - decompose [<ident list>] <ident> [<intros_spec>] + <emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec; decompose - decompose ??? + + decompose (T1 ... Tn) H hips + 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. + + + + + + + + <emphasis role="bold">demodulation</emphasis> &pattern; + demodulation + demodulation patt + + + + Pre-conditions: + + None. + + + + Action: + + &TODO; + + + + New sequents to prove: + + None. - discriminate <term> + <emphasis role="bold">discriminate</emphasis> &sterm; discriminate discriminate p @@ -354,21 +395,21 @@ 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>] + <emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec; elim elim t using th hyps @@ -385,7 +426,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,18 +434,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>] + <emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec; elimType - elimType T using th + elimType T using th hyps @@ -429,7 +473,7 @@ its constructor takes no arguments. - exact <term> + <emphasis role="bold">exact</emphasis> &sterm; exact exact p @@ -437,27 +481,27 @@ 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. - exists + <emphasis role="bold">exists</emphasis> exists exists @@ -465,7 +509,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 one constructor. @@ -473,13 +517,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 +532,21 @@ its constructor takes no arguments. - fail - failt + <emphasis role="bold">fail</emphasis> + fail fail Pre-conditions: - none. + None. Action: - this tactic always fail. + This tactic always fail. @@ -515,7 +559,7 @@ its constructor takes no arguments. - fold <reduction_kind> <term> <pattern> + <emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern; fold fold red t patt @@ -523,13 +567,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 @@ -540,14 +584,14 @@ its constructor takes no arguments. New sequents to prove: - none. + None. - fourier + <emphasis role="bold">fourier</emphasis> fourier fourier @@ -555,7 +599,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. @@ -564,20 +608,20 @@ 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>] + <emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>] fwd fwd ...TODO @@ -604,7 +648,7 @@ its constructor takes no arguments. - generalize <pattern> [as <id>] + <emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;] generalize generalize patt as H @@ -612,21 +656,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,7 +684,7 @@ its constructor takes no arguments. - id + <emphasis role="bold">id</emphasis> id id @@ -648,27 +692,27 @@ its constructor takes no arguments. 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. - injection <term> - injection + <emphasis role="bold">injection</emphasis> &sterm; + injection injection p @@ -682,14 +726,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. @@ -698,7 +742,7 @@ its constructor takes no arguments. - intro [<ident>] + <emphasis role="bold">intro</emphasis> [&id;] intro intro H @@ -706,21 +750,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 @@ -731,7 +775,7 @@ its constructor takes no arguments. - intros <intros_spec> + <emphasis role="bold">intros</emphasis> &intros-spec; intros intros hyps @@ -748,14 +792,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,7 +812,7 @@ its constructor takes no arguments. - inversion <term> + <emphasis role="bold">inversion</emphasis> &sterm; inversion inversion t @@ -776,14 +820,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. @@ -791,7 +835,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,9 +847,12 @@ its constructor takes no arguments. - lapply [depth=<int>] <term> [to <term list] [using <ident>] + <emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">as</emphasis> &id;] lapply - lapply ??? + + lapply depth=d t + to t1, ..., tn as H + @@ -830,7 +877,7 @@ its constructor takes no arguments. - left + <emphasis role="bold">left</emphasis> left left @@ -838,7 +885,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 one constructor. @@ -846,13 +893,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,7 +908,7 @@ its constructor takes no arguments. - letin <ident> ≝ <term> + <emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm; letin letin x ≝ t @@ -869,27 +916,27 @@ its constructor takes no arguments. 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> + <emphasis role="bold">normalize</emphasis> &pattern; normalize normalize patt @@ -897,27 +944,27 @@ its constructor takes no arguments. 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. - paramodulation <pattern> + <emphasis role="bold">paramodulation</emphasis> &pattern; paramodulation paramodulation patt @@ -944,7 +991,7 @@ its constructor takes no arguments. - reduce <pattern> + <emphasis role="bold">reduce</emphasis> &pattern; reduce reduce patt @@ -952,27 +999,27 @@ its constructor takes no arguments. 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. - reflexivity + <emphasis role="bold">reflexivity</emphasis> reflexivity reflexivity @@ -980,28 +1027,28 @@ its constructor takes no arguments. 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> + <emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm; change change patt with t @@ -1009,13 +1056,13 @@ its constructor takes no arguments. 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 +1071,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,7 +1080,7 @@ its constructor takes no arguments. - rewrite {<|>} <term> <pattern> + <emphasis role="bold">rewrite</emphasis> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern; rewrite rewrite dir p patt @@ -1048,7 +1095,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 +1106,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. @@ -1068,7 +1115,7 @@ its constructor takes no arguments. - right + <emphasis role="bold">right</emphasis> right right @@ -1076,7 +1123,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. @@ -1084,13 +1131,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. @@ -1099,7 +1146,7 @@ its constructor takes no arguments. - ring + <emphasis role="bold">ring</emphasis> ring ring @@ -1107,7 +1154,7 @@ its constructor takes no arguments. 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 +1162,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,14 +1170,14 @@ its constructor takes no arguments. New sequents to prove: - none. + None. - simplify <pattern> + <emphasis role="bold">simplify</emphasis> &pattern; simplify simplify patt @@ -1138,27 +1185,27 @@ its constructor takes no arguments. 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. - split + <emphasis role="bold">split</emphasis> split split @@ -1166,7 +1213,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 one constructor. @@ -1174,13 +1221,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. @@ -1189,7 +1236,7 @@ its constructor takes no arguments. - symmetry + <emphasis role="bold">symmetry</emphasis> symmetry The tactic symmetry symmetry @@ -1198,27 +1245,27 @@ its constructor takes no arguments. 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> + <emphasis role="bold">transitivity</emphasis> &sterm; transitivity transitivity t @@ -1226,19 +1273,19 @@ its constructor takes no arguments. 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,7 +1294,7 @@ the current sequent to prove. - unfold [<term>] <pattern> + <emphasis role="bold">unfold</emphasis> [&sterm;] &pattern; unfold unfold t patt @@ -1255,13 +1302,13 @@ the current sequent to prove. 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,14 +1319,14 @@ the current sequent to prove. New sequents to prove: - none. + None. - whd <pattern> + <emphasis role="bold">whd</emphasis> &pattern; whd whd patt @@ -1287,20 +1334,20 @@ the current sequent to prove. 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.