diff options
Diffstat (limited to 'doc')
56 files changed, 2200 insertions, 552 deletions
diff --git a/doc/README.md b/doc/README.md index 3db1261656..c41d269437 100644 --- a/doc/README.md +++ b/doc/README.md @@ -101,18 +101,21 @@ Alternatively, you can use some specific targets: Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. -If you're editing Sphinx documentation, set SPHINXWARNERROR to 0 -to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits -upon detecting the first warning. You can set this on the Sphinx `make` -command line or as an environment variable: - -- `make refman SPHINXWARNERROR=0` - -- ~~~ - export SPHINXWARNERROR=0 - ⋮ - make refman - ~~~ +To build the Sphinx documentation without stopping at the first +warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such: + +``` +SPHINXWARNERROR=0 make refman-html +``` + +To do the same with the Dune build system, change the value of the +`SPHINXWARNOPT` variable (default is `-W`). The following will build +the Sphinx documentation without stopping at the first warning, and +store all the warnings in the file `/tmp/warn.log`: + +``` +SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html +``` Installation ------------ diff --git a/doc/dune b/doc/dune new file mode 100644 index 0000000000..6372fe4a91 --- /dev/null +++ b/doc/dune @@ -0,0 +1,26 @@ +(rule + (targets sphinx_build) + (deps + ; We could use finer dependencies here so the build is faster: + ; + ; - vo files: generated by sphinx after parsing the doc, promoted, + ; - Static files: + ; + %{bin:coqdoc} etc... + ; + config/coq_config.py + ; + tools/coqdoc/coqdoc.css + (package coq) + (source_tree sphinx) + (source_tree tools) + (env_var SPHINXWARNOPT)) + (action + (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + +(alias + (name refman-html) + (deps sphinx_build)) + +; The install target still needs more work. +; (install +; (section doc) +; (package coq-refman) +; (files sphinx_build)) diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore new file mode 100644 index 0000000000..3e4978fac4 --- /dev/null +++ b/doc/plugin_tutorial/.gitignore @@ -0,0 +1,13 @@ +*.ml*.d +*.cm[ixt]* +Makefile.coq* +*~ +*.[ao] +.coqdeps.d +*.vo +*.glob +*.aux +*/*/.merlin + +# by convention g_foo.ml is generated +g_*.ml diff --git a/doc/plugin_tutorial/.travis.yml b/doc/plugin_tutorial/.travis.yml new file mode 100644 index 0000000000..556e0ac45a --- /dev/null +++ b/doc/plugin_tutorial/.travis.yml @@ -0,0 +1,38 @@ +dist: trusty +sudo: required +language: generic + +services: + - docker + +env: + global: + - NJOBS="2" + - CONTRIB_NAME="plugin_tutorials" + matrix: + - COQ_IMAGE="coqorg/coq:dev" + +install: | + # Prepare the COQ container + docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/$CONTRIB_NAME -w /home/coq/$CONTRIB_NAME ${COQ_IMAGE} + docker exec COQ /bin/bash --login -c " + # This bash script is double-quoted to interpolate Travis CI env vars: + echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex # -e = exit on failure; -x = trace for debug + opam list + " +script: +- echo -e "${ANSI_YELLOW}Building $CONTRIB_NAME...${ANSI_RESET}" && echo -en 'travis_fold:start:testbuild\\r' +- | + docker exec COQ /bin/bash --login -c " + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex + sudo chown -R coq:coq /home/coq/$CONTRIB_NAME + ( cd tuto0 && make ) + ( cd tuto1 && make ) + ( cd tuto2 && make ) + ( cd tuto3 && make ) + " +- docker stop COQ # optional +- echo -en 'travis_fold:end:testbuild\\r' diff --git a/doc/plugin_tutorial/LICENSE b/doc/plugin_tutorial/LICENSE new file mode 100644 index 0000000000..cf1ab25da0 --- /dev/null +++ b/doc/plugin_tutorial/LICENSE @@ -0,0 +1,24 @@ +This is free and unencumbered software released into the public domain. + +Anyone is free to copy, modify, publish, use, compile, sell, or +distribute this software, either in source code form or as a compiled +binary, for any purpose, commercial or non-commercial, and by any +means. + +In jurisdictions that recognize copyright laws, the author or authors +of this software dedicate any and all copyright interest in the +software to the public domain. We make this dedication for the benefit +of the public at large and to the detriment of our heirs and +successors. We intend this dedication to be an overt act of +relinquishment in perpetuity of all present and future rights to this +software under copyright law. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR +OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. + +For more information, please refer to <http://unlicense.org> diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile new file mode 100644 index 0000000000..7f1833fadd --- /dev/null +++ b/doc/plugin_tutorial/Makefile @@ -0,0 +1,21 @@ + +TUTOS:= \ + tuto0 \ + tuto1 \ + tuto2 \ + tuto3 + +all: $(TUTOS) + +.PHONY: $(TUTOS) all + +$(TUTOS): %: + +$(MAKE) -C $@ + +CLEANS:=$(addsuffix -clean, $(TUTOS)) +.PHONY: clean $(CLEANS) + +clean: $(CLEANS) + +%-clean: + +$(MAKE) -C $* clean diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md new file mode 100644 index 0000000000..f82edb2352 --- /dev/null +++ b/doc/plugin_tutorial/README.md @@ -0,0 +1,86 @@ +How to write plugins in Coq +=========================== + # Working environment : merlin, tuareg (open question) + + ## OCaml & related tools + + These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) + +```shell +opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 +eval `opam config env --root=$PWD/CIW2018` +opam install camlp5 ocamlfind num # Coq's dependencies +opam install lablgtk # Coqide's dependencies (optional) +opam install merlin # prints instructions for vim and emacs +``` + + ## Coq + +```shell +git clone git@github.com:coq/coq.git +cd coq +./configure -profile devel +make -j2 +cd .. +export PATH=$PWD/coq/bin:$PATH +``` + + ## This tutorial + +```shell +git clone git@github.com:ybertot/plugin_tutorials.git +cd plugin_tutorials/tuto0 +make .merlin # run before opening .ml files in your editor +make # build +``` + + + + # tuto0 : basics of project organization + package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + - Example of syntax to add a new toplevel command + - Example of function call to print a simple message + - Example of syntax to add a simple tactic + (that does nothing and prints a message) + - To use it: + +```bash + cd tuto0; make + coqtop -I src -R theories Tuto0 +``` + + In the Coq session type: +```coq + Require Import Tuto0.Loader. HelloWorld. +``` + + # tuto1 : Ocaml to Coq communication + Explore the memory of Coq, modify it + - Commands that take arguments: strings, symbols, expressions of the calculus of constructions + - Commands that interact with type-checking in Coq + - A command that adds a new definition or theorem + - A command that uses a name and exploits the existing definitions + or theorems + - A command that exploits an existing ongoing proof + - A command that defines a new tactic + + Compilation and loading must be performed as for `tuto0`. + + # tuto2 : Ocaml to Coq communication + A more step by step introduction to writing commands + - Explanation of the syntax of entries + - Adding a new type to and parsing to the available choices + - Handling commands that store information in user-chosen registers and tables + + Compilation and loading must be performed as for `tuto1`. + + # tuto3 : manipulating terms of the calculus of constructions + Manipulating terms, inside commands and tactics. + - Obtaining existing values from memory + - Composing values + - Verifying types + - Using these terms in commands + - Using these terms in tactics + - Automatic proofs without tactics using type classes and canonical structures + + compilation and loading must be performed as for `tuto0`. diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject new file mode 100644 index 0000000000..76368e3ac7 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/_CoqProject @@ -0,0 +1,10 @@ +-R theories/ Tuto0 +-I src + +theories/Loader.v +theories/Demo.v + +src/tuto0_main.ml +src/tuto0_main.mli +src/g_tuto0.mlg +src/tuto0_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune new file mode 100644 index 0000000000..79d561061d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto0_plugin) + (public_name coq.plugins.tutorial.p0) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto0.ml) + (deps (:pp-file g_tuto0.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg new file mode 100644 index 0000000000..5c633fe862 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -0,0 +1,18 @@ +DECLARE PLUGIN "tuto0_plugin" + +{ + +open Pp +open Ltac_plugin + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } +END + +TACTIC EXTEND hello_world_tactic +| [ "hello_world" ] -> + { let _ = Feedback.msg_notice (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.ml b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml new file mode 100644 index 0000000000..93a807a800 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml @@ -0,0 +1 @@ +let message = "Hello world!" diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.mli b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli new file mode 100644 index 0000000000..846af3ed8c --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli @@ -0,0 +1 @@ +val message : string diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack new file mode 100644 index 0000000000..73be1bb561 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack @@ -0,0 +1,2 @@ +Tuto0_main +G_tuto0 diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v new file mode 100644 index 0000000000..bdc61986af --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Demo.v @@ -0,0 +1,8 @@ +From Tuto0 Require Import Loader. + +HelloWorld. + +Lemma test : True. +Proof. +hello_world. +Abort. diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v new file mode 100644 index 0000000000..7bce38382b --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto0_plugin". diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto1/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject new file mode 100644 index 0000000000..585d1360be --- /dev/null +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -0,0 +1,13 @@ +-R theories Tuto1 +-I src + +theories/Loader.v + +src/simple_check.mli +src/simple_check.ml +src/simple_declare.mli +src/simple_declare.ml +src/simple_print.ml +src/simple_print.mli +src/g_tuto1.mlg +src/tuto1_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune new file mode 100644 index 0000000000..cf9c674b14 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto1_plugin) + (public_name coq.plugins.tutorial.p1) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto1.ml) + (deps (:pp-file g_tuto1.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg new file mode 100644 index 0000000000..4df284d2d9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -0,0 +1,154 @@ +DECLARE PLUGIN "tuto1_plugin" + +{ + +(* If we forget this line and include our own tactic definition using + TACTIC EXTEND, as below, then we get the strange error message + no implementation available for Tacentries, only when compiling + theories/Loader.v +*) +open Ltac_plugin +open Attributes +open Pp +(* This module defines the types of arguments to be used in the + EXTEND directives below, for example the string one. *) +open Stdarg + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s) ] -> + { Feedback.msg_notice (strbrk "Hello " ++ str s) } +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Ppconstr.pr_qualid was found by searching all mli files + for a function of type qualid -> Pp.t *) + { Feedback.msg_notice + (strbrk "Hello again " ++ Ppconstr.pr_qualid r)} +END + +(* According to parsing/pcoq.mli, e has type constr_expr *) +(* this type is defined in pretyping/constrexpr.ml *) +(* Question for the developers: why is the file constrexpr.ml and not + constrexpr.mli --> Easier for packing the software in components. *) +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") } +END + +(* The next step is to make something of parsed expression. + Interesting information in interp/constrintern.mli *) + +(* There are several phases of transforming a parsed expression into + the final internal data-type (constr). There exists a collection of + functions that combine all the phases *) + +VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY +| [ "Cmd2" constr(e) ] -> + { let _ = Constrintern.interp_constr + (Global.env()) + (* Make sure you don't use Evd.empty here, as this does not + check consistency with existing universe constraints. *) + (Evd.from_env (Global.env())) e in + Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") } +END + +(* This is to show what happens when typing in an empty environment + with an empty evd. + Question for the developers: why does "Cmd3 (fun x : nat => x)." + raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) + +VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY +| [ "Cmd3" constr(e) ] -> + { let _ = Constrintern.interp_constr Environ.empty_env + Evd.empty e in + Feedback.msg_notice + (strbrk "Cmd3 accepted something in the empty context")} +END + +(* When adding a definition, we have to be careful that just + the operation of constructing a well-typed term may already change + the environment, at the level of universe constraints (which + are recorded in the evd component). The function + Constrintern.interp_constr ignores this side-effect, so it should + not be used here. *) + +(* Looking at the interface file interp/constrintern.ml4, I lost + some time because I did not see that the "constr" type appearing + there was "EConstr.constr" and not "Constr.constr". *) + +VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF +| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + Simple_declare.packed_declare_definition ~poly i v } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd5" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (_, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check1 v)) } +END + +VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY +| [ "Cmd6" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let evd, ty = Simple_check.simple_check2 v in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd ty) } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd7" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (a, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check3 v)) } +END + +(* This command takes a name and return its value. It does less + than Print, because it fails on constructors, axioms, and inductive types. + This should be improved, because the error message is an anomaly. + Anomalies should never appear even when using a command outside of its + intended use. *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "Cmd8" reference(r) ] -> + { let env = Global.env() in + let evd = Evd.from_env env in + Feedback.msg_notice + (Printer.pr_econstr_env env evd + (EConstr.of_constr + (Simple_print.simple_body_access (Nametab.global r)))) } +END + +TACTIC EXTEND my_intro +| [ "my_intro" ident(i) ] -> + { Tactics.introduction i } +END + +(* if one write this: + VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY + it gives an error message that is basically impossible to understand. *) + +VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY +| [ "Cmd9" ] -> + { let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let pprf = Proof.partial_proof p in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } +END diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml new file mode 100644 index 0000000000..1f636c531a --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -0,0 +1,32 @@ +let simple_check1 value_with_constraints = + begin + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This is reverse engineered from vernacentries.ml *) +(* The point of renaming is to make sure the bound names printed by Check + can be re-used in `apply with` tactics that use bound names to + refer to arguments. *) + let j = Termops.on_judgment EConstr.of_constr + (Arguments_renaming.rename_typing (Global.env()) + (EConstr.to_constr evd evalue)) in + let {Environ.uj_type=x}=j in x + end + +let simple_check2 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important, you want to really verify that the input is well-typed, + and if you want to obtain the type. *) +(* Note that the output value is a pair containing a new evar_map: + typing will fill out blanks in the term by add evar bindings. *) + Typing.type_of (Global.env()) evd evalue + +let simple_check3 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important and you already expect the input to have been type-checked + before. Set ~lax to false if you want an anomaly to be raised in + case of a type error. Otherwise a ReTypeError exception is raised. *) + Retyping.get_type_of ~lax:true (Global.env()) evd evalue diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli new file mode 100644 index 0000000000..bcf1bf56cf --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -0,0 +1,8 @@ +val simple_check1 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + +val simple_check2 : + EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr + +val simple_check3 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml new file mode 100644 index 0000000000..9d10a8ba72 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -0,0 +1,24 @@ +(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) +let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = + let sigma = Evd.minimize_universes sigma in + let body = EConstr.to_constr sigma body in + let tyopt = Option.map (EConstr.to_constr sigma) tyopt in + let uvars_fold uvars c = + Univ.LSet.union uvars (Vars.universes_of_constr c) in + let uvars = List.fold_left uvars_fold Univ.LSet.empty + (Option.List.cons tyopt [body]) in + let sigma = Evd.restrict_universe_context sigma uvars in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ubinders = Evd.universe_binders sigma in + let ce = Declare.definition_entry ?types:tyopt ~univs body in + DeclareDef.declare_definition ident k ce ubinders imps ~hook + +let packed_declare_definition ~poly ident value_with_constraints = + let body, ctx = value_with_constraints in + let sigma = Evd.from_ctx ctx in + let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in + let udecl = UState.default_univ_decl in + let nohook = Lemmas.mk_hook (fun _ x -> ()) in + ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) + +(* But this definition cannot be undone by Reset ident *) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli new file mode 100644 index 0000000000..fd74e81526 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -0,0 +1,5 @@ +open Names +open EConstr + +val packed_declare_definition : + poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml new file mode 100644 index 0000000000..cfc38ff9c9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -0,0 +1,17 @@ +(* A more advanced example of how to explore the structure of terms of + type constr is given in the coq-dpdgraph plugin. *) + +let simple_body_access gref = + match gref with + | Globnames.VarRef _ -> + failwith "variables are not covered in this example" + | Globnames.IndRef _ -> + failwith "inductive types are not covered in this example" + | Globnames.ConstructRef _ -> + failwith "constructors are not covered in this example" + | Globnames.ConstRef cst -> + let cb = Environ.lookup_constant cst (Global.env()) in + match Global.body_of_constant_body cb with + | Some(e, _) -> e + | None -> failwith "This term has no value" + diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli new file mode 100644 index 0000000000..254b56ff79 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli @@ -0,0 +1 @@ +val simple_body_access : Names.GlobRef.t -> Constr.constr diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack new file mode 100644 index 0000000000..a797a509e0 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack @@ -0,0 +1,4 @@ +Simple_check +Simple_declare +Simple_print +G_tuto1 diff --git a/doc/plugin_tutorial/tuto1/theories/Loader.v b/doc/plugin_tutorial/tuto1/theories/Loader.v new file mode 100644 index 0000000000..6e8e308b3f --- /dev/null +++ b/doc/plugin_tutorial/tuto1/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto1_plugin". diff --git a/doc/plugin_tutorial/tuto2/Makefile b/doc/plugin_tutorial/tuto2/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto2/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject new file mode 100644 index 0000000000..cf9cb5cc26 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/_CoqProject @@ -0,0 +1,6 @@ +-R theories/ Tuto +-I src + +theories/Test.v +src/demo.mlg +src/demo_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto2/src/.gitignore b/doc/plugin_tutorial/tuto2/src/.gitignore new file mode 100644 index 0000000000..5b1b6a902e --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/.gitignore @@ -0,0 +1 @@ +/demo.ml diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg new file mode 100644 index 0000000000..966c05acdc --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo.mlg @@ -0,0 +1,375 @@ +(* -------------------------------------------------------------------------- *) +(* *) +(* Initial ritual dance *) +(* *) +(* -------------------------------------------------------------------------- *) + +DECLARE PLUGIN "demo_plugin" + +(* + Use this macro before any of the other OCaml macros. + + Each plugin has a unique name. + We have decided to name this plugin as "demo_plugin". + That means that: + + (1) If we want to load this particular plugin to Coq toplevel, + we must use the following command. + + Declare ML Module "demo_plugin". + + (2) The above command will succeed only if there is "demo_plugin.cmxs" + in some of the directories that Coq is supposed to look + (i.e. the ones we specified via "-I ..." command line options). + + (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in + "demo_plugin.cmxs". + + (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files + are listed in the "_CoqProject" file. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY +| [ "Cmd1" ] -> { () } +END + +(* + These: + + VERNAC COMMAND EXTEND + + and + + END + + mark the beginning and the end of the definition of a new Vernacular command. + + Cmd1 is a unique identifier (which must start with an upper-case letter) + associated with the new Vernacular command we are defining. + + CLASSIFIED AS QUERY tells Coq that the new Vernacular command: + - changes neither the global environment + - nor does it modify the plugin's state. + + If the new command could: + - change the global environment + - or modify a plugin's state + then one would have to use CLASSIFIED AS SIDEFF instead. + + This: + + [ "Cmd1" ] -> { () } + + defines: + - the parsing rule + - the interpretation rule + + The parsing rule and the interpretation rule are separated by -> token. + + The parsing rule, in this case, is: + + [ "Cmd1" ] + + By convention, all vernacular command start with an upper-case letter. + + The [ and ] characters mark the beginning and the end of the parsing rule. + The parsing rule itself says that the syntax of the newly defined command + is composed from a single terminal Cmd1. + + The interpretation rule, in this case, is: + + { () } + + Similarly to the case of the parsing rule, + { and } characters mark the beginning and the end of the interpretation rule. + In this case, the following Ocaml expression: + + () + + defines the effect of the Vernacular command we have just defined. + That is, it behaves is no-op. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some terminal parameters? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY +| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () } +END + +(* + As shown above, the Vernacular command can be composed from + any number of terminals. + + By convention, each of these terminals starts with an upper-case letter. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some non-terminal parameter? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Stdarg + +} + +VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY +| [ "Cmd3" int(i) ] -> { () } +END + +(* + This: + + open Stdarg + + is needed as some identifiers in the Ocaml code generated by the + + VERNAC COMMAND EXTEND ... END + + macros are not fully qualified. + + This: + + int(i) + + means that the new command is expected to be followed by an integer. + The integer is bound in the parsing rule to variable i. + This variable i then can be used in the interpretation rule. + + To see value of which Ocaml types can be bound this way, + look at the wit_* function declared in interp/stdarg.mli + (in the Coq's codebase). + + If we drop the wit_ prefix, we will get the token + that we can use in the parsing rule. + That is, since there exists wit_int, we know that + we can write: + + int(i) + + By looking at the signature of the wit_int function: + + val wit_int : int uniform_genarg_type + + we also know that variable i will have the type int. + + The types of wit_* functions are either: + + 'c uniform_genarg_type + + or + + ('a,'b,'c) genarg_type + + In both cases, the bound variable will have type 'c. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with variable number of arguments? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY +| [ "Cmd4" int_list(l) ] -> { () } +END + +(* + This: + + int_list(l) + + means that the new Vernacular command is expected to be followed + by a (whitespace separated) list of integers. + This list of integers is bound to the indicated l. + + In this case, as well as in the cases we point out below, instead of int + in int_list we could use any other supported type, e.g. ident, bool, ... + + To see which other Ocaml type constructors (in addition to list) + are supported, have a look at the parse_user_entry function defined + in grammar/q_util.mlp file. + + E.g.: + - ne_int_list(x) would represent a non-empty list of integers, + - int_list(x) would represent a list of integers, + - int_opt(x) would represent a value of type int option, + - ··· +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command that takes values of a custom type? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Ltac_plugin + +} + +(* + If we want to avoid a compilation failure + + "no implementation available for Tacenv" + + then we have to open the Ltac_plugin module. +*) + +(* + Pp module must be opened because some of the macros that are part of the API + do not expand to fully qualified names. +*) + +{ + +type type_5 = Foo_5 | Bar_5 + +} + +(* + We define a type of values that we want to pass to our Vernacular command. +*) + +(* + By default, we are able to define new Vernacular commands that can take + parameters of some of the supported types. Which types are supported, + that was discussed earlier. + + If we want to be able to define Vernacular command that takes parameters + of a type that is not supported by default, we must use the following macro: +*) + +{ + +open Pp + +} + +VERNAC ARGUMENT EXTEND custom5 +| [ "Foo_5" ] -> { Foo_5 } +| [ "Bar_5" ] -> { Bar_5 } +END + +(* + where: + + custom5 + + indicates that, from now on, in our parsing rules we can write: + + custom5(some_variable) + + in those places where we expect user to provide an input + that can be parsed by the parsing rules above + (and interpreted by the interpretations rules above). +*) + +(* Here: *) + +VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY +| [ "Cmd5" custom5(x) ] -> { () } +END + +(* + we define a new Vernacular command whose parameters, provided by the user, + can be mapped to values of type_5. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to give a feedback to the user? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY +| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") } +END + +(* + The following functions: + + - Feedback.msg_info : Pp.t -> unit + - Feedback.msg_notice : Pp.t -> unit + - Feedback.msg_warning : Pp.t -> unit + - Feedback.msg_error : Pp.t -> unit + - Feedback.msg_debug : Pp.t -> unit + + enable us to give user a textual feedback. + + Pp module enable us to represent and construct pretty-printing instructions. + The concepts defined and the services provided by the Pp module are in + various respects related to the concepts and services provided + by the Format module that is part of the Ocaml standard library. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command with (undoable) side-effects? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Summary.Local + +} + +(* + By opening Summary.Local module we shadow the original functions + that we traditionally use for implementing stateful behavior. + + ref + ! + := + + are now shadowed by their counterparts in Summary.Local. *) + +{ + +let counter = ref ~name:"counter" 0 + +} + +VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF +| [ "Cmd7" ] -> { counter := succ !counter; + Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) } +END + +TACTIC EXTEND tactic1 +| [ "tactic1" ] -> { Proofview.tclUNIT () } +END + +(* ---- *) + +{ + +type custom = Foo_2 | Bar_2 + +let pr_custom _ _ _ = function + | Foo_2 -> Pp.str "Foo_2" + | Bar_2 -> Pp.str "Bar_2" + +} + +ARGUMENT EXTEND custom2 PRINTED BY { pr_custom } +| [ "Foo_2" ] -> { Foo_2 } +| [ "Bar_2" ] -> { Bar_2 } +END + +TACTIC EXTEND tactic2 +| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () } +END diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack new file mode 100644 index 0000000000..4f0b8480b5 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack @@ -0,0 +1 @@ +Demo diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune new file mode 100644 index 0000000000..f2bc405455 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto2_plugin) + (public_name coq.plugins.tutorial.p2) + (libraries coq.plugins.ltac)) + +(rule + (targets demo.ml) + (deps (:pp-file demo.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v new file mode 100644 index 0000000000..38e83bfff1 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Test.v @@ -0,0 +1,19 @@ +Declare ML Module "demo_plugin". + +Cmd1. +Cmd2 With Some Terminal Parameters. +Cmd3 42. +Cmd4 100 200 300 400. +Cmd5 Foo_5. +Cmd5 Bar_5. +Cmd6. +Cmd7. +Cmd7. +Cmd7. + +Goal True. +Proof. + tactic1. + tactic2 Foo_2. + tactic2 Bar_2. +Abort. diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto3/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto3/_CoqProject b/doc/plugin_tutorial/tuto3/_CoqProject new file mode 100644 index 0000000000..e2a60a430f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/_CoqProject @@ -0,0 +1,12 @@ +-R theories Tuto3 +-I src + +theories/Data.v +theories/Loader.v + +src/tuto_tactic.ml +src/tuto_tactic.mli +src/construction_game.ml +src/construction_game.mli +src/g_tuto3.mlg +src/tuto3_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml new file mode 100644 index 0000000000..9d9f894e18 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -0,0 +1,186 @@ +open Pp + +let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] + +let example_sort evd = +(* creating a new sort requires that universes should be recorded + in the evd datastructure, so this datastructure also needs to be + passed around. *) + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type = EConstr.mkSort s in + evd, new_type + +let c_one evd = +(* In the general case, global references may refer to universe polymorphic + objects, and their universe has to be made afresh when creating an instance. *) + let gr_S = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in +(* the long name of "S" was found with the command "About S." *) + let gr_O = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + let evd, c_O = Evarutil.new_global evd gr_O in + let evd, c_S = Evarutil.new_global evd gr_S in +(* Here is the construction of a new term by applying functions to argument. *) + evd, EConstr.mkApp (c_S, [| c_O |]) + +let dangling_identity env evd = +(* I call this a dangling identity, because it is not polymorph, but + the type on which it applies is left unspecified, as it is + represented by an existential variable. The declaration for this + existential variable needs to be added in the evd datastructure. *) + let evd, type_type = example_sort evd in + let evd, arg_type = Evarutil.new_evar env evd type_type in +(* Notice the use of a De Bruijn index for the inner occurrence of the + bound variable. *) + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let dangling_identity2 env evd = +(* This example uses directly a function that produces an evar that + is meant to be a type. *) + let evd, (arg_type, type_type) = + Evarutil.new_type_evar env evd Evd.univ_rigid in + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let example_sort_app_lambda () = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_v = c_one evd in +(* dangling_identity and dangling_identity2 can be used interchangeably here *) + let evd, c_f = dangling_identity2 env evd in + let c_1 = EConstr.mkApp (c_f, [| c_v |]) in + let _ = Feedback.msg_notice + (Printer.pr_econstr_env env evd c_1) in + (* type verification happens here. Type verification will update + existential variable information in the evd part. *) + let evd, the_type = Typing.type_of env evd c_1 in +(* At display time, you will notice that the system knows about the + existential variable being instantiated to the "nat" type, even + though c_1 still contains the meta-variable. *) + Feedback.msg_notice + ((Printer.pr_econstr_env env evd c_1) ++ + str " has type " ++ + (Printer.pr_econstr_env env evd the_type)) + + +let c_S evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in + Evarutil.new_global evd gr + +let c_O evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + Evarutil.new_global evd gr + +let c_E evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in + Evarutil.new_global evd gr + +let c_D evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in + Evarutil.new_global evd gr + +let c_Q evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in + Evarutil.new_global evd gr + +let c_R evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in + Evarutil.new_global evd gr + +let c_N evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in + Evarutil.new_global evd gr + +let c_C evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in + Evarutil.new_global evd gr + +let c_F evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in + Evarutil.new_global evd gr + +let c_P evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in + Evarutil.new_global evd gr + +(* If c_S was universe polymorphic, we should have created a new constant + at each iteration of buildup. *) +let mk_nat evd n = + let evd, c_S = c_S evd in + let evd, c_O = c_O evd in + let rec buildup = function + | 0 -> c_O + | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in + if n <= 0 then evd, c_O else evd, buildup n + +let example_classes n = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_n = mk_nat evd n in + let evd, n_half = mk_nat evd (n / 2) in + let evd, c_N = c_N evd in + let evd, c_div = c_D evd in + let evd, c_even = c_E evd in + let evd, c_Q = c_Q evd in + let evd, c_R = c_R evd in + let arg_type = EConstr.mkApp (c_even, [| c_n |]) in + let evd0 = evd in + let evd, instance = Evarutil.new_evar env evd arg_type in + let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let evd, the_type = Typing.type_of env evd c_half in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let proved_equality = + EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, + EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in +(* This is where we force the system to compute with type classes. *) +(* Question to coq developers: why do we pass two evd arguments to + solve_remaining_evars? Is the choice of evd0 relevant here? *) + let evd = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env evd ~initial:evd0 in + let evd, final_type = Typing.type_of env evd proved_equality in + Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) + +(* This function, together with definitions in Data.v, shows how to + trigger automatic proofs at the time of typechecking, based on + canonical structures. + + n is a number for which we want to find the half (and a proof that + this half is indeed the half) +*) +let example_canonical n = + let env = Global.env () in + let evd = Evd.from_env env in +(* Construct a natural representation of this integer. *) + let evd, c_n = mk_nat evd n in +(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) + let evd, c_N = c_N evd in + let evd, c_F = c_F evd in + let evd, c_R = c_R evd in + let evd, c_C = c_C evd in + let evd, c_P = c_P evd in +(* the last argument of C *) + let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in +(* Now we build two existential variables, for the value of the half and for + the "S_ev" structure that triggers the proof search. *) + let evd, ev1 = Evarutil.new_evar env evd c_N in +(* This is the type for the second existential variable *) + let csev = EConstr.mkApp (c_F, [| ev1 |]) in + let evd, ev2 = Evarutil.new_evar env evd csev in +(* Now we build the C structure. *) + let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in +(* Type-checking this term will compute values for the existential variables *) + let evd, final_type = Typing.type_of env evd test_term in +(* The computed type has two parameters, the second one is the proof. *) + let value = match EConstr.kind evd final_type with + | Constr.App(_, [| _; the_half |]) -> the_half + | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in +(* I wish for a nicer way to get the value of ev2 in the evar_map *) + let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in + let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in + let evd, the_statement = Typing.type_of env evd the_prf in + Feedback.msg_notice + (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++ + Printer.pr_econstr_env env evd the_statement) diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.mli b/doc/plugin_tutorial/tuto3/src/construction_game.mli new file mode 100644 index 0000000000..1832ed6630 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.mli @@ -0,0 +1,4 @@ +val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t +val example_sort_app_lambda : unit -> unit +val example_classes : int -> unit +val example_canonical : int -> unit diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune new file mode 100644 index 0000000000..ba6d8b288f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -0,0 +1,10 @@ +(library + (name tuto3_plugin) + (public_name coq.plugins.tutorial.p3) + (flags :standard -warn-error -3) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto3.ml) + (deps (:pp-file g_tuto3.mlg)) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg new file mode 100644 index 0000000000..82ba45726e --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -0,0 +1,46 @@ +DECLARE PLUGIN "tuto3_plugin" + +{ + +open Ltac_plugin + +open Construction_game + +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +} + +VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY +| [ "Tuto3_1" ] -> + { let env = Global.env () in + let evd = Evd.from_env env in + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type_2 = EConstr.mkSort s in + let evd, _ = + Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in + Feedback.msg_notice + (Printer.pr_econstr_env env evd new_type_2) } +END + +VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY +| [ "Tuto3_2" ] -> { example_sort_app_lambda () } +END + +TACTIC EXTEND collapse_hyps +| [ "pack" "hypothesis" ident(i) ] -> + { Tuto_tactic.pack_tactic i } +END + +(* More advanced examples, where automatic proof happens but + no tactic is being called explicitely. The first one uses + type classes. *) +VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY +| [ "Tuto3_3" int(n) ] -> { example_classes n } +END + +(* The second one uses canonical structures. *) +VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY +| [ "Tuto3_4" int(n) ] -> { example_canonical n } +END + diff --git a/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack new file mode 100644 index 0000000000..f4645ad7ed --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack @@ -0,0 +1,3 @@ +Construction_game +Tuto_tactic +G_tuto3 diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml new file mode 100644 index 0000000000..8f2c387d09 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -0,0 +1,143 @@ +open Proofview + +let constants = ref ([] : EConstr.t list) + +(* This is a pattern to collect terms from the Coq memory of valid terms + and proofs. This pattern extends all the way to the definition of function + c_U *) +let collect_constants () = + if (!constants = []) then + let open EConstr in + let open UnivGen in + let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] in + let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in + let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in + let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in + let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in + let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in + constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x)) + [gr_H; gr_M; gr_R; gr_P; gr_U]; + !constants + else + !constants + +let c_H () = + match collect_constants () with + it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack" + +let c_M () = + match collect_constants () with + _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack_marker" + +let c_R () = + match collect_constants () with + _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pair" + +let c_P () = + match collect_constants () with + _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +let c_U () = + match collect_constants () with + _ :: _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +(* The following tactic is meant to pack an hypothesis when no other + data is already packed. + + The main difficulty in defining this tactic is to understand how to + construct the input expected by apply_in. *) +let package i = Goal.enter begin fun gl -> + Tactics.apply_in true false i + [(* this means that the applied theorem is not to be cleared. *) + None, (CAst.make (c_M (), + (* we don't specialize the theorem with extra values. *) + Tactypes.NoBindings))] + (* we don't destruct the result according to any intro_pattern *) + None + end + +(* This function is meant to observe a type of shape (f a) + and return the value a. *) + +(* Remark by Maxime: look for destApp combinator. *) +let unpack_type evd term = + let report () = + CErrors.user_err (Pp.str "expecting a packed type") in + match EConstr.kind evd term with + | Constr.App (_, [| ty |]) -> ty + | _ -> report () + +(* This function is meant to observe a type of shape + A -> pack B -> C and return A, B, C + but it is not used in the current version of our tactic. + It is kept as an example. *) +let two_lambda_pattern evd term = + let report () = + CErrors.user_err (Pp.str "expecting two nested implications") in +(* Note that pattern-matching is always done through the EConstr.kind function, + which only provides one-level deep patterns. *) + match EConstr.kind evd term with + (* Here we recognize the outer implication *) + | Constr.Prod (_, ty1, l1) -> + (* Here we recognize the inner implication *) + (match EConstr.kind evd l1 with + | Constr.Prod (n2, packed_ty2, deep_conclusion) -> + (* Here we recognized that the second type is an application *) + ty1, unpack_type evd packed_ty2, deep_conclusion + | _ -> report ()) + | _ -> report () + +(* In the environment of the goal, we can get the type of an assumption + directly by a lookup. The other solution is to call a low-cost retyping + function like *) +let get_type_of_hyp env id = + match EConstr.lookup_named id env with + | Context.Named.Declaration.LocalAssum (_, ty) -> ty + | _ -> CErrors.user_err (let open Pp in + str (Names.Id.to_string id) ++ + str " is not a plain hypothesis") + +let repackage i h_hyps_id = Goal.enter begin fun gl -> + let env = Goal.env gl in + let evd = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let (ty1 : EConstr.t) = get_type_of_hyp env i in + let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in + let ty2 = unpack_type evd packed_ty2 in + let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in + let open EConstr in + let new_packed_value = + mkApp (c_R (), [| ty1; ty2; mkVar i; + mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in + Refine.refine ~typecheck:true begin fun evd -> + let evd, new_goal = Evarutil.new_evar env evd + (mkProd (Names.Name.Anonymous, + mkApp(c_H (), [| new_packed_type |]), + Vars.lift 1 concl)) in + evd, mkApp (new_goal, + [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) + end + end + +let pack_tactic i = + let h_hyps_id = (Names.Id.of_string "packed_hyps") in + Proofview.Goal.enter begin fun gl -> + let hyps = Environ.named_context_val (Proofview.Goal.env gl) in + if not (Termops.mem_named_context_val i hyps) then + (CErrors.user_err + (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i)))) + else + if Termops.mem_named_context_val h_hyps_id hyps then + tclTHEN (repackage i h_hyps_id) + (tclTHEN (Tactics.clear [h_hyps_id; i]) + (Tactics.introduction h_hyps_id)) + else + tclTHEN (package i) + (tclTHEN (Tactics.rename_hyp [i, h_hyps_id]) + (Tactics.move_hyp h_hyps_id Logic.MoveLast)) + end diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli new file mode 100644 index 0000000000..dbf6cf48e2 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli @@ -0,0 +1,3 @@ +val two_lambda_pattern : + Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t +val pack_tactic : Names.Id.t -> unit Proofview.tactic diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v new file mode 100644 index 0000000000..f7395d686b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -0,0 +1,73 @@ + + +Inductive pack (A: Type) : Type := + packer : A -> pack A. + +Arguments packer {A}. + +Definition uncover (A : Type) (packed : pack A) : A := + match packed with packer v => v end. + +Notation "!!!" := (pack _) (at level 0, only printing). + +(* The following data is used as material for automatic proofs + based on type classes. *) + +Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. + +Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. + +Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. + +Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := + {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. + +Definition tuto_div2 n (p : EvenNat n) := @half _ p. + +(* to be used in the following examples +Compute (@half 8 _). + +Check (@half_prop 8 _). + +Check (@half_prop 7 _). + +and in command Tuto3_3 8. *) + +(* The following data is used as material for automatic proofs + based on canonical structures. *) + +Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}. + +Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r := + match r with Build_S_ev _ _ h => h end. + +Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n := + Build_S_ev n d Pd. + +Canonical Structure can_ev0 : S_ev 0 := + Build_S_ev 0 0 (@eq_refl _ 0). + +Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). +Proof. +intros s; exists (S (S (double_of _ s))). +destruct s as [a P]. +exact (even_rec _ _ P). +Defined. + +Canonical Structure can_ev_rec. + +Record cmp (n : nat) (k : nat) := + C {h : S_ev k; _ : double_of k h = n}. + +(* To be used in, e.g., + +Check (C _ _ _ eq_refl : cmp 6 _). + +Check (C _ _ _ eq_refl : cmp 7 _). + +*) diff --git a/doc/plugin_tutorial/tuto3/theories/Loader.v b/doc/plugin_tutorial/tuto3/theories/Loader.v new file mode 100644 index 0000000000..1351cff63b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Loader.v @@ -0,0 +1,3 @@ +From Tuto3 Require Export Data. + +Declare ML Module "tuto3_plugin". diff --git a/doc/plugin_tutorial/tuto3/theories/test.v b/doc/plugin_tutorial/tuto3/theories/test.v new file mode 100644 index 0000000000..43204ddf34 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/test.v @@ -0,0 +1,23 @@ +(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *) + +Require Import Tuto3.Loader. + +(* This should print Type. *) +Tuto3_1. + +(* This should print a term that contains an existential variable. *) +(* And then print the same term, where the variable has been correctly + instantiated. *) +Tuto3_2. + +Lemma tutu x y (A : 0 < x) (B : 10 < y) : True. +Proof. +pack hypothesis A. +(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis + should have appeared, with unreadable content. *) +pack hypothesis B. +(* Hypothesis B should have disappeared *) +destruct packed_hyps as [unpacked_hyps]. +(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *) +exact I. +Qed. diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index e681d0f3ff..39047f4f23 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -61,7 +61,7 @@ extensions = [ # Change this to "info" or "warning" to get notifications about undocumented Coq # objects (objects with no contents). -report_undocumented_coq_objects = None +report_undocumented_coq_objects = "warning" # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] diff --git a/doc/sphinx/dune b/doc/sphinx/dune new file mode 100644 index 0000000000..fff025c919 --- /dev/null +++ b/doc/sphinx/dune @@ -0,0 +1 @@ +(dirs :standard _static) diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1a33a9a46e..8fa631174f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Set` is is the universe of *program types* or *specifications*. The +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 9fbac95f0c..92bd4dbd1d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -418,30 +418,29 @@ each point of use, e.g., the above definition can be written: Prenex Implicits null. Definition all_null (s : list T) := all null s. -Better yet, it can be omitted entirely, since ``all_null s`` isn’t much of -an improvement over ``all null s``. +Better yet, it can be omitted entirely, since :g:`all_null s` isn’t much of +an improvement over :g:`all null s`. The syntax of the new declaration is -.. cmd:: Prenex Implicits {+ @ident} +.. cmd:: Prenex Implicits {+ @ident__i} -Let us denote :math:`c_1` … :math:`c_n` the list of identifiers given to a -``Prenex Implicits`` command. The command checks that each ci is the name of -a functional constant, whose implicit arguments are prenex, i.e., the first -:math:`n_i > 0` arguments of :math:`c_i` are implicit; then it assigns -``Maximal Implicit`` status to these arguments. + This command checks that each :n:`@ident__i` is the name of a functional + constant, whose implicit arguments are prenex, i.e., the first + :math:`n_i > 0` arguments of :n:`@ident__i` are implicit; then it assigns + ``Maximal Implicit`` status to these arguments. -As these prenex implicit arguments are ubiquitous and have often large -display strings, it is strongly recommended to change the default -display settings of |Coq| so that they are not printed (except after -a ``Set Printing All`` command). All |SSR| library files thus start -with the incantation + As these prenex implicit arguments are ubiquitous and have often large + display strings, it is strongly recommended to change the default + display settings of |Coq| so that they are not printed (except after + a ``Set Printing All`` command). All |SSR| library files thus start + with the incantation -.. coqtop:: all undo + .. coqtop:: all undo - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. Anonymous arguments @@ -601,25 +600,21 @@ resemble ML-like definitions of polymorphic functions. Abbreviations ~~~~~~~~~~~~~ -The |SSR| set tactic performs abbreviations: it introduces a -defined constant for a subterm appearing in the goal and/or in the -context. - -|SSR| extends the set tactic by supplying: - +.. tacn:: set @ident {? : @term } := {? @occ_switch } @term + :name: set (ssreflect) -+ an open syntax, similarly to the pose tactic; -+ a more aggressive matching algorithm; -+ an improved interpretation of wildcards, taking advantage of the - matching algorithm; -+ an improved occurrence selection mechanism allowing to abstract only - selected occurrences of a term. + The |SSR| ``set`` tactic performs abbreviations: it introduces a + defined constant for a subterm appearing in the goal and/or in the + context. + |SSR| extends the :tacn:`set` tactic by supplying: -The general syntax of this tactic is - -.. tacn:: set @ident {? : @term } := {? @occ_switch } @term - :name: set (ssreflect) + + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic; + + a more aggressive matching algorithm; + + an improved interpretation of wildcards, taking advantage of the + matching algorithm; + + an improved occurrence selection mechanism allowing to abstract only + selected occurrences of a term. .. prodn:: occ_switch ::= { {? + %| - } {* @num } } @@ -903,23 +898,15 @@ Basic localization ~~~~~~~~~~~~~~~~~~ It is possible to define an abbreviation for a term appearing in the -context of a goal thanks to the in tactical. - -A tactic of the form: +context of a goal thanks to the ``in`` tactical. .. tacv:: set @ident := @term in {+ @ident} -introduces a defined constant called ``x`` in the context, and folds it in -the context entries mentioned on the right hand side of ``in``. -The body of ``x`` is the first subterm matching these context entries -(taken in the given order). - -A tactic of the form: - -.. tacv:: set @ident := @term in {+ @ident} * - -matches term and then folds ``x`` similarly in all the given context entries -but also folds ``x`` in the goal. + This variant of :tacn:`set (ssreflect)` introduces a defined constant + called :token:`ident` in the context, and folds it in + the context entries mentioned on the right hand side of ``in``. + The body of :token:`ident` is the first subterm matching these context + entries (taken in the given order). .. example:: @@ -932,7 +919,10 @@ but also folds ``x`` in the goal. Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. -If the localization also mentions the goal, then the result is the following one: +.. tacv:: set @ident := @term in {+ @ident} * + + This variant matches :token:`term` and then folds :token:`ident` similarly + in all the given context entries but also folds :token:`ident` in the goal. .. example:: @@ -945,7 +935,7 @@ If the localization also mentions the goal, then the result is the following one Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx * . -Indeed, remember that 4 is just a notation for (S 3). + Indeed, remember that 4 is just a notation for (S 3). The use of the ``in`` tactical is not limited to the localization of abbreviations: for a complete description of the in tactical, see @@ -1202,77 +1192,82 @@ context manipulations and the main backward chaining tool. The move tactic. ```````````````` -The move tactic, in its defective form, behaves like the primitive ``hnf`` -|Coq| tactic. For example, such a defective: - .. tacn:: move :name: move -exposes the first assumption in the goal, i.e. its changes the -goal ``not False`` into ``False -> False``. + This tactic, in its defective form, behaves like the :tacn:`hnf` tactic. -More precisely, the ``move`` tactic inspects the goal and does nothing -(``idtac``) if an introduction step is possible, i.e. if the goal is a -product or a ``let…in``, and performs ``hnf`` otherwise. + .. example:: -Of course this tactic is most often used in combination with the -bookkeeping tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). These -combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, :tacn:`revert`, :tacn:`rename`, -:tacn:`clear` and :tacn:`pattern` tactics. + .. coqtop:: reset all + + Require Import ssreflect. + Goal not False. + move. + + More precisely, the :tacn:`move` tactic inspects the goal and does nothing + (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a + product or a ``let … in``, and performs :tacn:`hnf` otherwise. + + Of course this tactic is most often used in combination with the bookkeeping + tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). + These combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, + :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. The case tactic ``````````````` -The ``case`` tactic performs *primitive case analysis* on (co)inductive -types; specifically, it destructs the top variable or assumption of -the goal, exposing its constructor(s) and its arguments, as well as -setting the value of its type family indices if it belongs to a type -family (see section :ref:`type_families_ssr`). +.. tacn:: case + :name: case (ssreflect) + + This tactic performs *primitive case analysis* on (co)inductive + types; specifically, it destructs the top variable or assumption of + the goal, exposing its constructor(s) and its arguments, as well as + setting the value of its type family indices if it belongs to a type + family (see section :ref:`type_families_ssr`). -The |SSR| case tactic has a special behavior on equalities. If the -top assumption of the goal is an equality, the case tactic “destructs” -it as a set of equalities between the constructor arguments of its -left and right hand sides, as per the tactic injection. For example, -``case`` changes the goal:: + The |SSR| case tactic has a special behavior on equalities. If the + top assumption of the goal is an equality, the case tactic “destructs” + it as a set of equalities between the constructor arguments of its + left and right hand sides, as per the tactic injection. For example, + ``case`` changes the goal:: - (x, y) = (1, 2) -> G. + (x, y) = (1, 2) -> G. -into:: + into:: - x = 1 -> y = 2 -> G. + x = 1 -> y = 2 -> G. -Note also that the case of |SSR| performs ``False`` elimination, even -if no branch is generated by this case operation. Hence the command: -``case.`` on a goal of the form ``False -> G`` will succeed and -prove the goal. + Note also that the case of |SSR| performs :g:`False` elimination, even + if no branch is generated by this case operation. Hence the tactic + :tacn:`case` on a goal of the form :g:`False -> G` will succeed and + prove the goal. The elim tactic ``````````````` -The ``elim`` tactic performs inductive elimination on inductive types. The -defective: - .. tacn:: elim :name: elim (ssreflect) -tactic performs inductive elimination on a goal whose top assumption -has an inductive type. + This tactic performs inductive elimination on inductive types. In its + defective form, the tactic performs inductive elimination on a goal whose + top assumption has an inductive type. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all - Lemma test m : forall n : nat, m <= n. - elim. + Lemma test m : forall n : nat, m <= n. + elim. .. _apply_ssr: @@ -1280,27 +1275,25 @@ has an inductive type. The apply tactic ```````````````` -The ``apply`` tactic is the main backward chaining tactic of the proof -system. It takes as argument any :token:`term` and applies it to the goal. -Assumptions in the type of :token:`term` that don’t directly match the goal -may generate one or more subgoals. - -In fact the |SSR| tactic: - -.. tacn:: apply +.. tacn:: apply {? @term } :name: apply (ssreflect) -is a synonym for:: + This is the main backward chaining tactic of the proof system. + It takes as argument any :token:`term` and applies it to the goal. + Assumptions in the type of :token:`term` that don’t directly match the goal + may generate one or more subgoals. + + In its defective form, this tactic is a synonym for:: - intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top. + intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top. -where ``top`` is a fresh name, and the sequence of refine tactics tries to -catch the appropriate number of wildcards to be inserted. Note that -this use of the refine tactic implies that the tactic tries to match -the goal up to expansion of constants and evaluation of subterms. + where :g:`top` is a fresh name, and the sequence of :tacn:`refine` tactics + tries to catch the appropriate number of wildcards to be inserted. Note that + this use of the :tacn:`refine` tactic implies that the tactic tries to match + the goal up to expansion of constants and evaluation of subterms. -|SSR|’s apply has a special behavior on goals containing -existential metavariables of sort Prop. +:tacn:`apply (ssreflect)` has a special behavior on goals containing +existential metavariables of sort :g:`Prop`. .. example:: @@ -1348,6 +1341,7 @@ The general syntax of the discharging tactical ``:`` is: .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch } :name: ... : ... (ssreflect) + :undocumented: .. prodn:: d_item ::= {? @occ_switch %| @clear_switch } @term @@ -1502,8 +1496,8 @@ The abstract tactic .. tacn:: abstract: {+ d_item} :name: abstract (ssreflect) -This tactic assigns an abstract constant previously introduced with the ``[: -name ]`` intro pattern (see section :ref:`introduction_ssr`). + This tactic assigns an abstract constant previously introduced with the + :n:`[: @ident ]` intro pattern (see section :ref:`introduction_ssr`). In a goal like the following:: @@ -1553,22 +1547,29 @@ whose general syntax is .. tacn:: @tactic => {+ @i_item } :name: => + :undocumented: .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term + i_item ::= @i_pattern %| @s_item %| @clear_switch %| @i_view %| @i_block .. prodn:: s_item ::= /= %| // %| //= .. prodn:: - i_pattern ::= @ident %| _ %| ? %| * %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) -The ``=>`` tactical first executes tactic, then the :token:`i_item` s, +.. prodn:: + i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + +.. prodn:: + i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] + +The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a simplification operation; a :token:`clear_switch` -h specifies context pruning as in :ref:`discharge_ssr`. -The :token:`i_pattern` s can be seen as a variant of *intro patterns* -:ref:`tactics`: each performs an introduction operation, i.e., pops some +specifies context pruning as in :ref:`discharge_ssr`. +The :token:`i_pattern`\s can be seen as a variant of *intro patterns* +(see :tacn:`intros`:) each performs an introduction operation, i.e., pops some variables or assumptions from the goal. An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: @@ -1577,7 +1578,7 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: |SSR| tactic :tacn:`done` described in :ref:`terminators_ssr`, i.e., it executes ``try done``. + ``/=`` simplifies the goal by performing partial evaluation, as per the - tactic ``simpl`` [#5]_. + tactic :tacn:`simpl` [#5]_. + ``//=`` combines both kinds of simplification; it is equivalent to ``/= //``, i.e., ``simpl; try done``. @@ -1588,21 +1589,43 @@ When an :token:`s_item` bears a :token:`clear_switch`, then the possibly using the fact ``IHn``, and will erase ``IHn`` from the context of the remaining subgoals. -The last entry in the :token:`i_item` grammar rule, ``/``:token:`term`, +The first entry in the :token:`i_view` grammar rule, :n:`/@term`, represents a view (see section :ref:`views_and_reflection_ssr`). +It interprets the top of the stack with the view :token:`term`. +It is equivalent to ``move/term``. The optional flag ``{}`` can +be used to signal that the :token:`term`, when it is a context entry, +has to be cleared. If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. -The view is applied to the top assumption. +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:: + + Notation myop := (ltac:(some ltac code)) : ssripat_scope. -|SSR| supports the following :token:`i_pattern` s: +lets one write just ``/myop`` in the intro pattern. Note the scope +annotation: views are interpreted opening the ``ssripat`` scope. + +|SSR| supports the following :token:`i_pattern`\s: :token:`ident` pops the top variable, assumption, or local definition into a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. +``>`` + pops every variable occurring in the rest of the stack. + Type class instances are popped even if they don't occur + in the rest of the stack. + The tactic ``move=> >`` is equivalent to + ``move=> ? ?`` on a goal such as:: + + forall x y, x < y -> G + + A typical use if ``move=>> H`` to name ``H`` the first assumption, + in the example above ``x < y``. ``?`` pops the top variable into an anonymous constant or fact, whose name is picked by the tactic interpreter. |SSR| only generates names that cannot @@ -1625,7 +1648,17 @@ The view is applied to the top assumption. a first ``move=> *`` adds only ``_a_ : bool`` and ``_b_ : bool`` to the context; it takes a second ``move=> *`` to add ``_Hyp_ : _a_ = _b_``. -:token:`occ_switch` ``->`` +``+`` + temporarily introduces the top variable. It is discharged at the end + of the intro pattern. For example ``move=> + y`` on a goal:: + + forall x y, P + + is equivalent to ``move=> _x_ y; move: _x_`` that results in the goal:: + + forall x, P + +:n:`{? occ_switch } ->` (resp. :token:`occ_switch` ``<-``) pops the top assumption (which should be a rewritable proposition) into an anonymous fact, rewrites (resp. rewrites right to left) the goal with this @@ -1650,18 +1683,13 @@ The view is applied to the top assumption. variable, using the |SSR| ``case`` tactic described in :ref:`the_defective_tactics_ssr`. It then behaves as the corresponding branching :token:`i_pattern`, executing the - sequence:token:`i_item`:math:`_i` in the i-th subgoal generated by the + sequence :n:`@i_item__i` in the i-th subgoal generated by the case analysis; unless we have the trivial destructing :token:`i_pattern` ``[]``, the latter should generate exactly m subgoals, i.e., the top variable should have an inductive type with exactly m constructors [#7]_. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. -``/`` :token:`term` - Interprets the top of the stack with the view :token:`term`. - It is equivalent to ``move/term``. The optional flag ``{}`` can - be used to signal that the :token:`term`, when it is a context entry, - has to be cleared. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` @@ -1726,6 +1754,40 @@ interpretation, e.g.: are all equivalent. +|SSR| supports the following :token:`i_block`\s: + +:n:`[^ @ident ]` + *block destructing* :token:`i_pattern`. It performs a case analysis + on the top variable and introduces, in one go, all the variables coming + from the case analysis. The names of these variables are obtained by + taking the names used in the inductive type declaration and prefixing them + with :token:`ident`. If the intro pattern immediately follows a call + to ``elim`` with a custom eliminator (see :ref:`custom_elim_ssr`) then + the names are taken from the ones used in the type of the eliminator. + + .. example:: + + .. coqtop:: reset + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + .. coqtop:: all + + Record r := { a : nat; b := (a, 3); _ : bool; }. + + Lemma test : r -> True. + Proof. move => [^ x ]. + +:n:`[^~ @ident ]` + *block destructing* using :token:`ident` as a suffix. +:n:`[^~ @num ]` + *block destructing* using :token:`num` as a suffix. + + Only a :token:`s_item` is allowed between the elimination tactic and + the block destructing. .. _generation_of_equations_ssr: @@ -1803,136 +1865,132 @@ Type families ~~~~~~~~~~~~~ When the top assumption of a goal has an inductive type, two specific -operations are possible: the case analysis performed by the ``case`` +operations are possible: the case analysis performed by the :tacn:`case` tactic, and the application of an induction principle, performed by -the ``elim`` tactic. When this top assumption has an inductive type, which +the :tacn:`elim` tactic. When this top assumption has an inductive type, which is moreover an instance of a type family, |Coq| may need help from the user to specify which occurrences of the parameters of the type should be substituted. -A specific ``/`` switch indicates the type family parameters of the type -of a :token:`d_item` immediately following this ``/`` switch, -using the syntax: - .. tacv:: case: {+ @d_item } / {+ @d_item } - :name: case (ssreflect) + elim: {+ @d_item } / {+ @d_item } + + A specific ``/`` switch indicates the type family parameters of the type + of a :token:`d_item` immediately following this ``/`` switch. + The :token:`d_item` on the right side of the ``/`` switch are discharged as + described in section :ref:`discharge_ssr`. The case analysis or elimination + will be done on the type of the top assumption after these discharge + operations. + + Every :token:`d_item` preceding the ``/`` is interpreted as arguments of this + type, which should be an instance of an inductive type family. These terms + are not actually generalized, but rather selected for substitution. + Occurrence switches can be used to restrict the substitution. If a term is + left completely implicit (e.g. writing just ``_``), then a pattern is + inferred looking at the type of the top assumption. This allows for the + compact syntax: -.. tacv:: elim: {+ @d_item } / {+ @d_item } + .. coqtop:: in -The :token:`d_item` on the right side of the ``/`` switch are discharged as -described in section :ref:`discharge_ssr`. The case analysis or elimination -will be done on the type of the top assumption after these discharge -operations. + case: {2}_ / eqP. -Every :token:`d_item` preceding the ``/`` is interpreted as arguments of this -type, which should be an instance of an inductive type family. These terms -are not actually generalized, but rather selected for substitution. -Occurrence switches can be used to restrict the substitution. If a term is -left completely implicit (e.g. writing just ``_``), then a pattern is -inferred looking at the type of the top assumption. This allows for the -compact syntax: + where ``_`` is interpreted as ``(_ == _)`` since + ``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with + one index. -.. coqtop:: in + Moreover if the :token:`d_item` list is too short, it is padded with an + initial sequence of ``_`` of the right length. - case: {2}_ / eqP. + .. example:: -where ``_`` is interpreted as ``(_ == _)`` since -``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with -one index. + Here is a small example on lists. We define first a function which + adds an element at the end of a given list. -Moreover if the :token:`d_item` list is too short, it is padded with an -initial sequence of ``_`` of the right length. + .. coqtop:: reset -.. example:: + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - Here is a small example on lists. We define first a function which - adds an element at the end of a given list. + .. coqtop:: all - .. coqtop:: reset + Require Import List. + Section LastCases. + Variable A : Type. + Implicit Type l : list A. + Fixpoint add_last a l : list A := + match l with + | nil => a :: nil + | hd :: tl => hd :: (add_last a tl) end. - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Then we define an inductive predicate for case analysis on lists + according to their last element: - .. coqtop:: all + .. coqtop:: all - Require Import List. - Section LastCases. - Variable A : Type. - Implicit Type l : list A. - Fixpoint add_last a l : list A := - match l with - | nil => a :: nil - | hd :: tl => hd :: (add_last a tl) end. + Inductive last_spec : list A -> Type := + | LastSeq0 : last_spec nil + | LastAdd s x : last_spec (add_last x s). - Then we define an inductive predicate for case analysis on lists - according to their last element: + Theorem lastP : forall l : list A, last_spec l. + Admitted. - .. coqtop:: all + We are now ready to use ``lastP`` in conjunction with ``case``. - Inductive last_spec : list A -> Type := - | LastSeq0 : last_spec nil - | LastAdd s x : last_spec (add_last x s). + .. coqtop:: all - Theorem lastP : forall l : list A, last_spec l. - Admitted. + Lemma test l : (length l) * 2 = length (l ++ l). + case: (lastP l). - We are now ready to use ``lastP`` in conjunction with ``case``. + Applied to the same goal, the command: + ``case: l / (lastP l).`` + generates the same subgoals but ``l`` has been cleared from both contexts. - .. coqtop:: all + Again applied to the same goal, the command. - Lemma test l : (length l) * 2 = length (l ++ l). - case: (lastP l). + .. coqtop:: none - Applied to the same goal, the command: - ``case: l / (lastP l).`` - generates the same subgoals but ``l`` has been cleared from both contexts. + Abort. - Again applied to the same goal, the command. + .. coqtop:: all - .. coqtop:: none + Lemma test l : (length l) * 2 = length (l ++ l). + case: {1 3}l / (lastP l). - Abort. + Note that selected occurrences on the left of the ``/`` + switch have been substituted with l instead of being affected by + the case analysis. - .. coqtop:: all + The equation name generation feature combined with a type family ``/`` + switch generates an equation for the *first* dependent :token:`d_item` + specified by the user. Again starting with the above goal, the + command: - Lemma test l : (length l) * 2 = length (l ++ l). - case: {1 3}l / (lastP l). + .. example:: - Note that selected occurrences on the left of the ``/`` - switch have been substituted with l instead of being affected by - the case analysis. + .. coqtop:: none -The equation name generation feature combined with a type family / -switch generates an equation for the *first* dependent :token:`d_item` -specified by the user. Again starting with the above goal, the -command: + Abort. -.. example:: + .. coqtop:: all - .. coqtop:: none + Lemma test l : (length l) * 2 = length (l ++ l). + case E: {1 3}l / (lastP l) => [|s x]. + Show 2. - Abort. - .. coqtop:: all + There must be at least one :token:`d_item` to the left of the ``/`` switch; this + prevents any confusion with the view feature. However, the :token:`d_item` + to the right of the ``/`` are optional, and if they are omitted the first + assumption provides the instance of the type family. - Lemma test l : (length l) * 2 = length (l ++ l). - case E: {1 3}l / (lastP l) => [|s x]. - Show 2. - - -There must be at least one :token:`d_item` to the left of the / switch; this -prevents any confusion with the view feature. However, the :token:`d_item` -to the right of the ``/`` are optional, and if they are omitted the first -assumption provides the instance of the type family. - -The equation always refers to the first :token:`d_item` in the actual tactic -call, before any padding with initial ``_``. Thus, if an inductive type -has two family parameters, it is possible to have|SSR| generate an -equation for the second one by omitting the pattern for the first; -note however that this will fail if the type of the second parameter -depends on the value of the first parameter. + The equation always refers to the first :token:`d_item` in the actual tactic + call, before any padding with initial ``_``. Thus, if an inductive type + has two family parameters, it is possible to have|SSR| generate an + equation for the second one by omitting the pattern for the first; + note however that this will fail if the type of the second parameter + depends on the value of the first parameter. Control flow @@ -1991,13 +2049,14 @@ closed tactic fails to prove its subgoal. It is hence recommended practice that the proof of any subgoal should end with a tactic which *fails if it does not solve the current goal*, -like discriminate, contradiction or assumption. +like :tacn:`discriminate`, :tacn:`contradiction` or :tacn:`assumption`. In fact, |SSR| provides a generic tactical which turns any tactic -into a closing one (similar to now). Its general syntax is: +into a closing one (similar to :tacn:`now`). Its general syntax is: .. tacn:: by @tactic :name: by + :undocumented: The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to :n:`[by @tactic | by @tactic | ...]` and this form should be preferred @@ -2014,39 +2073,29 @@ with a ``by``, like in: .. tacn:: done :name: done -The :tacn:`by` tactical is implemented using the user-defined, and extensible -:tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some -trivial means and fails if it doesn’t succeed. Indeed, the tactic -expression :n:`by @tactic` is equivalent to :n:`@tactic; done`. - -Conversely, the tactic - -.. coqtop:: - - by [ ]. - -is equivalent to: + The :tacn:`by` tactical is implemented using the user-defined, and extensible + :tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some + trivial means and fails if it doesn’t succeed. Indeed, the tactic + expression :n:`by @tactic` is equivalent to :n:`@tactic; done`. -.. coqtop:: + Conversely, the tactic ``by [ ]`` is equivalent to :tacn:`done`. - done. + The default implementation of the done tactic, in the ``ssreflect.v`` + file, is: -The default implementation of the done tactic, in the ``ssreflect.v`` -file, is: + .. coqdoc:: -.. coqtop:: in + Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | apply: sym_equal; trivial] + | discriminate | contradiction | split] + | case not_locked_false_eq_true; assumption + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. - Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] - | discriminate | contradiction | split] - | case not_locked_false_eq_true; assumption - | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. - -The lemma ``not_locked_false_eq_true`` is needed to discriminate -*locked* boolean predicates (see section :ref:`locking_ssr`). The iterator -tactical do is presented in section :ref:`iteration_ssr`. This tactic can be -customized by the user, for instance to include an ``auto`` tactic. + The lemma :g:`not_locked_false_eq_true` is needed to discriminate + *locked* boolean predicates (see section :ref:`locking_ssr`). The iterator + tactical do is presented in section :ref:`iteration_ssr`. This tactic can be + customized by the user, for instance to include an :tacn:`auto` tactic. A natural and common way of closing a goal is to apply a lemma which is the exact one needed for the goal to be solved. The defective form @@ -2063,7 +2112,7 @@ is equivalent to: do [done | by move=> top; apply top]. where ``top`` is a fresh name assigned to the top assumption of the goal. -This applied form is supported by the : discharge tactical, and the +This applied form is supported by the ``:`` discharge tactical, and the tactic: .. coqtop:: in @@ -2106,57 +2155,47 @@ is equivalent to: Selectors ~~~~~~~~~ -When composing tactics, the two tacticals ``first`` and ``last`` let the user -restrict the application of a tactic to only one of the subgoals -generated by the previous tactic. This covers the frequent cases where -a tactic generates two subgoals one of which can be easily disposed -of. - -This is another powerful way of linearization of scripts, since it -happens very often that a trivial subgoal can be solved in a less than -one line tactic. For instance, the tactic: - -.. tacn:: @tactic ; last by @tactic - :name: last - -tries to solve the last subgoal generated by the first -tactic using the given second tactic, and fails if it does not succeed. -Its analogue - -.. tacn:: @tactic ; first by @tactic - :name: first (ssreflect) - -tries to solve the first subgoal generated by the first tactic using the -second given tactic, and fails if it does not succeed. +.. tacn:: last + first + :name: last; first (ssreflect) + + When composing tactics, the two tacticals ``first`` and ``last`` let the user + restrict the application of a tactic to only one of the subgoals + generated by the previous tactic. This covers the frequent cases where + a tactic generates two subgoals one of which can be easily disposed + of. + + This is another powerful way of linearization of scripts, since it + happens very often that a trivial subgoal can be solved in a less than + one line tactic. For instance, :n:`@tactic ; last by @tactic` + tries to solve the last subgoal generated by the first + tactic using the given second tactic, and fails if it does not succeed. + Its analogue :n:`@tactic ; first by @tactic` + tries to solve the first subgoal generated by the first tactic using the + second given tactic, and fails if it does not succeed. |SSR| also offers an extension of this facility, by supplying -tactics to *permute* the subgoals generated by a tactic. The tactic: +tactics to *permute* the subgoals generated by a tactic. -.. tacv:: @tactic; last first +.. tacv:: last first + first last + :name: last first; first last -inverts the order of the subgoals generated by tactic. It is -equivalent to: + These two equivalent tactics invert the order of the subgoals in focus. -.. tacv:: @tactic; first last + .. tacv:: last @num first -More generally, the tactic: + If :token:`num`\'s value is :math:`k`, + this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` + in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the + circular order of subgoals remains unchanged. -.. tacn:: @tactic; last @num first - :name: last first + .. tacn:: first @num last -where :token:`num` is a |Coq| numeral, or an Ltac variable -denoting a |Coq| -numeral, having the value k. It rotates the n subgoals G1 , …, Gn -generated by tactic. The first subgoal becomes Gn + 1 − k and the -circular order of subgoals remains unchanged. - -Conversely, the tactic: - -.. tacn:: @tactic; first @num last - :name: first last - -rotates the n subgoals G1 , …, Gn generated by tactic in order that -the first subgoal becomes Gk . + If :token:`num`\'s value is :math:`k`, + this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` + in focus. The first subgoal becomes :math:`G_k` and the circular order + of subgoals remains unchanged. Finally, the tactics ``last`` and ``first`` combine with the branching syntax of Ltac: if the tactic generates n subgoals on a given goal, @@ -2200,16 +2239,14 @@ to the others. Iteration ~~~~~~~~~ -|SSR| offers an accurate control on the repetition of tactics, -thanks to the do tactical, whose general syntax is: - -.. tacn:: do {? @mult } ( @tactic | [ {+| @tactic } ] ) +.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] ) :name: do (ssreflect) -where :token:`mult` is a *multiplier*. + This tactical offers an accurate control on the repetition of tactics. + :token:`mult` is a *multiplier*. -Brackets can only be omitted if a single tactic is given *and* a -multiplier is present. + Brackets can only be omitted if a single tactic is given *and* a + multiplier is present. A tactic of the form: @@ -2274,6 +2311,7 @@ already presented the *localization* tactical in, whose general syntax is: .. tacn:: @tactic in {+ @ident} {? * } :name: in + :undocumented: where :token:`ident` is a name in the context. On the left side of ``in``, @@ -2318,17 +2356,15 @@ of a local definition during the generalization phase, the name of the local definition must be written between parentheses, like in ``rewrite H in H1 (def_n) H2.`` -From |SSR| 1.5 the grammar for the in tactical has been extended -to the following one: - .. tacv:: @tactic in {+ @clear_switch | {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) } {? * } -In its simplest form the last option lets one rename hypotheses that -can’t be cleared (like section variables). For example, ``(y := x)`` -generalizes over ``x`` and reintroduces the generalized variable under the -name ``y`` (and does not clear ``x``). -For a more precise description of this form of localization refer -to :ref:`advanced_generalization_ssr`. + This is the most general form of the ``in`` tactical. + In its simplest form the last option lets one rename hypotheses that + can’t be cleared (like section variables). For example, ``(y := x)`` + generalizes over ``x`` and reintroduces the generalized variable under the + name ``y`` (and does not clear ``x``). + For a more precise description of this form of localization refer + to :ref:`advanced_generalization_ssr`. .. _structure_ssr: @@ -2352,25 +2388,23 @@ intermediate statement. The have tactic. ```````````````` -The main |SSR| forward reasoning tactic is the ``have`` tactic. It can -be use in two modes: one starts a new (sub)proof for an intermediate -result in the main proof, and the other provides explicitly a proof -term for this intermediate step. - -In the first mode, the syntax of have in its defective form is: - .. tacn:: have : @term :name: have -This tactic supports open syntax for :token:`term`. Applied to a goal ``G``, it -generates a first subgoal requiring a proof of ``term`` in the context of -``G``. The second generated subgoal is of the form ``term -> G``, where term -becomes the new top assumption, instead of being introduced with a -fresh name. At the proof-term level, the have tactic creates a β -redex, and introduces the lemma under a fresh name, automatically -chosen. + This is the main |SSR| forward reasoning tactic. It can + be used in two modes: one starts a new (sub)proof for an intermediate + result in the main proof, and the other provides explicitly a proof + term for this intermediate step. + + This tactic supports open syntax for :token:`term`. Applied to a goal ``G``, it + generates a first subgoal requiring a proof of :token:`term` in the context of + ``G``. The second generated subgoal is of the form :n:`term -> G`, where term + becomes the new top assumption, instead of being introduced with a + fresh name. At the proof-term level, the have tactic creates a β + redex, and introduces the lemma under a fresh name, automatically + chosen. -Like in the case of the ``pose`` tactic (see section :ref:`definitions_ssr`), the types of +Like in the case of the :n:`pose (ssreflect)` tactic (see section :ref:`definitions_ssr`), the types of the holes are abstracted in term. .. example:: @@ -2425,6 +2459,7 @@ The behavior of the defective have tactic makes it possible to generalize it in the following general construction: .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } + :undocumented: Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -2433,6 +2468,7 @@ have tactic, which opens a sub-proof for an intermediate result, uses tactics of the form: .. tacv:: have @clear_switch @i_item : @term by @tactic + :undocumented: which behave like: @@ -2446,7 +2482,7 @@ allows to reuse a name of the context, possibly used by the proof of the assumption, to introduce the new assumption itself. -The``by`` feature is especially convenient when the proof script of the +The ``by`` feature is especially convenient when the proof script of the statement is very short, basically when it fits in one line like in: .. coqtop:: in @@ -2503,13 +2539,13 @@ term for the intermediate lemma, using tactics of the form: .. tacv:: have {? @ident } := term -This tactic creates a new assumption of type the type of :token:`term`. -If the -optional :token:`ident` is present, this assumption is introduced under the -name :token:`ident`. Note that the body of the constant is lost for the user. + This tactic creates a new assumption of type the type of :token:`term`. + If the + optional :token:`ident` is present, this assumption is introduced under the + name :token:`ident`. Note that the body of the constant is lost for the user. -Again, non inferred implicit arguments and explicit holes are -abstracted. + Again, non inferred implicit arguments and explicit holes are + abstracted. .. example:: @@ -2781,9 +2817,9 @@ hypothesis and by pointing at the elements of the initial goals which should be generalized. The general syntax of without loss is: .. tacn:: wlog {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term - :name: wlog -.. tacv:: without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term - :name: without loss + without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term + :name: wlog; without loss + :undocumented: where each :token:`ident` is a constant in the context of the goal. Open syntax is supported for :token:`term`. @@ -2791,8 +2827,8 @@ of the goal. Open syntax is supported for :token:`term`. In its defective form: .. tacv:: wlog: / @term -.. tacv:: without loss: / @term - + without loss: / @term + :undocumented: on a goal G, it creates two subgoals: a first one to prove the formula (term -> G) -> G and a second one to prove the formula @@ -2873,6 +2909,7 @@ The complete syntax for the items on the left hand side of the ``/`` separator is the following one: .. tacv:: wlog … : {? @clear_switch | {? @ } @ident | ( {? @ } @ident := @c_pattern) } / @term + :undocumented: Clear operations are intertwined with generalization operations. This helps in particular avoiding dependency issues while generalizing some @@ -2957,8 +2994,9 @@ The general form of an |SSR| rewrite tactic is: .. tacn:: rewrite {+ @rstep } :name: rewrite (ssreflect) + :undocumented: -The combination of a rewrite tactic with the in tactical (see section +The combination of a rewrite tactic with the ``in`` tactical (see section :ref:`localization_ssr`) performs rewriting in both the context and the goal. A rewrite step :token:`rstep` has the general form: @@ -3692,14 +3730,12 @@ definition. rewrite /=. unlock lid. -We provide a special tactic unlock for unfolding such definitions -while removing “locks”, e.g., the tactic: - .. tacn:: unlock {? @occ_switch } @ident :name: unlock -replaces the occurrence(s) of :token:`ident` coded by the -:token:`occ_switch` with the corresponding body. + This tactic unfolds such definitions while removing “locks”, i.e. it + replaces the occurrence(s) of :token:`ident` coded by the + :token:`occ_switch` with the corresponding body. We found that it was usually preferable to prevent the expansion of some functions by the partial evaluation switch ``/=``, unless this @@ -3775,103 +3811,102 @@ which the function is supplied: .. tacn:: congr {? @num } @term :name: congr -This tactic: - + This tactic: + checks that the goal is a Leibniz equality; + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. -The goal can be a non dependent product ``P -> Q``. In that case, the -system asserts the equation ``P = Q``, uses it to solve the goal, and -calls the ``congr`` tactic on the remaining goal ``P = Q``. This can be useful -for instance to perform a transitivity step, like in the following -situation. + The goal can be a non dependent product ``P -> Q``. In that case, the + system asserts the equation ``P = Q``, uses it to solve the goal, and + calls the ``congr`` tactic on the remaining goal ``P = Q``. This can be useful + for instance to perform a transitivity step, like in the following + situation. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Lemma test (x y z : nat) (H : x = y) : x = z. - congr (_ = _) : H. - Abort. + Lemma test (x y z : nat) (H : x = y) : x = z. + congr (_ = _) : H. + Abort. - Lemma test (x y z : nat) : x = y -> x = z. - congr (_ = _). + Lemma test (x y z : nat) : x = y -> x = z. + congr (_ = _). -The optional :token:`num` forces the number of arguments for which the -tactic should generate equality proof obligations. + The optional :token:`num` forces the number of arguments for which the + tactic should generate equality proof obligations. -This tactic supports equalities between applications with dependent -arguments. Yet dependent arguments should have exactly the same -parameters on both sides, and these parameters should appear as first -arguments. + This tactic supports equalities between applications with dependent + arguments. Yet dependent arguments should have exactly the same + parameters on both sides, and these parameters should appear as first + arguments. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Definition f n := - if n is 0 then plus else mult. - Definition g (n m : nat) := plus. + Definition f n := + if n is 0 then plus else mult. + Definition g (n m : nat) := plus. - Lemma test x y : f 0 x y = g 1 1 x y. - congr plus. + Lemma test x y : f 0 x y = g 1 1 x y. + congr plus. - This script shows that the ``congr`` tactic matches ``plus`` - with ``f 0`` on the left hand side and ``g 1 1`` on the right hand - side, and solves the goal. + This script shows that the ``congr`` tactic matches ``plus`` + with ``f 0`` on the left hand side and ``g 1 1`` on the right hand + side, and solves the goal. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. - congr S; rewrite -/plus. + Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. + congr S; rewrite -/plus. - The tactic ``rewrite -/plus`` folds back the expansion of plus - which was necessary for matching both sides of the equality with - an application of ``S``. + The tactic ``rewrite -/plus`` folds back the expansion of plus + which was necessary for matching both sides of the equality with + an application of ``S``. -Like most |SSR| arguments, term can contain wildcards. + Like most |SSR| arguments, :token:`term` can contain wildcards. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Lemma test x y : x + (y * (y + x - x)) = x * 1 + (y + 0) * y. - congr ( _ + (_ * _)). + Lemma test x y : x + (y * (y + x - x)) = x * 1 + (y + 0) * y. + congr ( _ + (_ * _)). .. _contextual_patterns_ssr: @@ -4192,6 +4227,7 @@ interpretation operations with the proof stack operations. This *view mechanism* relies on the combination of the ``/`` view switch with bookkeeping tactics and tacticals. +.. _custom_elim_ssr: Interpreting eliminations ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -4883,6 +4919,7 @@ Interpreting assumptions The general form of an assumption view tactic is: .. tacv:: [move | case] / @term + :undocumented: The term , called the *view lemma* can be: @@ -4997,6 +5034,7 @@ Interpreting goals A goal interpretation view tactic of the form: .. tacv:: apply/@term + :undocumented: applied to a goal ``top`` is interpreted in the following way: @@ -5027,6 +5065,7 @@ both sides. The syntax of double views is: .. tacv:: apply/@term/@term + :undocumented: The first term is the view lemma applied to the left hand side of the equality, while the second term is the one applied to the right hand side. @@ -5074,31 +5113,30 @@ In this context, the identity view can be used when no view has to be applied: Declaring new Hint Views ~~~~~~~~~~~~~~~~~~~~~~~~ -The database of hints for the view mechanism is extensible via a -dedicated vernacular command. As library ``ssrbool.v`` already declares a -corpus of hints, this feature is probably useful only for users who -define their own logical connectives. Users can declare their own -hints following the syntax used in ``ssrbool.v``: - .. cmd:: Hint View for move / @ident {? | @num } -.. cmd:: Hint View for apply / @ident {? | @num } + Hint View for apply / @ident {? | @num } -The :token:`ident` is the name of the lemma to be -declared as a hint. If `move` is used as -tactic, the hint is declared for assumption interpretation tactics, -`apply` declares hints for goal interpretations. Goal interpretation -view hints are declared for both simple views and left hand side -views. The optional natural number is the number of implicit -arguments to be considered for the declared hint view lemma. + This command can be used to extend the database of hints for the view + mechanism. -The command: + As library ``ssrbool.v`` already declares a + corpus of hints, this feature is probably useful only for users who + define their own logical connectives. -.. cmd:: Hint View for apply//@ident {? | @num } + The :token:`ident` is the name of the lemma to be + declared as a hint. If ``move`` is used as + tactic, the hint is declared for assumption interpretation tactics, + ``apply`` declares hints for goal interpretations. Goal interpretation + view hints are declared for both simple views and left hand side + views. The optional natural number is the number of implicit + arguments to be considered for the declared hint view lemma. -with a double slash ``//``, declares hint views for right hand sides of -double views. + .. cmdv:: Hint View for apply//@ident {? | @num } -See the files ``ssreflect.v`` and ``ssrbool.v`` for examples. + This variant with a double slash ``//``, declares hint views for right + hand sides of double views. + + See the files ``ssreflect.v`` and ``ssrbool.v`` for examples. Multiple views @@ -5157,73 +5195,66 @@ equivalences are indeed taken into account, otherwise only single |SSR| searching tool -------------------- -|SSR| proposes an extension of the Search command. Its syntax is: - .. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } :name: Search (ssreflect) -where :token:`qualid` is the name of an open module. This command returns -the list of lemmas: - - -+ whose *conclusion* contains a subterm matching the optional first - pattern. A - reverses the test, producing the list of lemmas whose - conclusion does not contain any subterm matching the pattern; -+ whose name contains the given string. A ``-`` prefix reverses the test, - producing the list of lemmas whose name does not contain the string. A - string that contains symbols or is followed by a scope key, is - interpreted as the constant whose notation involves that string (e.g., - `+` for `addn`), if this is unambiguous; otherwise the diagnostic - includes the output of the ``Locate`` vernacular command. -+ whose statement, including assumptions and types, contains a subterm - matching the next patterns. If a pattern is prefixed by ``-``, the test is - reversed; -+ contained in the given list of modules, except the ones in the - modules prefixed by a ``-``. - + This is the |SSR| extension of the Search command. :token:`qualid` is the + name of an open module. This command returns the list of lemmas: + + + whose *conclusion* contains a subterm matching the optional first + pattern. A - reverses the test, producing the list of lemmas whose + conclusion does not contain any subterm matching the pattern; + + whose name contains the given string. A ``-`` prefix reverses the test, + producing the list of lemmas whose name does not contain the string. A + string that contains symbols or is followed by a scope key, is + interpreted as the constant whose notation involves that string (e.g., + :g:`+` for :g:`addn`), if this is unambiguous; otherwise the diagnostic + includes the output of the :cmd:`Locate` vernacular command. + + whose statement, including assumptions and types, contains a subterm + matching the next patterns. If a pattern is prefixed by ``-``, the test is + reversed; + + contained in the given list of modules, except the ones in the + modules prefixed by a ``-``. + +.. note:: + + + As for regular terms, patterns can feature scope indications. For + instance, the command: ``Search _ (_ + _)%N.`` lists all the lemmas whose + statement (conclusion or hypotheses) involves an application of the + binary operation denoted by the infix ``+`` symbol in the ``N`` scope (which is + |SSR| scope for natural numbers). + + Patterns with holes should be surrounded by parentheses. + + Search always volunteers the expansion of the notation, avoiding the + need to execute Locate independently. Moreover, a string fragment + looks for any notation that contains fragment as a substring. If the + ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : -Note that: - - -+ As for regular terms, patterns can feature scope indications. For - instance, the command: ``Search _ (_ + _)%N.`` lists all the lemmas whose - statement (conclusion or hypotheses) involves an application of the - binary operation denoted by the infix ``+`` symbol in the ``N`` scope (which is - |SSR| scope for natural numbers). -+ Patterns with holes should be surrounded by parentheses. -+ Search always volunteers the expansion of the notation, avoiding the - need to execute Locate independently. Moreover, a string fragment - looks for any notation that contains fragment as a substring. If the - ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : - - .. example:: - - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect ssrbool. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + From Coq Require Import ssreflect ssrbool. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all - Search "~~". + Search "~~". -+ A diagnostic is issued if there are different matching notations; it - is an error if all matches are partial. -+ Similarly, a diagnostic warns about multiple interpretations, and - signals an error if there is no default one. -+ The command ``Search in M.`` is a way of obtaining the complete - signature of the module ``M``. -+ Strings and pattern indications can be interleaved, but the first - indication has a special status if it is a pattern, and only filters - the conclusion of lemmas: + + A diagnostic is issued if there are different matching notations; it + is an error if all matches are partial. + + Similarly, a diagnostic warns about multiple interpretations, and + signals an error if there is no default one. + + The command ``Search in M.`` is a way of obtaining the complete + signature of the module ``M``. + + Strings and pattern indications can be interleaved, but the first + indication has a special status if it is a pattern, and only filters + the conclusion of lemmas: - + The command : ``Search (_ =1 _) "bij".`` lists all the lemmas whose - conclusion features a ``=1`` and whose name contains the string ``bij``. - + The command : ``Search "bij" (_ =1 _).`` lists all the lemmas whose - statement, including hypotheses, features a ``=1`` and whose name - contains the string ``bij``. + + The command : ``Search (_ =1 _) "bij".`` lists all the lemmas whose + conclusion features a ``=1`` and whose name contains the string ``bij``. + + The command : ``Search "bij" (_ =1 _).`` lists all the lemmas whose + statement, including hypotheses, features a ``=1`` and whose name + contains the string ``bij``. Synopsis and Index ------------------ @@ -5275,11 +5306,21 @@ discharge item see :ref:`discharge_ssr` generalization item see :ref:`structure_ssr` -.. prodn:: i_pattern ::= @ident %| _ %| ? %| * %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {*| {* @i_item } } %| - %| [: {+ @ident } ] +.. prodn:: i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term +.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| @i_view %| @i_block + +view :ref:`introduction_ssr` + +.. prodn:: + i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) + +intro block :ref:`introduction_ssr` + +.. prodn:: + i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] intro item see :ref:`introduction_ssr` @@ -5327,80 +5368,78 @@ respectively. .. tacn:: move -idtac or hnf see :ref:`bookkeeping_ssr` + :tacn:`idtac` or :tacn:`hnf` (see :ref:`bookkeeping_ssr`) .. tacn:: apply -.. tacn:: exact + exact -application see :ref:`the_defective_tactics_ssr` + application (see :ref:`the_defective_tactics_ssr`) .. tacn:: abstract - see :ref:`abstract_ssr` and :ref:`generating_let_ssr` + see :ref:`abstract_ssr` and :ref:`generating_let_ssr` .. tacn:: elim -induction see :ref:`the_defective_tactics_ssr` + induction (see :ref:`the_defective_tactics_ssr`) .. tacn:: case -case analysis see :ref:`the_defective_tactics_ssr` + case analysis (see :ref:`the_defective_tactics_ssr`) .. tacn:: rewrite {+ @r_step } -rewrite see :ref:`rewriting_ssr` + rewrite (see :ref:`rewriting_ssr`) .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } -.. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term -.. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } -.. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } -.. tacv:: generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } - :name: generally have - -forward chaining see :ref:`structure_ssr` + have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } + have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term + have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } + generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } + :name: _; _; _; _; _; generally have + forward chaining (see :ref:`structure_ssr`) .. tacn:: wlog {? suff } {? @i_item } : {* @gen_item %| @clear_switch } / @term -specializing see :ref:`structure_ssr` + specializing (see :ref:`structure_ssr`) .. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } - :name: suff -.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } - :name: suffices -.. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } -.. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } + suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + :name: suff; suffices; _; _ -backchaining see :ref:`structure_ssr` + backchaining (see :ref:`structure_ssr`) .. tacn:: pose @ident := @term -local definition :ref:`definitions_ssr` + local definition (see :ref:`definitions_ssr`) .. tacv:: pose @ident {+ @ssr_binder } := @term -local function definition + local function definition .. tacv:: pose fix @fix_body -local fix definition + local fix definition .. tacv:: pose cofix @fix_body -local cofix definition + local cofix definition .. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %) -abbreviation see :ref:`abbreviations_ssr` + abbreviation (see :ref:`abbreviations_ssr`) .. tacn:: unlock {* {? @r_prefix } @ident } -unlock see :ref:`locking_ssr` + unlock (see :ref:`locking_ssr`) .. tacn:: congr {? @num } @term -congruence :ref:`congruence_ssr` + congruence (see :ref:`congruence_ssr`) Tacticals @@ -5439,15 +5478,15 @@ Commands .. cmd:: Hint View for %( move %| apply %) / @ident {? | @num } -view hint declaration see :ref:`declaring_new_hints_ssr` + view hint declaration (see :ref:`declaring_new_hints_ssr`) .. cmd:: Hint View for apply // @ident {? @num } -right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr` + right hand side double , view hint declaration (see :ref:`declaring_new_hints_ssr`) .. cmd:: Prenex Implicits {+ @ident } -prenex implicits declaration see :ref:`parametric_polymorphism_ssr` + prenex implicits declaration (see :ref:`parametric_polymorphism_ssr`) Settings ~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ad80cb62e1..59602581c7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3425,7 +3425,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint @hint_definition - No database name is given: the hint is registered in the core database. + No database name is given: the hint is registered in the ``core`` database. + + .. deprecated:: 8.10 .. cmdv:: Local Hint @hint_definition : {+ @ident} diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a5869055fa..47afa5ba0c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -70,7 +70,7 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments - <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the + <ImplicitArguments>` and other notations are resolved at the time of the declaration of the notation. Precedences and associativity @@ -1583,6 +1583,104 @@ Numeral notations As noted above, the :n:`(abstract after @num)` directive has no effect when :n:`@ident__2` lands in an :g:`option` type. +String notations +----------------- + +.. cmd:: String Notation @ident__1 @ident__2 @ident__3 : @scope. + :name: String Notation + + This command allows the user to customize the way strings are parsed + and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: + + * :n:`Byte.byte -> @ident__1` + * :n:`Byte.byte -> option @ident__1` + * :n:`list Byte.byte -> @ident__1` + * :n:`list Byte.byte -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Byte.byte` + * :n:`@ident__1 -> option Byte.byte` + * :n:`@ident__1 -> list Byte.byte` + * :n:`@ident__1 -> option (list Byte.byte)` + + When parsing, the application of the parsing function + :n:`@ident__2` to the string will be fully reduced, and universes + of the resulting term will be refreshed. + + .. exn:: Cannot interpret this string as a value of type @type + + The string notation registered for :token:`type` does not support + the given string. This error is given when the interpretation + function returns :g:`None`. + + .. exn:: @ident should go from Byte.byte or (list Byte.byte) to @type or (option @type). + + The parsing function given to the :cmd:`String Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)). + + The printing function given to the :cmd:`String Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type. + + String notations can only be declared for inductive types with no + arguments. + + .. exn:: Unexpected term @term while parsing a string notation. + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term @term while parsing a string notation. + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete string expressed as a decimal. They may not return + opaque constants. + + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the string notation is no + longer available in the environment. Most likely, this is because + the string notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`String Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`String Notation` must be single + identifiers. + + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`String Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + + Identifiers passed to :cmd:`String Notation` must be global + references, or notations which denote to single identifiers. + .. _TacticNotation: Tactic Notations diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4fc9bf9e19..51f94d7e5a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -17,6 +17,7 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Datatypes.v theories/Init/Logic.v theories/Init/Logic_Type.v + theories/Init/Byte.v theories/Init/Nat.v theories/Init/Decimal.v theories/Init/Peano.v @@ -497,6 +498,7 @@ through the <tt>Require Import</tt> command.</p> Implementation of string as list of ascii characters </dt> <dd> + theories/Strings/Byte.v theories/Strings/Ascii.v theories/Strings/String.v theories/Strings/BinaryString.v diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 57adcb287c..1de9890992 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -35,7 +35,7 @@ COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SY def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" - coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN", ""), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") if platform.system().startswith("CYGWIN"): # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 2c69dcfe08..067af954ad 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -198,6 +198,25 @@ class CoqObject(ObjectDescription): self._add_index_entry(name, target) return target + def _prepare_names(self): + sigs = self.get_signatures() + names = self.options.get("name") + if names is None: + self._names = {} + else: + names = [n.strip() for n in names.split(";")] + if len(names) != len(sigs): + ERR = ("Expected {} semicolon-separated names, got {}. " + + "Please provide one name per signature line.") + raise self.error(ERR.format(len(names), len(sigs))) + self._names = dict(zip(sigs, names)) + + def run(self): + self._prepare_names() + return super().run() + +class DocumentableObject(CoqObject): + def _warn_if_undocumented(self): document = self.state.document config = document.settings.env.config @@ -212,30 +231,16 @@ class CoqObject(ObjectDescription): if report == "warning": raise self.warning(msg) - def _prepare_names(self): - sigs = self.get_signatures() - names = self.options.get("name") - if names is None: - self._names = {} - else: - names = [n.strip() for n in names.split(";")] - if len(names) != len(sigs): - ERR = ("Expected {} semicolon-separated names, got {}. " + - "Please provide one name per signature line.") - raise self.error(ERR.format(len(names), len(sigs))) - self._names = dict(zip(sigs, names)) - def run(self): self._warn_if_undocumented() - self._prepare_names() return super().run() -class PlainObject(CoqObject): +class PlainObject(DocumentableObject): """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): signode += addnodes.desc_name(signature, signature) -class NotationObject(CoqObject): +class NotationObject(DocumentableObject): """A base class for objects whose signatures should be rendered as nested boxes. Objects that inherit from this class can use the notation grammar (“{+ …}”, @@ -1184,7 +1189,6 @@ def setup(app): app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles - app.add_stylesheet("fonts.css") app.add_stylesheet("ansi.css") app.add_stylesheet("coqdoc.css") app.add_javascript("notations.js") |