X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=0fabbbf7ca5f8a68167a62bcaa68334f59363eb3;hb=a3f4c0a8b4328cb9a9fe3b4c2e577be2a258675c;hp=712ce837a524ec2cd360fc94ad45f12e04fdf5e2;hpb=93cc0505102768f7d4337907bafa31d1528a7289;p=helm.git diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 712ce837a..0fabbbf7c 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -86,6 +86,61 @@ + + applyS + applyS + applyS t auto_params + + + + Synopsis: + + applyS &sterm; &autoparams; + + + + Pre-conditions: + + t must have type + T1 → ... → + Tn → G. + + + + 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. + + + + + 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. + + + + + assumption assumption @@ -123,13 +178,13 @@ auto auto - auto depth=d width=w paramodulation full + auto params Synopsis: - auto [depth=&nat;] [width=&nat;] [paramodulation] [full] + auto &autoparams; @@ -137,10 +192,10 @@ 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. + 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 ...TODO + a sequent is ...&TODO; @@ -160,30 +215,89 @@ + + cases + cases + + cases t hyps + + + + + Synopsis: + + + cases + &term; [([&id;]…)] + + + + + Pre-conditions: + + + t must inhabit an inductive type + + + + + Action: + + + It proceed by cases on t. The new generated + hypothesis in each branch are named according to + hyps. + + + + + 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. + + + + + clear clear - clear H + + clear H1 ... Hm + Synopsis: - clear &id; + + clear + &id; [&id;…] + Pre-conditions: - H must be an hypothesis of the - current sequent to prove. + + + H1 ... Hm + must be hypotheses of the + current sequent to prove. + Action: - It hides the hypothesis H from the - current sequent. + + It hides the hypotheses + + H1 ... Hm + from the current sequent. + @@ -230,6 +344,58 @@ + + compose + compose + compose n t1 with t2 hyps + + + + Synopsis: + + compose [&nat;] &sterm; [with &sterm;] [&intros-spec;] + + + + Pre-conditions: + + + + + + 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. + + + + New sequents to prove: + + The same, but with more hypothesis eventually introduced + by the &intros-spec;. + + + + + change change @@ -382,35 +548,38 @@ decompose decompose - decompose (T1 ... Tn) H hips + decompose as H1 ... Hm Synopsis: - decompose &id; [&id;]… &intros-spec; + + decompose + [as &id;…] + Pre-conditions: - - H must inhabit one inductive type among - - T1 ... Tn - - and the types of a predefined list. - + None. Action: - Runs elim H hyps, clears H and tries to run - itself recursively on each new identifier introduced by - elim in the opened sequents. + 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. @@ -425,16 +594,16 @@ - - demodulation - demodulation - demodulation patt + + demodulate + demodulate + demodulate Synopsis: - demodulation &pattern; + demodulate @@ -458,30 +627,35 @@ - - discriminate - discriminate - discriminate p + + destruct + destruct + destruct p Synopsis: - discriminate &sterm; + destruct &sterm; 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. + p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type. Action: - It closes the current sequent by proving the absurdity of - p. + 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. + @@ -750,31 +924,48 @@ its constructor takes no arguments. fwd fwd - fwd ...TODO + fwd H as H0 ... Hn Synopsis: - fwd &id; [([&id;]…)] + fwd &id; [as &id; [&id;]…] Pre-conditions: - TODO. + + The type of H must be the premise of a + forward simplification theorem. + Action: - TODO. + + 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: - TODO. + + The ones opened by the tactics fwd invokes. + @@ -855,43 +1046,6 @@ its constructor takes no arguments. - - injection - injection - injection p - - - - Synopsis: - - injection &sterm; - - - - 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. - - - - - intro intro @@ -1019,7 +1173,7 @@ its constructor takes no arguments. lapply lapply - lapply depth=d t + lapply linear depth=d t to t1, ..., tn as H @@ -1027,25 +1181,59 @@ its constructor takes no arguments. Synopsis: - lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]…] [as &id;] + + lapply + [linear] + [depth=&nat;] + &sterm; + [to + &sterm; + [,&sterm;…] + ] + [as &id;] + Pre-conditions: - TODO. + + t must have at least d + independent premises and n must not be + greater than d. + Action: - TODO. + + 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. + New sequents to prove: - TODO. + + The ones opened by the tactics lapply invokes. + @@ -1156,39 +1344,6 @@ its constructor takes no arguments. - - paramodulation - paramodulation - paramodulation patt - - - - Synopsis: - - paramodulation &pattern; - - - - Pre-conditions: - - TODO. - - - - Action: - - TODO. - - - - New sequents to prove: - - TODO. - - - - - reduce reduce @@ -1482,6 +1637,46 @@ its constructor takes no arguments. + + + subst + subst + subst + + + + Synopsis: + + subst + + + + Pre-conditions: + + None. + + + + 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. + + + + New sequents to prove: + + The one opened by the applied tactics. + + + + + symmetry symmetry