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=a423f37c419e08dd60bb1e14b3a7e21f326c3569;hpb=1da3c8d481853c3d6b9f33385ebde848866a37b5;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index a423f37c4..cc0043724 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -1,189 +1,1358 @@
-
+
Tactics
-
- absurd <term>
- The tactic absurd
-
-
-
-
- apply <term>
- The tactic apply
-
-
- assumption
- The tactic assumption
-
-
- auto [depth=<int>] [width=<int>] [paramodulation] [full]
- The tactic auto
-
-
- clear <id>
- The tactic clear
-
-
- clearbody <id>
- The tactic clearbody
-
-
- change <pattern> with <term>
- The tactic change
-
-
- compare <term>
- The tactic compare
-
-
- constructor <int>
- The tactic constructor
-
-
- contradiction
- The tactic contradiction
-
-
- cut <term> [as <id>]
- The tactic cut
-
-
- decide
- The tactic decide equality
-
-
- decompose [<ident list>] <ident> [<intros_spec>]
- The tactic decompose
-
-
- discriminate <term>
- The tactic discriminate
-
-
- elim <term> [using <term>] [<intros_spec>]
- The tactic elim
-
-
- elimType <term> [using <term>]
- The tactic elimType
-
-
- exact <term>
- The tactic exact
-
-
- exists
- The tactic exists
-
-
- fail
- The tactic fail
-
-
- fold <reduction_kind> <term> <pattern>
- The tactic fold
-
-
- fourier
- The tactic fourier
-
-
- fwd <ident> [<ident list>]
- The tactic fwd
-
-
- generalize <pattern> [as <id>]
- The tactic generalize
-
-
- id
- The tactic id
-
-
- injection <term>
- The tactic injection
-
-
- intro [<ident>]
- The tactic intro
-
-
- intros <intros_spec>
- The tactic intros
-
-
- intros <term>
- The tactic intros
-
-
- lapply [depth=<int>] <term> [to <term list] [using <ident>]
- The tactic lapply
-
-
- left
- The tactic left
-
-
- letin <ident> â <term>
- The tactic letin
-
-
- normalize <pattern>
- The tactic normalize
-
-
- paramodulation <pattern>
- The tactic paramodulation
-
-
- reduce <pattern>
- The tactic reduce
-
-
- reflexivity
- The tactic reflexivity
-
-
- replace <pattern> with <term>
- The tactic replace
-
-
- rewrite {<|>} <term> <pattern>
- The tactic rewrite
-
-
- right
- The tactic right
-
-
- ring
- The tactic ring
-
-
- simplify <pattern>
- The tactic simplify
-
-
- split
- The tactic split
-
-
- symmetry
+
+ <emphasis role="bold">absurd</emphasis> &sterm;
+ absurd
+ absurd P
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">apply</emphasis> &sterm;
+ apply
+ apply t
+
+
+
+ Pre-conditions:
+
+ t must have type
+ T1 â ... â
+ Tn â G
+ where G can be unified with the conclusion
+ of the current sequent.
+
+
+
+ Action:
+
+ 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
+ Ti that is not
+ instantiated by unification. Ti is
+ the conclusion of the i-th new sequent to
+ prove.
+
+
+
+
+
+
+ <emphasis role="bold">assumption</emphasis>
+ 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
+
+
+
+
+
+
+ <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
+
+
+
+ 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
+
+
+
+
+
+
+ <emphasis role="bold">clear</emphasis> &id;
+ 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
+
+
+
+
+
+
+ <emphasis role="bold">clearbody</emphasis> &id;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">change</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;
+ change
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">constructor</emphasis> &nat;
+ constructor
+ constructor n
+
+
+
+ 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.
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">contradiction</emphasis>
+ 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
+
+
+
+
+
+
+ <emphasis role="bold">cut</emphasis> &sterm; [<emphasis role="bold">as</emphasis> &id;]
+ cut
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">decompose</emphasis> &id; [&id;]⦠&intros-spec;
+ decompose
+
+ decompose (T1 ... Tn) H hips
+
+
+
+
+ Pre-conditions:
+
+
+ H must inhabit one inductive type among
+
+ T1 ... Tn
+
+ and the types of a predefined list.
+
+
+
+
+ Action:
+
+
+ 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:
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">discriminate</emphasis> &sterm;
+ discriminate
+ discriminate p
+
+
+
+ Pre-conditions:
+
+ p must have type K t1 ... tn = K' 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.
+
+
+
+
+
+
+ <emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;
+ 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. 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.
+
+
+
+
+
+
+ <emphasis role="bold">elimType</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;
+ elimType
+ elimType T using th hyps
+
+
+
+ Pre-conditions:
+
+ T must be an inductive type.
+
+
+
+ Action:
+
+ TODO (severely bugged now).
+
+
+
+ New sequents to prove:
+
+ TODO
+
+
+
+
+
+
+ <emphasis role="bold">exact</emphasis> &sterm;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">exists</emphasis>
+ exists
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">fail</emphasis>
+ fail
+ fail
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ This tactic always fail.
+
+
+
+ New sequents to prove:
+
+ N.A.
+
+
+
+
+
+
+ <emphasis role="bold">fold</emphasis> &reduction-kind; &sterm; &pattern;
+ fold
+ fold red t patt
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">fourier</emphasis>
+ fourier
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]â¦<emphasis role="bold">)</emphasis>]
+ fwd
+ fwd ...TODO
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
+
+
+ <emphasis role="bold">generalize</emphasis> &pattern; [<emphasis role="bold">as</emphasis> &id;]
+ generalize
+ generalize patt as H
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">id</emphasis>
+ id
+ id
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ This identity tactic does nothing without failing.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ <emphasis role="bold">injection</emphasis> &sterm;
+ injection
+ injection p
+
+
+
+ Pre-conditions:
+
+ p must have type K t1 ... tn = K t'1 ... t'n where both argument lists are empty if
+K takes no arguments.
+
+
+
+ Action:
+
+ It derives new hypotheses by injectivity of
+ K.
+
+
+
+ New sequents to prove:
+
+ The new sequent to prove is equal to the current sequent
+ with the additional hypotheses
+ t1=t'1 ... tn=t'n.
+
+
+
+
+
+
+ <emphasis role="bold">intro</emphasis> [&id;]
+ intro
+ intro H
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">intros</emphasis> &intros-spec;
+ intros
+ intros hyps
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">inversion</emphasis> &sterm;
+ inversion
+ inversion t
+
+
+
+ Pre-conditions:
+
+ 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
+ to the constraints imposed by the actual "right arguments"
+ of the inductive type.
+
+
+
+ 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.
+
+
+
+
+
+
+ <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 depth=d t
+ to t1, ..., tn as H
+
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
+
+
+ <emphasis role="bold">left</emphasis>
+ left
+ left
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">â</emphasis> &sterm;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">normalize</emphasis> &pattern;
+ normalize
+ normalize patt
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It replaces all the terms matched by patt
+ with their βδιζ-normal form.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ <emphasis role="bold">paramodulation</emphasis> &pattern;
+ paramodulation
+ paramodulation patt
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
+
+
+ <emphasis role="bold">reduce</emphasis> &pattern;
+ reduce
+ reduce patt
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It replaces all the terms matched by patt
+ with their βδιζ-normal form.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ <emphasis role="bold">reflexivity</emphasis>
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">rewrite</emphasis> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">right</emphasis>
+ right
+ right
+
+
+
+ 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.
+
+
+
+ Action:
+
+ Equivalent to constructor 2.
+
+
+
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">ring</emphasis>
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">simplify</emphasis> &pattern;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">split</emphasis>
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">symmetry</emphasis>
+ symmetry
The tactic symmetry
-
-
- transitivity <term>
- The tactic transitivity
-
-
- unfold [<term>] <pattern>
- The tactic unfold
-
-
- whd <pattern>
- The tactic whd
-
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">transitivity</emphasis> &sterm;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;
+ 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.
+
+
+
+
+
+
+ <emphasis role="bold">whd</emphasis> &pattern;
+ 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.
+
+
+
+
+
+
+
-