diff options
Diffstat (limited to 'doc')
27 files changed, 392 insertions, 1740 deletions
diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst new file mode 100644 index 0000000000..83ff177380 --- /dev/null +++ b/doc/changelog/04-tactics/11883-fix-autounfold.rst @@ -0,0 +1,13 @@ +- **Fixed:** + The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + fixes `#7812 <https://github.com/coq/coq/issues/7812>`_, + by Attila Gáspár). +- **Changed:** + `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). +- **Changed:** + :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst new file mode 100644 index 0000000000..f10208e9b2 --- /dev/null +++ b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst @@ -0,0 +1,6 @@ +- **Changed:** + Tactics with qualified name of the form ``Coq.Init.Notations`` are + now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit + option should now import Coq.Init.Ltac if they want to use Ltac + (`#12023 <https://github.com/coq/coq/pull/12023>`_, + by Hugo Herbelin; minor source of incompatibilities). diff --git a/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst new file mode 100644 index 0000000000..7af2b4d97b --- /dev/null +++ b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Anomaly with induction schemes whose conclusion is not normalized + (`#12116 <https://github.com/coq/coq/pull/12116>`_, + by Hugo Herbelin; fixes + `#12045 <https://github.com/coq/coq/pull/12045>`_) diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst new file mode 100644 index 0000000000..ad7cf44482 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst @@ -0,0 +1,5 @@ +- **Changed:** + Added :flag:`Cumulative StrictProp` to control cumulativity of + |SProp| and deprecated now redundant command line + ``--cumulative-sprop`` (`#12034 + <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst new file mode 100644 index 0000000000..5c4ef82b8b --- /dev/null +++ b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst @@ -0,0 +1,4 @@ +- **Added:** + Definitions in coqdoc link to themselves, giving access in html to their own url + (`#12026 <https://github.com/coq/coq/pull/12026>`_, + by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_). diff --git a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst new file mode 100644 index 0000000000..f6af5d40e8 --- /dev/null +++ b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Coqdoc``: Highlighting of the exact position of the target of links + (`#12091 <https://github.com/coq/coq/pull/12091>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst new file mode 100644 index 0000000000..c305b384d9 --- /dev/null +++ b/doc/changelog/08-tools/12126-adjust-timed-name.rst @@ -0,0 +1,8 @@ +- **Changed:** + The output of ``make TIMED=1`` (and therefore the timing targets + such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now + displays the full name of the output file being built, rather than + the stem of the rule (which was usually the filename without the + extension, but in general could be anything for user-defined rules + involving ``%``) (`#12126 + <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). diff --git a/doc/changelog/09-coqide/12060-ide-disable-csd.rst b/doc/changelog/09-coqide/12060-ide-disable-csd.rst new file mode 100644 index 0000000000..b61ab26007 --- /dev/null +++ b/doc/changelog/09-coqide/12060-ide-disable-csd.rst @@ -0,0 +1,6 @@ +- **Changed:** + CoqIDE now uses native window frames by default on Windows. + The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1` + (`#12060 <https://github.com/coq/coq/pull/12060>`_, + fixes `#11080 <https://github.com/coq/coq/issues/11080>`_, + by Attila Gáspár). diff --git a/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst index a17e9956b9..6b1148a9a8 100644 --- a/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst +++ b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst @@ -1,5 +1,5 @@ - **Fixed:** - Highlighting style and language settings consistently apply to all three buffers of CoqIDE + Highlighting style consistently applied to all three buffers of CoqIDE (`#12106 <https://github.com/coq/coq/pull/12106>`_, by Hugo Herbelin; fixes `#11506 <https://github.com/coq/coq/pull/11506>`_). diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst new file mode 100644 index 0000000000..87625dd23b --- /dev/null +++ b/doc/changelog/10-standard-library/12014-ollibs-vector.rst @@ -0,0 +1,10 @@ +- **Added:** + Properties of some operations on vectors: + + - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext`` + - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq`` + - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext`` + - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order`` + + (`#12014 <https://github.com/coq/coq/pull/12014>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst new file mode 100644 index 0000000000..95b4cce2f7 --- /dev/null +++ b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst @@ -0,0 +1,4 @@ +- **Added:** + Definition and properties of cyclic permutations / circular shifts: ``CPermutation`` + (`#12031 <https://github.com/coq/coq/pull/12031>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12119-issue12119.rst b/doc/changelog/10-standard-library/12119-issue12119.rst new file mode 100644 index 0000000000..42672b1465 --- /dev/null +++ b/doc/changelog/10-standard-library/12119-issue12119.rst @@ -0,0 +1,5 @@ +- **Changed:** + new lemma ``NoDup_incl_NoDup`` in ``List.v`` + to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis`` + (`#12119 <https://github.com/coq/coq/pull/12119>`_, + by Olivier Laurent). diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css deleted file mode 100644 index d23ea8f362..0000000000 --- a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css +++ /dev/null @@ -1,329 +0,0 @@ -body { padding: 0px 0px; - margin: 0px 0px; - background-color: white } - -#page { display: block; - padding: 0px; - margin: 0px; - padding-bottom: 10px; } - -#header { display: block; - position: relative; - padding: 0; - margin: 0; - vertical-align: middle; - border-bottom-style: solid; - border-width: thin } - -#header h1 { padding: 0; - margin: 0;} - - -/* Contents */ - -#main{ display: block; - padding: 10px; - font-family: sans-serif; - font-size: 100%; - line-height: 100% } - -#main h1 { line-height: 95% } /* allow for multi-line headers */ - -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #cf1d1d } -#main { color: black } - -.section { background-color: rgb(60%,60%,100%); - padding-top: 13px; - padding-bottom: 13px; - padding-left: 3px; - margin-top: 5px; - margin-bottom: 5px; - font-size : 175% } - -h2.section { background-color: rgb(80%,80%,100%); - padding-left: 3px; - padding-top: 12px; - padding-bottom: 10px; - font-size : 130% } - -h3.section { background-color: rgb(90%,90%,100%); - padding-left: 3px; - padding-top: 7px; - padding-bottom: 7px; - font-size : 115% } - -h4.section { -/* - background-color: rgb(80%,80%,80%); - max-width: 20em; - padding-left: 5px; - padding-top: 5px; - padding-bottom: 5px; -*/ - background-color: white; - padding-left: 0px; - padding-top: 0px; - padding-bottom: 0px; - font-size : 100%; - font-weight : bold; - text-decoration : underline; - } - -#main .doc { margin: 0px; - font-family: sans-serif; - font-size: 100%; - line-height: 125%; - max-width: 40em; - color: black; - padding: 10px; - background-color: #90bdff} - -.inlinecode { - display: inline; -/* font-size: 125%; */ - color: #666666; - font-family: monospace } - -.doc .inlinecode { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.doc .inlinecode .id { - color: rgb(30%,30%,70%); -} - -.inlinecodenm { - display: inline; - color: #444444; -} - -.doc .code { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.comment { - display: inline; - font-family: monospace; - color: rgb(50%,50%,80%); -} - -.code { - display: block; -/* padding-left: 15px; */ - font-size: 110%; - font-family: monospace; - } - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: 10px; - margin-bottom: 10px; -} - -td.infrule { - font-family: monospace; - text-align: center; -/* color: rgb(35%,35%,70%); */ - padding: 0px; - line-height: 100%; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - font-size: 80%; - padding-left: 1em; - padding-bottom: 0.1em -} - -/* Pied de page */ - -#footer { font-size: 65%; - font-family: sans-serif; } - -/* Identifiers: <span class="id" title="...">) */ - -.id { display: inline; } - -.id[title="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[title="var"] { - color: rgb(40%,0%,40%); -} - -.id[title="variable"] { - color: rgb(40%,0%,40%); -} - -.id[title="definition"] { - color: rgb(0%,40%,0%); -} - -.id[title="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[title="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[title="instance"] { - color: rgb(0%,40%,0%); -} - -.id[title="projection"] { - color: rgb(0%,40%,0%); -} - -.id[title="method"] { - color: rgb(0%,40%,0%); -} - -.id[title="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[title="record"] { - color: rgb(0%,0%,80%); -} - -.id[title="class"] { - color: rgb(0%,0%,80%); -} - -.id[title="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */ - -.id[type="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[type="var"] { - color: rgb(40%,0%,40%); -} - -.id[type="variable"] { - color: rgb(40%,0%,40%); -} - -.id[type="definition"] { - color: rgb(0%,40%,0%); -} - -.id[type="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[type="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[type="instance"] { - color: rgb(0%,40%,0%); -} - -.id[type="projection"] { - color: rgb(0%,40%,0%); -} - -.id[type="method"] { - color: rgb(0%,40%,0%); -} - -.id[type="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[type="record"] { - color: rgb(0%,0%,80%); -} - -.id[type="class"] { - color: rgb(0%,0%,80%); -} - -.id[type="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -.inlinecode .id { - color: rgb(0%,0%,0%); -} - - -/* TOC */ - -#toc h2 { - padding: 10px; - background-color: rgb(60%,60%,100%); -} - -#toc li { - padding-bottom: 8px; -} - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; -} - -#index #frontispiece { - margin: 1em auto; - padding: 1em; - width: 60%; -} - -.booktitle { font-size : 140% } -.authors { font-size : 90%; - line-height: 115%; } -.moreauthors { font-size : 60% } - -#index #entrance { - text-align: center; -} - -#index #entrance .spacer { - margin: 0 30px 0 30px; -} - -#index #footer { - position: absolute; - bottom: 0; -} - -.paragraph { - height: 0.75em; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css deleted file mode 100644 index 32c0b33166..0000000000 --- a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css +++ /dev/null @@ -1,801 +0,0 @@ -body -{ - background: white; - color:#444; - font:normal normal normal small/1.5em "Lucida Grande", Verdana, sans-serif; - margin:0; - padding:0; -} - -h2 -{ - font-size:150%; - font-weight:normal; - margin:20px 0 0; -} - -h3 -{ - font-size:130%; - font-weight:normal; -} - -a:link,a:visited -{ - color:#660403; - font-weight:normal; - text-decoration:none; -} - -a:hover -{ - color: red; - text-decoration:none; -} - -#container -{ - margin: 0; - padding: 0; - } - - /*----------header, logo and site name styles----------*/ - #headertop - { - display: block; - /* position:absolute; */ - min-width: 700px; - top: 0; - width: 100%; - height:30px; - z-index: 1; - background: transparent url('images/header_top.png') repeat-x; - } - - #header - { - min-width: 700px; - width: 100%; height:70px; - position: relative; - left: 0; top: 0; - background: transparent url('images/header_bot.png') repeat-x; - } - - #logo - { - float:left; - z-index: 2; - position: absolute; - top: -15px; - left: 0px; - } - - #logo img - { - border:0; - float:left; - } - - #logoWrapper - { - line-height:4em; - } - - #siteName - { - position: relative; - top: 10px; left: 80px; - color:#fff; - float:left; - font-size:350%; - } - - #siteName a - { - color:#fff; - text-decoration:none; - } - - #siteName a:hover - { - color:#ddd; - text-decoration:none; - } - - #siteSlogan - { - color:#eee; - float:left; - font-size:170%; - margin:50px 0 0 10px; - text-transform:lowercase; - white-space:nowrap; - } - - /*----------nav styles -- primary links in header----------*/ - - #nav -{ - position:absolute; right:0; - margin: 0; - padding: 5px; - } - -#nav ul - { - list-style:none outside none; - list-style-image:none; - margin:0; - padding:0; - } - - #nav li - { - display: inline; - margin: 0; padding: 4px; - } - - #nav li a - { - border:medium none; - color:#ccc; - font-weight:normal; - padding-left:10px; - padding-right:10px; - text-decoration:none; - } - - #nav li a:hover - { - background:#7B0505 none repeat; - border:medium none; - border-left:1px solid #ddd; - border-right:1px solid #ddd; - color:#fff; - padding: 6px 9px 5px 9px; - } - - -/************** FOOTER *******************/ - - -#footer -{ - background:transparent url('images/footer.png') repeat-x; - width:100%; - clear:both; - font-size:85%; - text-align:center; - /* position:fixed; */ - margin: 0; - padding: 0; -} - - -#nav-footer -{ - display: inline; - color:#444; - margin: 0; - padding: 0; - text-align:right; - } - -#nav-footer ul - { - list-style:none outside none; - list-style-image:none; - margin:0; - padding:0px; padding-right: 5px; - } - -#nav-footer li -{ - display:inline; padding: 4px; -} - - #nav-footer li a - { - border:medium none; - color:#ccc; - font-size: 11px; - font-weight:normal; - padding-left: 10px; - padding-right: 10px; - text-decoration:none; - } - - #nav-footer li a:hover - { - background:#7B0505 none repeat; - border:medium none; - border-left:1px solid #ddd; - border-right:1px solid #ddd; - color:#fff; - margin:0; - padding: 3px 9px 0px 9px; - } - - - /*----------main content----------*/ - #content - { - display: block; - position: static; - -/* min-width: 640px; */ - max-width: 800px; - - margin-left:40px; - margin-right:300px; - padding: 2ex 2ex; - - z-index:1; - } - -.content { - display: block; - position: relative; - - margin: 0; - padding: 0; -} - - /*----------sidebar styles----------*/ - #sidebarWrapper - { - /* background:transparent url('images/sidebar_bottom.jpg') no-repeat scroll left bottom;*/ - display:block; - position:fixed; - /* avant : top: 100px; right:0px*/ - top: 15px; /* 180 */ - right:0px; - left: auto; - - margin-right: 0px; - - /* avant - width: 12%; - min-width:80px; */ - - /* width: 18%; */ - /* min-*/ - width:270px; - - z-index:0; - overflow:hidden; - -/* ajout precedent:*/ -/* min-height:320px; - padding:10px; - background-image:url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/rttr340bis.png'); - background-repeat : repeat-x ;*/ - -/* last ajout */ - /* min-height:510px; */ /* 360 */ - padding-left:0px; - padding-right:0px; - padding-top:105px; /* 40 */ - padding-bottom:/*105px*/115px; - /* background:transparent url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/trig6b.png') no-repeat scroll left top; */ - background:transparent url('images/sidebarbot.png') no-repeat scroll right bottom; - - } - -#sidebar { - padding-left: 40px; - padding-top: 105px; - overflow: visible; - background:transparent url('images/sidebartop.png') no-repeat scroll right top; -} - -#sidebar .title -{ - /* avant :border-bottom:1px solid #eee;*/ - /* avant : color:#660403;*/ - color:#2D0102; - font-size:120%; - font-weight:bold; - line-height:19px; - margin:10px 0; -} - -/*----------page styles----------*/ -.pageTitle -{ - color:#2D0102; - font-size:220%; - margin:10px 0 20px; -} - -.mission -{ - background-color:#efefef; - border:solid 1px #ccc; - margin:0 0 10px 0; - padding:10px; -} - -.messages -{ - color:#C80000; - font-size:110%; - margin:10px 0; -} - -/*----------node styles----------*/ -.nodeTitle -{ - background: url('images/nodeTitle.gif') no-repeat 0 100%; - color:#9a0000; - font-size: 100%; - margin:0; -} - -.nodeTitle a -{ - color:#660403; - text-decoration:none; -} - -.nodeTitle a:hover -{ - color:#d00000; - text-decoration:none; -} - -.node -{ - margin:0 0 20px; -} - -.content p -{ - margin:10px 0; -} - -.submitted -{ - color:#a3a3a3; - font-size:70%; -} - -.nodeLinks -{ - font-size:95%; - margin:0; - padding:0; -} - -.taxonomy -{ - background:url('icons/tag_red.png') no-repeat 0 7px; - font-size:80%; - padding:0 0 5px 16px; -} - -/*----------comment styles----------*/ -.commentTitle -{ - Border-bottom:1px solid #ddd; - color:#9a0000; - font-size:130%; - margin:20px 0 0; -} - -.commentTitle a -{ - color:#660403; - text-decoration:none; -} - -.commentTitle a:hover -{ - color:#d00000; - text-decoration:none; -} - -.commentLinks -{ - background:#f7f7f7; - border:1px solid #e1e1e1; - color:#444; - font-size:95%; - margin:20px 0 30px; - padding:4px 0 4px 4px; -} - - -/*----------img styles----------*/ -img -{ - padding:3px; -} - -/*----------icons for links----------*/ -.comment_comments a -{ - background:url('icons/comment.png') no-repeat 0 2px; - padding-bottom:5px; - padding-left:20px; -} - -.node_read_more a -{ - background:url('icons/page_white_go.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} - -.comment_add a,.comment_reply a -{ - background:url('icons/comment_add.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} -.comment_delete a -{ - background:url('icons/comment_delete.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} - -.comment_edit a -{ - background:url('icons/comment_edit.png') no-repeat; - padding-bottom:5px; - padding-left:20px; -} - -/*----------TinyMCE editor----------*/ -body.mceContentBody -{ - background:#fff; - color:#000; - font-size:12px; -} - -body.mceContentBody a:link -{ - color:#ff0000; -} - -/*----------table styles----------*/ -table -{ - margin:1em 0; - width:100%; -} - -thead th -{ - border-bottom:2px solid #AAA; - color:#494949; - font-weight:bold; -} - -td,th -{ - padding:.3em 0 .5em; -} - -tr.even,tr.odd,tbody th -{ - border:solid #D5D6D7; - border-width:1px 0; -} - -tr.even -{ - background:#fff; -} - -td.region,td.module,td.container -{ - background:#D5D6D7; - border-bottom:1px solid #AAA; - border-top:1.5em solid #fff; - color:#455067; - font-weight:bold; -} - -tr:first-child td.region,tr:first-child td.module,tr:first-child td.container -{ - border-top-width:0; -} - -td.menu-disabled,td.menu-disabled a -{ - background-color:#D5C2C2; - color:#000; -} - -/*----------other styles----------*/ - -.block -{ - margin:5px 0 20px; -} - -.thumbnail,.preview -{ - border:1px solid #ccc; -} - -.lstlisting { - display: block; - font-family: monospace; - white-space: pre; - margin: 1em 0; -} -.center { - text-align: center; -} -.centered { - display: block-inline; -} - -/*----------download table------------*/ - -table.downloadtable -{ - width:90%; - margin-left:auto; - margin-right:auto; -} - -table.downloadtable td.downloadheader -{ -padding: 2px 1em; -font-weight: bold; -font-size: 120%; -color: white; -background: transparent url('images/header_bot.png') repeat-x; -/*background-color: #660403; */ -border: solid 2px white; -border-left: none; -} - -table.downloadtable td.downloadcategory -{ -padding: 2px 1em; -background-color: #dfbfbe; -text-indent: 0; -} - -table.downloadtable td.downloadsize -{ -text-indent: 0; -white-space: nowrap; -height: 52px; -} - -table.downloadtable td -{ -padding: 2px 1em; -background-color: #dfbfbe; -border-right: solid white 2px; -} - - -table.downloadtable td.downloadtopline -{ -border-top: solid white 2px; -} - -table.downloadtable td.downloadtoprightline -{ -border-top: solid 2px white; -border-right: solid 2px white; -} - -table.downloadtable td.downloadbottomline -{ -border-bottom: solid 2px white; -border-right: solid 2px white; -} - -table.downloadtable td.downloadbottomrightline -{ -border-bottom: solid 2px white; -border-right: solid 2px white; -} - -table.downloadtable td.downloadrightline -{ -border-right: solid 2px white; -} - -table.downloadtable td.downloadback -{ -background-color: #efe4e4; -} - -table.downloadtable td.downloadbottomback -{ -border-bottom: solid 2px white; -background-color: #efe4e4; -} - - -/*********** Normal text style ************/ - -p { - text-indent:3em; -} - -ul { - margin: 0px; - margin-left:4em; - padding: 0px; - list-style-type:square; -} - -li -{ - text-indent: 0px; - margin: 0px; - padding: 0px; -} - -tt { font-size: 1em; } - -pre { font-size: 1em; } - -/*********** Framework ***********/ -.framework -{ - display: block; - position:relative; - border:solid 1px #660033; - margin: 8ex 1em; /* 8ex 8ex 1em 1em; */ - padding: 0; -} - -.frameworkcontent -{ - position:relative; - left:0px; - - - margin: 0; - padding: .5ex 2em; - - text-indent: 2em; - text-align: justify; -} - - -.frameworklabel -{ - display: inline; - position:relative; - top:-1.3ex; - - margin-left:2ex; - padding-top:.4ex; - padding-bottom:.4ex; - padding-right:1ex; - padding-left:1ex; - - border: none; - background: white; - color: black; - - font-weight: bold; - font-size:115%; -} - -.frameworklinks { - display:block; - position:relative; - top:1.4ex; - - margin-right:2ex; - - text-align:right; - font-size:100% - } - -.frameworklinks ul -{ - display: inline; - padding: 0px 1ex; - - border: none; - background: white; -} - - -.frameworklinks li - { - display:inline; - padding: 1ex 0px; - } - - .frameworklinks li a -{ - border:medium none; - - margin: 0px 1ex; - padding-left:2px; - padding-right:3px; - - font-weight:normal; - text-decoration:none; - - color: #660003; -} - - .frameworklinks li a:hover - { - color: red; - - border: none; - } - -/* General flat lists */ -.flatlist li {display: inline} - -/* For sections in bycat.html */ -.bycatsection dt { - text-indent: 3em -} - -.bycatsection dt a -{ - font-weight: bold; - color:#444; -} - -/* footnote is used in the new contribution form */ -.footnote { - text-indent: 0pt; - font-size: 80%; - color: silver; - text-align: justify -} - -/****************** CoqIDE Screenshots *****************/ - - -.SCpager { - position:relative; - top:5px; - width:630px; - background: transparent url('images/header_bot.png') repeat-x; - padding:4px; -} - -.SCpagercontent { - width:390px; - position:relative; - margin-left:auto; - margin-right:auto; -} - -.SCthumb { - height:45px; - margin-left:2px; - margin-right:2px; -} - -.SCthumbselected { - height:55px; - margin-left:2px; - margin-right:2px; -} - -.SCcontent { - position:relative; - top:5px; - width:638px; - background-color: #dfbfbe; -} - -.SCscreenshot { - position:relative; - height:400px; - width:auto; - margin:15px auto 15px 19px; -} diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 9acdd18b89..b2d3687780 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``. the kernel when it is passed a term with incorrect relevance marks. To avoid conversion issues as in ``late_mark`` you may wish to use it to find when your tactics are producing incorrect marks. + +.. flag:: Cumulative StrictProp + :name: Cumulative StrictProp + + Set this flag (it is off by default) to make the kernel accept + cumulativity between |SProp| and other universes. This makes + typechecking incomplete. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index a08495badd..2958d866ac 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -227,7 +227,7 @@ constraints by prefixing the level names with symbols. Because inductive subtypings are only produced by comparing inductives to themselves with universes changed, they amount to variance information: each universe is either invariant, covariant or -irrelevant (there are no contravariant subtypings in Coq), +irrelevant (there are no contravariant subtypings in |Coq|), respectively represented by the symbols `=`, `+` and `*`. Here we see that :g:`list` binds an irrelevant universe, so any two @@ -426,6 +426,19 @@ mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one can use :cmd:`Show Universes` to display the current context of universes. +It is possible to provide only some universe levels and let |Coq| infer the others +by adding a :g:`+` in the list of bound universe levels: + +.. coqtop:: all + + Fail Definition foobar@{u} : Type@{u} := Type. + Definition foobar@{u +} : Type@{u} := Type. + Set Printing Universes. + Print foobar. + +This can be used to find which universes need to be explicitly bound in a given +definition. + Definitions can also be instantiated explicitly, giving their full instance: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index f72654b33b..6615b98660 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -482,10 +482,12 @@ Changes in 8.11+beta1 .. _811Reals: - **Added:** - Module `Reals.ConstructiveCauchyReals` defines constructive real numbers + Module `Reals.Cauchy.ConstructiveCauchyReals` defines constructive real numbers by Cauchy sequences of rational numbers (`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria, with the help and review of Guillaume Melquiond and Bas Spitters). + This module is not meant to be imported directly, please import + `Reals.Abstract.ConstructiveReals` instead. - **Added:** New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers as boolean-valued functions along with 3 logical axioms: diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css deleted file mode 100644 index a325a33842..0000000000 --- a/doc/sphinx/coqdoc.css +++ /dev/null @@ -1,338 +0,0 @@ -/************************************************************************/ -/* * The Coq Proof Assistant / The Coq Development Team */ -/* v * Copyright INRIA, CNRS and contributors */ -/* <O___,, * (see version control and CREDITS file for authors & dates) */ -/* \VV/ **************************************************************/ -/* // * This file is distributed under the terms of the */ -/* * GNU Lesser General Public License Version 2.1 */ -/* * (see LICENSE file for the text of the license) */ -/************************************************************************/ -body { padding: 0px 0px; - margin: 0px 0px; - background-color: white } - -#page { display: block; - padding: 0px; - margin: 0px; - padding-bottom: 10px; } - -#header { display: block; - position: relative; - padding: 0; - margin: 0; - vertical-align: middle; - border-bottom-style: solid; - border-width: thin } - -#header h1 { padding: 0; - margin: 0;} - - -/* Contents */ - -#main{ display: block; - padding: 10px; - font-family: sans-serif; - font-size: 100%; - line-height: 100% } - -#main h1 { line-height: 95% } /* allow for multi-line headers */ - -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #cf1d1d } -#main { color: black } - -.section { background-color: rgb(60%,60%,100%); - padding-top: 13px; - padding-bottom: 13px; - padding-left: 3px; - margin-top: 5px; - margin-bottom: 5px; - font-size : 175% } - -h2.section { background-color: rgb(80%,80%,100%); - padding-left: 3px; - padding-top: 12px; - padding-bottom: 10px; - font-size : 130% } - -h3.section { background-color: rgb(90%,90%,100%); - padding-left: 3px; - padding-top: 7px; - padding-bottom: 7px; - font-size : 115% } - -h4.section { -/* - background-color: rgb(80%,80%,80%); - max-width: 20em; - padding-left: 5px; - padding-top: 5px; - padding-bottom: 5px; -*/ - background-color: white; - padding-left: 0px; - padding-top: 0px; - padding-bottom: 0px; - font-size : 100%; - font-weight : bold; - text-decoration : underline; - } - -#main .doc { margin: 0px; - font-family: sans-serif; - font-size: 100%; - line-height: 125%; - max-width: 40em; - color: black; - padding: 10px; - background-color: #90bdff } - -.inlinecode { - display: inline; -/* font-size: 125%; */ - color: #666666; - font-family: monospace } - -.doc .inlinecode { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.doc .inlinecode .id { - color: rgb(30%,30%,70%); -} - -.inlinecodenm { - display: inline; - color: #444444; -} - -.doc .code { - display: inline; - font-size: 120%; - color: rgb(30%,30%,70%); - font-family: monospace } - -.comment { - display: inline; - font-family: monospace; - color: rgb(50%,50%,80%); -} - -.code { - display: block; -/* padding-left: 15px; */ - font-size: 110%; - font-family: monospace; - } - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: 10px; - margin-bottom: 10px; -} - -td.infrule { - font-family: monospace; - text-align: center; -/* color: rgb(35%,35%,70%); */ - padding: 0px; - line-height: 100%; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - font-size: 80%; - padding-left: 1em; - padding-bottom: 0.1em -} - -/* Pied de page */ - -#footer { font-size: 65%; - font-family: sans-serif; } - -/* Identifiers: <span class="id" title="...">) */ - -.id { display: inline; } - -.id[title="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[title="var"] { - color: rgb(40%,0%,40%); -} - -.id[title="variable"] { - color: rgb(40%,0%,40%); -} - -.id[title="definition"] { - color: rgb(0%,40%,0%); -} - -.id[title="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[title="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[title="instance"] { - color: rgb(0%,40%,0%); -} - -.id[title="projection"] { - color: rgb(0%,40%,0%); -} - -.id[title="method"] { - color: rgb(0%,40%,0%); -} - -.id[title="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[title="record"] { - color: rgb(0%,0%,80%); -} - -.id[title="class"] { - color: rgb(0%,0%,80%); -} - -.id[title="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */ - -.id[type="constructor"] { - color: rgb(60%,0%,0%); -} - -.id[type="var"] { - color: rgb(40%,0%,40%); -} - -.id[type="variable"] { - color: rgb(40%,0%,40%); -} - -.id[type="definition"] { - color: rgb(0%,40%,0%); -} - -.id[type="abbreviation"] { - color: rgb(0%,40%,0%); -} - -.id[type="lemma"] { - color: rgb(0%,40%,0%); -} - -.id[type="instance"] { - color: rgb(0%,40%,0%); -} - -.id[type="projection"] { - color: rgb(0%,40%,0%); -} - -.id[type="method"] { - color: rgb(0%,40%,0%); -} - -.id[type="inductive"] { - color: rgb(0%,0%,80%); -} - -.id[type="record"] { - color: rgb(0%,0%,80%); -} - -.id[type="class"] { - color: rgb(0%,0%,80%); -} - -.id[type="keyword"] { - color : #cf1d1d; -/* color: black; */ -} - -.inlinecode .id { - color: rgb(0%,0%,0%); -} - - -/* TOC */ - -#toc h2 { - padding: 10px; - background-color: rgb(60%,60%,100%); -} - -#toc li { - padding-bottom: 8px; -} - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; -} - -#index #frontispiece { - margin: 1em auto; - padding: 1em; - width: 60%; -} - -.booktitle { font-size : 140% } -.authors { font-size : 90%; - line-height: 115%; } -.moreauthors { font-size : 60% } - -#index #entrance { - text-align: center; -} - -#index #entrance .spacer { - margin: 0 30px 0 30px; -} - -#index #footer { - position: absolute; - bottom: 0; -} - -.paragraph { - height: 0.75em; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 921c7bbbf7..bc77e2e58c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -245,9 +245,9 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.34 mem: 395448 ko) + Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v - Fast (user: 0.01 mem: 45184 ko) + Fast.vo (user: 0.01 mem: 45184 ko) + ``pretty-timed`` this target stores the output of ``make TIMED=1`` into @@ -280,15 +280,15 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.36 mem: 393912 ko) + Slow.vo (user: 0.36 mem: 393912 ko) COQC Fast.v - Fast (user: 0.05 mem: 45992 ko) + Fast.vo (user: 0.05 mem: 45992 ko) Time | File Name -------------------- 0m00.41s | Total -------------------- - 0m00.36s | Slow - 0m00.05s | Fast + 0m00.36s | Slow.vo + 0m00.05s | Fast.vo + ``print-pretty-timed-diff`` @@ -338,8 +338,8 @@ file timing data: -------------------------------------------------------- 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% -------------------------------------------------------- - 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% - 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + 0m00.37s | Slow.vo | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast.vo | 0m00.34s || -0m00.32s | -94.11% The following targets and ``Makefile`` variables allow collection of per- diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b5d1e8bffd..28c5359a04 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1624,9 +1624,15 @@ previous :token:`i_item` have been performed. The second entry in the :token:`i_view` grammar rule, ``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`. -Notations can be used to name tactics, for example:: +Notations can be used to name tactics, for example - Notation myop := (ltac:(some ltac code)) : ssripat_scope. +.. coqtop:: none + + Tactic Notation "my" "ltac" "code" := idtac. + +.. coqtop:: in warn + + Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope. lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 1ecfa05f99..7e6da490fb 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1875,6 +1875,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Lemma induction_test : forall n:nat, n = n -> n <= n. intros n H. induction n. + exact (le_n 0). .. exn:: Not an inductive product. :undocumented: @@ -2076,7 +2077,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Now we are in a contradictory context and the proof can be solved. - .. coqtop:: all + .. coqtop:: all abort inversion H. @@ -2104,68 +2105,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) See also the larger example of :tacn:`dependent induction` and an explanation of the underlying technique. -.. tacn:: function induction (@qualid {+ @term}) - :name: function induction - - The tactic functional induction performs case analysis and induction - following the definition of a function. It makes use of a principle - generated by ``Function`` (see :ref:`advanced-recursive-functions`) or - ``Functional Scheme`` (see :ref:`functional-scheme`). - Note that this tactic is only available after a ``Require Import FunInd``. - -.. example:: - - .. coqtop:: reset all - - Require Import FunInd. - Functional Scheme minus_ind := Induction for minus Sort Prop. - Check minus_ind. - Lemma le_minus (n m:nat) : n - m <= n. - functional induction (minus n m) using minus_ind; simpl; auto. - Qed. - -.. note:: - :n:`(@qualid {+ @term})` must be a correct full application - of :n:`@qualid`. In particular, the rules for implicit arguments are the - same as usual. For example use :n:`@qualid` if you want to write implicit - arguments explicitly. - -.. note:: - Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped. - -.. note:: - :n:`functional induction (f x1 x2 x3)` is actually a wrapper for - :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning - phase, where :n:`@qualid` is the induction principle registered for :g:`f` - (by the ``Function`` (see :ref:`advanced-recursive-functions`) or - ``Functional Scheme`` (see :ref:`functional-scheme`) - command) corresponding to the sort of the goal. Therefore - ``functional induction`` may fail if the induction scheme :n:`@qualid` is not - defined. See also :ref:`advanced-recursive-functions` for the function - terms accepted by ``Function``. - -.. note:: - There is a difference between obtaining an induction scheme - for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`) - and by using :g:`Functional Scheme` after a normal definition using - :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions` - for details. - -.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` - -.. exn:: Cannot find induction information on @qualid. - :undocumented: - -.. exn:: Not the right number of induction arguments. - :undocumented: - -.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list - - Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving - explicitly the name of the introduced variables, the induction principle, and - the values of dependent premises of the elimination scheme, including - *predicates* for mutual induction when :n:`@qualid` is part of a mutually - recursive definition. +.. seealso:: :tacn:`functional induction` .. tacn:: discriminate @term :name: discriminate @@ -2672,6 +2612,8 @@ and an explanation of the underlying technique. assumption. Qed. +.. seealso:: :tacn:`functional inversion` + .. tacn:: fix @ident @num :name: fix @@ -4604,42 +4546,6 @@ symbol :g:`=`. Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to left. -Inversion ---------- - -.. tacn:: functional inversion @ident - :name: functional inversion - - :tacn:`functional inversion` is a tactic that performs inversion on hypothesis - :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid - {+ @term}` where :n:`@qualid` must have been defined using Function (see - :ref:`advanced-recursive-functions`). Note that this tactic is only - available after a ``Require Import FunInd``. - - .. exn:: Hypothesis @ident must contain at least one Function. - :undocumented: - - .. exn:: Cannot find inversion information for hypothesis @ident. - - This error may be raised when some inversion lemma failed to be generated by - Function. - - - .. tacv:: functional inversion @num - - This does the same thing as :n:`intros until @num` followed by - :n:`functional inversion @ident` where :token:`ident` is the - identifier for the last introduced hypothesis. - - .. tacv:: functional inversion @ident @qualid - functional inversion @num @qualid - - If the hypothesis :token:`ident` (or :token:`num`) has a type of the form - :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where - :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to - functional inversion, this variant allows choosing which :token:`qualid` - is inverted. - Classical tactics ----------------- diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7d031b9b7a..60fdbf0a9d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,9 +91,15 @@ capital letter. This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. They are described :ref:`here <set_unset_scope_qualifiers>`. - .. warn:: There is no option @setting_name. + .. warn:: There is no flag or option with this name: "@setting_name". - This message also appears for unknown flags. + This warning message can be raised by :cmd:`Set` and + :cmd:`Unset` when :n:`@setting_name` is unknown. It is a + warning rather than an error because this helps library authors + produce Coq code that is compatible with several Coq versions. + To preserve the same behavior, they may need to set some + compatibility flags or options that did not exist in previous + Coq versions. .. cmd:: Unset @setting_name :name: Unset @@ -119,6 +125,20 @@ capital letter. whether the table contains each specified value, otherise this is equivalent to :cmd:`Print Table`. The `for` clause is not valid for flags and options. + .. exn:: There is no flag, option or table with this name: "@setting_name". + + This error message is raised when calling the :cmd:`Test` + command (without the `for` clause), or the :cmd:`Print Table` + command, for an unknown :n:`@setting_name`. + + .. exn:: There is no qualid-valued table with this name: "@setting_name". + There is no string-valued table with this name: "@setting_name". + + These error messages are raised when calling the :cmd:`Add` or + :cmd:`Remove` commands, or the :cmd:`Test` command with the + `for` clause, if :n:`@setting_name` is unknown or does not have + the right type. + .. cmd:: Print Options Prints the current value of all flags and options, and the names of all tables. @@ -1076,6 +1096,8 @@ Controlling Typing Flags Print the status of the three typing flags: guard checking, positivity checking and universe checking. +See also :flag:`Cumulative StrictProp` in the |SProp| chapter. + .. example:: .. coqtop:: all reset diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 34197c4fcf..e05be7c2c2 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -190,146 +190,7 @@ Combined Scheme Check tree_forest_mutrect. -.. _functional-scheme: - -Generation of induction principles with ``Functional`` ``Scheme`` ------------------------------------------------------------------ - - -.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort} - - This command is a high-level experimental tool for - generating automatically induction principles corresponding to - (possibly mutually recursive) functions. First, it must be made - available via ``Require Import FunInd``. - Each :n:`@ident__i` is a different mutually defined function - name (the names must be in the same order as when they were defined). This - command generates the induction principle for each :n:`@ident__i`, following - the recursive structure and case analyses of the corresponding function - :n:`@ident__i'`. - -.. warning:: - - There is a difference between induction schemes generated by the command - :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, - :cmd:`Function` generally produces smaller principles that are closer to how - a user would implement them. See :ref:`advanced-recursive-functions` for details. - -.. example:: - - Induction scheme for div2. - - We define the function div2 as follows: - - .. coqtop:: all - - Require Import FunInd. - Require Import Arith. - - Fixpoint div2 (n:nat) : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. - - The definition of a principle of induction corresponding to the - recursive structure of `div2` is defined by the command: - - .. coqtop:: all - - Functional Scheme div2_ind := Induction for div2 Sort Prop. - - You may now look at the type of div2_ind: - - .. coqtop:: all - - Check div2_ind. - - We can now prove the following lemma using this principle: - - .. coqtop:: all - - Lemma div2_le' : forall n:nat, div2 n <= n. - intro n. - pattern n, (div2 n). - apply div2_ind; intros. - auto with arith. - auto with arith. - simpl; auto with arith. - Qed. - - We can use directly the functional induction (:tacn:`function induction`) tactic instead - of the pattern/apply trick: - - .. coqtop:: all - - Reset div2_le'. - - Lemma div2_le : forall n:nat, div2 n <= n. - intro n. - functional induction (div2 n). - auto with arith. - auto with arith. - auto with arith. - Qed. - -.. example:: - - Induction scheme for tree_size. - - We define trees by the following mutual inductive type: - - .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - - .. coqtop:: reset all - - Axiom A : Set. - - Inductive tree : Set := - node : A -> forest -> tree - with forest : Set := - | empty : forest - | cons : tree -> forest -> forest. - - We define the function tree_size that computes the size of a tree or a - forest. Note that we use ``Function`` which generally produces better - principles. - - .. coqtop:: all - - Require Import FunInd. - - Function tree_size (t:tree) : nat := - match t with - | node A f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | empty => 0 - | cons t f' => (tree_size t + forest_size f') - end. - - Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` - generated by ``Function`` are not mutual. - - .. coqtop:: all - - Check tree_size_ind. - - Mutual induction principles following the recursive structure of ``tree_size`` - and ``forest_size`` can be generated by the following command: - - .. coqtop:: all - - Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop - with forest_size_ind2 := Induction for forest_size Sort Prop. - - You may now look at the type of `tree_size_ind2`: - - .. coqtop:: all - - Check tree_size_ind2. +.. seealso:: :ref:`functional-scheme` .. _derive-inversion: diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst index ed00f3d455..40f9eedcf0 100644 --- a/doc/sphinx/using/libraries/funind.rst +++ b/doc/sphinx/using/libraries/funind.rst @@ -13,7 +13,7 @@ The following command is available when the ``FunInd`` library has been loaded v This command is a generalization of :cmd:`Fixpoint`. It is a wrapper for several ways of defining a function *and* other useful related objects, namely: an induction principle that reflects the recursive - structure of the function (see :tacn:`function induction`) and its fixpoint equality. + structure of the function (see :tacn:`functional induction`) and its fixpoint equality. This defines a function similar to those defined by :cmd:`Fixpoint`. As in :cmd:`Fixpoint`, the decreasing argument must be given (unless the function is not recursive), but it might not @@ -27,7 +27,7 @@ The following command is available when the ``FunInd`` library has been loaded v to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct` clause). - See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use + See :tacn:`functional induction` and :cmd:`Functional Scheme` for how to use the induction principle to reason easily about the function. The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses. @@ -166,4 +166,235 @@ terminating functions. :tacn:`functional inversion` will not be available for the function. -.. seealso:: :ref:`functional-scheme` and :tacn:`function induction` +Tactics +------- + +.. tacn:: functional induction (@qualid {+ @term}) + :name: functional induction + + The tactic functional induction performs case analysis and induction + following the definition of a function. It makes use of a principle + generated by :cmd:`Function` or :cmd:`Functional Scheme`. + Note that this tactic is only available after a ``Require Import FunInd``. + + .. example:: + + .. coqtop:: reset all + + Require Import FunInd. + Functional Scheme minus_ind := Induction for minus Sort Prop. + Check minus_ind. + Lemma le_minus (n m:nat) : n - m <= n. + functional induction (minus n m) using minus_ind; simpl; auto. + Qed. + + .. note:: + :n:`(@qualid {+ @term})` must be a correct full application + of :n:`@qualid`. In particular, the rules for implicit arguments are the + same as usual. For example use :n:`@qualid` if you want to write implicit + arguments explicitly. + + .. note:: + Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped. + + .. note:: + :n:`functional induction (f x1 x2 x3)` is actually a wrapper for + :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning + phase, where :n:`@qualid` is the induction principle registered for :g:`f` + (by the :cmd:`Function` or :cmd:`Functional Scheme` command) + corresponding to the sort of the goal. Therefore + :tacn:`functional induction` may fail if the induction scheme :n:`@qualid` is not + defined. + + .. note:: + There is a difference between obtaining an induction scheme + for a function by using :cmd:`Function` + and by using :cmd:`Functional Scheme` after a normal definition using + :cmd:`Fixpoint` or :cmd:`Definition`. + + .. exn:: Cannot find induction information on @qualid. + :undocumented: + + .. exn:: Not the right number of induction arguments. + :undocumented: + + .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list + + Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving + explicitly the name of the introduced variables, the induction principle, and + the values of dependent premises of the elimination scheme, including + *predicates* for mutual induction when :n:`@qualid` is part of a mutually + recursive definition. + +.. tacn:: functional inversion @ident + :name: functional inversion + + :tacn:`functional inversion` is a tactic that performs inversion on hypothesis + :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid + {+ @term}` where :n:`@qualid` must have been defined using :cmd:`Function`. + Note that this tactic is only available after a ``Require Import FunInd``. + + .. exn:: Hypothesis @ident must contain at least one Function. + :undocumented: + + .. exn:: Cannot find inversion information for hypothesis @ident. + + This error may be raised when some inversion lemma failed to be generated by + Function. + + + .. tacv:: functional inversion @num + + This does the same thing as :n:`intros until @num` followed by + :n:`functional inversion @ident` where :token:`ident` is the + identifier for the last introduced hypothesis. + + .. tacv:: functional inversion @ident @qualid + functional inversion @num @qualid + + If the hypothesis :token:`ident` (or :token:`num`) has a type of the form + :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where + :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to + functional inversion, this variant allows choosing which :token:`qualid` + is inverted. + +.. _functional-scheme: + +Generation of induction principles with ``Functional`` ``Scheme`` +----------------------------------------------------------------- + + +.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort} + + This command is a high-level experimental tool for + generating automatically induction principles corresponding to + (possibly mutually recursive) functions. First, it must be made + available via ``Require Import FunInd``. + Each :n:`@ident__i` is a different mutually defined function + name (the names must be in the same order as when they were defined). This + command generates the induction principle for each :n:`@ident__i`, following + the recursive structure and case analyses of the corresponding function + :n:`@ident__i'`. + +.. warning:: + + There is a difference between induction schemes generated by the command + :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, + :cmd:`Function` generally produces smaller principles that are closer to how + a user would implement them. See :ref:`advanced-recursive-functions` for details. + +.. example:: + + Induction scheme for div2. + + We define the function div2 as follows: + + .. coqtop:: all + + Require Import FunInd. + Require Import Arith. + + Fixpoint div2 (n:nat) : nat := + match n with + | O => 0 + | S O => 0 + | S (S n') => S (div2 n') + end. + + The definition of a principle of induction corresponding to the + recursive structure of `div2` is defined by the command: + + .. coqtop:: all + + Functional Scheme div2_ind := Induction for div2 Sort Prop. + + You may now look at the type of div2_ind: + + .. coqtop:: all + + Check div2_ind. + + We can now prove the following lemma using this principle: + + .. coqtop:: all + + Lemma div2_le' : forall n:nat, div2 n <= n. + intro n. + pattern n, (div2 n). + apply div2_ind; intros. + auto with arith. + auto with arith. + simpl; auto with arith. + Qed. + + We can use directly the functional induction (:tacn:`functional induction`) tactic instead + of the pattern/apply trick: + + .. coqtop:: all + + Reset div2_le'. + + Lemma div2_le : forall n:nat, div2 n <= n. + intro n. + functional induction (div2 n). + auto with arith. + auto with arith. + auto with arith. + Qed. + +.. example:: + + Induction scheme for tree_size. + + We define trees by the following mutual inductive type: + + .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning + + .. coqtop:: reset all + + Axiom A : Set. + + Inductive tree : Set := + node : A -> forest -> tree + with forest : Set := + | empty : forest + | cons : tree -> forest -> forest. + + We define the function tree_size that computes the size of a tree or a + forest. Note that we use ``Function`` which generally produces better + principles. + + .. coqtop:: all + + Require Import FunInd. + + Function tree_size (t:tree) : nat := + match t with + | node A f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | empty => 0 + | cons t f' => (tree_size t + forest_size f') + end. + + Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` + generated by ``Function`` are not mutual. + + .. coqtop:: all + + Check tree_size_ind. + + Mutual induction principles following the recursive structure of ``tree_size`` + and ``forest_size`` can be generated by the following command: + + .. coqtop:: all + + Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop + with forest_size_ind2 := Induction for forest_size Sort Prop. + + You may now look at the type of `tree_size_ind2`: + + .. coqtop:: all + + Check tree_size_ind2. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7fa621c11c..b2c9c936c9 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -13,6 +13,7 @@ through the <tt>Require Import</tt> command.</p> The core library (automatically loaded when starting Coq) </dt> <dd> + theories/Init/Ltac.v theories/Init/Notations.v theories/Init/Datatypes.v theories/Init/Logic.v @@ -444,6 +445,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sorting/PermutSetoid.v theories/Sorting/Mergesort.v theories/Sorting/Sorted.v + theories/Sorting/CPermutation.v </dd> <dt> <b>Wellfounded</b>: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5034d9a3c9..700170b3c6 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -906,14 +906,14 @@ command: [ | DELETE "Unset" option_table | REPLACE "Set" option_table option_setting | WITH OPT "Export" "Set" option_table (* set flag *) -| REPLACE "Test" option_table "for" LIST1 option_ref_value -| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) +| REPLACE "Test" option_table "for" LIST1 table_value +| WITH "Test" option_table OPT ( "for" LIST1 table_value ) | DELETE "Test" option_table (* hide the fact that table names are limited to 2 IDENTs *) -| REPLACE "Add" IDENT IDENT LIST1 option_ref_value -| WITH "Add" option_table LIST1 option_ref_value -| DELETE "Add" IDENT LIST1 option_ref_value +| REPLACE "Add" IDENT IDENT LIST1 table_value +| WITH "Add" option_table LIST1 table_value +| DELETE "Add" IDENT LIST1 table_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident @@ -969,9 +969,9 @@ command: [ | DELETE "Preterm" (* hide the fact that table names are limited to 2 IDENTs *) -| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value -| WITH "Remove" option_table LIST1 option_ref_value -| DELETE "Remove" IDENT LIST1 option_ref_value +| REPLACE "Remove" IDENT IDENT LIST1 table_value +| WITH "Remove" option_table LIST1 table_value +| DELETE "Remove" IDENT LIST1 table_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string | "Restore" "State" [ IDENT | ne_string ] @@ -1550,7 +1550,7 @@ SPLICE: [ | constructor_type | record_binder | at_level_opt -| option_ref_value +| table_value | positive_search_mark | in_or_out_modules | option_setting diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 04c20a7203..4274dccb40 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -524,12 +524,12 @@ command: [ | "Set" option_table option_setting | "Unset" option_table | "Print" "Table" option_table -| "Add" IDENT IDENT LIST1 option_ref_value -| "Add" IDENT LIST1 option_ref_value -| "Test" option_table "for" LIST1 option_ref_value +| "Add" IDENT IDENT LIST1 table_value +| "Add" IDENT LIST1 table_value +| "Test" option_table "for" LIST1 table_value | "Test" option_table -| "Remove" IDENT IDENT LIST1 option_ref_value -| "Remove" IDENT LIST1 option_ref_value +| "Remove" IDENT IDENT LIST1 table_value +| "Remove" IDENT LIST1 table_value | "Write" "State" IDENT | "Write" "State" ne_string | "Restore" "State" IDENT @@ -1318,7 +1318,7 @@ option_setting: [ | STRING ] -option_ref_value: [ +table_value: [ | global | STRING ] |