X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_declarative_tactics.xml;h=9c1ed995cea4f717e813ecb9b1d596944ceeef60;hp=bc0b424e0d3b0bb75ed6613a456fa904315136c8;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hpb=9ab5bcc58aa62e4ded71fd64cc5a4ea562195103
diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml
index bc0b424e0..9c1ed995c 100644
--- a/matita/matita/help/C/sec_declarative_tactics.xml
+++ b/matita/matita/help/C/sec_declarative_tactics.xml
@@ -14,13 +14,14 @@
assume
assume
- assume x : t
+ assume x : T that is equivalent to T'
Synopsis:
- assume &id; : &sterm;
+ assume &id; :
+ &sterm; [ that is equivalent to &term; ]
@@ -36,9 +37,10 @@
Action:
- It adds to the context of the current sequent to prove a new
- declaration x : T . The new conclusion becomes
- P.
+ 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'.
@@ -51,75 +53,126 @@
-
- by induction hypothesis we know
- by induction hypothesis we know
- by induction hypothesis we know t (id)
-
-
-
- Synopsis:
- by induction hypothesis we know &term; ( &id; )
-
-
-
- Pre-condition:
-
- To be used in a proof by induction to state the inductive
- hypothesis.
-
-
-
- Action:
-
- Introduces the inductive hypothesis.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
+
+ suppose
+ suppose
+ suppose T (x)Â that is equivalent to T'
+
+
+
+ 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).
+
+
+
+ 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'.
+
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
-
- case
- case
- case id (id1:t1) ⦠(idn:tn)
+
+ letin
+ letin
+ let x := T
+
+
+
+ Synopsis:
+
+ let &id; = &term;
+
+
+
+ Pre-condition:
+
+ None
+
+
+
+ Action:
+
+ It adds a new local definition x := T to the context of the sequent to prove.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+
+ we proved
+ we proved
+ justification we proved T (id) that is equivalent to T'
Synopsis:
- case &id; [( &id; : &term; )] â¦
-
-
-
- Pre-condition:
-
- To be used in a proof by induction or by cases to start
- a new case
-
-
-
- Action:
-
- Starts the new case id declaring
- the local parameters (id1:t1) ⦠(idn:tn)
-
-
-
- New sequents to prove:
-
- None
+ &justification; we proved &term;
+ ( &id;
+ ) [ that is equivalent to &term;] [ done]
-
-
-
-
+
+
+ Pre-condition:
+
+ T must have type Prop.
+
+
+
+
+ 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).
+
+
+
+
+ New sequent to prove:
+
+ None.
+
+
+
+
+
done
@@ -155,8 +208,7 @@
-
-
+
let such that
let such that
justification let x:t such that p (id)
@@ -199,123 +251,47 @@
-
- obtain
- obtain
- obtain H t1 = t2 justification
+
+ we have
+ we have
+ justification we have t1 (id1) and t2 (id2)
+
-
- Synopsis:
-
- [obtain &id; | conclude &term;] = &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.
-
-
-
- Action:
-
- Starts or continues an equality chain. If the chain starts
- with obtain H a new subproof named
- H is started.
-
-
-
- New sequent to prove:
-
- If the chain starts
- with obtain H a nre sequent for
- t2 = ? is opened.
-
-
-
-
-
-
-
-
- suppose
- suppose
- suppose t1 (x)Â that is equivalent to t2
-
-
-
- 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).
-
-
-
- Action:
+
+ Synopsis:
- It adds to the context of the current sequent to prove a new
- declaration x : T . The new conclusion becomes
- P.
+ &justification; we have &term;
+ ( &id; ) and &term;
+ ( &id; )
+
+
+
+ Pre-condition:
+
+
-
-
- New sequents to prove:
-
- None.
-
-
-
-
+
+
+ Action:
+
+ It derives t1â§t2 using the
+ justification then it introduces in the context
+ t1 labelled with id1 and
+ t2 labelled with id2.
+
+
+
+
+ New sequent to prove:
+
+ None.
+
+
+
+
-
- the thesis becomes
- the thesis becomes
- the thesis becomes t
-
-
-
- Synopsis:
-
- the thesis becomes &term;
-
-
-
- Pre-condition:
-
- The provided term t must be convertible with
- current sequent.
-
-
-
- Action:
-
- It changes the current goal to the one provided.
-
-
-
- New sequent to prove:
-
- None.
-
-
-
-
-
-
we need to prove
we need to prove
@@ -358,44 +334,39 @@
-
-
- we have
- we have
- justification we have t1 (id1) and t2 (id2)
-
+
+ we proceed by induction on
+ we proceed by induction on
+ we proceed by induction on t to prove th
-
+
Synopsis:
- &justification; we have &term;
- ( &id; ) and &term;
- ( &id; )
-
+ we proceed by induction on &term; to prove &term;
+
-
+
Pre-condition:
-
+ t must inhabitant of an inductive type and
+ th must be the conclusion to be proved by induction.
+
Action:
-
- It derives t1â§t2 using the
- justification then it introduces in the context
- t1 labelled with id1 and
- t2 labelled with id2.
-
-
-
-
- New sequent to prove:
-
- None.
-
+
+ It proceed by induction on t.
+
+
+ New sequents to prove:
+
+ It opens one new sequent for each constructor of the
+ type of t.
+
+
@@ -436,73 +407,100 @@
-
-
- we proceed by induction on
- we proceed by induction on
- we proceed by induction on t to prove th
-
-
-
- Synopsis:
-
- we proceed by induction on &term; to prove &term;
-
-
-
- Pre-condition:
-
- t must inhabitant of an inductive type and
- th must be the conclusion to be proved by induction.
-
-
-
-
- Action:
-
- It proceed by induction on t.
-
-
-
- New sequents to prove:
-
- It opens one new sequent for each constructor of the
- type of t.
-
-
-
-
-
-
-
- we proved
- we proved
- justification we proved t (id)
+
+ case
+ case
+ case id (id1:t1) ⦠(idn:tn)
Synopsis:
- &justification; we proved &term;
- ( &id;
- )
+ case &id; [( &id; : &term; )] â¦
+
+
+
+ Pre-condition:
+
+ To be used in a proof by induction or by cases to start
+ a new case
+
+
+
+ Action:
+
+ Starts the new case id declaring
+ the local parameters (id1:t1) ⦠(idn:tn)
+
+
+
+ New sequents to prove:
+
+ None
+
+
+
+
+
+
+ by induction hypothesis we know
+ by induction hypothesis we know
+ by induction hypothesis we know t (id)
+
+
+
+ Synopsis:
+ by induction hypothesis we know &term; ( &id; )
+
+
+
+ Pre-condition:
+
+ To be used in a proof by induction to state the inductive
+ hypothesis.
+
+
+
+ Action:
+
+ Introduces the inductive hypothesis.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+
+ the thesis becomes
+ the thesis becomes
+ the thesis becomes t
+
+
+
+ Synopsis:
+
+ the thesis becomes &term;
+
Pre-condition:
- tmust have type Prop.
-
+ The provided term t must be convertible with
+ current sequent.
Action:
- It derives t
- using the justification and labels the conclusion with
- id.
-
+ It changes the current goal to the one provided.
@@ -513,6 +511,53 @@
-
+
+
+ conclude/obtain
+ conclude/obtain
+ conclude/obtain (H) t1 = t2 justification
+
+
+
+ Synopsis:
+
+ [obtain &id; | conclude &term;] = &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.
+
+
+
+ Action:
+
+ Starts or continues an equality chain. If the chain starts
+ with obtain H a new subproof named
+ H is started.
+
+
+
+ New sequent to prove:
+
+ If the chain starts
+ with obtain H a nre sequent for
+ t2 = ? is opened.
+
+
+
+
+
+
+
+
+
+
+
+
+