X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=779f95eb81153022a73692038f7a2a2137d5b539;hb=1b9dcf31051dfcf1e80991954ecbcb6aa9744388;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..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.
@@ -860,37 +863,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
@@ -926,37 +1101,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.
+
+
+
+