From: Claudio Sacerdoti Coen Date: Thu, 9 Feb 2006 16:14:18 +0000 (+0000) Subject: Most of the tactics are now documented. X-Git-Tag: make_still_working~7576 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b9dcf31051dfcf1e80991954ecbcb6aa9744388;p=helm.git Most of the tactics are now documented. --- diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 5844ffcea..779f95eb8 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -229,7 +229,8 @@ Pre-conditions: the conclusion of the current sequent must be - an inductive type or the application of an inductive type. + an inductive type or the application of an inductive type with + at least n constructors. @@ -465,7 +466,8 @@ 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. + an inductive type or the application of an inductive type + with at least one constructor. @@ -837,7 +839,8 @@ 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. + an inductive type or the application of an inductive type + with at least one constructor. @@ -971,17 +974,98 @@ its constructor takes no arguments. 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 @@ -1017,7 +1101,33 @@ 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> @@ -1050,22 +1160,123 @@ its constructor takes no arguments. 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>