From 784f0d4d7cff3700363affe647f7b8b218726fcb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Oct 2019 09:06:34 +0200 Subject: [PATCH] Update online helper entries Fix a wrong message error in 'that is equivalent to' tactic Add a check on the context of the current proof in 'by induction hypothesis' tactic --- matita/components/ng_tactics/declarative.ml | 8 +- .../matita/help/C/sec_declarative_tactics.xml | 498 +++++++++++------- 2 files changed, 304 insertions(+), 202 deletions(-) diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml index d96e66811..a136a51dd 100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@ -169,7 +169,7 @@ let beta_rewriting_step t status = ( let newhypo = status_parameter "volatile_newhypo" status in if newhypo = "" then - fail (lazy "Invalid use of 'or equivalently'") + fail (lazy "Invalid use of 'that is equivalent to'") else change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status ) @@ -538,7 +538,11 @@ let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status = | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion") ;; -let byinduction t1 id = suppose t1 id ;; +let byinduction t1 id status = + let ctx = status_parameter "context" status in + if ctx <> "induction" then fail (lazy "You can't use this tactic outside of an induction context") + else suppose t1 id status +;; let name_of_conj conj = let mattrs,_,_ = conj in diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml index 9c1ed995c..76acf5e0a 100644 --- a/matita/matita/help/C/sec_declarative_tactics.xml +++ b/matita/matita/help/C/sec_declarative_tactics.xml @@ -14,39 +14,38 @@ assume assume - assume x : T that is equivalent to T' + assume x : T Synopsis: assume &id; : - &sterm; [ that is equivalent to &term; ] + &sterm; Pre-conditions: - The conclusion of the current proof must be - ∀x:T.P or - T→P where T is - a data type (i.e. T has type - Set or Type). + + The conclusion of the sequent to prove must be a universal quantification. + Action: - It adds to the context of the current sequent to prove a new declaration x : T - . The new conclusion becomes P. Alternatively, if a type - T' is supplied and T and T' are beta equivalent the new declaration that is added to the context is - x:T'. + + It applies the right introduction rule for the universal quantifier, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the quantifier). + New sequents to prove: - None. + + It opens a new sequent to prove the quantified subformula adding x : T to the hypotheses. + @@ -56,40 +55,38 @@ suppose suppose - suppose T (x) that is equivalent to T' + suppose A (H) Synopsis: suppose &term; ( &id; - ) [ that is equivalent to &term; ] + ) Pre-condition: - - The conclusion of the current proof must be - ∀x:T.P or - T→P where T is - a proposition (i.e. T has type - Prop or CProp). - + + + The conclusion of the sequent to prove must be an implication. + + Action: - It adds to the context of the current sequent to prove a new declaration x : T - . The new conclusion becomes P. Alternatively, if a type - T' is supplied and T and T' are beta equivalent the new declaration that is added to the context is - x:T'. + + It applies the right introduction rule for the implication, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the implication). New sequents to prove: - None. + + It opens a new sequent to prove the consequent of the implication adding the antecedent A to the hypotheses. The name of the new hypothesis is H. + @@ -130,88 +127,171 @@ + + that is equivalent to + that is equivalent to + that is equivalent to t + + + + Synopsis: + + + that is equivalent to &term; + + + + + Pre-condition: + + + The user must have applied one of the following tactics immediately before applying this tactic: assume, suppose, we need to prove, by just we proved,the thesis becomes, that is equivalent to. + + + + + Action: + + + If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term t is beta-equivalent to the term t1 on which this tactic is working (i.e. they can be reduced to a common term), t1 is changed with t. + + If the tactic that was applied before this tactic was that is equivalent to, and that tactic was working on a term t1, this tactic keeps working on t1. + + + + + New sequent to prove: + + + If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to t is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with t. + + + + + + + + + the thesis becomes + the thesis becomes + the thesis becomes P + + + + Synopsis: + + the thesis becomes &term; + + + + Pre-condition: + + The provided term P must be identical to the current conclusion. + + + + Action: + + It allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to, after stating the current conclusion. + + + + New sequent to prove: + + None. + + + + + + + + we need to prove + we need to prove + we need to prove T [(H)] + + + + Synopsis: + + we need to prove &term; + [(&id; + )] + + + + + Pre-condition: + + None. + + + + Action: + + If id is provided, it applies a logical cut on T. Otherwise, it allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to. + + + + + New sequents to prove: + + If id is supplied, a new sequent with T as the conclusion is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H:T added to the hypotheses. + + + + + + we proved we proved - justification we proved T (id) that is equivalent to T' + justification we proved T [(id)] Synopsis: &justification; we proved &term; - ( &id; - ) [ that is equivalent to &term;] [ done] + [( &id; + )] + Pre-condition: - T must have type Prop. - + + None. + Action: - It derives T - using the justification and labels the conclusion with - id. Alternatively, if a proposition - T' is supplied and T and T' are beta equivalent the new hypothesis that is added to the context is - id:T'. - - If the user does not supply a label and ends the command with done then if T is alpha equivalent to the conclusion of the current sequent then it closes it (if T' is supplied this must be alpha equivalent to the conclusion, but in this case T does not need to). - + + If id is supplied, a logical cut on T is made. Otherwise, if T is identical to the current conclusion, it allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to. + New sequent to prove: - None. + + If id is supplied, a new sequent with T as the conclusion is opened and then immediately closed using the supplied justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and a new hypotesis T is added to the context, with name id. + If id is not supplied, no new sequents are opened. + - - done - done - justification done - - - - Synopsis: - - &justification; done - - - - Pre-condition: - - - - - - Action: - - It closes the current sequent given the justification. - - - - New sequents to prove: - - None. - - - - - let such that let such that - justification let x:t such that p (id) + justification let x:T such that P (H) @@ -227,24 +307,22 @@ Pre-condition: + None. Action: - It derives ∃x:t.p using the - justification and then it introduces in the context - x and the hypothesis - p labelled with - id. - + + It applies the left introduction rule of the existential quantifier on the formula ∃ x. P(x) (in Natural Deduction this corresponds to the elimination rule for the quantifier). + New sequent to prove: - None. + A new sequent with ∃ x. P(x) as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses x : T and H : P are added to the context. @@ -254,7 +332,7 @@ we have we have - justification we have t1 (id1) and t2 (id2) + justification we have A (H1) and B (H2) @@ -269,75 +347,34 @@ Pre-condition: - + + None. + Action: - It derives t1∧t2 using the - justification then it introduces in the context - t1 labelled with id1 and - t2 labelled with id2. - + + It applies the left multiplicative introduction rule for the conjunction on the formula A ∧ B (in Natural Deduction this corresponds to the elimination rule for the conjunction). + New sequent to prove: - None. + A new sequent with A ∧ B as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses H1 : A and H2 : B are added to the context. - - we need to prove - we need to prove - we need to prove t1 (id) or equivalently t2 - - - - Synopsis: - - we need to prove &term; - [(&id; - )] - [ or equivalently &term;] - - - - Pre-condition: - - - - - - Action: - - If id is provided, starts a subproof that once concluded - will be named id. Otherwise states what needs to be proved. - If t2 is provided, the new goal is - immediately changed to t2 wich must - be equivalent to t1. - - - - - New sequents to prove: - - The stated one if id is provided - - - - - we proceed by induction on we proceed by induction on - we proceed by induction on t to prove th + we proceed by induction on t to prove P @@ -349,22 +386,20 @@ Pre-condition: - t must inhabitant of an inductive type and - th must be the conclusion to be proved by induction. + The type of t must be an inductive type and P must be identical to the current conclusion. Action: - It proceed by induction on t. + It applies the induction principle on t to prove P. New sequents to prove: - It opens one new sequent for each constructor of the - type of t. + It opens a new sequent for each constructor of the type of t, each with the conclusion P instantiated for the constructor. For the inductive constructors (i.e. if the inductive type is T, constructors with an argument of type T), the conclusion is a logical implication, where the antecedent is the inductive hypothesis for the constructor, and the consequent is P. @@ -374,7 +409,7 @@ we proceed by cases on we proceed by cases on - we proceed by cases on t to prove th + we proceed by cases on t to prove P @@ -386,22 +421,24 @@ Pre-condition: - t must inhabitant of an inductive type and + The type of t must be an inductive type and P must be identical to the current conclusion. + + Action: - It proceeds by cases on t + It proceeds by case-analysis on t New sequents to prove: It opens one new sequent for each constructor of the - type of t. + type of t, each with the conclusion P instantiated for the constructor. @@ -411,33 +448,31 @@ case case - case id (id1:t1) … (idn:tn) + case id (id1:T1) … (idn:Tn) Synopsis: - case &id; [( &id; : &term; )] … + case &id; [( &id; : &term; )] … [( &id; : &term; )] Pre-condition: - To be used in a proof by induction or by cases to start - a new case + The user must have started a proof by induction/cases that has not been concluded yet, id must be a constructor for the inductive type of the term under induction/case-analysis, and the case must not have already been proved. Action: - Starts the new case id declaring - the local parameters (id1:t1) … (idn:tn) + It starts the proof for the case id, where id1:T1,…,idn:Tn are the arguments of the constructor, each declared with its type. New sequents to prove: - None + The sequent for the case id. @@ -447,7 +482,7 @@ by induction hypothesis we know by induction hypothesis we know - by induction hypothesis we know t (id) + by induction hypothesis we know P (id) @@ -458,14 +493,13 @@ Pre-condition: - To be used in a proof by induction to state the inductive - hypothesis. + The user must have started proving a case for a proof by induction/case-analysis. Action: - Introduces the inductive hypothesis. + It introduces the inductive hypothesis. @@ -478,86 +512,150 @@ - - the thesis becomes - the thesis becomes - the thesis becomes t - - - - Synopsis: + + conclude + conclude + conclude t1 + + + + Synopsis: + + conclude &term; + + + + Pre-condition: - the thesis becomes &term; - - - - Pre-condition: + + The current conclusion must be an equality t1 = tk + + + + + Action: + + It starts an equality chain on the conclusion. It allows the user to apply the tactic = to continue the chain. + + + + New sequent to prove: - The provided term t must be convertible with - current sequent. + None. - - - Action: + + + + + + obtain + obtain + obtain H t1 + + + + Synopsis: + + obtain &id; &term; + + + + Pre-condition: - It changes the current goal to the one provided. - - - - New sequent to prove: + + None. + + + + + Action: + + It starts an equality chain t1 = ?, which, when concluded, will be added to hypoteses of the current sequent. It allows the user to apply the tactic = to continue the chain. + + + + New sequent to prove: - None. + A new sequent for t1 = ? is opened, a new sequent for ? is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H: t1 = ? added to its hypotheses. This hypotesis will be changed when the equality chain is concluded with H: t1 = tk, where tk is the last term of the equality chain. The goal for ? can be safely ignored, as it will be automatically closed when the equality chain is concluded. - - - + + + - - - conclude/obtain - conclude/obtain - conclude/obtain (H) t1 = t2 justification + + = + = + = t2 justification Synopsis: - [obtain &id; | conclude &term;] = &term; [&autoparams; | using &term; | using once &term; | proof] [done] + + = &term; [&autoparams; | using &term; | using once &term; | proof] [done] + Pre-condition: - conclude can be used only if the current - sequent is stating an equality. The left hand side must be omitted - in an equality chain. + + The user must have started an equality chain with conclude or obtain that has not been concluded yet. + Action: - Starts or continues an equality chain. If the chain starts - with obtain H a new subproof named - H is started. + + It applies the transitivity of = on the left-hand-side of the current conclusion, t2, and the right-hand-side of the current conclusion, using the given justification. If done is supplied, this represents the last step in the equality chain. + New sequent to prove: - If the chain starts - with obtain H a nre sequent for - t2 = ? is opened. - + + A new sequent for lhs = t2 is opened and then immediately closed using the given justification. A new sequent with the conclusion t2 = rhs is opened. + + + done + done + justification done + + + + Synopsis: + + &justification; done + + + + Pre-condition: + + The user is proving a sequent which was opened with the tactic we need to prove, or the user is proving a sequent which was opened with the tactic we proceed by induction/cases on, or the user is proving a chain of equalities that was started with either the tactic conclude or obtain. + + + + Action: + + It closes the current sequent with the given justification. + + + + New sequents to prove: + + None. + + + + + - - - - - -- 2.39.2