From 4cf4be7fdb7af84271b3e20964b63dcbc653e01b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Feb 2006 14:15:34 +0000 Subject: [PATCH] Several more tactics documented. --- matita/help/C/sec_tactics.xml | 420 +++++++++++++++++++++++++++++++--- 1 file changed, 392 insertions(+), 28 deletions(-) diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 82bc536d7..2c1afb0cf 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -10,14 +10,14 @@ Pre-conditions: - P must have type Type. + P must have type Prop. Action: - it closes the current goal by eliminating an + it closes the current sequent by eliminating an absurd term. @@ -49,15 +49,17 @@ Action: - it closes the current goal by applying t. + it closes the current sequent by applying t to n implicit arguments (that become new sequents). New sequents to prove: - it opens a new goal for each premise + it opens a new sequent for each premise Ti that is not - instantiated by unification. + instantiated by unification. Ti is + the conclusion of the i-th new sequent to + prove. @@ -65,71 +67,433 @@ 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> -- 2.39.2