From: maiorino Date: Tue, 14 Nov 2006 15:30:25 +0000 (+0000) Subject: New: on-line help for declarative tactics (first version). X-Git-Tag: 0.4.95@7852~812 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20b60553cce4dc729f58a078619207d82e94192f;p=helm.git New: on-line help for declarative tactics (first version). --- diff --git a/matita/help/C/Makefile b/matita/help/C/Makefile index e85ad9a99..2ca1a16b1 100644 --- a/matita/help/C/Makefile +++ b/matita/help/C/Makefile @@ -14,9 +14,12 @@ DESTDIR = /usr/local/share/doc/matita/ all: quickref -quickref: tactic_quickref.xml -tactic_quickref.xml: xsl/tactic_quickref.xsl sec_tactics.xml - $(XSLTPROC) $< matita.xml > tactic_quickref.xml +quickref: tactics_quickref.xml declarative_tactics_quickref.xml + +tactics_quickref.xml: xsl/tactic_quickref.xsl sec_tactics.xml + $(XSLTPROC) --param declarative "''" $< matita.xml > tactics_quickref.xml +declarative_tactics_quickref.xml: xsl/tactic_quickref.xsl sec_declarative_tactics.xml + $(XSLTPROC) --param declarative "'declarative_'" $< matita.xml > declarative_tactics_quickref.xml # one of: "fop", "pdflatex" PDF_METHOD=pdflatex @@ -40,7 +43,7 @@ test: .PHONY: html html: html-stamp html-stamp: $(MAIN) $(DEPS) $(XHTML_XSL) - xsltproc $(XHTML_XSL) $< + $(XSLTPROC) $(XHTML_XSL) $< touch $@ # TXTs generation @@ -61,13 +64,13 @@ pdf-stamp: $(patsubst %.xml,%.pdf,$(MAIN)) touch $@ %.fo: %.xml - xsltproc $(FO_XSL) $< | xmllint --format - > $@ + $(XSLTPROC) $(FO_XSL) $< | xmllint --format - > $@ ifeq ($(TEX_METHOD),docbook2tex) %.tex: %.xml $(DEPS) docbook2tex $< else ifeq ($(TEX_METHOD),xsl) %.tex: %.xml $(TEX_XSL) $(DEPS) - xsltproc $(TEX_XSL) $< > $@ + $(XSLTPROC) $(TEX_XSL) $< > $@ endif ifeq ($(PDF_METHOD),fop) diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml index bb281ac67..e20e17ad8 100644 --- a/matita/help/C/matita.xml +++ b/matita/help/C/matita.xml @@ -10,10 +10,12 @@ + - + + @@ -127,6 +129,7 @@ &usernotation; &tacticals; &tactics; +&declarative_tactics; &othercommands; &license; diff --git a/matita/help/C/sec_declarative_tactics.xml b/matita/help/C/sec_declarative_tactics.xml new file mode 100644 index 000000000..1bbbd57bd --- /dev/null +++ b/matita/help/C/sec_declarative_tactics.xml @@ -0,0 +1,471 @@ + + + Tactics Declarative + + + Quick reference card + + &declarativetacticref; + + + + + + assume + assume + assume x : t + + + + Synopsis: + + assume &id; : &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). + + + + Action: + + It adds to the context of the current sequent to prove a new + declaration x : T . The new conclusion becomes + P. + + + + New sequents to prove: + + None. + + + + + + + + suppose + suppose + suppose t(x) + + + + Synopsis: + + suppose &term; ( &id; + ) [ that is equivalent to &term; ] + + + + Pre-condition: + + Da Fare + + + + Action: + + Da Fare + + + + New sequents to prove: + + None. + + + + + + + + by done + by done + by [ t | _ ] done + + + + Synopsis: + + by &term; done + + + + Pre-condition: + + The term can be omitted with a "_", the running term will come found automatically. + + + + Action: + + It closes the current sequent by applying t, taht it can be one under proof or the main proof. + + + + New sequents to prove: + + None. + + + + + + + + we need to prove + we need to prove + we need to prove t [(id)] [or equivalent t] + + + + Synopsis: + + we need to prove &term; + + + + Pre-condition: + + Da Fare + + + + Action: + + Da Fare + + + + New sequents to prove: + + None. + + + + + + + + we proceed by induction + we proceed by induction + we proceed by induction on t to prove th + + + + Synopsis: + + we proceed by induction on &term; to prove &term; + + + + Pre-condition: + + t must inhabit an inductive type and th must be an elimination principle for that inductive type. + + + + Action: + + It proceed on the values of t. + + + + New sequents to prove: + + It opens one new sequent to demonstrate. + + + + + + + + we proceed by cases + we proceed by cases + we proceed by cases on t to prove t + + + + Synopsis: + + we proceed by cases on &term; to prove &term; + + + + Pre-condition: + + Da Fare + + + + Action: + + Da Fare + + + + New sequents to prove: + + None. + + + + + + + + by induction + by induction + by induction hypothesis we know t (id) + + + + Synopsis: + + by induction hypothesis we know &term; ( &id; ) + + + + Pre-condition: + + Da Fare + + + + Action: + + Da Fare + + + + New sequents to prove: + + None. + + + + + + + + thesis becomes + thesis becomes + the thesis becomes t + + + + Synopsis: + + the thesis becomes &sterm; + + + + Pre-condition: + + Each subterm must be convertible with the term t disambiguate in the context of the matched subterm. + + + + Action: + + It replaces the subterm of the current sequent with the new term + + + + New sequence to prove: + + None. + + + + + + + + case + case + case id (id:t)list + + + + Synopsis: + + case &id; ( &id; : &term; ) + + + + Pre-condition: + + Da Fare + + + + Action: + + Da Fare + + + + New sequents to prove: + + Da Fare + + + + + + + + obtain + obtain + obtain t=t by [t|_] + + + + Synopsis: + + obtain &term; = &term; by [ &term; | _ ] + + + + Pre-condition: + + Da Fare + + + + Action: + + Da Fare + + + + New sequence to prove: + + Da Fare + + + + + + + + by term we proved + by term we proved + by th we proved t [""|(id)] + + + + Synopsis: + + by &term; we proved &term; + ( &id; ) + + + + Pre-condition: + + thmust have type Prop. + idcan to be omitted with null + + + + Action: + + It closes the current sequent by applyingth to t. + + + + New sequence to prove: + + Da fare + + + + + + + + exits elim + exits elim + by t let id:t such that t (id) + + + + Synopsis: + + by &term; let &id; + : &term; such that &term; + ( &id; ) + + + + Pre-condition: + + t must be an inductive type,existential and + t (id) must be an elimanation priciple for that inductive type. + + + + + Action: + + it proceeds on t to the elimination of the existential one + + + + New sequence to prove: + + It opens one new sequent. The names of the new hypotheses are picked byt (id) + + + + + + + + and elim + and elim + by t we have t (id) and t (id) + + + + Synopsis: + + by &term; we have &term; + ( &id; ) and &term; + ( &id; ) + + + + Pre-condition: + + t must be an logical type,type and + + + + Action: + + It proceeds on the values of t, according to the elimination principle + + + + New sequence to prove: + + It opens one new sequent, the names of the new hypotheses are picked by t(id) and t(id) + + + + + + + diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index 5f682eb83..2e5f406c9 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -426,6 +426,7 @@ <emphasis role="bold">letrec</emphasis> &TODO; &TODO; + &TODO [<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]… diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index 1549d3794..e1ff24b38 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -1,303 +1,6 @@ <table frame="topbot" rowsep="0" colsep="0" role="grammar"> - <title>tactics + tacticssec__tactics - - - &tactic; - ::= - absurd sterm - - - - | - apply sterm - - - - | - applyS sterm - - - - | - - - assumption - - - - - - | - auto [depth=nat] [width=nat] [paramodulation] [full] - - - - | - change pattern with sterm - - - - | - - clear - id [id…] - - - - - | - clearbody id - - - - | - constructor nat - - - - | - - - contradiction - - - - - - | - cut sterm [as id] - - - - | - - decompose - [( - id… - )] - [id] - [as id…] - - - - - | - - - demodulate - - - - - - | - destruct sterm - - - - | - elim sterm [using sterm] intros-spec - - - - | - elimType sterm [using sterm] intros-spec - - - - | - exact sterm - - - - | - - - exists - - - - - - | - - - fail - - - - - - | - fold reduction-kind sterm pattern - - - - | - - - fourier - - - - - - | - fwd id [as id [id]…] - - - - | - generalize pattern [as id] - - - - | - - - id - - - - - - | - intro [id] - - - - | - intros intros-spec - - - - | - inversion sterm - - - - | - - lapply - [linear] - [depth=nat] - sterm - [to - sterm - [,sterm…] - ] - [as id] - - - - - | - - - left - - - - - - | - letin id ≝ sterm - - - - | - normalize pattern - - - - | - reduce pattern - - - - | - - - reflexivity - - - - - - | - replace pattern with sterm - - - - | - rewrite [<|>] sterm pattern - - - - | - - - right - - - - - - | - - - ring - - - - - - | - simplify pattern - - - - | - - - split - - - - - - | - - - subst - - - - - - | - - - symmetry - - - - - - | - transitivity sterm - - - - | - unfold [sterm] pattern - - - - | - whd pattern - - + diff --git a/matita/help/C/xsl/tactic_quickref.xsl b/matita/help/C/xsl/tactic_quickref.xsl index 42e435740..3a46261e0 100644 --- a/matita/help/C/xsl/tactic_quickref.xsl +++ b/matita/help/C/xsl/tactic_quickref.xsl @@ -7,12 +7,14 @@ omit-xml-declaration="yes" /> + + tactics - + @@ -30,7 +32,7 @@ - grammar.tactic + grammar.tactic &tactic;