X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=2ac2cfc65a459961f869ccbb7644437f7c4c7e04;hb=874cacec64d0aab52ab1a21aad23208f52f50caf;hp=ebd100a26c408c5a242e0b87d221d43838e78692;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git
diff --git a/matita/matita/help/C/sec_tactics.xml b/matita/matita/help/C/sec_tactics.xml
index ebd100a26..2ac2cfc65 100644
--- a/matita/matita/help/C/sec_tactics.xml
+++ b/matita/matita/help/C/sec_tactics.xml
@@ -10,51 +10,16 @@
-
- absurd
- absurd
- absurd P
-
-
-
- Synopsis:
-
- absurd &sterm;
-
-
-
- Pre-conditions:
-
- P must have type Prop.
-
-
-
- Action:
-
- It closes the current sequent by eliminating an
- absurd term.
-
-
-
- New sequents to prove:
-
- It opens two new sequents of conclusion P
- and ¬P.
-
-
-
-
-
- apply
- apply
- apply t
+ @
+ @
+ @tSynopsis:
- apply &sterm;
+ @ &sterm;
@@ -86,203 +51,163 @@
-
- applyS
- applyS
- applyS t auto_params
+
+ //
+ //
+ /params/Synopsis:
- applyS &sterm; &autoparams;
+ /&autoparams;/.
+
Pre-conditions:
- t must have type
- T1 â ... â
- Tn â G.
+ 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 the optional params.
+ Moreover, only lemmas whose type signature is a subset of the
+ signature of the current sequent are considered. The signature of
+ a sequent is essentially the set of constats appearing in it.
+ Action:
- applyS is useful when
- apply fails because the current goal
- and the conclusion of the applied theorems are extensionally
- equivalent up to instantiation of metavariables, but cannot
- be unified. E.g. the goal is P(n*O+m) and
- the theorem to be applied proves âm.P(m+O).
-
-
- It tries to automatically rewrite the current goal using
- auto paramodulation
- to make it unifiable with G.
- Then it closes the current sequent by applying
- t to n
- implicit arguments (that become new sequents).
- The auto_params parameters are passed
- directly to auto paramodulation.
-
+ 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:
- 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
- prove.
+ None
-
- assumption
- assumption
- assumption
+
+ #
+ #
+ #HSynopsis:
- assumption
+ #&id;Pre-conditions:
- There must exist an hypothesis whose type can be unified with
- the conclusion of the current sequent.
+ The conclusion of the sequent to prove must be an implication
+ or a universal quantification.Action:
- It closes the current sequent exploiting an hypothesis.
+ It applies the right introduction rule for implication,
+ closing the current sequent.New sequents to prove:
- None
+ 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.
-
- auto
- auto
- auto params
+
+ #_
+ #_
+ #_Synopsis:
- auto &autoparams;.
- autobatch &autoparams;
+ #_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 the optional params.
- Moreover, only lemmas whose type signature is a subset of the
- signature of the current sequent are considered. The signature of
- a sequent is essentially the set of constats appearing in it.
-
+ The conclusion of the sequent to prove must be an implication.
+ Action:
- It closes the current sequent by repeated application of
- rewriting steps (unless paramodulation is
- omitted), hypothesis and lemmas in the library.
+ It applies the ``a fortiori'' rule for implication,
+ closing the current sequent.New sequents to prove:
- None
+ It opens a new sequent whose conclusion is the conclusion
+ of the implication of the original sequent.
-
- cases
- cases
-
- cases t pattern hyps
-
+
+ ##
+ ##
+ ##Synopsis:
-
- cases
- &term; &pattern; [([&id;]â¦)]
-
+ ##Pre-conditions:
-
- t must inhabit an inductive type
-
+ None.Action:
-
- It proceed by cases on t. The new generated
- hypothesis in each branch are named according to
- hyps.
- The elimintation predicate is restricted by
- pattern. In particular, if some hypothesis
- is listed in pattern, the hypothesis is
- generalized and cleared before proceeding by cases on
- t. Currently, we only support patterns of the
- form H1 ⦠Hn ⢠%. This limitation will be lifted in the future.
-
-
-
-
- New sequents to prove:
-
- One new sequent for each constructor of the type of
- t. Each sequent has a new hypothesis for
- each argument of the constructor.
+ This macro expands to the longest possible list of
+ #Hi tactics. The
+ names of the introduced hypotheses are automatically
+ generated.
- clear
- clear
-
- clear H1 ... Hm
-
+ -
+ -
+ -HSynopsis:
- clear
- &id; [&id;â¦]
+ -&id;
@@ -290,9 +215,7 @@
Pre-conditions:
-
- H1 ... Hm
- must be hypotheses of the
+ H must be an hypothesis of the
current sequent to prove.
@@ -301,10 +224,8 @@
Action:
- It hides the hypotheses
-
- H1 ... Hm
- from the current sequent.
+ It hides the hypothesis H
+ from the current sequent.
@@ -317,876 +238,228 @@
-
- clearbody
- clearbody
- clearbody H
+
+ %
+ %
+ %n {args}Synopsis:
- clearbody &id;
+ % [&nat;] [{&sterm;â¦}]Pre-conditions:
- H must be an hypothesis of the
- current sequent to prove.
+ 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 hides the definiens of a definition in the current
- sequent context. Thus the definition becomes an hypothesis.
+ It applies the n-th constructor of the
+ inductive type of the conclusion of the current sequent to
+ the arguments args.
+ If n is omitted, it defaults to 1.New sequents to prove:
- None.
+ 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.
-
- compose
- compose
- compose n t1 with t2 hyps
+
+ *
+ *
+
+ * as H
+ Synopsis:
- compose [&nat;] &sterm; [with &sterm;] [&intros-spec;]
+
+ *
+ [as &id;]
+ Pre-conditions:
-
+ The current conclusion must be of the form
+ T â G where I is
+ an inductive type applied to its arguments, if any.Action:
- Composes t1 with t2 in every possible way
- n times introducing generated terms
- as if intros hyps was issued.
- If t1:âx:A.B[x] and
- t2:âx,y:A.B[x]âB[y]âC[x,y] it generates:
-
-
- λx,y:A.t2 x y (t1 x) : âx,y:A.B[y]âC[x,y]
-
-
- λx,y:A.λH:B[x].t2 x y H (t1 y) : âx,y:A.B[x]âC[x,y]
-
-
-
-
- If t2 is omitted it composes
- t1
- with every hypothesis that can be introduced.
- n iterates the process.
+
+ It introduces a new hypothesis H of type
+ T. Then it proceeds by cases over
+ H. Finally, if the name H
+ is not specified, it clears the new hypothesis from all contexts.
+ New sequents to prove:
- The same, but with more hypothesis eventually introduced
- by the &intros-spec;.
+
+ The ones generated by case analysis.
+
-
- change
- change
- change patt with t
+
+ >
+ >
+ > p pattSynopsis:
- change &pattern; with &sterm;
+ [<|>] &sterm; &pattern;Pre-conditions:
- Each subterm matched by the pattern must be convertible
- with the term t disambiguated in the context
- of the matched subterm.
+ p must be the proof of an equality,
+ possibly under some hypotheses.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.
+ 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 < is used).
+ Every occurence found is replaced with
+ the opposite side of the equality.New sequents to prove:
- None.
+ It opens one new sequent for each hypothesis of the
+ equality proved by p that is not closed
+ by unification.
-
- constructor
- constructor
- constructor n
+
+ applyS
+ applyS
+ applyS t auto_paramsSynopsis:
- constructor &nat;
+ applyS &sterm; &autoparams;Pre-conditions:
- The conclusion of the current sequent must be
- an inductive type or the application of an inductive type with
- at least n constructors.
+ t must have type
+ T1 â ... â
+ Tn â G.Action:
- It applies the n-th constructor of the
- inductive type of the conclusion of the current sequent.
+ applyS is useful when
+ apply fails because the current goal
+ and the conclusion of the applied theorems are extensionally
+ equivalent up to instantiation of metavariables, but cannot
+ be unified. E.g. the goal is P(n*O+m) and
+ the theorem to be applied proves âm.P(m+O).
+
+
+ It tries to automatically rewrite the current goal using
+ auto paramodulation
+ to make it unifiable with G.
+ Then it closes the current sequent by applying
+ t to n
+ implicit arguments (that become new sequents).
+ The auto_params parameters are passed
+ directly to auto paramodulation.
+ 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
- contradiction
- contradiction
-
-
-
- Synopsis:
-
- 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
- cut
- cut P as H
-
-
-
- Synopsis:
-
- cut &sterm; [as &id;]
-
-
-
- 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
- decompose
-
- decompose as H1 ... Hm
-
-
-
-
- Synopsis:
-
-
- decompose
- [as &id;â¦]
-
-
-
-
- Pre-conditions:
-
- None.
-
-
-
- Action:
-
-
- For each each premise H of type
- T in the current context where
- T is a non-recursive inductive type without
- right parameters and of sort Prop or CProp, the tactic runs
-
- elim H as H1 ... Hm
- , clears H and runs itself
- recursively on each new premise introduced by
- elim in the opened sequents.
-
-
-
-
- New sequents to prove:
-
-
- The ones generated by all the elim tactics run.
-
-
-
-
-
-
-
- demodulate
- demodulate
- demodulate auto_params
-
-
-
- Synopsis:
-
- demodulate &autoparams;
-
-
-
- Pre-conditions:
-
- None.
-
-
-
- Action:
-
- &TODO;
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
- destruct
- destruct
- destruct p
-
-
-
- Synopsis:
-
- destruct &sterm;
-
-
-
- Pre-conditions:
-
- p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type.
-
-
-
- Action:
-
- The tactic recursively compare the two sides of the equality
- looking for different constructors in corresponding position.
- If two of them are found, the tactic closes the current sequent
- by proving the absurdity of p. Otherwise
- it adds a new hypothesis for each leaf of the formula that
- states the equality of the subformulae in the corresponding
- positions on the two sides of the equality.
-
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
- elim
- elim
- elim t pattern using th hyps
-
-
-
- Synopsis:
-
- elim &sterm; &pattern; [using &sterm;] &intros-spec;
-
-
-
- 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.
- The induction predicate is restricted by
- pattern. In particular, if some hypothesis
- is listed in pattern, the hypothesis is
- generalized and cleared before eliminating t
-
-
-
-
- New sequents to prove:
-
- It opens one new sequent for each case. The names of
- the new hypotheses are picked by hyps, if
- 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
- elimType
- elimType T using th hyps
-
-
-
- Synopsis:
-
- elimType &sterm; [using &sterm;] &intros-spec;
-
-
-
- Pre-conditions:
-
- T must be an inductive type.
-
-
-
- Action:
-
- TODO (severely bugged now).
-
-
-
- New sequents to prove:
-
- TODO
-
-
-
-
-
-
- exact
- exact
- exact p
-
-
-
- Synopsis:
-
- exact &sterm;
-
-
-
- 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
- exists
- exists
-
-
-
- Synopsis:
-
- exists
-
-
-
- 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.
-
-
-
-
-
-
- fail
- fail
- fail
-
-
-
- Synopsis:
-
- fail
-
-
-
- Pre-conditions:
-
- None.
-
-
-
- Action:
-
- This tactic always fail.
-
-
-
- New sequents to prove:
-
- N.A.
-
-
-
-
-
-
- fold
- fold
- fold red t patt
-
-
-
- Synopsis:
-
- fold &reduction-kind; &sterm; &pattern;
-
-
-
- Pre-conditions:
-
- The pattern must not specify the wanted term.
-
-
-
- Action:
-
- 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
- t every occurrence of the normal form in the
- matched subterm.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
- fourier
- fourier
- fourier
-
-
-
- Synopsis:
-
- fourier
-
-
-
- Pre-conditions:
-
- 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.
-
-
-
- Action:
-
- It closes the current sequent by applying the Fourier method.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
- fwd
- fwd
- fwd H as H0 ... Hn
-
-
-
- Synopsis:
-
- fwd &id; [as &id; [&id;]â¦]
-
-
-
- Pre-conditions:
-
-
- The type of H must be the premise of a
- forward simplification theorem.
-
-
-
-
- Action:
-
-
- This tactic is under development.
- It simplifies the current context by removing
- H using the following methods:
- forward application (by lapply) of a suitable
- simplification theorem, chosen automatically, of which the type
- of H is a premise,
- decomposition (by decompose),
- rewriting (by rewrite).
- H0 ... Hn
- are passed to the tactics fwd invokes, as
- names for the premise they introduce.
-
-
-
-
- New sequents to prove:
-
-
- The ones opened by the tactics fwd invokes.
-
-
-
-
-
-
-
- generalize
- generalize
- generalize patt as H
-
-
-
- Synopsis:
-
- generalize &pattern; [as &id;]
-
-
-
- Pre-conditions:
-
- 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
- lemma that is proved using the new generated sequent.
-
-
-
- New sequents to prove:
-
- 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
- the occurrences of the term t matched by
- patt. If patt matches no
- subterm then t is defined as the
- wanted part of the pattern.
-
-
-
-
-
-
- id
- id
- id
-
-
-
- Synopsis:
-
- id
-
-
-
- Pre-conditions:
-
- None.
-
-
-
- Action:
-
- This identity tactic does nothing without failing.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
- intro
- intro
- intro H
-
-
-
- Synopsis:
-
- intro [&id;]
-
-
-
- Pre-conditions:
-
- The conclusion of the sequent to prove must be an implication
- or a universal quantification.
-
-
-
- Action:
-
- 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
- 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
- is automatically generated.
-
-
-
-
-
-
- intros
- intros
- intros hyps
-
-
-
- Synopsis:
-
- intros &intros-spec;
-
-
-
- Pre-conditions:
-
- If hyps specifies a number of hypotheses
- to introduce, then the conclusion of the current sequent must
- be formed by at least that number of imbricated implications
- or universal quantifications.
-
-
-
- Action:
-
- 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
- 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.
- The name of each new hypothesis is either popped from the
- user provided list of names, or it is automatically generated when
- the list is (or becomes) empty.
+ 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
+ prove.
-
- inversion
- inversion
- inversion t
+
+ assumption
+ assumption
+ assumption Synopsis:
- inversion &sterm;
+ assumptionPre-conditions:
- The type of the term t must be an inductive
- type or the application of an inductive type.
+ There must exist an hypothesis whose type can be unified with
+ the conclusion of the current sequent.Action:
- It proceeds by cases on t paying attention
- to the constraints imposed by the actual "right arguments"
- of the inductive type.
+ It closes the current sequent exploiting an hypothesis.New sequents to prove:
- 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"
- of the inductive type with terms originally present in the
- sequent to prove.
+ None
-
- lapply
- lapply
+
+ cases
+ cases
- lapply linear depth=d t
- to t1, ..., tn as H
+ cases t pattern
@@ -1194,15 +467,8 @@
Synopsis:
- lapply
- [linear]
- [depth=&nat;]
- &sterm;
- [to
- &sterm;
- [,&sterm;â¦]
- ]
- [as &id;]
+ cases
+ &term; &pattern;
@@ -1210,9 +476,7 @@
Pre-conditions:
- t must have at least d
- independent premises and n must not be
- greater than d.
+ t must inhabit an inductive type
@@ -1220,131 +484,147 @@
Action:
- Invokes letin H â (t ? ... ?)
- with enough ?'s to reach the
- d-th independent premise of
- t
- (d is maximum if unspecified).
- Then istantiates (by apply) with
- t1, ..., tn
- the ?'s corresponding to the first
- n independent premises of
- t.
- Usually the other ?'s preceding the
- n-th independent premise of
- t are istantiated as a consequence.
- If the linear flag is specified and if
- t, t1, ..., tn
- are (applications of) premises in the current context, they are
- cleared.
+ It proceed by cases on t. The new generated
+ hypothesis in each branch are named according to
+ hyps.
+ The elimintation predicate is restricted by
+ pattern. In particular, if some hypothesis
+ is listed in pattern, the hypothesis is
+ generalized and cleared before proceeding by cases on
+ t. Currently, we only support patterns of the
+ form H1 ⦠Hn ⢠%. This limitation will be lifted in the future.
New sequents to prove:
-
- The ones opened by the tactics lapply invokes.
-
+ One new sequent for each constructor of the type of
+ t. Each sequent has a new hypothesis for
+ each argument of the constructor.
-
- left
- left
- left
+
+
+
+ change
+ change
+ change patt with tSynopsis:
- normalize &pattern;
+ change &pattern; with &sterm;Pre-conditions:
- None.
+ Each subterm matched by the pattern must be convertible
+ with the term t disambiguated in the context
+ of the matched subterm.Action:
- It replaces all the terms matched by patt
- with their βδιζ-normal form.
+ 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.
@@ -1356,51 +636,54 @@
-
- reflexivity
- reflexivity
- reflexivity
+
+ cut
+ cut
+ cut PSynopsis:
- reflexivity
+ cut &sterm;Pre-conditions:
- The conclusion of the current sequent must be
- t=t for some term t
+ P must be a type.Action:
- It closes the current sequent by reflexivity
- of equality.
+ It closes the current sequent.New sequents to prove:
- None.
+ It opens two new sequents. The first one has conclusion
+ P â G where G is the
+ old conclusion.
+ The second sequent has conclusion P and
+ hypotheses the hypotheses of the current sequent to prove.
-
- replace
- change
- change patt with t
+
+
+ destruct
+ destruct
+ destruct (H0 ... Hn) skip (K0 ... Km)Synopsis:
- rewrite [<|>] &sterm; &pattern;
+ destruct
+ [(&id;â¦)] [skip(&id;â¦)]Pre-conditions:
- p must be the proof of an equality,
- possibly under some hypotheses.
+ Each hypothesis Hi must be either a Leibniz or a John Major equality where the two sides of the equality are possibly applied constructors of an inductive type.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.
+ The tactic recursively compare the two sides of each equality
+ looking for different constructors in corresponding position.
+ If two of them are found, the tactic closes the current sequent
+ by proving the absurdity of p. Otherwise
+ it adds a new hypothesis for each leaf of the formula that
+ states the equality of the subformulae in the corresponding
+ positions on the two sides of the equality. If the newly
+ added hypothesis is an equality between a variable and a term,
+ the variable is substituted for the term everywhere in the
+ sequent, except for the hypotheses Kj, and it is then cleared from the list of hypotheses.
+ New sequents to prove:
- It opens one new sequent for each hypothesis of the
- equality proved by p that is not closed
- by unification.
+ None.
-
- right
- right
- right
+
+ elim
+ elim
+ elim t patternSynopsis:
- right
+ elim &sterm; &pattern;Pre-conditions:
- The conclusion of the current sequent must be
- an inductive type or the application of an inductive type with
- at least two constructors.
+ t must inhabit an inductive type.
+ Action:
- Equivalent to constructor 2.
+ It proceeds by cases on the values of t,
+ according to the most appropriate elimination principle for
+ the current goal.
+ The induction predicate is restricted by
+ pattern. In particular, if some hypothesis
+ is listed in pattern, the hypothesis is
+ generalized and cleared before eliminating t
+ New sequents to prove:
- 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.
+ It opens one new sequent for each case.
-
- ring
- ring
- ring
+
+
+ generalize
+ generalize
+ generalize pattSynopsis:
- simplify &pattern;
+ generalize &pattern;Pre-conditions:
- None.
+ All the terms matched by patt must be
+ convertible and close in the context of the current sequent.Action:
- It replaces all the terms matched by patt
- with other convertible terms that are supposed to be simpler.
+ It closes the current sequent by applying a stronger
+ lemma that is proved using the new generated sequent.New sequents to prove:
- None.
+ 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
+ the occurrences of the term t matched by
+ patt. If patt matches no
+ subterm then t is defined as the
+ wanted part of the pattern.
-
- split
- split
- split
+
+
+ inversion
+ inversion
+ inversion tSynopsis:
- subst
+ inversion &sterm;Pre-conditions:
-
- None.
-
+
+ The type of the term t must be an inductive
+ type or the application of an inductive type.
+ Action:
-
- For each premise of the form
- H: x = t or H: t = x
- where x is a local variable and
- t does not depend on x,
- the tactic rewrites H wherever
- x appears clearing H and
- x afterwards.
-
+
+ It proceeds by cases on t paying attention
+ to the constraints imposed by the actual "right arguments"
+ of the inductive type.
+ New sequents to prove:
-
- The one opened by the applied tactics.
-
+
+ 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"
+ of the inductive type with terms originally present in the
+ sequent to prove. It uses either Leibniz or John Major equality
+ for the new hypotheses, according to the included files.
+
-
- symmetry
- symmetry
- The tactic symmetry
- symmetry
+
+ lapply
+ lapply
+
+ lapply t
+ Synopsis:
- symmetry
+
+ lapply
+ &sterm;
+ Pre-conditions:
- The conclusion of the current proof must be an equality.
+ None.Action:
- It swaps the two sides of the equalityusing the symmetric
- property.
+
+ It generalizes the conclusion of the current goal
+ adding as a premise the type of t,
+ closing the current goal.
+ New sequents to prove:
- None.
+
+ The new sequent has conclusion T â G where
+ T is the type of t
+ and G the old conclusion.
+
-
- transitivity
- transitivity
- transitivity t
+
+ letin
+ letin
+ letin x â tSynopsis:
- transitivity &sterm;
+ letin &id; â &sterm;Pre-conditions:
- The conclusion of the current proof must be an equality.
+ None.Action:
- It closes the current sequent by transitivity of the equality.
+ It adds to the context of the current sequent to prove a new
+ definition x â t.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.
+ None.
-
- unfold
- unfold
- unfold t patt
+
+ normalize
+ normalize
+ normalize patt nodeltaSynopsis:
- unfold [&sterm;] &pattern;
+ normalize &pattern;
+ [nodelta]
@@ -1746,12 +1049,9 @@ the current sequent to prove.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.
+ It replaces all the terms matched by patt
+ with their βδιζ-normal form. If nodelta is
+ specified, δ-expansions are not performed.
@@ -1766,13 +1066,13 @@ the current sequent to prove.
whdwhd
- whd patt
+ whd patt nodeltaSynopsis:
- whd &pattern;
+ whd &pattern; [nodelta]
@@ -1785,7 +1085,7 @@ the current sequent to prove.Action:It replaces all the terms matched by patt
- with their βδιζ-weak-head normal form.
+ with their βδιζ-weak-head normal form. If nodelta is specified, δ-expansions are not performed.