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: make_still_working~6671
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=746d4e4529b367d13bf0d92be65590a71baa8cbb;p=helm.git
New: on-line help for declarative tactics (first version).
---
diff --git a/helm/software/matita/help/C/Makefile b/helm/software/matita/help/C/Makefile
index e85ad9a99..2ca1a16b1 100644
--- a/helm/software/matita/help/C/Makefile
+++ b/helm/software/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/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index bb281ac67..e20e17ad8 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -10,10 +10,12 @@
+
-
+
+
@@ -127,6 +129,7 @@
&usernotation;
&tacticals;
&tactics;
+&declarative_tactics;
&othercommands;
&license;
diff --git a/helm/software/matita/help/C/sec_declarative_tactics.xml b/helm/software/matita/help/C/sec_declarative_tactics.xml
new file mode 100644
index 000000000..1bbbd57bd
--- /dev/null
+++ b/helm/software/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/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 5f682eb83..2e5f406c9 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -426,6 +426,7 @@
letrec &TODO;&TODO;
+ &TODO[inductive|coinductive] &id; [&args2;]⦠: &term; â [|] [&id;:&term;] [| &id;:&term;]â¦
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index 1549d3794..e1ff24b38 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,303 +1,6 @@