diff options
86 files changed, 4785 insertions, 474 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 095099690..c010da4cf 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,6 +1,7 @@ -image: coqci/base:V2018-05-07-V2 +image: "$IMAGE" stages: + - docker - build - test @@ -9,11 +10,28 @@ variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] CACHEKEY: bionic_coq-V2018-05-07-V2 + IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" # Used to select special compiler switches such as flambda, 32bits, etc... OPAM_VARIANT: "" +docker-boot: + stage: docker + image: docker:stable + services: + - docker:dind + before_script: [] + script: + - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY" + - cd dev/ci/docker/bionic_coq/ + - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi + - docker build -t "$IMAGE" . + - docker push "$IMAGE" + except: + variables: + - $SKIP_DOCKER == "true" + before_script: - cat /proc/{cpu,mem}info || true - ls -a # figure out if artifacts are around @@ -76,7 +94,7 @@ before_script: - set +e variables: &warnings-variables - COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -199,6 +217,7 @@ warnings:base: warnings:edge: <<: *warnings-template variables: + <<: *warnings-variables OPAM_SWITCH: edge test-suite:base: diff --git a/.travis.yml b/.travis.yml index 25acbf726..23b6f7f60 100644 --- a/.travis.yml +++ b/.travis.yml @@ -49,18 +49,24 @@ env: - NATIVE_COMP="yes" - COQ_DEST="-local" - MAIN_TARGET="world" - # Main test suites - matrix: - - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - - TEST_TARGET="validate" TW="travis_wait" - - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" matrix: include: - if: NOT (type = pull_request) env: + - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="validate" TW="travis_wait" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-bignums" - if: NOT (type = pull_request) env: @@ -125,7 +131,8 @@ matrix: - dev/lint-repository.sh # Full Coq test-suite with two compilers - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="${LABLGTK}" @@ -153,7 +160,8 @@ matrix: - python3-pip - python3-setuptools - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" @@ -168,7 +176,8 @@ matrix: packages: *extra-packages # Full test-suite with flambda - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - COMPILER="${COMPILER_BE}+flambda" - FINDLIB_VER="${FINDLIB_VER_BE}" @@ -184,7 +193,8 @@ matrix: packages: *extra-packages # Ocaml warnings with two compilers - - env: + - if: NOT (type = pull_request) + env: - MAIN_TARGET="coqocaml" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="${LABLGTK}" @@ -198,7 +208,8 @@ matrix: - libgtk2.0-dev - libgtksourceview2.0-dev - - env: + - if: NOT (type = pull_request) + env: - MAIN_TARGET="coqocaml" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" diff --git a/dev/ci/README.md b/dev/ci/README.md index 87f03aa99..dee3d2aff 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -96,7 +96,8 @@ PR by running GitLab CI on your private branches. To do so follow these steps: 2. Click on "New Project". 3. Choose "CI / CD for external repository" then click on "GitHub". 4. Find your fork of the Coq repository and click on "Connect". -5. You are encouraged to go to the CI / CD general settings and increase the +5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project). +6. You are encouraged to go to the CI / CD general settings and increase the timeout from 1h to 2h for better reliability. Now everytime you push (including force-push unless you changed the default @@ -137,3 +138,27 @@ Currently, available artifacts are: As an exception to the above, jobs testing that compilation triggers no OCaml warnings build Coq in parallel with other tests. + +### GitLab and Windows + + +If your repository has access to runners tagged `windows`, setting the +secret variable `WINDOWS` to `enabled` will add jobs building Windows +versions of Coq (32bit and 64bit). + +The Windows jobs are enabled on Coq's repository, where pipelines for +pull requests run. + +### GitLab and Docker + +System and opam packages are installed in a Docker image. The image is +automatically built and uploaded to your GitLab registry, and is +loaded by subsequent jobs. + +The Docker building job reuses the uploaded image if it is available, +but if you wish to save more time you can skip the job by setting +`SKIP_DOCKER` to `true`. + +This means you will need to change its value when the Docker image +needs to be updated. You can do so for a single pipeline by starting +it through the web interface. diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 03de1d53b..f867fd189 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ]; then export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi else if [ -n "${TRAVIS}" ]; then diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 000000000..517088a24 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 84ff94c66..a466124c1 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -109,9 +109,8 @@ There are two cases to consider: The merge script passes option `-S` to `git merge` to ensure merge commits are signed. Consequently, it depends on the GnuPG command utility being -installed and a GPG key being available. Here is a short tutorial to -creating your own GPG key: -<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. The script depends on a few other utilities. If you are a Nix user, the simplest way of getting them is to run `nix-shell` first. diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 9dd12087a..70a9756e5 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -23,7 +23,7 @@ ;; If you load this file from a git repository, checking out an old ;; commit will make it disappear and cause errors for your Emacs -;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; startup. To ignore those errors use (require 'coqdev nil t). If you ;; check out a malicious commit Emacs startup would allow it to run ;; arbitrary code, to avoid this you can copy coqdev.el to any ;; location and adjust the load path accordingly (of course if you run @@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'." (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) (add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) +(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end) + "Add LEFT and RIGHT around the BEG..END. +Leave the point after RIGHT. BEG and END default to the bounds +of the current region. Leave point OFFSET characters after the +left quote (if OFFSET is nil, leave the point after the right +quote)." + (unless beg + (if (region-active-p) + (setq beg (region-beginning) end (region-end)) + (setq beg (point) end nil))) + (save-excursion + (goto-char (or end beg)) + (insert right)) + (save-excursion + (goto-char beg) + (insert left)) + (if (and end (not offset)) ;; Second test handles the ::`` case + (goto-char (+ end (length left) (length right))) + (goto-char (+ beg (or offset (length left)))))) + +(defun coqdev-sphinx-rst-coq-action () + "Insert a Sphinx role template or quote the current region." + (interactive) + (pcase (read-char "Command [gntm:`]?") + (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`")) + (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`")) + (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`")) + (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`")) + (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1)) + (?` (coqdev-sphinx-quote-coq-refman-region "``" "``")))) + (provide 'coqdev) ;;; coqdev ends here diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING deleted file mode 100644 index fa6fe1537..000000000 --- a/doc/sphinx/MIGRATING +++ /dev/null @@ -1,238 +0,0 @@ -How to migrate the Coq Reference Manual to Sphinx -================================================= - -# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools) - - * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex - -# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/ - - * pip3 install virtualenv - * virtualenv coqsphinxing # you may want to use -p to specify the python version - * source coqsphinxing/bin/activate # activate the virtual environment - -# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session. - -# Add this Elisp code to .emacs, if you're using emacs (recommended): - - (defun sphinx/quote-coq-refman-region (left right &optional beg end count) - (unless beg - (if (region-active-p) - (setq beg (region-beginning) end (region-end)) - (setq beg (point) end nil))) - (unless count - (setq count 1)) - (save-excursion - (goto-char (or end beg)) - (dotimes (_ count) (insert right))) - (save-excursion - (goto-char beg) - (dotimes (_ count) (insert left))) - (if (and end (characterp left)) ;; Second test handles the ::`` case - (goto-char (+ (* 2 count) end)) - (goto-char (+ count beg)))) - - (defun sphinx/coqtop (beg end) - (interactive (list (region-beginning) (region-end))) - (replace-regexp "^Coq < " " " nil beg end) - (indent-rigidly beg end -3) - (goto-char beg) - (insert ".. coqtop:: all\n\n")) - - (defun sphinx/rst-coq-action () - (interactive) - (pcase (read-char "Command?") - (?g (sphinx/quote-coq-refman-region ":g:`" "`")) - (?n (sphinx/quote-coq-refman-region ":n:`" "`")) - (?t (sphinx/quote-coq-refman-region ":token:`" "`")) - (?m (sphinx/quote-coq-refman-region ":math:`" "`")) - (?: (sphinx/quote-coq-refman-region "::`" "`")) - (?` (sphinx/quote-coq-refman-region "``" "``")) - (?c (sphinx/coqtop (region-beginning) (region-end))))) - - (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action) - - With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text - (this will make more sense once you've started editing the text). - -# Fork the Coq repo, if needed: - - https://github.com/coq/coq - -# Clone the repo to your work machine - -# Add Maxime Dénès's repo as a remote: - - git remote add sphinx https://github.com/maximedenes/coq.git - - (or choose a name other than "sphinx") - - Verify with: - - git remote -v - -# Fetch from the remote - - git fetch sphinx - -# Checkout the sphinx-doc branch - - git checkout sphinx-doc - - You should pull from the repo from time to time to keep your local copy up-to-date: - - git pull sphinx sphinx-doc - - You may want to create a new branch to do your work in. - -# Choose a Reference Manual chapter to work on at - - https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU - -# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility, - is available in the directory porting/raw-rst/ - - Elsewhere, depending on the chapter, there should be an almost-empty template file already created, - which is in the location where the final version should go - -# Manually edit the .rst file, place it in the correct location - - There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst - - (N.B.: the migration is a work-in-progress, your suggestions are welcome) - - Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/. - At the top of the file, after the chapter heading, add: - - :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html - :Converted by: Your Name - - N.B.: These source and converted-by annotations should help for the migration phase. Later on, - those annotations will be removed, and contributors will be mentioned in the Coq credits. - - Remove chapter numbers - - Replace section, subsection numbers with reference labels: - - .. _some-reference-label: - - Place the label before the section or subsection, followed by a blank line. - - Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted. - Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form - `TODO-n.n.n-mnemonic` we can fixup later. Example: - - :ref:`TODO-1.3.2-definitions` - - We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual. - - For the particular case of references to chapters, we can use a -convention for the cross-reference name, so no TODO is needed. - - :ref:`thegallinaspecificationlanguage` - -That is, the chapter label is the chapter title, all in lower-case, -with no spaces or punctuation. For chapters with subtitles marked with -a ":", like those for Omega and Nsatz, use just the chapter part -preceding the ":". These labels should already be in the -placeholder .rst files for each chapter. - - - You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a - section or subsection, use the syntax - - :ref:`Some link text <label-name>` - - Yes, the angle-brackets are needed here! - - For bibliographic references (those in biblio.bib), use :cite:`thecitation`. - - Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see - http://www.sphinx-doc.org/en/stable/markup/para.html. - - For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx - script will run coqtop on those examples, and can show the output (or not). - - The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise. - Use - - .. include:: replaces.rst - - to gain access to those definitions in your file (you might need a path prefix). Some especially-important - replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them, - so that they're rendered consistently. - - Similarly, there are some LaTeX macros in preamble.rst that can be useful. - - Conventions: - - - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``). - - - Metavariables are single-backquotes (e.g. `term`, `ident`) - - - Use the cmd directive for Vernacular commands, like: - - .. cmd:: Set Printing All. - - Within this directive, prefix metavariables (ident, term) with @: - - .. cmd:: Add Printing Let @ident. - - There's also the "cmdv" directive for variants of a command. - - - Use the "exn" and "warn" directives for errors and warnings: - - .. exn:: Something's not right. - .. warn:: You shouldn't do that. - - - Use the "example" directive for examples - - - Use the "g" role for inline Gallina, like :g:`fun x => x` - - - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line:: - - your code here - - which prints a single colon, or put the double-colon on a newline. - -:: - - your other code here - -# Making changes to the text - - The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not - to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong - verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days - called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed. - -# Build, view the manual - - In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file - associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory. - Make any changes you need until there are no build warnings and the output is perfect. :-) - -# Creating pull requests - - When your changes are done, commit them, push to your fork: - - git commit -m "useful commit message" file - git push origin sphinx-doc - - (or push to another branch, if you've created one). Then go to your GitHub - fork and create a pull request against Maxime's sphinx-doc - branch. If your commit is recent, you should see a link on your - fork's code page to do that. Otherwise, you may need to go to your - branch on GitHub to do that. - -# Issues/Questions/Suggestions - - As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact: - - Paul Steckler <steck@stecksoft.com> - Maxime Dénès <maxime.denes@inria.fr> - -# Issues - - Should the stuff in replaces.rst go in preamble.rst? - In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that? diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst new file mode 100644 index 000000000..5f2f21f2b --- /dev/null +++ b/doc/sphinx/README.rst @@ -0,0 +1,325 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + README.rst is auto-generated from README.template.rst and the coqrst docs; + use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + +Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. + +In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands. + +Coq objects +=========== + +Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: + + .. tacv:: simpl @pattern at {+ @num} + :name: simpl_at + + This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences + +Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. + +Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above. + +- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```. +- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. +- Vernac variants, tactic notations, and tactic variants do not have a default name. + +Notations +--------- + +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_): + +``@…`` + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + +``{? …}`` + an optional block + +``{* …}``, ``{+ …}`` + an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces + +``{*, …}``, ``{+, …}`` + an optional or mandatory repeatable block, with repetitions separated by commas + +``%|``, ``%{``, … + an escaped character (rendered without the leading ``%``) + +.. + FIXME document the new subscript support + +As an exercise, what do the following patterns mean? + +.. code:: + + pattern {+, @term {? at {+ @num}}} + generalize {+, @term at {+ @num} as @ident} + fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + +Objects +------- + +Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): + +``.. cmd::`` :black_nib: A Coq command. + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + +``.. cmdv::`` :black_nib: A variant of a Coq command. + Example:: + + .. cmd:: Axiom @ident : @term. + + This command links :token:`term` to the name :token:`term` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a + postulate. + + .. cmdv:: Parameter @ident : @term. + + This is equivalent to :n:`Axiom @ident : @term`. + +``.. exn::`` :black_nib: An error raised by a Coq command or tactic. + This commonly appears nested in the ``.. tacn::`` that raises the + exception. + + Example:: + + .. tacv:: assert @form by @tactic + + This tactic applies :n:`@tactic` to solve the subgoals generated by + ``assert``. + + .. exn:: Proof is not complete + + Raised if :n:`@tactic` does not fully solve the goal. + +``.. opt::`` :black_nib: A Coq option. + Example:: + + .. opt:: Nonrecursive Elimination Schemes + + This option controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + +``.. prodn::`` :black_nib: Grammar productions. + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + +``.. tacn::`` :black_nib: A tactic, or a tactic notation. + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + +``.. tacv::`` :black_nib: A variant of a tactic. + Example:: + + .. tacn:: fail + + This is the always-failing tactic: it does not solve any goal. It is + useful for defining other tacticals since it can be caught by + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching + tacticals. … + + .. tacv:: fail @natural + + The number is the failure level. If no level is specified, it + defaults to 0. … + +``.. thm::`` A theorem. + Example:: + + .. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + +``.. warn::`` :black_nib: An warning raised by a Coq command or tactic.. + Do not mistake this for ``.. warning::``; this directive is for warning + messages produced by Coq. + + + Example:: + + .. warn:: Ambiguous path + + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored. + +Coq directives +============== + +In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: + +``.. coqtop::`` A reST directive to describe interactions with Coqtop. + Usage:: + + .. coqtop:: options… + + Coq code to send to coqtop + + Example:: + + .. coqtop:: in reset undo + + Print nat. + Definition a := 1. + + Here is a list of permissible options: + + - Display options + + - ``all``: Display input and output + - ``in``: Display only input + - ``out``: Display only output + - ``none``: Display neither (useful for setup commands) + + - Behavior options + + - ``reset``: Send a ``Reset Initial`` command before running this block + - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after + running all the commands in this block + + ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + of the same document (``coqrst`` creates a single ``coqtop`` process per + reST source file). Use the ``reset`` option to reset Coq's state. + +``.. coqdoc::`` A reST directive to display Coqtop-formatted source code. + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + +``.. example::`` A reST directive for examples. + This behaves like a generic admonition; see + http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition + for more details. + + Example:: + + .. example:: Adding a hint to a database + + The following adds ``plus_comm`` to the ``plu`` database: + + .. coqdoc:: + + Hint Resolve plus_comm : plu. + +``.. inference::`` A reST directive to format inference rules. + This also serves as a small illustration of the way to create new Sphinx + directives. + + Usage:: + + .. inference:: name + + newline-separated premisses + ------------------------ + conclusion + + Example:: + + .. inference:: Prod-Pro + + \WTEG{T}{s} + s \in \Sort + \WTE{\Gamma::(x:T)}{U}{\Prop} + ----------------------------- + \WTEG{\forall~x:T,U}{\Prop} + +``.. preamble::`` A reST directive for hidden math. + Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} + +Coq roles +========= + +In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: + +``:g:`` Coq code. + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + +``:n:`` Any text using the notation syntax (``@id``, ``{+, …}``, etc.). + Use this to explain tactic equivalences. For example, you might write + this:: + + :n:`generalize @term as @ident` is just like :n:`generalize @term`, but + it names the introduced hypothesis :token:`ident`. + + Note that this example also uses ``:token:``. That's because ``ident`` is + defined in the the Coq manual as a grammar production, and ``:token:`` + creates a link to that. When referring to a placeholder that happens to be + a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. + +``:production:`` A grammar production not included in a ``productionlist`` directive. + Useful to informally introduce a production, as part of running text. + + Example:: + + :production:`string` indicates a quoted string. + + You're not likely to use this role very commonly; instead, use a + `production list + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. + +Tips and tricks +=============== + +Nested lemmas +------------- + +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: + + .. coqtop:: all + + Lemma l1: 1 + 1 = 2. + + .. coqtop:: all + + Lemma l2: 2 + 2 <> 1. + +Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. + +Abbreviations and macros +------------------------ + +Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. + +Emacs +----- + +The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. + +Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: + + (with-eval-after-load 'rst + (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst new file mode 100644 index 000000000..203251abf --- /dev/null +++ b/doc/sphinx/README.template.rst @@ -0,0 +1,117 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + README.rst is auto-generated from README.template.rst and the coqrst docs; + use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + +Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. + +In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands. + +Coq objects +=========== + +Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: + + .. tacv:: simpl @pattern at {+ @num} + :name: simpl_at + + This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences + +Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. + +Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above. + +- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```. +- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. +- Vernac variants, tactic notations, and tactic variants do not have a default name. + +Notations +--------- + +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_): + +``@…`` + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + +``{? …}`` + an optional block + +``{* …}``, ``{+ …}`` + an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces + +``{*, …}``, ``{+, …}`` + an optional or mandatory repeatable block, with repetitions separated by commas + +``%|``, ``%{``, … + an escaped character (rendered without the leading ``%``) + +.. + FIXME document the new subscript support + +As an exercise, what do the following patterns mean? + +.. code:: + + pattern {+, @term {? at {+ @num}}} + generalize {+, @term at {+ @num} as @ident} + fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + +Objects +------- + +Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): + +[OBJECTS] + +Coq directives +============== + +In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: + +[DIRECTIVES] + +Coq roles +========= + +In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: + +[ROLES] + +Tips and tricks +=============== + +Nested lemmas +------------- + +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: + + .. coqtop:: all + + Lemma l1: 1 + 1 = 2. + + .. coqtop:: all + + Lemma l2: 2 + 2 <> 1. + +Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. + +Abbreviations and macros +------------------------ + +Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. + +Emacs +----- + +The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. + +Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: + + (with-eval-after-load 'rst + (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 152f4f655..09faa0676 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -140,29 +140,29 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f887a5fee..0e9c23b9b 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin .. _ceil_thm: -**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then +.. thm:: Bound on the ceiling function - :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. For instance, from 2 x = 1 we can deduce diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 80ea8a116..b6c35d8fa 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -11,7 +11,7 @@ Program derivation |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations of program refinements. To use the Derive extension it must first be -required with ``Require Coq.Derive.Derive``. When the extension is loaded, +required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: .. cmd:: Derive @ident SuchThat @term As @ident diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 23bc9a2e4..1f7dd9d68 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -96,11 +96,13 @@ language = None # directories to ignore when looking for source files. # This patterns also effect to html_static_path and html_extra_path exclude_patterns = [ - '_build', - 'Thumbs.db', - '.DS_Store', - 'introduction.rst', - 'credits.rst' + '_build', + 'Thumbs.db', + '.DS_Store', + 'introduction.rst', + 'credits.rst', + 'README.rst', + 'README.template.rst' ] # The reST default role (used for this markup: `text`) to use for all diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index aa41f8058..4dcd7deb1 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -553,8 +553,8 @@ has type :token:`type`. .. cmd:: Axiom @ident : @term - This command links *term* to the name *ident* as its specification in - the global context. The fact asserted by *term* is thus assumed as a + This command links :token:`term` to the name :token:`ident` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a postulate. .. exn:: @ident already exists. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 83dddab4f..ad1f0caa6 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -55,15 +55,20 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file -``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default its home -directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is -searched. You can also specify an arbitrary name for the resource file +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). -This file may contain, for instance, ``Add LoadPath`` commands to add +The resource file may contain, for instance, ``Add LoadPath`` commands to add directories to the load path of |Coq|. It is possible to skip the loading of the resource file with the option ``-q``. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0318bddde..3835524f0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -653,7 +653,7 @@ be applied or the goal is not head-reducible. This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. -.. tac:: intro @ident +.. tacn:: intro @ident This applies ``intro`` but forces :n:`@ident` to be the name of the introduced hypothesis. @@ -904,15 +904,15 @@ quantification or an implication. .. tacn:: revert {+ @ident} :name: revert -This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses -(possibly defined) to the goal, if this respects dependencies. This tactic is -the inverse of :tacn:`intro`. + This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses + (possibly defined) to the goal, if this respects dependencies. This tactic is + the inverse of :tacn:`intro`. .. exn:: No such hypothesis. .. exn:: @ident is used in the hypothesis @ident. -.. tac:: revert dependent @ident +.. tacn:: revert dependent @ident This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that depend on it. @@ -1122,7 +1122,7 @@ Controlling the proof flow This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by Coq. -.. tacv:: assert form by tactic +.. tacv:: assert @form by @tactic This tactic behaves like :n:`assert` but applies tactic to solve the subgoals generated by assert. @@ -1130,7 +1130,7 @@ Controlling the proof flow .. exn:: Proof is not complete. :name: Proof is not complete. (assert) -.. tacv:: assert form as intro_pattern +.. tacv:: assert @form as @intro_pattern If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), the hypothesis is named after this introduction pattern (in particular, if @@ -1139,7 +1139,7 @@ Controlling the proof flow introduction pattern, the tactic behaves like :n:`assert form` followed by the action done by this introduction pattern. -.. tacv:: assert form as intro_pattern by tactic +.. tacv:: assert @form as @intro_pattern by @tactic This combines the two previous variants of :n:`assert`. @@ -1192,9 +1192,9 @@ Controlling the proof flow This behaves like :n:`enough form` using :n:`intro_pattern` to name or destruct the new hypothesis. -.. tacv:: enough (@ident : form) by tactic -.. tacv:: enough form by tactic -.. tacv:: enough form as intro_pattern by tactic +.. tacv:: enough (@ident : @form) by @tactic +.. tacv:: enough @form by @tactic +.. tacv:: enough @form as @intro_pattern by @tactic This behaves as above but with :n:`tactic` expected to solve the initial goal after the extra assumption :n:`form` is added and possibly destructed. If the @@ -3240,7 +3240,9 @@ the processing of the rewriting rules. The rewriting rule bases are built with the ``Hint Rewrite vernacular`` command. -.. warn:: This tactic may loop if you build non terminating rewriting systems. +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. .. tacv:: autorewrite with {+ @ident} using @tactic @@ -3444,7 +3446,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. - .. cmdv:: Hint Extern @num {? @pattern} => tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 682553c31..838926d65 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -106,15 +106,15 @@ Automatic declaration of schemes .. opt:: Elimination Schemes -It is possible to deactivate the automatic declaration of the -induction principles when defining a new inductive type with the -``Unset Elimination Schemes`` command. It may be reactivated at any time with -``Set Elimination Schemes``. + It is possible to deactivate the automatic declaration of the + induction principles when defining a new inductive type with the + ``Unset Elimination Schemes`` command. It may be reactivated at any time with + ``Set Elimination Schemes``. .. opt:: Nonrecursive Elimination Schemes -This option controls whether types declared with the keywords :cmd:`Variant` and -:cmd:`Record` get an automatic declaration of the induction principles. + This option controls whether types declared with the keywords :cmd:`Variant` and + :cmd:`Record` get an automatic declaration of the induction principles. .. opt:: Case Analysis Schemes @@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and .. opt:: Decidable Equality Schemes -These flags control the automatic declaration of those Boolean equalities (see -the second variant of ``Scheme``). + These flags control the automatic declaration of those Boolean equalities (see + the second variant of ``Scheme``). .. warning:: diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index d464f75bb..a004959eb 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -32,8 +32,9 @@ COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) -def coqdoc(coq_code, coqdoc_bin = os.path.join(os.getenv("COQBIN"),"coqdoc")): +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") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") try: os.write(fd, COQDOC_HEADER.encode("utf-8")) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 21093bd90..606d725bf 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## ## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## @@ -57,30 +58,37 @@ def make_target(objtype, targetid): return "coq:{}.{}".format(objtype, targetid) class CoqObject(ObjectDescription): - """A generic Coq object; all Coq objects are subclasses of this. + """A generic Coq object for Sphinx; all Coq objects are subclasses of this. The fields and methods to override are listed at the top of this class' implementation. Each object supports the :name: option, which gives an explicit name to link to. - See the documentation of CoqDomain for high-level information. + See the comments and docstrings in CoqObject for more information. """ - # The semantic domain in which this object lives. + # The semantic domain in which this object lives (eg. “tac”, “cmd”, “chm”…). # It matches exactly one of the roles used for cross-referencing. - subdomain = None + subdomain = None # type: str - # The suffix to use in indices for objects of this type - index_suffix = None + # The suffix to use in indices for objects of this type (eg. “(tac)”) + index_suffix = None # type: str # The annotation to add to headers of objects of this type - annotation = None + # (eg. “Command”, “Theorem”) + annotation = None # type: str def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument """Convert a signature into a name to link to. + ‘Signature’ is Sphinx parlance for an object's header (think “type + signature”); for example, the signature of the simplest form of the + ``exact`` tactic is ``exact @id``. + Returns None by default, in which case no name will be automatically - generated. + generated. This is a convenient way to automatically generate names + (link targets) without having to write explicit names everywhere. + """ return None @@ -100,7 +108,7 @@ class CoqObject(ObjectDescription): def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using - _render_signature. + ``_render_signature`` (for example, add “Command” in front of commands). :returns: the name given to the resulting node, if any """ @@ -110,11 +118,6 @@ class CoqObject(ObjectDescription): self._render_signature(signature, signode) return self.options.get("name") or self._name_from_signature(signature) - @property - def _index_suffix(self): - if self.index_suffix: - return " " + self.index_suffix - def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -141,12 +144,14 @@ class CoqObject(ObjectDescription): return targetid def _add_index_entry(self, name, target): - """Add name (with target) to the main index.""" - index_text = name + self._index_suffix + """Add `name` (pointing to `target`) to the main index.""" + index_text = name + if self.index_suffix: + index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) def add_target_and_index(self, name, _, signode): - """Create a target and an index entry for name""" + """Attach a link target to `signode` and an index entry for `name`.""" if name: target = self._add_target(signode, name) # remove trailing . , found in commands, but not ... (ellipsis) @@ -156,31 +161,44 @@ class CoqObject(ObjectDescription): return target class PlainObject(CoqObject): - """A base class for objects whose signatures should be rendered literaly.""" + """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): - """A base class for objects whose signatures should be rendered as nested boxes.""" + """A base class for objects whose signatures should be rendered as nested boxes. + + Objects that inherit from this class can use the notation grammar (“{+ …}”, + “@…”, etc.) in their signature. + """ def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) tacn_node = parse_notation(signature, *position) signode += addnodes.desc_name(signature, '', tacn_node) -class TacticObject(PlainObject): - """An object to represent Coq tactics""" - subdomain = "tac" - index_suffix = "(tac)" - annotation = None - class GallinaObject(PlainObject): - """An object to represent Coq theorems""" + r"""A theorem. + + Example:: + + .. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + """ subdomain = "thm" index_suffix = "(thm)" annotation = "Theorem" class VernacObject(NotationObject): - """An object to represent Coq commands""" + """A Coq command. + + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + """ subdomain = "cmd" index_suffix = "(cmd)" annotation = "Command" @@ -191,7 +209,20 @@ class VernacObject(NotationObject): return m.group(0).strip() class VernacVariantObject(VernacObject): - """An object to represent variants of Coq commands""" + """A variant of a Coq command. + + Example:: + + .. cmd:: Axiom @ident : @term. + + This command links :token:`term` to the name :token:`term` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a + postulate. + + .. cmdv:: Parameter @ident : @term. + + This is equivalent to :n:`Axiom @ident : @term`. + """ index_suffix = "(cmdv)" annotation = "Variant" @@ -199,18 +230,49 @@ class VernacVariantObject(VernacObject): return None class TacticNotationObject(NotationObject): - """An object to represent Coq tactic notations""" + """A tactic, or a tactic notation. + + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + """ subdomain = "tacn" index_suffix = "(tacn)" annotation = None class TacticNotationVariantObject(TacticNotationObject): - """An object to represent variants of Coq tactic notations""" + """A variant of a tactic. + + Example:: + + .. tacn:: fail + + This is the always-failing tactic: it does not solve any goal. It is + useful for defining other tacticals since it can be caught by + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching + tacticals. … + + .. tacv:: fail @natural + + The number is the failure level. If no level is specified, it + defaults to 0. … + """ index_suffix = "(tacnv)" annotation = "Variant" class OptionObject(NotationObject): - """An object to represent Coq options""" + """A Coq option. + + Example:: + + .. opt:: Nonrecursive Elimination Schemes + + This option controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + """ subdomain = "opt" index_suffix = "(opt)" annotation = "Option" @@ -219,7 +281,13 @@ class OptionObject(NotationObject): return stringify_with_ellipses(signature) class ProductionObject(NotationObject): - """An object to represent grammar productions""" + """Grammar productions. + + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + """ + # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" index_suffix = None annotation = None @@ -258,7 +326,22 @@ class ProductionObject(NotationObject): return [idx, node] class ExceptionObject(NotationObject): - """An object to represent Coq errors.""" + """An error raised by a Coq command or tactic. + + This commonly appears nested in the ``.. tacn::`` that raises the + exception. + + Example:: + + .. tacv:: assert @form by @tactic + + This tactic applies :n:`@tactic` to solve the subgoals generated by + ``assert``. + + .. exn:: Proof is not complete + + Raised if :n:`@tactic` does not fully solve the goal. + """ subdomain = "exn" index_suffix = "(err)" annotation = "Error" @@ -269,7 +352,19 @@ class ExceptionObject(NotationObject): return stringify_with_ellipses(signature) class WarningObject(NotationObject): - """An object to represent Coq warnings.""" + """An warning raised by a Coq command or tactic.. + + Do not mistake this for ``.. warning::``; this directive is for warning + messages produced by Coq. + + + Example:: + + .. warn:: Ambiguous path + + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored. + """ subdomain = "warn" index_suffix = "(warn)" annotation = "Warning" @@ -280,14 +375,33 @@ class WarningObject(NotationObject): def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=unused-argument, dangerous-default-value - """And inline role for notations""" + """Any text using the notation syntax (``@id``, ``{+, …}``, etc.). + + Use this to explain tactic equivalences. For example, you might write + this:: + + :n:`generalize @term as @ident` is just like :n:`generalize @term`, but + it names the introduced hypothesis :token:`ident`. + + Note that this example also uses ``:token:``. That's because ``ident`` is + defined in the the Coq manual as a grammar production, and ``:token:`` + creates a link to that. When referring to a placeholder that happens to be + a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. + """ notation = utils.unescape(text, 1) position = inliner.reporter.get_source_and_line(lineno) return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=dangerous-default-value - """And inline role for Coq source code""" + """Coq code. + + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + """ options['language'] = 'Coq' return code_role(role, rawtext, text, lineno, inliner, options, content) ## Too heavy: @@ -300,15 +414,14 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): # node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes) # return [node], [] -# TODO pass different languages? -LtacRole = GallinaRole = VernacRole = coq_code_role +CoqCodeRole = coq_code_role class CoqtopDirective(Directive): """A reST directive to describe interactions with Coqtop. Usage:: - .. coqtop:: (options)+ + .. coqtop:: options… Coq code to send to coqtop @@ -321,20 +434,28 @@ class CoqtopDirective(Directive): Here is a list of permissible options: - Display - - ‘all’: Display input and output - - ‘in’: Display only input - - ‘out’: Display only output - - ‘none’: Display neither (useful for setup commands) - Behaviour - - ‘reset’: Send a `Reset Initial` command before running this block - - ‘undo’: Send an `Undo n` (n=number of sentences) command after running - all the commands in this block + - Display options + + - ``all``: Display input and output + - ``in``: Display only input + - ``out``: Display only output + - ``none``: Display neither (useful for setup commands) + + - Behavior options + + - ``reset``: Send a ``Reset Initial`` command before running this block + - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after + running all the commands in this block + + ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + of the same document (``coqrst`` creates a single ``coqtop`` process per + reST source file). Use the ``reset`` option to reset Coq's state. """ has_content = True required_arguments = 0 optional_arguments = 1 final_argument_whitespace = True + directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -349,12 +470,26 @@ class CoqtopDirective(Directive): return [node] class CoqdocDirective(Directive): - """A reST directive to display Coqtop-formatted source code""" + """A reST directive to display Coqtop-formatted source code. + + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + """ # TODO implement this as a Pygments highlighter? has_content = True required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + directive_name = "coqdoc" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -365,8 +500,24 @@ class CoqdocDirective(Directive): return [wrapper] class ExampleDirective(BaseAdmonition): - """A reST directive for examples""" + """A reST directive for examples. + + This behaves like a generic admonition; see + http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition + for more details. + + Example:: + + .. example:: Adding a hint to a database + + The following adds ``plus_comm`` to the ``plu`` database: + + .. coqdoc:: + + Hint Resolve plus_comm : plu. + """ node_class = nodes.admonition + directive_name = "example" def run(self): # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’, @@ -380,8 +531,17 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(MathDirective): r"""A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s + Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} """ + + directive_name = "preamble" + def run(self): self.options['nowrap'] = True [node] = super().run() @@ -389,14 +549,17 @@ class PreambleDirective(MathDirective): return [node] class InferenceDirective(Directive): - r"""A small example of what directives let you do in Sphinx. + r"""A reST directive to format inference rules. + + This also serves as a small illustration of the way to create new Sphinx + directives. Usage:: .. inference:: name - \n-separated premisses - ---------------------- + newline-separated premisses + ------------------------ conclusion Example:: @@ -413,6 +576,7 @@ class InferenceDirective(Directive): optional_arguments = 0 has_content = True final_argument_whitespace = True + directive_name = "inference" def make_math_node(self, latex): node = displaymath() @@ -613,7 +777,7 @@ class CoqSubdomainsIndex(Index): Just as in the original manual, we want to have separate indices for each Coq subdomain (tactics, commands, options, etc)""" - name, localname, shortname, subdomains = None, None, None, None # Must be overwritten + name, localname, shortname, subdomains = None, None, None, [] # Must be overwritten def generate(self, docnames=None): content = defaultdict(list) @@ -635,7 +799,7 @@ class CoqVernacIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"] class CoqTacticIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tac", "tacn"] + name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] @@ -665,10 +829,18 @@ class IndexXRefRole(XRefRole): return title, target def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): - """An inline role to declare grammar productions that are not in fact included - in a `productionlist` directive. + """A grammar production not included in a ``productionlist`` directive. - Useful to informally introduce a production, as part of running text + Useful to informally introduce a production, as part of running text. + + Example:: + + :production:`string` indicates a quoted string. + + You're not likely to use this role very commonly; instead, use a + `production list + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env @@ -681,6 +853,8 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte env.domaindata['std']['objects']['token', text] = env.docname, targetid return [node], [] +GrammarProductionRole.role_name = "production" + class CoqDomain(Domain): """A domain to document Coq code. @@ -703,7 +877,6 @@ class CoqDomain(Domain): # ObjType (= directive type) → (Local name, *xref-roles) 'cmd': ObjType('cmd', 'cmd'), 'cmdv': ObjType('cmdv', 'cmd'), - 'tac': ObjType('tac', 'tac'), 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), @@ -720,7 +893,6 @@ class CoqDomain(Domain): # the same role. 'cmd': VernacObject, 'cmdv': VernacVariantObject, - 'tac': TacticObject, 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, @@ -733,7 +905,6 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” 'cmd': XRefRole(warn_dangling=True), - 'tac': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), @@ -743,12 +914,8 @@ class CoqDomain(Domain): # This one is special 'index': IndexXRefRole(), # These are used for highlighting - 'notation': NotationRole, - 'gallina': GallinaRole, - 'ltac': LtacRole, 'n': NotationRole, - 'g': GallinaRole, - 'l': LtacRole, #FIXME unused? + 'g': CoqCodeRole } indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] @@ -759,7 +926,6 @@ class CoqDomain(Domain): # others, such as “version” 'objects' : { # subdomain → name → docname, objtype, targetid 'cmd': {}, - 'tac': {}, 'tacn': {}, 'opt': {}, 'thm': {}, @@ -829,11 +995,18 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: node.rawsource = '' # Prevent pygments from kicking in + elif 'coqtop-hidden' in node['classes']: + node.parent.remove(node) else: - if 'coqtop-hidden' in node['classes']: - node.parent.remove(node) - else: - node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + +COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective, + CoqdocDirective, + ExampleDirective, + InferenceDirective, + PreambleDirective] + +COQ_ADDITIONAL_ROLES = [GrammarProductionRole] def setup(app): """Register the Coq domain""" @@ -845,12 +1018,13 @@ def setup(app): # Add domain, directives, and roles app.add_domain(CoqDomain) - app.add_role("production", GrammarProductionRole) - app.add_directive("coqtop", CoqtopDirective) - app.add_directive("coqdoc", CoqdocDirective) - app.add_directive("example", ExampleDirective) - app.add_directive("inference", InferenceDirective) - app.add_directive("preamble", PreambleDirective) + + for role in COQ_ADDITIONAL_ROLES: + app.add_role(role.role_name, role) + + for directive in COQ_ADDITIONAL_DIRECTIVES: + app.add_directive(directive.directive_name, directive) + app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py new file mode 100755 index 000000000..e56882a52 --- /dev/null +++ b/doc/tools/coqrst/regen_readme.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- + +"""Rebuild sphinx/README.rst from sphinx/README.template.rst.""" + +import re +from os import sys, path + +SCRIPT_DIR = path.dirname(path.abspath(__file__)) +if __name__ == "__main__" and __package__ is None: + sys.path.append(path.dirname(SCRIPT_DIR)) + +import sphinx +from coqrst import coqdomain + +README_ROLES_MARKER = "[ROLES]" +README_OBJECTS_MARKER = "[OBJECTS]" +README_DIRECTIVES_MARKER = "[DIRECTIVES]" + +FIRST_LINE_BLANKS = re.compile("^(.*)\n *\n") +def format_docstring(template, obj, *strs): + docstring = obj.__doc__.strip() + strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),) + return template.format(*strs) + +SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") +README_PATH = path.join(SPHINX_DIR, "README.rst") +README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") + +def notation_symbol(d): + return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else "" + +def regen_readme(): + objects_docs = [format_docstring("``.. {}::``{} {}", obj, objname, notation_symbol(obj)) + for objname, obj in sorted(coqdomain.CoqDomain.directives.items())] + + roles = ([(name, cls) + for name, cls in sorted(coqdomain.CoqDomain.roles.items()) + if not isinstance(cls, (sphinx.roles.XRefRole, coqdomain.IndexXRefRole))] + + [(fn.role_name, fn) + for fn in coqdomain.COQ_ADDITIONAL_ROLES]) + roles_docs = [format_docstring("``:{}:`` {}", role, name) + for (name, role) in roles] + + directives_docs = [format_docstring("``.. {}::`` {}", d, d.directive_name) + for d in coqdomain.COQ_ADDITIONAL_DIRECTIVES] + + with open(README_TEMPLATE_PATH, encoding="utf-8") as readme: + contents = readme.read() + + with open(README_PATH, mode="w", encoding="utf-8") as readme: + readme.write(contents + .replace(README_ROLES_MARKER, "\n\n".join(roles_docs)) + .replace(README_OBJECTS_MARKER, "\n\n".join(objects_docs)) + .replace(README_DIRECTIVES_MARKER, "\n\n".join(directives_docs))) + +if __name__ == '__main__': + regen_readme() diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index efb5cb550..aeadce4c4 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -41,7 +41,9 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN'),"coqtop") + self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") + if not pexpect.utils.which(self.coqtop_bin): + raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) self.args = (args or []) + ["-boot", "-color", "on"] * color self.coqtop = None diff --git a/engine/evd.ml b/engine/evd.ml index af22de5cd..20a7c80ea 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -842,12 +842,12 @@ let universe_rigidity evd l = else UnivRigid let normalize_universe evd = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l diff --git a/engine/uState.ml b/engine/uState.ml index 6c8dbe3f4..df50bae86 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs = let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in - let normalize = normalize_univ_variable_opt_subst vars in + let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) diff --git a/engine/universes.ml b/engine/universes.ml index 938f5ad9c..a13663cba 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -605,31 +605,25 @@ let fresh_universe_context_set_instance ctx = let cst' = subst_univs_level_constraints subst cst in subst, (univs', cst') -let normalize_univ_variable ~find ~update = +let normalize_univ_variable ~find = let rec aux cur = let b = find cur in let b' = subst_univs_universe aux b in if Universe.equal b' b then b - else update cur b' + else b' in aux let normalize_univ_variable_opt_subst ectx = let find l = - match Univ.LMap.find l !ectx with + match Univ.LMap.find l ectx with | Some b -> b | None -> raise Not_found in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false - in normalize_univ_variable ~find ~update + normalize_univ_variable ~find let normalize_univ_variable_subst subst = - let find l = Univ.LMap.find l !subst in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in - normalize_univ_variable ~find ~update + let find l = Univ.LMap.find l subst in + normalize_univ_variable ~find let normalize_universe_opt_subst subst = let normlevel = normalize_univ_variable_opt_subst subst in @@ -640,13 +634,10 @@ let normalize_universe_subst subst = subst_univs_universe normlevel let normalize_opt_subst ctx = - let ectx = ref ctx in - let normalize = normalize_univ_variable_opt_subst ectx in - let () = - Univ.LMap.iter (fun u v -> - if Option.is_empty v then () - else try ignore(normalize u) with Not_found -> assert(false)) ctx - in !ectx + let normalize = normalize_universe_opt_subst ctx in + Univ.LMap.mapi (fun u -> function + | None -> None + | Some v -> Some (normalize v)) ctx type universe_opt_subst = Universe.t option universe_map @@ -655,7 +646,7 @@ let subst_univs_fn_puniverses f (c, u as cu) = if u' == u then cu else (c, u') let nf_evars_and_universes_opt_subst f subst = - let subst = normalize_univ_variable_opt_subst (ref subst) in + let subst = normalize_univ_variable_opt_subst subst in let lsubst = level_subst_of subst in let rec aux c = match kind c with @@ -975,7 +966,7 @@ let normalize_context_set g ctx us algs weak = (* Process weak constraints: when one side is flexible and the 2 universes are unrelated unify them. *) let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> - let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in let u = norm u and v = norm v in let set_to a b = (LSet.remove a ctx, @@ -994,7 +985,6 @@ let normalize_context_set g ctx us algs weak = (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = - let us = ref us in let norm = level_subst_of (normalize_univ_variable_opt_subst us) in Constraint.fold (fun (u,d,v) noneqs -> let u = norm u and v = norm v in diff --git a/engine/universes.mli b/engine/universes.mli index e6bee42bb..df2e961d6 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -184,19 +184,18 @@ val normalize_univ_variables : universe_opt_subst -> val normalize_univ_variable : find:(Level.t -> Universe.t) -> - update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> +val normalize_univ_variable_opt_subst : universe_opt_subst -> (Level.t -> Universe.t) -val normalize_univ_variable_subst : universe_subst ref -> +val normalize_univ_variable_subst : universe_subst -> (Level.t -> Universe.t) -val normalize_universe_opt_subst : universe_opt_subst ref -> +val normalize_universe_opt_subst : universe_opt_subst -> (Universe.t -> Universe.t) -val normalize_universe_subst : universe_subst ref -> +val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) (** Create a fresh global in the global environment, without side effects. diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index d5feafbf9..be2b05da8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -18,6 +18,7 @@ #include <caml/misc.h> #include <caml/mlvalues.h> #include <caml/fail.h> +#include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz) } value coq_makeaccu (value i) { - code_t q; - code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); - q = res; + CAMLparam1(i); + CAMLlocal1(res); + code_t q = coq_stat_alloc(2 * sizeof(opcode_t)); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = q; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); - return (value)res; + CAMLreturn(res); } value coq_pushpop (value i) { - code_t res; - int n; - n = Int_val(i); + CAMLparam1(i); + CAMLlocal1(res); + code_t q; + res = caml_alloc_small(1, Abstract_tag); + int n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(sizeof(opcode_t)); - *res = VALINSTR(STOP); - return (value)res; + q = coq_stat_alloc(sizeof(opcode_t)); + Code_val(res) = q; + *q = VALINSTR(STOP); + CAMLreturn(res); } else { - code_t q; - res = coq_stat_alloc(3 * sizeof(opcode_t)); - q = res; + q = coq_stat_alloc(3 * sizeof(opcode_t)); + Code_val(res) = q; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; *q = VALINSTR(STOP); - return (value)res; + CAMLreturn(res); } } value coq_is_accumulate_code(value code){ - code_t q; + code_t q = Code_val(code); int res; - q = (code_t)code; res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } @@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){ #define COPY32(dst,src) (*dst=*src) #endif /* ARCH_BIG_ENDIAN */ -value coq_tcode_of_code (value code, value size) { - code_t p, q, res; - asize_t len = (asize_t) Long_val(size); - res = coq_stat_alloc(len); - q = res; +value coq_tcode_of_code (value code) { + CAMLparam1 (code); + CAMLlocal1 (res); + code_t p, q; + asize_t len = (asize_t) caml_string_length(code); + res = caml_alloc_small(1, Abstract_tag); + q = coq_stat_alloc(len); + Code_val(res) = q; len /= sizeof(opcode_t); for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; @@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) { for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } - return (value)res; + CAMLreturn(res); } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 5c85389dd..638d6b5ab 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -26,7 +26,7 @@ void init_arity(); #define Is_instruction(pc,instr) (*pc == VALINSTR(instr)) -value coq_tcode_of_code(value code, value len); +value coq_tcode_of_code(value code); value coq_makeaccu (value i); value coq_pushpop (value i); value coq_is_accumulate_code(value code); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index cfeb0a9ee..8ac1ecc79 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,6 +16,7 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <caml/memory.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -629,7 +630,7 @@ value coq_interprete print_instr("CLOSUREREC"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfuncs, 0); + Alloc_small(accu, nfuncs, Abstract_tag); for(i = 0; i < nfuncs; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -665,7 +666,7 @@ value coq_interprete print_instr("CLOSURECOFIX"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfunc, 0); + Alloc_small(accu, nfunc, Abstract_tag); for(i = 0; i < nfunc; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -1071,12 +1072,22 @@ value coq_interprete } } *--sp = accu; - /* We create the switch zipper */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; + /* Create bytecode wrappers */ + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = typlbl; + *--sp = accu; + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = swlbl; + *--sp = accu; + /* We create the switch zipper */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + Field(accu, 2) = sp[3]; + Field(accu, 3) = sp[2]; + Field(accu, 4) = coq_env; + sp += 3; + sp[0] = accu; /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; @@ -1476,7 +1487,8 @@ value coq_interprete #endif } -value coq_push_ra(value tcode) { +value coq_push_ra(value code) { + code_t tcode = Code_val(code); print_instr("push_ra"); coq_sp -= 3; coq_sp[0] = (value) tcode; @@ -1516,8 +1528,10 @@ value coq_push_vstack(value stk, value max_stack_size) { } value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { + // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete + CAMLparam1(tcode); print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea)); + CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea))); print_instr("end coq_interprete"); } diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index b2917a55e..542a05fd2 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,6 +10,8 @@ #include <stdio.h> #include <string.h> +#include <caml/alloc.h> +#include <caml/address_class.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -46,7 +48,11 @@ value coq_static_alloc(value size) /* ML */ value accumulate_code(value unit) /* ML */ { - return (value) accumulate; + CAMLparam1(unit); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = accumulate; + CAMLreturn(res); } static void (*coq_prev_scan_roots_hook) (scanning_action); @@ -56,6 +62,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { +#ifdef NO_NAKED_POINTERS + /* The VM stack may contain C-allocated bytecode */ + if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; +#endif (*action) (*i, i); }; /* Hook */ @@ -94,8 +104,12 @@ value init_coq_vm(value unit) /* ML */ /* Initialing the interpreter */ init_coq_interpreter(); - /* Some predefined pointer code */ - accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + /* Some predefined pointer code. + * It is typically contained in accumlator blocks whose tag is 0 and thus + * scanned by the GC, so make it look like an OCaml block. */ + value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); + Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ + accumulate = (code_t) Val_hp(accu_block); *accumulate = VALINSTR(ACCUMULATE); /* Initialize GC */ diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 528babebf..e05f3fb82 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -9,6 +9,7 @@ /***********************************************************************/ #include <stdio.h> +#include <caml/memory.h> #include "coq_fix_code.h" #include "coq_instruct.h" #include "coq_memory.h" @@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){ return (value)&Field(v, Int_val(offset)); } +value coq_set_bytecode_field(value v, value i, value code) { + // No write barrier because the bytecode does not live on the OCaml heap + Field(v, Long_val(i)) = (value) Code_val(code); + return Val_unit; +} + value coq_offset_tcode(value code,value offset){ - return((value)((code_t)code + Int_val(offset))); + CAMLparam1(code); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = Code_val(code) + Int_val(offset); + CAMLreturn(res); } -value coq_int_tcode(value code, value offset) { +value coq_int_tcode(value pc, value offset) { + code_t code = Code_val(pc); return Val_int(*((code_t) code + Int_val(offset))); } + +value coq_tcode_array(value tcodes) { + CAMLparam1(tcodes); + CAMLlocal2(res, tmp); + int i; + /* Assumes that the vector of types is small. This was implicit in the + previous code which was building the type array using Alloc_small. */ + res = caml_alloc_small(Wosize_val(tcodes), Default_tag); + for (i = 0; i < Wosize_val(tcodes); i++) { + tmp = caml_alloc_small(1, Abstract_tag); + Code_val(tmp) = (code_t) Field(tcodes, i); + Store_field(res, i, tmp); + } + CAMLreturn(res); +} diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 14f4f27c0..cea09c510 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -20,7 +20,7 @@ open Mod_subst type emitcodes = String.t -external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" +external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code" (* Relocation information *) type reloc_info = @@ -82,7 +82,7 @@ let patch buff pl f = (** Order seems important here? *) let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in let buff = patch_int buff reloc in - tcode_of_code buff (Bytes.length buff) + tcode_of_code buff (* Buffering of bytecode *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 6a41efac2..7a703e653 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -59,14 +59,17 @@ let vm_global (v : values array) = (Obj.magic v : vm_global) (*******************************************) type tcode +(** A block whose first field is a C-allocated VM bytecode, encoded as char*. + This is compatible with the representation of the Coq VM closures. *) + +type tcode_array external mkAccuCode : int -> tcode = "coq_makeaccu" external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) -let fix_code v = fun_code v -let cofix_upd_code v = fun_code v +let fun_code v = (Obj.magic v : tcode) +let fix_code = fun_code +let cofix_upd_code = fun_code type vswitch = { @@ -255,6 +258,7 @@ external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" external is_accumulate : tcode -> bool = "coq_is_accumulate_code" external int_tcode : tcode -> int -> int = "coq_int_tcode" external accumulate : unit -> tcode = "accumulate_code" +external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field" let accumulate = accumulate () let whd_val : values -> whd = @@ -284,7 +288,7 @@ let whd_val : values -> whd = let obj_of_atom : atom -> Obj.t = fun a -> let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); + set_bytecode_field res 0 accumulate; Obj.set_field res 1 (Obj.repr a); res @@ -370,17 +374,20 @@ external closure_arity : vfun -> int = "coq_closure_arity" external offset : Obj.t -> int = "coq_offset" external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +external tcode_array : tcode_array -> tcode array = "coq_tcode_array" let first o = (offset_closure o (offset o)) let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) let last o = (Obj.field o (Obj.size o - 1)) -let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) -let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) +let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) let current_fix vf = - (offset (Obj.repr vf) / 2) -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) +let unsafe_fb_code fb i = + let off = (2 * i) * (Sys.word_size / 8) in + Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off)) let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 @@ -442,13 +449,12 @@ let relaccu_code i = let mk_fix_body k ndef fb = let e = Obj.dup (Obj.repr fb) in for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + set_bytecode_field e (2 * i) (relaccu_code (k + i)) done; let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in + let c = offset_tcode (unsafe_fb_code fb i) 2 in let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); + set_bytecode_field res 0 c; Obj.set_field res 1 (offset_closure e (2*i)); ((Obj.obj res) : vfun) in Array.init ndef fix_body @@ -486,7 +492,7 @@ let mk_cofix_body apply_varray k ndef vcf = Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); + set_bytecode_field self 0 accumulate; Obj.set_field self 1 (Obj.repr atom); apply_varray (Obj.obj e) [|Obj.obj self|] in Array.init ndef cofix_body diff --git a/man/coqtop.1 b/man/coqtop.1 index b1fbb3262..084adfe45 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -110,7 +110,7 @@ print Coq version and exit .TP .B \-q -skip loading of rcfile +skip loading of rcfile (resource file) if any .TP .BI \-init\-file \ filename diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index b6462c810..c949589e2 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) let id_map_try_add id x m = match id with - | Some id -> Id.Map.add id x m + | Some id -> Id.Map.add id (Lazy.force x) m | None -> m (** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a41..b4e1a1b10 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -427,7 +427,7 @@ let special_meta = (-1) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : constr; } + m_ctx : constr Lazy.t; } let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) @@ -451,7 +451,7 @@ let authorized_occ env sigma closed pat c mk_ctx = let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) - else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next) with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 3c2c73915..d19789ef4 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : EConstr.t } + m_ctx : EConstr.t Lazy.t } (** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], diff --git a/test-suite/Makefile b/test-suite/Makefile index 9d84cd5c7..2531b8c67 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -94,7 +94,7 @@ INTERACTIVE := interactive VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc + coqdoc ssr # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile @@ -158,6 +158,7 @@ summary: $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ $(call summary_dir, "STM tests", stm); \ + $(call summary_dir, "SSR tests", ssr); \ $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ @@ -261,7 +262,8 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) +ssr: $(wildcard ssr/*.v:%.v=%.v.log) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh index f303214b9..0ae7873fd 100755 --- a/test-suite/misc/coqc_dash_o.sh +++ b/test-suite/misc/coqc_dash_o.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash DOUT=misc/tmp_coqc_dash_o/ OUT=${DOUT}coqc_dash_o.vo diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out new file mode 100644 index 000000000..fa2393b91 --- /dev/null +++ b/test-suite/output/ssr_explain_match.out @@ -0,0 +1,55 @@ +File "stdin", line 12, characters 0-61: +Warning: Notation _ - _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ <= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ < _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ >= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ > _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ <= _ <= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ < _ <= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ <= _ < _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ < _ < _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ + _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ * _ was already used in scope nat_scope. +[notation-overridden,parsing] +BEGIN INSTANCES +instance: (x + y + z) matches: (x + y + z) +instance: (x + y) matches: (x + y) +instance: (x + y) matches: (x + y) +END INSTANCES +BEGIN INSTANCES +instance: (addnC (x + y) z) matches: (x + y + z) +instance: (addnC x y) matches: (x + y) +instance: (addnC x y) matches: (x + y) +END INSTANCES +BEGIN INSTANCES +instance: (addnA x y z) matches: (x + y + z) +END INSTANCES +BEGIN INSTANCES +instance: (addnA x y z) matches: (x + y + z) +instance: (addnC z (x + y)) matches: (x + y + z) +instance: (addnC y x) matches: (x + y) +instance: (addnC y x) matches: (x + y) +END INSTANCES +The command has indeed failed with message: +Ltac call to "ssrinstancesoftpat (cpattern)" failed. +Not supported diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v new file mode 100644 index 000000000..56ca24b6e --- /dev/null +++ b/test-suite/output/ssr_explain_match.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssrmatching. +Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp. + +Definition addnAC := (addnA, addnC). + +Lemma test x y z : x + y + z = x + y. + +ssrinstancesoftpat (_ + _). +ssrinstancesofruleL2R addnC. +ssrinstancesofruleR2L addnA. +ssrinstancesofruleR2L addnAC. +Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *) +Admitted. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v new file mode 100644 index 000000000..cb2c56736 --- /dev/null +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -0,0 +1,1472 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Some code from mathcomp needed in order to run ssr_* tests *) + +Require Import ssreflect ssrfun ssrbool. + +Global Set SsrOldRewriteGoalsOrder. +Global Set Asymmetric Patterns. +Global Set Bullet Behavior "None". + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(* eqtype ---------------------------------------------------------- *) + +Module Equality. + +Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y). + +Structure mixin_of T := Mixin {op : rel T; _ : axiom op}. +Notation class_of := mixin_of (only parsing). + +Section ClassDef. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Variables (T : Type) (cT : type). + +Definition class := let: Pack _ c _ := cT return class_of cT in c. + +Definition pack c := @Pack T c T. +Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c. + +End ClassDef. + +Module Exports. +Coercion sort : type >-> Sortclass. +Notation eqType := type. +Notation EqMixin := Mixin. +Notation EqType T m := (@pack T m). +Notation "[ 'eqMixin' 'of' T ]" := (class _ : mixin_of T) + (at level 0, format "[ 'eqMixin' 'of' T ]") : form_scope. +Notation "[ 'eqType' 'of' T 'for' C ]" := (@clone T C _ idfun id) + (at level 0, format "[ 'eqType' 'of' T 'for' C ]") : form_scope. +Notation "[ 'eqType' 'of' T ]" := (@clone T _ _ id id) + (at level 0, format "[ 'eqType' 'of' T ]") : form_scope. +End Exports. + +End Equality. +Export Equality.Exports. + +Definition eq_op T := Equality.op (Equality.class T). + +Lemma eqE T x : eq_op x = Equality.op (Equality.class T) x. +Proof. by []. Qed. + +Lemma eqP T : Equality.axiom (@eq_op T). +Proof. by case: T => ? []. Qed. +Arguments eqP [T x y]. + +Delimit Scope eq_scope with EQ. +Open Scope eq_scope. + +Notation "x == y" := (eq_op x y) + (at level 70, no associativity) : bool_scope. +Notation "x == y :> T" := ((x : T) == (y : T)) + (at level 70, y at next level) : bool_scope. +Notation "x != y" := (~~ (x == y)) + (at level 70, no associativity) : bool_scope. +Notation "x != y :> T" := (~~ (x == y :> T)) + (at level 70, y at next level) : bool_scope. +Notation "x =P y" := (eqP : reflect (x = y) (x == y)) + (at level 70, no associativity) : eq_scope. +Notation "x =P y :> T" := (eqP : reflect (x = y :> T) (x == y :> T)) + (at level 70, y at next level, no associativity) : eq_scope. + +Prenex Implicits eq_op eqP. + +Lemma eq_refl (T : eqType) (x : T) : x == x. Proof. exact/eqP. Qed. +Notation eqxx := eq_refl. + +Lemma eq_sym (T : eqType) (x y : T) : (x == y) = (y == x). +Proof. exact/eqP/eqP. Qed. + +Hint Resolve eq_refl eq_sym. + + +Definition eqb b := addb (~~ b). + +Lemma eqbP : Equality.axiom eqb. +Proof. by do 2!case; constructor. Qed. + +Canonical bool_eqMixin := EqMixin eqbP. +Canonical bool_eqType := Eval hnf in EqType bool bool_eqMixin. + +Section ProdEqType. + +Variable T1 T2 : eqType. + +Definition pair_eq := [rel u v : T1 * T2 | (u.1 == v.1) && (u.2 == v.2)]. + +Lemma pair_eqP : Equality.axiom pair_eq. +Proof. +move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=. +by do 2!move/eqP->. +Qed. + +Definition prod_eqMixin := EqMixin pair_eqP. +Canonical prod_eqType := Eval hnf in EqType (T1 * T2) prod_eqMixin. + +End ProdEqType. + +Section OptionEqType. + +Variable T : eqType. + +Definition opt_eq (u v : option T) : bool := + oapp (fun x => oapp (eq_op x) false v) (~~ v) u. + +Lemma opt_eqP : Equality.axiom opt_eq. +Proof. +case=> [x|] [y|] /=; by [constructor | apply: (iffP eqP) => [|[]] ->]. +Qed. + +Canonical option_eqMixin := EqMixin opt_eqP. +Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin. + +End OptionEqType. + +Notation xpred1 := (fun a1 x => x == a1). +Notation xpredU1 := (fun a1 (p : pred _) x => (x == a1) || p x). + +Section EqPred. + +Variable T : eqType. + +Definition pred1 (a1 : T) := SimplPred (xpred1 a1). +Definition predU1 (a1 : T) p := SimplPred (xpredU1 a1 p). + +End EqPred. + +Section TransferEqType. + +Variables (T : Type) (eT : eqType) (f : T -> eT). + +Lemma inj_eqAxiom : injective f -> Equality.axiom (fun x y => f x == f y). +Proof. by move=> f_inj x y; apply: (iffP eqP) => [|-> //]; apply: f_inj. Qed. + +Definition InjEqMixin f_inj := EqMixin (inj_eqAxiom f_inj). + +Definition PcanEqMixin g (fK : pcancel f g) := InjEqMixin (pcan_inj fK). + +Definition CanEqMixin g (fK : cancel f g) := InjEqMixin (can_inj fK). + +End TransferEqType. + +(* We use the module system to circumvent a silly limitation that *) +(* forbids using the same constant to coerce to different targets. *) +Module Type EqTypePredSig. +Parameter sort : eqType -> predArgType. +End EqTypePredSig. +Module MakeEqTypePred (eqmod : EqTypePredSig). +Coercion eqmod.sort : eqType >-> predArgType. +End MakeEqTypePred. +Module Export EqTypePred := MakeEqTypePred Equality. + + +Section SubType. + +Variables (T : Type) (P : pred T). + +Structure subType : Type := SubType { + sub_sort :> Type; + val : sub_sort -> T; + Sub : forall x, P x -> sub_sort; + _ : forall K (_ : forall x Px, K (@Sub x Px)) u, K u; + _ : forall x Px, val (@Sub x Px) = x +}. + +Arguments Sub [s]. +Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed. +Definition vrefl_rect := vrefl. + +Definition clone_subType U v := + fun sT & sub_sort sT -> U => + fun c Urec cK (sT' := @SubType U v c Urec cK) & phant_id sT' sT => sT'. + +Variable sT : subType. + +CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). + +Lemma SubP u : Sub_spec u. +Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. + +Lemma SubK x Px : @val sT (Sub x Px) = x. +Proof. by case: sT. Qed. + +Definition insub x := + if @idP (P x) is ReflectT Px then @Some sT (Sub x Px) else None. + +Definition insubd u0 x := odflt u0 (insub x). + +CoInductive insub_spec x : option sT -> Type := + | InsubSome u of P x & val u = x : insub_spec x (Some u) + | InsubNone of ~~ P x : insub_spec x None. + +Lemma insubP x : insub_spec x (insub x). +Proof. +by rewrite /insub; case: {-}_ / idP; [left; rewrite ?SubK | right; apply/negP]. +Qed. + +Lemma insubT x Px : insub x = Some (Sub x Px). +Admitted. + +Lemma insubF x : P x = false -> insub x = None. +Proof. by move/idP; case: insubP. Qed. + +Lemma insubN x : ~~ P x -> insub x = None. +Proof. by move/negPf/insubF. Qed. + +Lemma isSome_insub : ([eta insub] : pred T) =1 P. +Proof. by apply: fsym => x; case: insubP => // /negPf. Qed. + +Lemma insubK : ocancel insub (@val _). +Proof. by move=> x; case: insubP. Qed. + +Lemma valP (u : sT) : P (val u). +Proof. by case/SubP: u => x Px; rewrite SubK. Qed. + +Lemma valK : pcancel (@val _) insub. +Proof. by case/SubP=> x Px; rewrite SubK; apply: insubT. Qed. + +Lemma val_inj : injective (@val sT). +Proof. exact: pcan_inj valK. Qed. + +Lemma valKd u0 : cancel (@val _) (insubd u0). +Proof. by move=> u; rewrite /insubd valK. Qed. + +Lemma val_insubd u0 x : val (insubd u0 x) = if P x then x else val u0. +Proof. by rewrite /insubd; case: insubP => [u -> | /negPf->]. Qed. + +Lemma insubdK u0 : {in P, cancel (insubd u0) (@val _)}. +Proof. by move=> x Px; rewrite /= val_insubd [P x]Px. Qed. + +Definition insub_eq x := + let Some_sub Px := Some (Sub x Px : sT) in + let None_sub _ := None in + (if P x as Px return P x = Px -> _ then Some_sub else None_sub) (erefl _). + +Lemma insub_eqE : insub_eq =1 insub. +Proof. +rewrite /insub_eq /insub => x; case: {2 3}_ / idP (erefl _) => // Px Px'. +by congr (Some _); apply: val_inj; rewrite !SubK. +Qed. + +End SubType. + +Arguments SubType [T P]. +Arguments Sub [T P s]. +Arguments vrefl [T P]. +Arguments vrefl_rect [T P]. +Arguments clone_subType [T P] U v [sT] _ [c Urec cK]. +Arguments insub [T P sT]. +Arguments insubT [T] P [sT x]. +Arguments val_inj [T P sT]. +Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj. + +Local Notation inlined_sub_rect := + (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). + +Local Notation inlined_new_rect := + (fun K K_S u => let (x) as u return K u := u in K_S x). + +Notation "[ 'subType' 'for' v ]" := (SubType _ v _ inlined_sub_rect vrefl_rect) + (at level 0, only parsing) : form_scope. + +Notation "[ 'sub' 'Type' 'for' v ]" := (SubType _ v _ _ vrefl_rect) + (at level 0, format "[ 'sub' 'Type' 'for' v ]") : form_scope. + +Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl) + (at level 0, format "[ 'subType' 'for' v 'by' rec ]") : form_scope. + +Notation "[ 'subType' 'of' U 'for' v ]" := (clone_subType U v id idfun) + (at level 0, format "[ 'subType' 'of' U 'for' v ]") : form_scope. + +(* +Notation "[ 'subType' 'for' v ]" := (clone_subType _ v id idfun) + (at level 0, format "[ 'subType' 'for' v ]") : form_scope. +*) +Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id) + (at level 0, format "[ 'subType' 'of' U ]") : form_scope. + +Definition NewType T U v c Urec := + let Urec' P IH := Urec P (fun x : T => IH x isT : P _) in + SubType U v (fun x _ => c x) Urec'. +Arguments NewType [T U]. + +Notation "[ 'newType' 'for' v ]" := (NewType v _ inlined_new_rect vrefl_rect) + (at level 0, only parsing) : form_scope. + +Notation "[ 'new' 'Type' 'for' v ]" := (NewType v _ _ vrefl_rect) + (at level 0, format "[ 'new' 'Type' 'for' v ]") : form_scope. + +Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl) + (at level 0, format "[ 'newType' 'for' v 'by' rec ]") : form_scope. + +Definition innew T nT x := @Sub T predT nT x (erefl true). +Arguments innew [T nT]. +Prenex Implicits innew. + +Lemma innew_val T nT : cancel val (@innew T nT). +Proof. by move=> u; apply: val_inj; apply: SubK. Qed. + +(* Prenex Implicits and renaming. *) +Notation sval := (@proj1_sig _ _). +Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'"). + +Section SubEqType. + +Variables (T : eqType) (P : pred T) (sT : subType P). + +Local Notation ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)). +Lemma val_eqP : ev_ax sT val. Proof. exact: inj_eqAxiom val_inj. Qed. + +Definition sub_eqMixin := EqMixin val_eqP. +Canonical sub_eqType := Eval hnf in EqType sT sub_eqMixin. + +Definition SubEqMixin := + (let: SubType _ v _ _ _ as sT' := sT + return ev_ax sT' val -> Equality.class_of sT' in + fun vP : ev_ax _ v => EqMixin vP + ) val_eqP. + +Lemma val_eqE (u v : sT) : (val u == val v) = (u == v). +Proof. by []. Qed. + +End SubEqType. + +Arguments val_eqP [T P sT x y]. +Prenex Implicits val_eqP. + +Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) + (at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope. + +(* ssrnat ---------------------------------------------------------- *) + +Notation succn := Datatypes.S. +Notation predn := Peano.pred. + +Notation "n .+1" := (succn n) (at level 2, left associativity, + format "n .+1") : nat_scope. +Notation "n .+2" := n.+1.+1 (at level 2, left associativity, + format "n .+2") : nat_scope. +Notation "n .+3" := n.+2.+1 (at level 2, left associativity, + format "n .+3") : nat_scope. +Notation "n .+4" := n.+2.+2 (at level 2, left associativity, + format "n .+4") : nat_scope. + +Notation "n .-1" := (predn n) (at level 2, left associativity, + format "n .-1") : nat_scope. +Notation "n .-2" := n.-1.-1 (at level 2, left associativity, + format "n .-2") : nat_scope. + +Fixpoint eqn m n {struct m} := + match m, n with + | 0, 0 => true + | m'.+1, n'.+1 => eqn m' n' + | _, _ => false + end. + +Lemma eqnP : Equality.axiom eqn. +Proof. +move=> n m; apply: (iffP idP) => [|<-]; last by elim n. +by elim: n m => [|n IHn] [|m] //= /IHn->. +Qed. + +Canonical nat_eqMixin := EqMixin eqnP. +Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. + +Arguments eqnP [x y]. +Prenex Implicits eqnP. + +Coercion nat_of_bool (b : bool) := if b then 1 else 0. + +Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false. + +Lemma oddb (b : bool) : odd b = b. Proof. by case: b. Qed. + +Definition subn_rec := minus. +Notation "m - n" := (subn_rec m n) : nat_rec_scope. + +Definition subn := nosimpl subn_rec. +Notation "m - n" := (subn m n) : nat_scope. + +Definition leq m n := m - n == 0. + +Notation "m <= n" := (leq m n) : nat_scope. +Notation "m < n" := (m.+1 <= n) : nat_scope. +Notation "m >= n" := (n <= m) (only parsing) : nat_scope. +Notation "m > n" := (n < m) (only parsing) : nat_scope. + + +Notation "m <= n <= p" := ((m <= n) && (n <= p)) : nat_scope. +Notation "m < n <= p" := ((m < n) && (n <= p)) : nat_scope. +Notation "m <= n < p" := ((m <= n) && (n < p)) : nat_scope. +Notation "m < n < p" := ((m < n) && (n < p)) : nat_scope. + +Open Scope nat_scope. + + +Lemma ltnS m n : (m < n.+1) = (m <= n). Proof. by []. Qed. +Lemma leq0n n : 0 <= n. Proof. by []. Qed. +Lemma ltn0Sn n : 0 < n.+1. Proof. by []. Qed. +Lemma ltn0 n : n < 0 = false. Proof. by []. Qed. +Lemma leqnn n : n <= n. Proof. by elim: n. Qed. +Hint Resolve leqnn. +Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed. + +Lemma leq_trans n m p : m <= n -> n <= p -> m <= p. +Admitted. +Lemma leqW m n : m <= n -> m <= n.+1. +Admitted. +Hint Resolve leqnSn. +Lemma ltnW m n : m < n -> m <= n. +Proof. exact: leq_trans. Qed. +Hint Resolve ltnW. + +Definition addn_rec := plus. +Notation "m + n" := (addn_rec m n) : nat_rec_scope. + +Definition addn := nosimpl addn_rec. +Notation "m + n" := (addn m n) : nat_scope. + +Lemma addn0 : right_id 0 addn. Proof. by move=> n; apply/eqP; elim: n. Qed. +Lemma add0n : left_id 0 addn. Proof. by []. Qed. +Lemma addSn m n : m.+1 + n = (m + n).+1. Proof. by []. Qed. +Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by elim: m. Qed. + +Lemma addnCA : left_commutative addn. +Proof. by move=> m n p; elim: m => //= m; rewrite addnS => <-. Qed. + +Lemma addnC : commutative addn. +Proof. by move=> m n; rewrite -{1}[n]addn0 addnCA addn0. Qed. + +Lemma addnA : associative addn. +Proof. by move=> m n p; rewrite (addnC n) addnCA addnC. Qed. + +Lemma subnK m n : m <= n -> (n - m) + m = n. +Admitted. + + +Definition muln_rec := mult. +Notation "m * n" := (muln_rec m n) : nat_rec_scope. + +Definition muln := nosimpl muln_rec. +Notation "m * n" := (muln m n) : nat_scope. + +Lemma mul0n : left_zero 0 muln. Proof. by []. Qed. +Lemma muln0 : right_zero 0 muln. Proof. by elim. Qed. +Lemma mul1n : left_id 1 muln. Proof. exact: addn0. Qed. + +Lemma mulSn m n : m.+1 * n = n + m * n. Proof. by []. Qed. +Lemma mulSnr m n : m.+1 * n = m * n + n. Proof. exact: addnC. Qed. + +Lemma mulnS m n : m * n.+1 = m + m * n. +Proof. by elim: m => // m; rewrite !mulSn !addSn addnCA => ->. Qed. + +Lemma mulnSr m n : m * n.+1 = m * n + m. +Proof. by rewrite addnC mulnS. Qed. + +Lemma muln1 : right_id 1 muln. +Proof. by move=> n; rewrite mulnSr muln0. Qed. + +Lemma mulnC : commutative muln. +Proof. +by move=> m n; elim: m => [|m]; rewrite (muln0, mulnS) // mulSn => ->. +Qed. + +Lemma mulnDl : left_distributive muln addn. +Proof. by move=> m1 m2 n; elim: m1 => //= m1 IHm; rewrite -addnA -IHm. Qed. + +Lemma mulnDr : right_distributive muln addn. +Proof. by move=> m n1 n2; rewrite !(mulnC m) mulnDl. Qed. + +Lemma mulnA : associative muln. +Proof. by move=> m n p; elim: m => //= m; rewrite mulSn mulnDl => ->. Qed. + +Lemma mulnCA : left_commutative muln. +Proof. by move=> m n1 n2; rewrite !mulnA (mulnC m). Qed. + +Lemma mulnAC : right_commutative muln. +Proof. by move=> m n p; rewrite -!mulnA (mulnC n). Qed. + +Lemma mulnACA : interchange muln muln. +Proof. by move=> m n p q; rewrite -!mulnA (mulnCA n). Qed. + +(* seq ------------------------------------------------------------- *) + +Delimit Scope seq_scope with SEQ. +Open Scope seq_scope. + +(* Inductive seq (T : Type) : Type := Nil | Cons of T & seq T. *) +Notation seq := list. +Prenex Implicits cons. +Notation Cons T := (@cons T) (only parsing). +Notation Nil T := (@nil T) (only parsing). + +Bind Scope seq_scope with list. +Arguments cons _%type _ _%SEQ. + +(* As :: and ++ are (improperly) declared in Init.datatypes, we only rebind *) +(* them here. *) +Infix "::" := cons : seq_scope. + +(* GG - this triggers a camlp4 warning, as if this Notation had been Reserved *) +Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope. + +Notation "[ :: x1 ]" := (x1 :: [::]) + (at level 0, format "[ :: x1 ]") : seq_scope. + +Notation "[ :: x & s ]" := (x :: s) (at level 0, only parsing) : seq_scope. + +Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..) + (at level 0, format + "'[hv' [ :: '[' x1 , '/' x2 , '/' .. , '/' xn ']' '/ ' & s ] ']'" + ) : seq_scope. + +Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: .. [:: xn] ..) + (at level 0, format "[ :: '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]" + ) : seq_scope. + +Section Sequences. + +Variable n0 : nat. (* numerical parameter for take, drop et al *) +Variable T : Type. (* must come before the implicit Type *) +Variable x0 : T. (* default for head/nth *) + +Implicit Types x y z : T. +Implicit Types m n : nat. +Implicit Type s : seq T. + +Fixpoint size s := if s is _ :: s' then (size s').+1 else 0. + +Fixpoint cat s1 s2 := if s1 is x :: s1' then x :: s1' ++ s2 else s2 +where "s1 ++ s2" := (cat s1 s2) : seq_scope. + +Lemma cat0s s : [::] ++ s = s. Proof. by []. Qed. + +Lemma cats0 s : s ++ [::] = s. +Proof. by elim: s => //= x s ->. Qed. + +Lemma catA s1 s2 s3 : s1 ++ s2 ++ s3 = (s1 ++ s2) ++ s3. +Proof. by elim: s1 => //= x s1 ->. Qed. + +Fixpoint nth s n {struct n} := + if s is x :: s' then if n is n'.+1 then @nth s' n' else x else x0. + +Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z]. + +CoInductive last_spec : seq T -> Type := + | LastNil : last_spec [::] + | LastRcons s x : last_spec (rcons s x). + +Lemma lastP s : last_spec s. +Proof using. Admitted. + +Lemma last_ind P : + P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s. +Proof using. Admitted. + + +Section Map. + +Variables (T2 : Type) (f : T -> T2). + +Fixpoint map s := if s is x :: s' then f x :: map s' else [::]. + +End Map. + +Section SeqFind. + +Variable a : pred T. + +Fixpoint count s := if s is x :: s' then a x + count s' else 0. + +Fixpoint filter s := + if s is x :: s' then if a x then x :: filter s' else filter s' else [::]. + +End SeqFind. + +End Sequences. + +Infix "++" := cat : seq_scope. + +Notation count_mem x := (count (pred_of_simpl (pred1 x))). + +Section EqSeq. + +Variables (n0 : nat) (T : eqType) (x0 : T). +Local Notation nth := (nth x0). +Implicit Type s : seq T. +Implicit Types x y z : T. + +Fixpoint eqseq s1 s2 {struct s2} := + match s1, s2 with + | [::], [::] => true + | x1 :: s1', x2 :: s2' => (x1 == x2) && eqseq s1' s2' + | _, _ => false + end. + +Lemma eqseqP : Equality.axiom eqseq. +Proof. +move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl]. +case: (x1 =P x2) => [<-|neqx]; last by right; case. +by apply: (iffP (IHs s2)) => [<-|[]]. +Qed. + +Canonical seq_eqMixin := EqMixin eqseqP. +Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin. + +Fixpoint mem_seq (s : seq T) := + if s is y :: s' then xpredU1 y (mem_seq s') else xpred0. + +Definition eqseq_class := seq T. +Identity Coercion seq_of_eqseq : eqseq_class >-> seq. +Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s]. + +Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq. + +Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true. + +End EqSeq. + +Definition bitseq := seq bool. +Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. +Canonical bitseq_predType := Eval hnf in [predType of bitseq]. + +Section Pmap. + +Variables (aT rT : Type) (f : aT -> option rT) (g : rT -> aT). + +Fixpoint pmap s := + if s is x :: s' then let r := pmap s' in oapp (cons^~ r) r (f x) else [::]. + +End Pmap. + +Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::]. + +Section FoldRight. + +Variables (T : Type) (R : Type) (f : T -> R -> R) (z0 : R). + +Fixpoint foldr s := if s is x :: s' then f x (foldr s') else z0. + +End FoldRight. + +Lemma mem_iota m n i : (i \in iota m n) = (m <= i) && (i < m + n). +Admitted. + + +(* choice ------------------------------------------------------------- *) + +Module Choice. + +Section ClassDef. + +Record mixin_of T := Mixin { + find : pred T -> nat -> option T; + _ : forall P n x, find P n = Some x -> P x; + _ : forall P : pred T, (exists x, P x) -> exists n, find P n; + _ : forall P Q : pred T, P =1 Q -> find P =1 find Q +}. + +Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}. +Local Coercion base : class_of >-> Equality.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Variables (T : Type) (cT : type). +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c T. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition pack m := + fun b bT & phant_id (Equality.class bT) b => Pack (@Class T b m) T. + +(* Inheritance *) +Definition eqType := @Equality.Pack cT xclass xT. + +End ClassDef. + +Module Import Exports. +Coercion base : class_of >-> Equality.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Notation choiceType := type. +Notation choiceMixin := mixin_of. +Notation ChoiceType T m := (@pack T m _ _ id). +Notation "[ 'choiceType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) + (at level 0, format "[ 'choiceType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'choiceType' 'of' T ]" := (@clone T _ _ id) + (at level 0, format "[ 'choiceType' 'of' T ]") : form_scope. + +End Exports. + +End Choice. +Export Choice.Exports. + +Section ChoiceTheory. + +Variable T : choiceType. + +Section CanChoice. + +Variables (sT : Type) (f : sT -> T). + +Lemma PcanChoiceMixin f' : pcancel f f' -> choiceMixin sT. +Admitted. + +Definition CanChoiceMixin f' (fK : cancel f f') := + PcanChoiceMixin (can_pcan fK). + +End CanChoice. + +Section SubChoice. + +Variables (P : pred T) (sT : subType P). + +Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT). +Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin. +Canonical sub_choiceType := Choice.Pack sub_choiceClass sT. + +End SubChoice. + + +Fact seq_choiceMixin : choiceMixin (seq T). +Admitted. +Canonical seq_choiceType := Eval hnf in ChoiceType (seq T) seq_choiceMixin. +End ChoiceTheory. + +Fact nat_choiceMixin : choiceMixin nat. +Proof. +pose f := [fun (P : pred nat) n => if P n then Some n else None]. +exists f => [P n m | P [n Pn] | P Q eqPQ n] /=; last by rewrite eqPQ. + by case: ifP => // Pn [<-]. +by exists n; rewrite Pn. +Qed. +Canonical nat_choiceType := Eval hnf in ChoiceType nat nat_choiceMixin. + +Definition bool_choiceMixin := CanChoiceMixin oddb. +Canonical bool_choiceType := Eval hnf in ChoiceType bool bool_choiceMixin. +Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq]. + + +Notation "[ 'choiceMixin' 'of' T 'by' <: ]" := + (sub_choiceMixin _ : choiceMixin T) + (at level 0, format "[ 'choiceMixin' 'of' T 'by' <: ]") : form_scope. + + + + +Module Countable. + +Record mixin_of (T : Type) : Type := Mixin { + pickle : T -> nat; + unpickle : nat -> option T; + pickleK : pcancel pickle unpickle +}. + +Definition EqMixin T m := PcanEqMixin (@pickleK T m). +Definition ChoiceMixin T m := PcanChoiceMixin (@pickleK T m). + +Section ClassDef. + +Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }. +Local Coercion base : class_of >-> Choice.class_of. + +Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Variables (T : Type) (cT : type). +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c T. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition pack m := + fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T. + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> Choice.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Notation countType := type. +Notation CountType T m := (@pack T m _ _ id). +Notation CountMixin := Mixin. +Notation CountChoiceMixin := ChoiceMixin. +Notation "[ 'countType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) + (at level 0, format "[ 'countType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'countType' 'of' T ]" := (@clone T _ _ id) + (at level 0, format "[ 'countType' 'of' T ]") : form_scope. + +End Exports. + +End Countable. +Export Countable.Exports. + +Definition unpickle T := Countable.unpickle (Countable.class T). +Definition pickle T := Countable.pickle (Countable.class T). +Arguments unpickle [T]. +Prenex Implicits pickle unpickle. + +Section CountableTheory. + +Variable T : countType. + +Lemma pickleK : @pcancel nat T pickle unpickle. +Proof. exact: Countable.pickleK. Qed. + +Definition pickle_inv n := + obind (fun x : T => if pickle x == n then Some x else None) (unpickle n). + +Lemma pickle_invK : ocancel pickle_inv pickle. +Proof. +by rewrite /pickle_inv => n; case def_x: (unpickle n) => //= [x]; case: eqP. +Qed. + +Lemma pickleK_inv : pcancel pickle pickle_inv. +Proof. by rewrite /pickle_inv => x; rewrite pickleK /= eqxx. Qed. + +Lemma pcan_pickleK sT f f' : + @pcancel T sT f f' -> pcancel (pickle \o f) (pcomp f' unpickle). +Proof. by move=> fK x; rewrite /pcomp pickleK /= fK. Qed. + +Definition PcanCountMixin sT f f' (fK : pcancel f f') := + @CountMixin sT _ _ (pcan_pickleK fK). + +Definition CanCountMixin sT f f' (fK : cancel f f') := + @PcanCountMixin sT _ _ (can_pcan fK). + +Definition sub_countMixin P sT := PcanCountMixin (@valK T P sT). + +End CountableTheory. +Notation "[ 'countMixin' 'of' T 'by' <: ]" := + (sub_countMixin _ : Countable.mixin_of T) + (at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope. + +Section SubCountType. + +Variables (T : choiceType) (P : pred T). +Import Countable. + +Structure subCountType : Type := + SubCountType {subCount_sort :> subType P; _ : mixin_of subCount_sort}. + +Coercion sub_countType (sT : subCountType) := + Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id. +Canonical sub_countType. + +Definition pack_subCountType U := + fun sT cT & sub_sort sT * sort cT -> U * U => + fun b m & phant_id (Class b m) (class cT) => @SubCountType sT m. + +End SubCountType. + +(* This assumes that T has both countType and subType structures. *) +Notation "[ 'subCountType' 'of' T ]" := + (@pack_subCountType _ _ T _ _ id _ _ id) + (at level 0, format "[ 'subCountType' 'of' T ]") : form_scope. + +Lemma nat_pickleK : pcancel id (@Some nat). Proof. by []. Qed. +Definition nat_countMixin := CountMixin nat_pickleK. +Canonical nat_countType := Eval hnf in CountType nat nat_countMixin. + +(* fintype --------------------------------------------------------- *) + +Module Finite. + +Section RawMixin. + +Variable T : eqType. + +Definition axiom e := forall x : T, count_mem x e = 1. + +Lemma uniq_enumP e : uniq e -> e =i T -> axiom e. +Admitted. + +Record mixin_of := Mixin { + mixin_base : Countable.mixin_of T; + mixin_enum : seq T; + _ : axiom mixin_enum +}. + +End RawMixin. + +Section Mixins. + +Variable T : countType. + +Definition EnumMixin := + let: Countable.Pack _ (Countable.Class _ m) _ as cT := T + return forall e : seq cT, axiom e -> mixin_of cT in + @Mixin (EqType _ _) m. + +Definition UniqMixin e Ue eT := @EnumMixin e (uniq_enumP Ue eT). + +Variable n : nat. + +End Mixins. + +Section ClassDef. + +Record class_of T := Class { + base : Choice.class_of T; + mixin : mixin_of (Equality.Pack base T) +}. +Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)). +Local Coercion base : class_of >-> Choice.class_of. + +Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Variables (T : Type) (cT : type). +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c T. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition pack b0 (m0 : mixin_of (EqType T b0)) := + fun bT b & phant_id (Choice.class bT) b => + fun m & phant_id m0 m => Pack (@Class T b m) T. + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (base2 xclass) xT. + +End ClassDef. + +Module Import Exports. +Coercion mixin_base : mixin_of >-> Countable.mixin_of. +Coercion base : class_of >-> Choice.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion base2 : class_of >-> Countable.class_of. +Coercion sort : type >-> Sortclass. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Notation finType := type. +Notation FinType T m := (@pack T _ m _ _ id _ id). +Notation FinMixin := EnumMixin. +Notation UniqFinMixin := UniqMixin. +Notation "[ 'finType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) + (at level 0, format "[ 'finType' 'of' T 'for' cT ]") : form_scope. +Notation "[ 'finType' 'of' T ]" := (@clone T _ _ id) + (at level 0, format "[ 'finType' 'of' T ]") : form_scope. +End Exports. + +Module Type EnumSig. +Parameter enum : forall cT : type, seq cT. +Axiom enumDef : enum = fun cT => mixin_enum (class cT). +End EnumSig. + +Module EnumDef : EnumSig. +Definition enum cT := mixin_enum (class cT). +Definition enumDef := erefl enum. +End EnumDef. + +Notation enum := EnumDef.enum. + +End Finite. +Export Finite.Exports. + +Section SubFinType. + +Variables (T : choiceType) (P : pred T). +Import Finite. + +Structure subFinType := SubFinType { + subFin_sort :> subType P; + _ : mixin_of (sub_eqType subFin_sort) +}. + +Definition pack_subFinType U := + fun cT b m & phant_id (class cT) (@Class U b m) => + fun sT m' & phant_id m' m => @SubFinType sT m'. + +Implicit Type sT : subFinType. + +Definition subFin_mixin sT := + let: SubFinType _ m := sT return mixin_of (sub_eqType sT) in m. + +Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT). +Canonical subFinType_subCountType. + +Coercion subFinType_finType sT := + Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)) sT. +Canonical subFinType_finType. + +Definition enum_mem T (mA : mem_pred _) := filter mA (Finite.enum T). +Definition image_mem T T' f mA : seq T' := map f (@enum_mem T mA). +Definition codom T T' f := @image_mem T T' f (mem T). + +Lemma codom_val sT x : (x \in codom (val : sT -> T)) = P x. +Admitted. + +End SubFinType. + + +(* This assumes that T has both finType and subCountType structures. *) +Notation "[ 'subFinType' 'of' T ]" := (@pack_subFinType _ _ T _ _ _ id _ _ id) + (at level 0, format "[ 'subFinType' 'of' T ]") : form_scope. + + + +Section OrdinalSub. + +Variable n : nat. + +Inductive ordinal : predArgType := Ordinal m of m < n. + +Coercion nat_of_ord i := let: Ordinal m _ := i in m. + +Canonical ordinal_subType := [subType for nat_of_ord]. +Definition ordinal_eqMixin := Eval hnf in [eqMixin of ordinal by <:]. +Canonical ordinal_eqType := Eval hnf in EqType ordinal ordinal_eqMixin. +Definition ordinal_choiceMixin := [choiceMixin of ordinal by <:]. +Canonical ordinal_choiceType := + Eval hnf in ChoiceType ordinal ordinal_choiceMixin. +Definition ordinal_countMixin := [countMixin of ordinal by <:]. +Canonical ordinal_countType := Eval hnf in CountType ordinal ordinal_countMixin. +Canonical ordinal_subCountType := [subCountType of ordinal]. + +Lemma ltn_ord (i : ordinal) : i < n. Proof. exact: valP i. Qed. + +Lemma ord_inj : injective nat_of_ord. Proof. exact: val_inj. Qed. + +Definition ord_enum : seq ordinal := pmap insub (iota 0 n). + +Lemma val_ord_enum : map val ord_enum = iota 0 n. +Admitted. + +Lemma ord_enum_uniq : uniq ord_enum. +Admitted. + +Lemma mem_ord_enum i : i \in ord_enum. +Admitted. + +Definition ordinal_finMixin := + Eval hnf in UniqFinMixin ord_enum_uniq mem_ord_enum. +Canonical ordinal_finType := Eval hnf in FinType ordinal ordinal_finMixin. +Canonical ordinal_subFinType := Eval hnf in [subFinType of ordinal]. + +End OrdinalSub. + +Notation "''I_' n" := (ordinal n) + (at level 8, n at level 2, format "''I_' n"). + +(* bigop ----------------------------------------------------------------- *) + +Reserved Notation "\big [ op / idx ]_ i F" + (at level 36, F at level 36, op, idx at level 10, i at level 0, + right associativity, + format "'[' \big [ op / idx ]_ i '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i <- r | P ) F" + (at level 36, F at level 36, op, idx at level 10, i, r at level 50, + format "'[' \big [ op / idx ]_ ( i <- r | P ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i <- r ) F" + (at level 36, F at level 36, op, idx at level 10, i, r at level 50, + format "'[' \big [ op / idx ]_ ( i <- r ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" + (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). +Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F" + (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i | P ) F" + (at level 36, F at level 36, op, idx at level 10, i at level 50, + format "'[' \big [ op / idx ]_ ( i | P ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i : t | P ) F" + (at level 36, F at level 36, op, idx at level 10, i at level 50, + format "'[' \big [ op / idx ]_ ( i : t | P ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i : t ) F" + (at level 36, F at level 36, op, idx at level 10, i at level 50, + format "'[' \big [ op / idx ]_ ( i : t ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i < n | P ) F" + (at level 36, F at level 36, op, idx at level 10, i, n at level 50, + format "'[' \big [ op / idx ]_ ( i < n | P ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i < n ) F" + (at level 36, F at level 36, op, idx at level 10, i, n at level 50, + format "'[' \big [ op / idx ]_ ( i < n ) F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i 'in' A | P ) F" + (at level 36, F at level 36, op, idx at level 10, i, A at level 50, + format "'[' \big [ op / idx ]_ ( i 'in' A | P ) '/ ' F ']'"). +Reserved Notation "\big [ op / idx ]_ ( i 'in' A ) F" + (at level 36, F at level 36, op, idx at level 10, i, A at level 50, + format "'[' \big [ op / idx ]_ ( i 'in' A ) '/ ' F ']'"). + +Module Monoid. + +Section Definitions. +Variables (T : Type) (idm : T). + +Structure law := Law { + operator : T -> T -> T; + _ : associative operator; + _ : left_id idm operator; + _ : right_id idm operator +}. +Local Coercion operator : law >-> Funclass. + +Structure com_law := ComLaw { + com_operator : law; + _ : commutative com_operator +}. +Local Coercion com_operator : com_law >-> law. + +Structure mul_law := MulLaw { + mul_operator : T -> T -> T; + _ : left_zero idm mul_operator; + _ : right_zero idm mul_operator +}. +Local Coercion mul_operator : mul_law >-> Funclass. + +Structure add_law (mul : T -> T -> T) := AddLaw { + add_operator : com_law; + _ : left_distributive mul add_operator; + _ : right_distributive mul add_operator +}. +Local Coercion add_operator : add_law >-> com_law. + +Let op_id (op1 op2 : T -> T -> T) := phant_id op1 op2. + +Definition clone_law op := + fun (opL : law) & op_id opL op => + fun opmA op1m opm1 (opL' := @Law op opmA op1m opm1) + & phant_id opL' opL => opL'. + +Definition clone_com_law op := + fun (opL : law) (opC : com_law) & op_id opL op & op_id opC op => + fun opmC (opC' := @ComLaw opL opmC) & phant_id opC' opC => opC'. + +Definition clone_mul_law op := + fun (opM : mul_law) & op_id opM op => + fun op0m opm0 (opM' := @MulLaw op op0m opm0) & phant_id opM' opM => opM'. + +Definition clone_add_law mop aop := + fun (opC : com_law) (opA : add_law mop) & op_id opC aop & op_id opA aop => + fun mopDm mopmD (opA' := @AddLaw mop opC mopDm mopmD) + & phant_id opA' opA => opA'. + +End Definitions. + +Module Import Exports. +Coercion operator : law >-> Funclass. +Coercion com_operator : com_law >-> law. +Coercion mul_operator : mul_law >-> Funclass. +Coercion add_operator : add_law >-> com_law. +Notation "[ 'law' 'of' f ]" := (@clone_law _ _ f _ id _ _ _ id) + (at level 0, format"[ 'law' 'of' f ]") : form_scope. +Notation "[ 'com_law' 'of' f ]" := (@clone_com_law _ _ f _ _ id id _ id) + (at level 0, format "[ 'com_law' 'of' f ]") : form_scope. +Notation "[ 'mul_law' 'of' f ]" := (@clone_mul_law _ _ f _ id _ _ id) + (at level 0, format"[ 'mul_law' 'of' f ]") : form_scope. +Notation "[ 'add_law' m 'of' a ]" := (@clone_add_law _ _ m a _ _ id id _ _ id) + (at level 0, format "[ 'add_law' m 'of' a ]") : form_scope. +End Exports. + +Section CommutativeAxioms. + +Variable (T : Type) (zero one : T) (mul add : T -> T -> T) (inv : T -> T). +Hypothesis mulC : commutative mul. + +Lemma mulC_id : left_id one mul -> right_id one mul. +Proof. by move=> mul1x x; rewrite mulC. Qed. + +Lemma mulC_zero : left_zero zero mul -> right_zero zero mul. +Proof. by move=> mul0x x; rewrite mulC. Qed. + +Lemma mulC_dist : left_distributive mul add -> right_distributive mul add. +Proof. by move=> mul_addl x y z; rewrite !(mulC x). Qed. + +End CommutativeAxioms. +Module Theory. + +Section Theory. +Variables (T : Type) (idm : T). + +Section Plain. +Variable mul : law idm. +Lemma mul1m : left_id idm mul. Proof. by case mul. Qed. +Lemma mulm1 : right_id idm mul. Proof. by case mul. Qed. +Lemma mulmA : associative mul. Proof. by case mul. Qed. +(*Lemma iteropE n x : iterop n mul x idm = iter n (mul x) idm.*) + +End Plain. + +Section Commutative. +Variable mul : com_law idm. +Lemma mulmC : commutative mul. Proof. by case mul. Qed. +Lemma mulmCA : left_commutative mul. +Proof. by move=> x y z; rewrite !mulmA (mulmC x). Qed. +Lemma mulmAC : right_commutative mul. +Proof. by move=> x y z; rewrite -!mulmA (mulmC y). Qed. +Lemma mulmACA : interchange mul mul. +Proof. by move=> x y z t; rewrite -!mulmA (mulmCA y). Qed. +End Commutative. + +Section Mul. +Variable mul : mul_law idm. +Lemma mul0m : left_zero idm mul. Proof. by case mul. Qed. +Lemma mulm0 : right_zero idm mul. Proof. by case mul. Qed. +End Mul. + +Section Add. +Variables (mul : T -> T -> T) (add : add_law idm mul). +Lemma addmA : associative add. Proof. exact: mulmA. Qed. +Lemma addmC : commutative add. Proof. exact: mulmC. Qed. +Lemma addmCA : left_commutative add. Proof. exact: mulmCA. Qed. +Lemma addmAC : right_commutative add. Proof. exact: mulmAC. Qed. +Lemma add0m : left_id idm add. Proof. exact: mul1m. Qed. +Lemma addm0 : right_id idm add. Proof. exact: mulm1. Qed. +Lemma mulm_addl : left_distributive mul add. Proof. by case add. Qed. +Lemma mulm_addr : right_distributive mul add. Proof. by case add. Qed. +End Add. + +Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA). + +End Theory. + +End Theory. +Include Theory. + +End Monoid. +Export Monoid.Exports. + +Section PervasiveMonoids. + +Import Monoid. + +Canonical andb_monoid := Law andbA andTb andbT. +Canonical andb_comoid := ComLaw andbC. + +Canonical andb_muloid := MulLaw andFb andbF. +Canonical orb_monoid := Law orbA orFb orbF. +Canonical orb_comoid := ComLaw orbC. +Canonical orb_muloid := MulLaw orTb orbT. +Canonical addb_monoid := Law addbA addFb addbF. +Canonical addb_comoid := ComLaw addbC. +Canonical orb_addoid := AddLaw andb_orl andb_orr. +Canonical andb_addoid := AddLaw orb_andl orb_andr. +Canonical addb_addoid := AddLaw andb_addl andb_addr. + +Canonical addn_monoid := Law addnA add0n addn0. +Canonical addn_comoid := ComLaw addnC. +Canonical muln_monoid := Law mulnA mul1n muln1. +Canonical muln_comoid := ComLaw mulnC. +Canonical muln_muloid := MulLaw mul0n muln0. +Canonical addn_addoid := AddLaw mulnDl mulnDr. + +Canonical cat_monoid T := Law (@catA T) (@cat0s T) (@cats0 T). + +End PervasiveMonoids. +Delimit Scope big_scope with BIG. +Open Scope big_scope. + +(* The bigbody wrapper is a workaround for a quirk of the Coq pretty-printer, *) +(* which would fail to redisplay the \big notation when the <general_term> or *) +(* <condition> do not depend on the bound index. The BigBody constructor *) +(* packages both in in a term in which i occurs; it also depends on the *) +(* iterated <op>, as this can give more information on the expected type of *) +(* the <general_term>, thus allowing for the insertion of coercions. *) +CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R. + +Definition applybig {R I} (body : bigbody R I) x := + let: BigBody _ op b v := body in if b then op v x else x. + +Definition reducebig R I idx r (body : I -> bigbody R I) := + foldr (applybig \o body) idx r. + +Module Type BigOpSig. +Parameter bigop : forall R I, R -> seq I -> (I -> bigbody R I) -> R. +Axiom bigopE : bigop = reducebig. +End BigOpSig. + +Module BigOp : BigOpSig. +Definition bigop := reducebig. +Lemma bigopE : bigop = reducebig. Proof. by []. Qed. +End BigOp. + +Notation bigop := BigOp.bigop (only parsing). +Canonical bigop_unlock := Unlockable BigOp.bigopE. + +Definition index_iota m n := iota m (n - m). + +Definition index_enum (T : finType) := Finite.enum T. + +Lemma mem_index_iota m n i : i \in index_iota m n = (m <= i < n). +Admitted. + +Lemma mem_index_enum T i : i \in index_enum T. +Admitted. + +Hint Resolve mem_index_enum. + +(* +Lemma filter_index_enum T P : filter P (index_enum T) = enum P. +Proof. by []. Qed. +*) + +Notation "\big [ op / idx ]_ ( i <- r | P ) F" := + (bigop idx r (fun i => BigBody i op P%B F)) : big_scope. +Notation "\big [ op / idx ]_ ( i <- r ) F" := + (bigop idx r (fun i => BigBody i op true F)) : big_scope. +Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%B F)) + : big_scope. +Notation "\big [ op / idx ]_ ( m <= i < n ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)) + : big_scope. +Notation "\big [ op / idx ]_ ( i | P ) F" := + (bigop idx (index_enum _) (fun i => BigBody i op P%B F)) : big_scope. +Notation "\big [ op / idx ]_ i F" := + (bigop idx (index_enum _) (fun i => BigBody i op true F)) : big_scope. +Notation "\big [ op / idx ]_ ( i : t | P ) F" := + (bigop idx (index_enum _) (fun i : t => BigBody i op P%B F)) + (only parsing) : big_scope. +Notation "\big [ op / idx ]_ ( i : t ) F" := + (bigop idx (index_enum _) (fun i : t => BigBody i op true F)) + (only parsing) : big_scope. +Notation "\big [ op / idx ]_ ( i < n | P ) F" := + (\big[op/idx]_(i : ordinal n | P%B) F) : big_scope. +Notation "\big [ op / idx ]_ ( i < n ) F" := + (\big[op/idx]_(i : ordinal n) F) : big_scope. +Notation "\big [ op / idx ]_ ( i 'in' A | P ) F" := + (\big[op/idx]_(i | (i \in A) && P) F) : big_scope. +Notation "\big [ op / idx ]_ ( i 'in' A ) F" := + (\big[op/idx]_(i | i \in A) F) : big_scope. + +Notation BIG_F := (F in \big[_/_]_(i <- _ | _) F i)%pattern. +Notation BIG_P := (P in \big[_/_]_(i <- _ | P i) _)%pattern. + +(* Induction loading *) +Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F : + K (\big[op/idx]_(i <- r | P i) F i) * K' (\big[op/idx]_(i <- r | P i) F i) + -> K' (\big[op/idx]_(i <- r | P i) F i). +Proof. by case. Qed. + +Arguments big_load [R] K [K'] idx op [I]. + +Section Elim3. + +Variables (R1 R2 R3 : Type) (K : R1 -> R2 -> R3 -> Type). +Variables (id1 : R1) (op1 : R1 -> R1 -> R1). +Variables (id2 : R2) (op2 : R2 -> R2 -> R2). +Variables (id3 : R3) (op3 : R3 -> R3 -> R3). + +Hypothesis Kid : K id1 id2 id3. + +Lemma big_rec3 I r (P : pred I) F1 F2 F3 + (K_F : forall i y1 y2 y3, P i -> K y1 y2 y3 -> + K (op1 (F1 i) y1) (op2 (F2 i) y2) (op3 (F3 i) y3)) : + K (\big[op1/id1]_(i <- r | P i) F1 i) + (\big[op2/id2]_(i <- r | P i) F2 i) + (\big[op3/id3]_(i <- r | P i) F3 i). +Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: K_F. Qed. + +Hypothesis Kop : forall x1 x2 x3 y1 y2 y3, + K x1 x2 x3 -> K y1 y2 y3-> K (op1 x1 y1) (op2 x2 y2) (op3 x3 y3). +Lemma big_ind3 I r (P : pred I) F1 F2 F3 + (K_F : forall i, P i -> K (F1 i) (F2 i) (F3 i)) : + K (\big[op1/id1]_(i <- r | P i) F1 i) + (\big[op2/id2]_(i <- r | P i) F2 i) + (\big[op3/id3]_(i <- r | P i) F3 i). +Proof. by apply: big_rec3 => i x1 x2 x3 /K_F; apply: Kop. Qed. + +End Elim3. + +Arguments big_rec3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ [I r P F1 F2 F3]. +Arguments big_ind3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ _ [I r P F1 F2 F3]. + +Section Elim2. + +Variables (R1 R2 : Type) (K : R1 -> R2 -> Type) (f : R2 -> R1). +Variables (id1 : R1) (op1 : R1 -> R1 -> R1). +Variables (id2 : R2) (op2 : R2 -> R2 -> R2). + +Hypothesis Kid : K id1 id2. + +Lemma big_rec2 I r (P : pred I) F1 F2 + (K_F : forall i y1 y2, P i -> K y1 y2 -> + K (op1 (F1 i) y1) (op2 (F2 i) y2)) : + K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i). +Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: K_F. Qed. + +Hypothesis Kop : forall x1 x2 y1 y2, + K x1 x2 -> K y1 y2 -> K (op1 x1 y1) (op2 x2 y2). +Lemma big_ind2 I r (P : pred I) F1 F2 (K_F : forall i, P i -> K (F1 i) (F2 i)) : + K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i). +Proof. by apply: big_rec2 => i x1 x2 /K_F; apply: Kop. Qed. + +Hypotheses (f_op : {morph f : x y / op2 x y >-> op1 x y}) (f_id : f id2 = id1). +Lemma big_morph I r (P : pred I) F : + f (\big[op2/id2]_(i <- r | P i) F i) = \big[op1/id1]_(i <- r | P i) f (F i). +Proof. by rewrite unlock; elim: r => //= i r <-; rewrite -f_op -fun_if. Qed. + +End Elim2. + +Arguments big_rec2 [R1 R2] K [id1 op1 id2 op2] _ [I r P F1 F2]. +Arguments big_ind2 [R1 R2] K [id1 op1 id2 op2] _ _ [I r P F1 F2]. +Arguments big_morph [R1 R2] f [id1 op1 id2 op2] _ _ [I]. + +Section Elim1. + +Variables (R : Type) (K : R -> Type) (f : R -> R). +Variables (idx : R) (op op' : R -> R -> R). + +Hypothesis Kid : K idx. + +Lemma big_rec I r (P : pred I) F + (Kop : forall i x, P i -> K x -> K (op (F i) x)) : + K (\big[op/idx]_(i <- r | P i) F i). +Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: Kop. Qed. + +Hypothesis Kop : forall x y, K x -> K y -> K (op x y). +Lemma big_ind I r (P : pred I) F (K_F : forall i, P i -> K (F i)) : + K (\big[op/idx]_(i <- r | P i) F i). +Proof. by apply: big_rec => // i x /K_F /Kop; apply. Qed. + +Hypothesis Kop' : forall x y, K x -> K y -> op x y = op' x y. +Lemma eq_big_op I r (P : pred I) F (K_F : forall i, P i -> K (F i)) : + \big[op/idx]_(i <- r | P i) F i = \big[op'/idx]_(i <- r | P i) F i. +Proof. +by elim/(big_load K): _; elim/big_rec2: _ => // i _ y Pi [Ky <-]; auto. +Qed. + +Hypotheses (fM : {morph f : x y / op x y}) (f_id : f idx = idx). +Lemma big_endo I r (P : pred I) F : + f (\big[op/idx]_(i <- r | P i) F i) = \big[op/idx]_(i <- r | P i) f (F i). +Proof. exact: big_morph. Qed. + +End Elim1. + +Arguments big_rec [R] K [idx op] _ [I r P F]. +Arguments big_ind [R] K [idx op] _ _ [I r P F]. +Arguments eq_big_op [R] K [idx op] op' _ _ _ [I]. +Arguments big_endo [R] f [idx op] _ _ [I]. + +(* zmodp -------------------------------------------------------------------- *) + +Lemma ord1 : all_equal_to (@Ordinal 1 0 is_true_true : 'I_1). +Admitted. diff --git a/test-suite/prerequisite/ssr_ssrsyntax1.v b/test-suite/prerequisite/ssr_ssrsyntax1.v new file mode 100644 index 000000000..2b404e2de --- /dev/null +++ b/test-suite/prerequisite/ssr_ssrsyntax1.v @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require ssreflect. +Require Import Arith. + +Goal (forall a b, a + b = b + a). +intros. +rewrite plus_comm, plus_comm. +split. +Abort. + +Module Foo. +Import ssreflect. + +Goal (forall a b, a + b = b + a). +intros. +rewrite 2![_ + _]plus_comm. +split. +Abort. +End Foo. + +Goal (forall a b, a + b = b + a). +intros. +rewrite plus_comm, plus_comm. +split. +Abort. diff --git a/test-suite/ssr/absevarprop.v b/test-suite/ssr/absevarprop.v new file mode 100644 index 000000000..fa1de0095 --- /dev/null +++ b/test-suite/ssr/absevarprop.v @@ -0,0 +1,96 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect ssrbool ssrfun. +Require Import TestSuite.ssr_mini_mathcomp. + +Lemma test15: forall (y : nat) (x : 'I_2), y < 1 -> val x = y -> Some x = insub y. +move=> y x le_1 defx; rewrite insubT ?(leq_trans le_1) // => ?. +by congr (Some _); apply: val_inj=> /=; exact: defx. +Qed. + +Axiom P : nat -> Prop. +Axiom Q : forall n, P n -> Prop. +Definition R := fun (x : nat) (p : P x) m (q : P (x+1)) => m > 0. + +Inductive myEx : Type := ExI : forall n (pn : P n) pn', Q n pn -> R n pn n pn' -> myEx. + +Variable P1 : P 1. +Variable P11 : P (1 + 1). +Variable Q1 : forall P1, Q 1 P1. + +Lemma testmE1 : myEx. +Proof. +apply: ExI 1 _ _ _ _. + match goal with |- P 1 => exact: P1 | _ => fail end. + match goal with |- P (1+1) => exact: P11 | _ => fail end. + match goal with |- forall p : P 1, Q 1 p => move=> *; exact: Q1 | _ => fail end. +match goal with |- forall (p : P 1) (q : P (1+1)), is_true (R 1 p 1 q) => done | _ => fail end. +Qed. + +Lemma testE2 : exists y : { x | P x }, sval y = 1. +Proof. +apply: ex_intro (exist _ 1 _) _. + match goal with |- P 1 => exact: P1 | _ => fail end. +match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end. +Qed. + +Lemma testE3 : exists y : { x | P x }, sval y = 1. +Proof. +have := (ex_intro _ (exist _ 1 _) _); apply. + match goal with |- P 1 => exact: P1 | _ => fail end. +match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end. +Qed. + +Lemma testE4 : P 2 -> exists y : { x | P x }, sval y = 2. +Proof. +move=> P2; apply: ex_intro (exist _ 2 _) _. +match goal with |- @sval _ _ (@exist _ _ 2 P2) = 2 => done | _ => fail end. +Qed. + +Hint Resolve P1. + +Lemma testmE12 : myEx. +Proof. +apply: ExI 1 _ _ _ _. + match goal with |- P (1+1) => exact: P11 | _ => fail end. + match goal with |- Q 1 P1 => exact: Q1 | _ => fail end. +match goal with |- forall (q : P (1+1)), is_true (R 1 P1 1 q) => done | _ => fail end. +Qed. + +Create HintDb SSR. + +Hint Resolve P11 : SSR. + +Ltac ssrautoprop := trivial with SSR. + +Lemma testmE13 : myEx. +Proof. +apply: ExI 1 _ _ _ _. + match goal with |- Q 1 P1 => exact: Q1 | _ => fail end. +match goal with |- is_true (R 1 P1 1 P11) => done | _ => fail end. +Qed. + +Definition R1 := fun (x : nat) (p : P x) m (q : P (x+1)) (r : Q x p) => m > 0. + +Inductive myEx1 : Type := + ExI1 : forall n (pn : P n) pn' (q : Q n pn), R1 n pn n pn' q -> myEx1. + +Hint Resolve (Q1 P1) : SSR. + +(* tests that goals in prop are solved in the right order, propagating instantiations, + thus the goal Q 1 ?p1 is faced by trivial after ?p1, and is thus evar free *) +Lemma testmE14 : myEx1. +Proof. +apply: ExI1 1 _ _ _ _. +match goal with |- is_true (R1 1 P1 1 P11 (Q1 P1)) => done | _ => fail end. +Qed. diff --git a/test-suite/ssr/abstract_var2.v b/test-suite/ssr/abstract_var2.v new file mode 100644 index 000000000..7c57d2024 --- /dev/null +++ b/test-suite/ssr/abstract_var2.v @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssreflect. + +Set Implicit Arguments. + +Axiom P : nat -> nat -> Prop. + +Axiom tr : + forall x y z, P x y -> P y z -> P x z. + +Lemma test a b c : P a c -> P a b. +Proof. +intro H. +Fail have [: s1 s2] H1 : P a b := @tr _ _ _ s1 s2. +have [: w s1 s2] H1 : P a b := @tr _ w _ s1 s2. +Abort. diff --git a/test-suite/ssr/binders.v b/test-suite/ssr/binders.v new file mode 100644 index 000000000..97b7d830f --- /dev/null +++ b/test-suite/ssr/binders.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Lemma test (x : bool) : True. +have H1 x := x. +have (x) := x => H2. +have H3 T (x : T) := x. +have ? : bool := H1 _ x. +have ? : bool := H2 _ x. +have ? : bool := H3 _ x. +have ? (z : bool) : forall y : bool, z = z := fun y => refl_equal _. +have ? w : w = w := @refl_equal nat w. +have ? y : true by []. +have ? (z : bool) : z = z. + exact: (@refl_equal _ z). +have ? (z w : bool) : z = z by exact: (@refl_equal _ z). +have H w (a := 3) (_ := 4) : w && true = w. + by rewrite andbT. +exact I. +Qed. + +Lemma test1 : True. +suff (x : bool): x = x /\ True. + by move/(_ true); case=> _. +split; first by exact: (@refl_equal _ x). +suff H y : y && true = y /\ True. + by case: (H true). +suff H1 /= : true && true /\ True. + by rewrite andbT; split; [exact: (@refl_equal _ y) | exact: I]. +match goal with |- is_true true /\ True => idtac end. +by split. +Qed. + +Lemma foo n : n >= 0. +have f i (j := i + n) : j < n. + match goal with j := i + n |- _ => idtac end. +Undo 2. +suff f i (j := i + n) : j < n. + done. +match goal with j := i + n |- _ => idtac end. +Undo 3. +done. +Qed. diff --git a/test-suite/ssr/binders_of.v b/test-suite/ssr/binders_of.v new file mode 100644 index 000000000..69b52eace --- /dev/null +++ b/test-suite/ssr/binders_of.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + + +Require Import ssreflect. +Require Import TestSuite.ssr_mini_mathcomp. + +Lemma test1 : True. +have f of seq nat & nat : nat. + exact 3. +have g of nat := 3. +have h of nat : nat := 3. +have _ : f [::] 3 = g 3 + h 4. +Admitted. diff --git a/test-suite/ssr/caseview.v b/test-suite/ssr/caseview.v new file mode 100644 index 000000000..94b064b02 --- /dev/null +++ b/test-suite/ssr/caseview.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Lemma test (A B : Prop) : A /\ B -> True. +Proof. by case=> _ /id _. Qed. diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v new file mode 100644 index 000000000..7e60b04a6 --- /dev/null +++ b/test-suite/ssr/congr.v @@ -0,0 +1,34 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Lemma test1 : forall a b : nat, a == b -> a == 0 -> b == 0. +Proof. move=> a b Eab Eac; congr (_ == 0) : Eac; exact: eqP Eab. Qed. + +Definition arrow A B := A -> B. + +Lemma test2 : forall a b : nat, a == b -> arrow (a == 0) (b == 0). +Proof. move=> a b Eab; congr (_ == 0); exact: eqP Eab. Qed. + +Definition equals T (A B : T) := A = B. + +Lemma test3 : forall a b : nat, a = b -> equals nat (a + b) (b + b). +Proof. move=> a b E; congr (_ + _); exact E. Qed. + +Variable S : eqType. +Variable f : nat -> S. +Coercion f : nat >-> Equality.sort. + +Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a). +Proof. move=> a b Eba; congr (_ + _); exact: Eba. Qed. diff --git a/test-suite/ssr/deferclear.v b/test-suite/ssr/deferclear.v new file mode 100644 index 000000000..85353dadf --- /dev/null +++ b/test-suite/ssr/deferclear.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Variable T : Type. + +Lemma test0 : forall a b c d : T, True. +Proof. by move=> a b {a} a c; exact I. Qed. + +Variable P : T -> Prop. + +Lemma test1 : forall a b c : T, P a -> forall d : T, True. +Proof. move=> a b {a} a _ d; exact I. Qed. + +Definition Q := forall x y : nat, x = y. +Axiom L : 0 = 0 -> Q. +Axiom L' : 0 = 0 -> forall x y : nat, x = y. +Lemma test3 : Q. +by apply/L. +Undo. +rewrite /Q. +by apply/L. +Undo 2. +by apply/L'. +Qed. diff --git a/test-suite/ssr/dependent_type_err.v b/test-suite/ssr/dependent_type_err.v new file mode 100644 index 000000000..a5789d8dd --- /dev/null +++ b/test-suite/ssr/dependent_type_err.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp. + +Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p. +move=> n m p Hmn Hnp; rewrite -ltnS. +Fail rewrite (_ : forall n0 m0 p0 : nat, m0 <= n0 -> n0 < p0 -> m0 < p0). +Fail rewrite leq_ltn_trans. +Admitted. diff --git a/test-suite/ssr/derive_inversion.v b/test-suite/ssr/derive_inversion.v new file mode 100644 index 000000000..abf63a20c --- /dev/null +++ b/test-suite/ssr/derive_inversion.v @@ -0,0 +1,29 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssreflect ssrbool. + +Set Implicit Arguments. + + Inductive wf T : bool -> option T -> Type := + | wf_f : wf false None + | wf_t : forall x, wf true (Some x). + + Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop. + + Lemma Problem T b (o : option T) : + wf b o -> + match b with + | true => exists x, o = Some x + | false => o = None + end. + Proof. + by case: b; elim/wf_inv=> //; case: o=> // a *; exists a. + Qed. diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v new file mode 100644 index 000000000..908249a36 --- /dev/null +++ b/test-suite/ssr/elim.v @@ -0,0 +1,279 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool ssrfun TestSuite.ssr_mini_mathcomp. +Axiom daemon : False. Ltac myadmit := case: daemon. + +(* Ltac debugging feature: recursive elim + eq generation *) +Lemma testL1 : forall A (s : seq A), s = s. +Proof. +move=> A s; elim branch: s => [|x xs _]. +match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. +match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. +Qed. + +(* The same but with explicit eliminator and a conflict in the intro pattern *) +Lemma testL2 : forall A (s : seq A), s = s. +Proof. +move=> A s; elim/last_ind branch: s => [|x s _]. +match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. +match goal with _ : _ = rcons _ _ |- rcons _ _ = rcons _ _ => move: branch => // | _ => fail end. +Qed. + +(* The same but without names for variables involved in the generated eq *) +Lemma testL3 : forall A (s : seq A), s = s. +Proof. +move=> A s; elim branch: s; move: (s) => _. +match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end. +move=> _; match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end. +Qed. + +Inductive foo : Type := K1 : foo | K2 : foo -> foo -> foo | K3 : (nat -> foo) -> foo. + +(* The same but with more intros to be done *) +Lemma testL4 : forall (o : foo), o = o. +Proof. +move=> o; elim branch: o. +match goal with _ : _ = K1 |- K1 = K1 => move: branch => // | _ => fail end. +move=> _; match goal with _ : _ = K2 _ _ |- K2 _ _ = K2 _ _ => move: branch => // | _ => fail end. +move=> _; match goal with _ : _ = K3 _ |- K3 _ = K3 _ => move: branch => // | _ => fail end. +Qed. + +(* Occurrence counting *) +Lemma testO1: forall (b : bool), b = b. +Proof. +move=> b; case: (b) / idP. +match goal with |- is_true b -> true = true => done | _ => fail end. +match goal with |- ~ is_true b -> false = false => done | _ => fail end. +Qed. + +(* The same but only the second occ *) +Lemma testO2: forall (b : bool), b = b. +Proof. +move=> b; case: {2}(b) / idP. +match goal with |- is_true b -> b = true => done | _ => fail end. +match goal with |- ~ is_true b -> b = false => move/(introF idP) => // | _ => fail end. +Qed. + +(* The same but with eq generation *) +Lemma testO3: forall (b : bool), b = b. +Proof. +move=> b; case E: {2}(b) / idP. +match goal with _ : is_true b, _ : b = true |- b = true => move: E => _; done | _ => fail end. +match goal with H : ~ is_true b, _ : b = false |- b = false => move: E => _; move/(introF idP): H => // | _ => fail end. +Qed. + +(* Views *) +Lemma testV1 : forall A (s : seq A), s = s. +Proof. +move=> A s; case/lastP E: {1}s => [| x xs]. +match goal with _ : s = [::] |- [::] = s => symmetry; exact E | _ => fail end. +match goal with _ : s = rcons x xs |- rcons _ _ = s => symmetry; exact E | _ => fail end. +Qed. + +Lemma testV2 : forall A (s : seq A), s = s. +Proof. +move=> A s; case/lastP E: s => [| x xs]. +match goal with _ : s = [::] |- [::] = [::] => done | _ => fail end. +match goal with _ : s = rcons x xs |- rcons _ _ = rcons _ _ => done | _ => fail end. +Qed. + +Lemma testV3 : forall A (s : seq A), s = s. +Proof. +move=> A s; case/lastP: s => [| x xs]. +match goal with |- [::] = [::] => done | _ => fail end. +match goal with |- rcons _ _ = rcons _ _ => done | _ => fail end. +Qed. + +(* Patterns *) +Lemma testP1: forall (x y : nat), (y == x) && (y == x) -> y == x. +move=> x y; elim: {2}(_ == _) / eqP. +match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end. +match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end. +Qed. + +(* The same but with an implicit pattern *) +Lemma testP2 : forall (x y : nat), (y == x) && (y == x) -> y == x. +move=> x y; elim: {2}_ / eqP. +match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end. +match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end. +Qed. + +(* The same but with an eq generation switch *) +Lemma testP3 : forall (x y : nat), (y == x) && (y == x) -> y == x. +move=> x y; elim E: {2}_ / eqP. +match goal with _ : y = x |- (is_true ((y == x) && true) -> is_true (y == x)) => rewrite E; reflexivity | _ => fail end. +match goal with _ : y <> x |- (is_true ((y == x) && false) -> is_true (y == x)) => rewrite E => /= H; exact H | _ => fail end. +Qed. + +Inductive spec : nat -> nat -> nat -> Prop := +| specK : forall a b c, a = 0 -> b = 2 -> c = 4 -> spec a b c. +Lemma specP : spec 0 2 4. Proof. by constructor. Qed. + +Lemma testP4 : (1+1) * 4 = 2 + (1+1) + (2 + 2). +Proof. +case: specP => a b c defa defb defc. +match goal with |- (a.+1 + a.+1) * c = b + (a.+1 + a.+1) + (b + b) => subst; done | _ => fail end. +Qed. + +Lemma testP5 : (1+1) * 4 = 2 + (1+1) + (2 + 2). +Proof. +case: (1 + 1) _ / specP => a b c defa defb defc. +match goal with |- b * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end. +Qed. + +Lemma testP6 : (1+1) * 4 = 2 + (1+1) + (2 + 2). +Proof. +case: {2}(1 + 1) _ / specP => a b c defa defb defc. +match goal with |- (a.+1 + a.+1) * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end. +Qed. + +Lemma testP7 : (1+1) * 4 = 2 + (1+1) + (2 + 2). +Proof. +case: _ (1 + 1) (2 + _) / specP => a b c defa defb defc. +match goal with |- b * a.+4 = c + c => subst; done | _ => fail end. +Qed. + +Lemma testP8 : (1+1) * 4 = 2 + (1+1) + (2 + 2). +Proof. +case E: (1 + 1) (2 + _) / specP=> [a b c defa defb defc]. +match goal with |- b * a.+4 = c + c => subst; done | _ => fail end. +Qed. + +Variables (T : Type) (tr : T -> T). + +Inductive exec (cf0 cf1 : T) : seq T -> Prop := +| exec_step : tr cf0 = cf1 -> exec cf0 cf1 [::] +| exec_star : forall cf2 t, tr cf0 = cf2 -> + exec cf2 cf1 t -> exec cf0 cf1 (cf2 :: t). + +Inductive execr (cf0 cf1 : T) : seq T -> Prop := +| execr_step : tr cf0 = cf1 -> execr cf0 cf1 [::] +| execr_star : forall cf2 t, execr cf0 cf2 t -> + tr cf2 = cf1 -> execr cf0 cf1 (t ++ [:: cf2]). + +Lemma execP : forall cf0 cf1 t, exec cf0 cf1 t <-> execr cf0 cf1 t. +Proof. +move=> cf0 cf1 t; split => [] Ecf. + elim: Ecf. + match goal with |- forall cf2 cf3 : T, tr cf2 = cf3 -> + execr cf2 cf3 [::] => myadmit | _ => fail end. + match goal with |- forall (cf2 cf3 cf4 : T) (t0 : seq T), + tr cf2 = cf4 -> exec cf4 cf3 t0 -> execr cf4 cf3 t0 -> + execr cf2 cf3 (cf4 :: t0) => myadmit | _ => fail end. +elim: Ecf. + match goal with |- forall cf2 : T, + tr cf0 = cf2 -> exec cf0 cf2 [::] => myadmit | _ => fail end. +match goal with |- forall (cf2 cf3 : T) (t0 : seq T), + execr cf0 cf3 t0 -> exec cf0 cf3 t0 -> tr cf3 = cf2 -> + exec cf0 cf2 (t0 ++ [:: cf3]) => myadmit | _ => fail end. +Qed. + +Fixpoint plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. + +Definition plus_equation : +forall m n : nat, + plus m n = + match n with + | 0 => m + | p.+1 => (plus m p).+1 + end +:= +fun m n : nat => +match + n as n0 + return + (forall m0 : nat, + plus m0 n0 = + match n0 with + | 0 => m0 + | p.+1 => (plus m0 p).+1 + end) +with +| 0 => @erefl nat +| n0.+1 => fun m0 : nat => erefl (plus m0 n0).+1 +end m. + +Definition plus_rect : +forall (m : nat) (P : nat -> nat -> Type), + (forall n : nat, n = 0 -> P 0 m) -> + (forall n p : nat, + n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) -> + forall n : nat, P n (plus m n) +:= +fun (m : nat) (P : nat -> nat -> Type) + (f0 : forall n : nat, n = 0 -> P 0 m) + (f : forall n p : nat, + n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) => +fix plus0 (n : nat) : P n (plus m n) := + eq_rect_r [eta P n] + (let f1 := f0 n in + let f2 := f n in + match + n as n0 + return + (n = n0 -> + (forall p : nat, + n0 = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) -> + (n0 = 0 -> P 0 m) -> + P n0 match n0 with + | 0 => m + | p.+1 => (plus m p).+1 + end) + with + | 0 => + fun (_ : n = 0) + (_ : forall p : nat, + 0 = p.+1 -> + P p (plus m p) -> P p.+1 (plus m p).+1) + (f4 : 0 = 0 -> P 0 m) => unkeyed (f4 (erefl 0)) + | n0.+1 => + fun (_ : n = n0.+1) + (f3 : forall p : nat, + n0.+1 = p.+1 -> + P p (plus m p) -> P p.+1 (plus m p).+1) + (_ : n0.+1 = 0 -> P 0 m) => + let f5 := + let p := n0 in + let H := erefl n0.+1 : n0.+1 = p.+1 in f3 p H in + unkeyed (let Hrec := plus0 n0 in f5 Hrec) + end (erefl n) f2 f1) (plus_equation m n). + +Definition plus_ind := plus_rect. + +Lemma exF x y z: plus (plus x y) z = plus x (plus y z). +elim/plus_ind: z / (plus _ z). +match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. +Undo 2. +elim/plus_ind: (plus _ z). +match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. +Undo 2. +elim/plus_ind: {z}(plus _ z). +match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. +Undo 2. +elim/plus_ind: {z}_. +match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. +Undo 2. +elim/plus_ind: z / _. +match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end. + done. +by move=> _ p _ ->. +Qed. + +(* BUG elim-False *) +Lemma testeF : False -> 1 = 0. +Proof. by elim. Qed. diff --git a/test-suite/ssr/elim2.v b/test-suite/ssr/elim2.v new file mode 100644 index 000000000..c7c20d8f8 --- /dev/null +++ b/test-suite/ssr/elim2.v @@ -0,0 +1,74 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. +(* div fintype finfun path bigop. *) + +Axiom daemon : False. Ltac myadmit := case: daemon. + +Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F : + let s := \big[op/idx]_(i <- r | P i) F i in + K s * K' s -> K' s. +Proof. by move=> /= [_]. Qed. +Arguments big_load [R] K [K' idx op I r P F]. + +Section Elim1. + +Variables (R : Type) (K : R -> Type) (f : R -> R). +Variables (idx : R) (op op' : R -> R -> R). + +Hypothesis Kid : K idx. + +Ltac ASSERT1 := match goal with |- (K idx) => myadmit end. +Ltac ASSERT2 K := match goal with |- (forall x1 : R, R -> + forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => myadmit end. + + +Lemma big_rec I r (P : pred I) F + (Kop : forall i x, P i -> K x -> K (op (F i) x)) : + K (\big[op/idx]_(i <- r | P i) F i). +Proof. +elim/big_ind2: {-}_. + ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4. +elim/big_ind2: _ / {-}_. + ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4. + +elim/big_rec2: (\big[op/idx]_(i <- r | P i) op idx (F i)) + / (\big[op/idx]_(i <- r | P i) F i). + ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => myadmit end. Undo 3. + +elim/(big_load (phantom R)): _. + Undo. + +Fail elim/big_rec2: {2}_. + +elim/big_rec2: (\big[op/idx]_(i <- r | P i) F i) + / {1}(\big[op/idx]_(i <- r | P i) F i). + Undo. + +elim/(big_load (phantom R)): _. +Undo. + +Fail elim/big_rec2: _ / {2}(\big[op/idx]_(i <- r | P i) F i). +Admitted. + +Definition morecomplexthannecessary A (P : A -> A -> Prop) x y := P x y. + +Lemma grab A (P : A -> A -> Prop) n m : (n = m) -> (P n n) -> morecomplexthannecessary A P n m. +by move->. +Qed. + +Goal forall n m, m + (n + m) = m + (n * 1 + m). +Proof. move=> n m; elim/grab : (_ * _) / {1}n => //; exact: muln1. Qed. + +End Elim1. diff --git a/test-suite/ssr/elim_pattern.v b/test-suite/ssr/elim_pattern.v new file mode 100644 index 000000000..ef4658287 --- /dev/null +++ b/test-suite/ssr/elim_pattern.v @@ -0,0 +1,27 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. +Axiom daemon : False. Ltac myadmit := case: daemon. + +Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1). +case: (X in _ = X) / eqP => _. +match goal with |- (x == x) = true => myadmit end. +match goal with |- (x == x) = false => myadmit end. +Qed. + +Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1). +elim: (x in RHS). +match goal with |- (x == x) = _ => myadmit end. +match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end. +Qed. diff --git a/test-suite/ssr/first_n.v b/test-suite/ssr/first_n.v new file mode 100644 index 000000000..4971add91 --- /dev/null +++ b/test-suite/ssr/first_n.v @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. + +Lemma test : False -> (bool -> False -> True -> True) -> True. +move=> F; let w := constr:(2) in apply; last w first. +- by apply: F. +- by apply: I. +- by apply: true. +Qed. diff --git a/test-suite/ssr/gen_have.v b/test-suite/ssr/gen_have.v new file mode 100644 index 000000000..249e006f9 --- /dev/null +++ b/test-suite/ssr/gen_have.v @@ -0,0 +1,174 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp. +Axiom daemon : False. Ltac myadmit := case: daemon. + +Axiom P : nat -> Prop. +Lemma clear_test (b1 b2 : bool) : b2 = b2. +Proof. +(* wlog gH : (b3 := b2) / b2 = b3. myadmit. *) +gen have {b1} H, gH : (b3 := b2) (w := erefl 3) / b2 = b3. + myadmit. +Fail exact (H b1). +exact (H b2 (erefl _)). +Qed. + + +Lemma test1 n (ngt0 : 0 < n) : P n. +gen have lt2le, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0). + match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. +Check (lt2le : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +Check (H1 : 0 <= n). +Check (H2 : n != 0). +myadmit. +Qed. + +Lemma test2 n (ngt0 : 0 < n) : P n. +gen have _, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0). + match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. +lazymatch goal with + | lt2le : forall n : nat, is_true(0 < n) -> is_true((0 <= n) && (n != 0)) + |- _ => fail "not cleared" + | _ => idtac end. +Check (H1 : 0 <= n). +Check (H2 : n != 0). +myadmit. +Qed. + +Lemma test3 n (ngt0 : 0 < n) : P n. +gen have H : n ngt0 / (0 <= n) && (n != 0). + match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. +Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +myadmit. +Qed. + +Lemma test4 n (ngt0 : 0 < n) : P n. +gen have : n ngt0 / (0 <= n) && (n != 0). + match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. +move=> H. +Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +myadmit. +Qed. + +Lemma test4bis n (ngt0 : 0 < n) : P n. +wlog suff : n ngt0 / (0 <= n) && (n != 0); last first. + match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end. +move=> H. +Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +myadmit. +Qed. + +Lemma test5 n (ngt0 : 0 < n) : P n. +Fail gen have : / (0 <= n) && (n != 0). +Abort. + +Lemma test6 n (ngt0 : 0 < n) : P n. +gen have : n ngt0 / (0 <= n) && (n != 0) by myadmit. +Abort. + +Lemma test7 n (ngt0 : 0 < n) : P n. +Fail gen have : n / (0 <= n) && (n != 0). +Abort. + +Lemma test3wlog2 n (ngt0 : 0 < n) : P n. +gen have H : (m := n) ngt0 / (0 <= m) && (m != 0). + match goal with + ngt0 : is_true(0 < m) |- is_true((0 <= m) && (m != 0)) => myadmit end. +Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)). +myadmit. +Qed. + +Lemma test3wlog3 n (ngt0 : 0 < n) : P n. +gen have H : {n} (m := n) (n := 0) ngt0 / (0 <= m) && (m != n). + match goal with + ngt0 : is_true(n < m) |- is_true((0 <= m) && (m != n)) => myadmit end. +Check (H : forall m n : nat, n < m -> (0 <= m) && (m != n)). +myadmit. +Qed. + +Lemma testw1 n (ngt0 : 0 < n) : n <= 0. +wlog H : (z := 0) (m := n) ngt0 / m != 0. + match goal with + |- (forall z m, + is_true(z < m) -> is_true(m != 0) -> is_true(m <= z)) -> + is_true(n <= 0) => myadmit end. +Check(n : nat). +Check(m : nat). +Check(z : nat). +Check(ngt0 : z < m). +Check(H : m != 0). +myadmit. +Qed. + +Lemma testw2 n (ngt0 : 0 < n) : n <= 0. +wlog H : (m := n) (z := (X in n <= X)) ngt0 / m != z. + match goal with + |- (forall m z : nat, + is_true(0 < m) -> is_true(m != z) -> is_true(m <= z)) -> + is_true(n <= 0) => idtac end. +Restart. +wlog H : (m := n) (one := (X in X <= _)) ngt0 / m != one. + match goal with + |- (forall m one : nat, + is_true(one <= m) -> is_true(m != one) -> is_true(m <= 0)) -> + is_true(n <= 0) => idtac end. +Restart. +wlog H : {n} (m := n) (z := (X in _ <= X)) ngt0 / m != z. + match goal with + |- (forall m z : nat, + is_true(0 < z) -> is_true(m != z) -> is_true(m <= 0)) -> + is_true(n <= 0) => idtac end. + myadmit. +Fail Check n. +myadmit. +Qed. + +Section Test. +Variable x : nat. +Definition addx y := y + x. + +Lemma testw3 (m n : nat) (ngt0 : 0 < n) : n <= addx x. +wlog H : (n0 := n) (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y. + myadmit. +myadmit. +Qed. + + +Definition twox := x + x. +Definition bis := twox. + +Lemma testw3x n (ngt0 : 0 < n) : n + x <= twox. +wlog H : (y := x) (@twoy := (X in _ <= X)) / twoy = 2 * y. + match goal with + |- (forall y : nat, + let twoy := y + y in + twoy = 2 * y -> is_true(n + y <= twoy)) -> + is_true(n + x <= twox) => myadmit end. +Restart. +wlog H : (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y. + match goal with + |- (forall y : nat, + let twoy := twox in + twoy = 2 * y -> is_true(n + y <= twoy)) -> + is_true(n + x <= twox) => myadmit end. +myadmit. +Qed. + +End Test. + +Lemma test_in n k (def_k : k = 0) (ngtk : k < n) : P n. +rewrite -(add0n n) in {def_k k ngtk} (m := k) (def_m := def_k) (ngtm := ngtk). +rewrite def_m add0n in {ngtm} (e := erefl 0 ) (ngt0 := ngtm) => {def_m}. +myadmit. +Qed. diff --git a/test-suite/ssr/gen_pattern.v b/test-suite/ssr/gen_pattern.v new file mode 100644 index 000000000..c0592e884 --- /dev/null +++ b/test-suite/ssr/gen_pattern.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Notation "( a 'in' c )" := (a + c) (only parsing) : myscope. +Delimit Scope myscope with myscope. + +Notation "( a 'in' c )" := (a + c) (only parsing). + +Lemma foo x y : x + x.+1 = x.+1 + y. +move: {x} (x.+1) {1}x y (x.+1 in RHS). + match goal with |- forall a b c d, b + a = d + c => idtac end. +Admitted. + +Lemma bar x y : x + x.+1 = x.+1 + y. +move E: ((x.+1 in y)) => w. + match goal with |- x + x.+1 = w => rewrite -{w}E end. +move E: (x.+1 in y)%myscope => w. + match goal with |- x + x.+1 = w => rewrite -{w}E end. +move E: ((x + y).+1 as RHS) => w. + match goal with |- x + x.+1 = w => rewrite -{}E -addSn end. +Admitted. diff --git a/test-suite/ssr/have_TC.v b/test-suite/ssr/have_TC.v new file mode 100644 index 000000000..b3a26ed2c --- /dev/null +++ b/test-suite/ssr/have_TC.v @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +Class foo (T : Type) := { n : nat }. +Instance five : foo nat := {| n := 5 |}. + +Definition bar T {f : foo T} m : Prop := + @n _ f = m. + +Eval compute in (bar nat 7). + +Lemma a : True. +set toto := bar _ 8. +have titi : bar _ 5. + reflexivity. +have titi2 : bar _ 5 := . + Fail reflexivity. + by myadmit. +have totoc (H : bar _ 5) : 3 = 3 := eq_refl. +move/totoc: nat => _. +exact I. +Qed. + +Set SsrHave NoTCResolution. + +Lemma a' : True. +set toto := bar _ 8. +have titi : bar _ 5. + Fail reflexivity. + by myadmit. +have titi2 : bar _ 5 := . + Fail reflexivity. + by myadmit. +have totoc (H : bar _ 5) : 3 = 3 := eq_refl. +move/totoc: nat => _. +exact I. +Qed. diff --git a/test-suite/ssr/have_transp.v b/test-suite/ssr/have_transp.v new file mode 100644 index 000000000..1c998da71 --- /dev/null +++ b/test-suite/ssr/have_transp.v @@ -0,0 +1,48 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp. + + +Lemma test1 n : n >= 0. +Proof. +have [:s1] @h m : 'I_(n+m).+1. + apply: Sub 0 _. + abstract: s1 m. + by auto. +cut (forall m, 0 < (n+m).+1); last assumption. +rewrite [_ 1 _]/= in s1 h *. +by []. +Qed. + +Lemma test2 n : n >= 0. +Proof. +have [:s1] @h m : 'I_(n+m).+1 := Sub 0 (s1 m). + move=> m; reflexivity. +cut (forall m, 0 < (n+m).+1); last assumption. +by []. +Qed. + +Lemma test3 n : n >= 0. +Proof. +Fail have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0 (s1 m)); auto. +have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract: s1 m; auto. +cut (forall m, 0 < (n+m).+1); last assumption. +by []. +Qed. + +Lemma test4 n : n >= 0. +Proof. +have @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract auto. +by []. +Qed. diff --git a/test-suite/ssr/have_view_idiom.v b/test-suite/ssr/have_view_idiom.v new file mode 100644 index 000000000..3d6c9d980 --- /dev/null +++ b/test-suite/ssr/have_view_idiom.v @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. + +Lemma test (a b : bool) (pab : a && b) : b. +have {pab} /= /andP [pa -> //] /= : true && (a && b) := pab. +Qed. diff --git a/test-suite/ssr/havesuff.v b/test-suite/ssr/havesuff.v new file mode 100644 index 000000000..aa1f71879 --- /dev/null +++ b/test-suite/ssr/havesuff.v @@ -0,0 +1,85 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Variables P G : Prop. + +Lemma test1 : (P -> G) -> P -> G. +Proof. +move=> pg p. +have suff {pg} H : P. + match goal with |- P -> G => move=> _; exact: pg p | _ => fail end. +match goal with H : P -> G |- G => exact: H p | _ => fail end. +Qed. + +Lemma test2 : (P -> G) -> P -> G. +Proof. +move=> pg p. +have suffices {pg} H : P. + match goal with |- P -> G => move=> _; exact: pg p | _ => fail end. +match goal with H : P -> G |- G => exact: H p | _ => fail end. +Qed. + +Lemma test3 : (P -> G) -> P -> G. +Proof. +move=> pg p. +suff have {pg} H : P. + match goal with H : P |- G => exact: pg H | _ => fail end. +match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. +Qed. + +Lemma test4 : (P -> G) -> P -> G. +Proof. +move=> pg p. +suffices have {pg} H: P. + match goal with H : P |- G => exact: pg H | _ => fail end. +match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. +Qed. + +(* +Lemma test5 : (P -> G) -> P -> G. +Proof. +move=> pg p. +suff have {pg} H : P := pg H. +match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. +Qed. +*) + +(* +Lemma test6 : (P -> G) -> P -> G. +Proof. +move=> pg p. +suff have {pg} H := pg H. +match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end. +Qed. +*) + +Lemma test7 : (P -> G) -> P -> G. +Proof. +move=> pg p. +have suff {pg} H : P := pg. +match goal with H : P -> G |- G => exact: H p | _ => fail end. +Qed. + +Lemma test8 : (P -> G) -> P -> G. +Proof. +move=> pg p. +have suff {pg} H := pg. +match goal with H : P -> G |- G => exact: H p | _ => fail end. +Qed. + +Goal forall x y : bool, x = y -> x = y. +move=> x y E. +by have {x E} -> : x = y by []. +Qed. diff --git a/test-suite/ssr/if_isnt.v b/test-suite/ssr/if_isnt.v new file mode 100644 index 000000000..b8f6b7739 --- /dev/null +++ b/test-suite/ssr/if_isnt.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Definition unopt (x : option bool) := + if x isn't Some x then false else x. + +Lemma test1 : unopt None = false /\ + unopt (Some false) = false /\ + unopt (Some true) = true. +Proof. by auto. Qed. diff --git a/test-suite/ssr/intro_beta.v b/test-suite/ssr/intro_beta.v new file mode 100644 index 000000000..8a164bd80 --- /dev/null +++ b/test-suite/ssr/intro_beta.v @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Axiom T : Type. + +Definition C (P : T -> Prop) := forall x, P x. + +Axiom P : T -> T -> Prop. + +Lemma foo : C (fun x => forall y, let z := x in P y x). +move=> a b. +match goal with |- (let y := _ in _) => idtac end. +Admitted. diff --git a/test-suite/ssr/intro_noop.v b/test-suite/ssr/intro_noop.v new file mode 100644 index 000000000..fdc85173a --- /dev/null +++ b/test-suite/ssr/intro_noop.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. +Axiom daemon : False. Ltac myadmit := case: daemon. + +Lemma v : True -> bool -> bool. Proof. by []. Qed. + +Reserved Notation " a -/ b " (at level 0). +Reserved Notation " a -// b " (at level 0). +Reserved Notation " a -/= b " (at level 0). +Reserved Notation " a -//= b " (at level 0). + +Lemma test : forall a b c, a || b || c. +Proof. +move=> ---a--- - -/=- -//- -/=- -//=- b [|-]. +move: {-}a => /v/v-H; have _ := H I I. +Fail move: {-}a {H} => /v-/v-H. +have - -> : a = (id a) by []. +have --> : a = (id a) by []. +have - - _ : a = (id a) by []. +have -{1}-> : a = (id a) by []. + by myadmit. +move: a. +case: b => -[] //. +by myadmit. +Qed. diff --git a/test-suite/ssr/ipatalternation.v b/test-suite/ssr/ipatalternation.v new file mode 100644 index 000000000..6aa9a954c --- /dev/null +++ b/test-suite/ssr/ipatalternation.v @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Lemma test1 : Prop -> Prop -> Prop -> Prop -> Prop -> True = False -> Prop -> True \/ True. +by move=> A /= /= /= B C {A} {B} ? _ {C} {1}-> *; right. +Qed. diff --git a/test-suite/ssr/ltac_have.v b/test-suite/ssr/ltac_have.v new file mode 100644 index 000000000..380e52af4 --- /dev/null +++ b/test-suite/ssr/ltac_have.v @@ -0,0 +1,39 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Ltac SUFF1 h t := suff h x (p := x < 0) : t. +Ltac SUFF2 h t := suff h x (p := x < 0) : t by apply h. +Ltac HAVE1 h t u := have h x (p := x < 0) : t := u. +Ltac HAVE2 h t := have h x (p := x < 0) : t by []. +Ltac HAVE3 h t := have h x (p := x < 0) : t. +Ltac HAVES h t := have suff h : t. +Ltac SUFFH h t := suff have h : t. + +Lemma foo z : z < 0. +SUFF1 h1 (z+1 < 0). +Undo. +SUFF2 h2 (z < 0). +Undo. +HAVE1 h3 (z = z) (refl_equal z). +Undo. +HAVE2 h4 (z = z). +Undo. +HAVE3 h5 (z < 0). +Undo. +HAVES h6 (z < 1). +Undo. +SUFFH h7 (z < 1). +Undo. +Admitted. diff --git a/test-suite/ssr/ltac_in.v b/test-suite/ssr/ltac_in.v new file mode 100644 index 000000000..bcdf96dde --- /dev/null +++ b/test-suite/ssr/ltac_in.v @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +(* error 1 *) + +Ltac subst1 H := move: H; rewrite {1} addnC; move => H. +Ltac subst2 H := rewrite addnC in H. + +Goal ( forall a b: nat, b+a = 0 -> b+a=0). +Proof. move=> a b hyp. subst1 hyp. subst2 hyp. done. Qed. diff --git a/test-suite/ssr/move_after.v b/test-suite/ssr/move_after.v new file mode 100644 index 000000000..a7a9afea0 --- /dev/null +++ b/test-suite/ssr/move_after.v @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Goal True -> True -> True. +move=> H1 H2. +move H1 after H2. +Admitted. diff --git a/test-suite/ssr/multiview.v b/test-suite/ssr/multiview.v new file mode 100644 index 000000000..f4e717b38 --- /dev/null +++ b/test-suite/ssr/multiview.v @@ -0,0 +1,58 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Goal forall m n p, n <= p -> m <= n -> m <= p. +by move=> m n p le_n_p /leq_trans; apply. +Undo 1. +by move=> m n p le_n_p /leq_trans /(_ le_n_p) le_m_p; exact: le_m_p. +Undo 1. +by move=> m n p le_n_p /leq_trans ->. +Qed. + +Goal forall P Q X : Prop, Q -> (True -> X -> Q = P) -> X -> P. +by move=> P Q X q V /V <-. +Qed. + +Lemma test0: forall a b, a && a && b -> b. +by move=> a b; repeat move=> /andP []; move=> *. +Qed. + +Lemma test1 : forall a b, a && b -> b. +by move=> a b /andP /andP /andP [] //. +Qed. + +Lemma test2 : forall a b, a && b -> b. +by move=> a b /andP /andP /(@andP a) [] //. +Qed. + +Lemma test3 : forall a b, a && (b && b) -> b. +by move=> a b /andP [_ /andP [_ //]]. +Qed. + +Lemma test4: forall a b, a && b = b && a. +by move=> a b; apply/andP/andP=> ?; apply/andP/andP/andP; rewrite andbC; apply/andP. +Qed. + +Lemma test5: forall C I A O, (True -> O) -> (O -> A) -> (True -> A -> I) -> (I -> C) -> C. +by move=> c i a o O A I C; apply/C/I/A/O. +Qed. + +Lemma test6: forall A B, (A -> B) -> A -> B. +move=> A B A_to_B a; move/A_to_B in a; exact: a. +Qed. + +Lemma test7: forall A B, (A -> B) -> A -> B. +move=> A B A_to_B a; apply A_to_B in a; exact: a. +Qed. diff --git a/test-suite/ssr/occarrow.v b/test-suite/ssr/occarrow.v new file mode 100644 index 000000000..49af7ae08 --- /dev/null +++ b/test-suite/ssr/occarrow.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import TestSuite.ssr_mini_mathcomp. + +Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n. +move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-. +by move: E => {3}->. +Qed. + +Lemma test2 : forall n m : nat, True /\ (n = m -> n * n = n * m). +by move=> n m; constructor=> [|{2}->]. +Qed. diff --git a/test-suite/ssr/patnoX.v b/test-suite/ssr/patnoX.v new file mode 100644 index 000000000..d69f03ac3 --- /dev/null +++ b/test-suite/ssr/patnoX.v @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. +Goal forall x, x && true = x. +move=> x. +Fail (rewrite [X in _ && _]andbT). +Abort. diff --git a/test-suite/ssr/pattern.v b/test-suite/ssr/pattern.v new file mode 100644 index 000000000..396f4f032 --- /dev/null +++ b/test-suite/ssr/pattern.v @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssrmatching. + +(*Set Debug SsrMatching.*) + +Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) := + let name := fresh in + let def_name := fresh in + ssrpattern pat; + intro name; + pose proof (refl_equal name) as def_name; + unfold name at 1 in def_name; + t def_name; + [ rewrite <- def_name | idtac.. ]; + clear name def_name. + +Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4. +Proof. +at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place). +- reflexivity. +- trivial. +- trivial. +Qed. diff --git a/test-suite/ssr/primproj.v b/test-suite/ssr/primproj.v new file mode 100644 index 000000000..cf61eb436 --- /dev/null +++ b/test-suite/ssr/primproj.v @@ -0,0 +1,164 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + + + +Require Import Setoid. +Set Primitive Projections. + + +Module CoqBug. +Record foo A := Foo { foo_car : A }. + +Definition bar : foo _ := Foo nat 10. + +Variable alias : forall A, foo A -> A. + +Parameter e : @foo_car = alias. + +Goal foo_car _ bar = alias _ bar. +Proof. +(* Coq equally fails *) +Fail rewrite -> e. +Fail rewrite e at 1. +Fail setoid_rewrite e. +Fail setoid_rewrite e at 1. +Set Keyed Unification. +Fail rewrite -> e. +Fail rewrite e at 1. +Fail setoid_rewrite e. +Fail setoid_rewrite e at 1. +Admitted. + +End CoqBug. + +(* ----------------------------------------------- *) +Require Import ssreflect. + +Set Primitive Projections. + +Module T1. + +Record foo A := Foo { foo_car : A }. + +Definition bar : foo _ := Foo nat 10. + +Goal foo_car _ bar = 10. +Proof. +match goal with +| |- foo_car _ bar = 10 => idtac +end. +rewrite /foo_car. +(* +Fail match goal with +| |- foo_car _ bar = 10 => idtac +end. +*) +Admitted. + +End T1. + + +Module T2. + +Record foo {A} := Foo { foo_car : A }. + +Definition bar : foo := Foo nat 10. + +Goal foo_car bar = 10. +match goal with +| |- foo_car bar = 10 => idtac +end. +rewrite /foo_car. +(* +Fail match goal with +| |- foo_car bar = 10 => idtac +end. +*) +Admitted. + +End T2. + + +Module T3. + +Record foo {A} := Foo { foo_car : A }. + +Definition bar : foo := Foo nat 10. + +Goal foo_car bar = 10. +Proof. +rewrite -[foo_car _]/(id _). +match goal with |- id _ = 10 => idtac end. +Admitted. + +Goal foo_car bar = 10. +Proof. +set x := foo_car _. +match goal with |- x = 10 => idtac end. +Admitted. + +End T3. + +Module T4. + +Inductive seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. +Arguments unseal {_ _} _. +Arguments seal_eq {_ _} _. + +Record uPred : Type := IProp { uPred_holds :> Prop }. + +Definition uPred_or_def (P Q : uPred) : uPred := + {| uPred_holds := P \/ Q |}. +Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed. +Definition uPred_or := unseal uPred_or_aux. +Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux. + +Lemma foobar (P1 P2 Q : uPred) : + (P1 <-> P2) -> (uPred_or P1 Q) <-> (uPred_or P2 Q). +Proof. + rewrite uPred_or_eq. (* This fails. *) +Admitted. + +End T4. + + +Module DesignFlaw. + +Record foo A := Foo { foo_car : A }. +Definition bar : foo _ := Foo nat 10. + +Definition app (f : foo nat -> nat) x := f x. + +Goal app (foo_car _) bar = 10. +Proof. +unfold app. (* mkApp should produce a Proj *) +Fail set x := (foo_car _ _). +Admitted. + +End DesignFlaw. + + +Module Bug. + +Record foo A := Foo { foo_car : A }. + +Definition bar : foo _ := Foo nat 10. + +Variable alias : forall A, foo A -> A. + +Parameter e : @foo_car = alias. + +Goal foo_car _ bar = alias _ bar. +Proof. +Fail rewrite e. (* Issue: #86 *) +Admitted. + +End Bug. diff --git a/test-suite/ssr/rewpatterns.v b/test-suite/ssr/rewpatterns.v new file mode 100644 index 000000000..f7993f402 --- /dev/null +++ b/test-suite/ssr/rewpatterns.v @@ -0,0 +1,146 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + + +Require Import ssreflect. +Require Import ssrbool ssrfun TestSuite.ssr_mini_mathcomp. + +Lemma test1 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1). +by move=> x y f; rewrite [_.+1](addnC x.+1). +Qed. + +Lemma test2 : forall x y f, x + y + f (y + x) + f (y + x) = x + y + f (y + x) + f (x + y). +by move=> x y f; rewrite {2}[in f _]addnC. +Qed. + +Lemma test2' : forall x y f, true && f (x * (y + x)) = true && f(x * (x + y)). +by move=> x y f; rewrite [in f _](addnC y). +Qed. + +Lemma test2'' : forall x y f, f (y + x) + f(y + x) + f(y + x) = f(x + y) + f(y + x) + f(x + y). +by move=> x y f; rewrite {1 3}[in f _](addnC y). +Qed. + +(* patterns catching bound vars not supported *) +Lemma test2_1 : forall x y f, true && (let z := x in f (z * (y + x))) = true && f(x * (x + y)). +by move=> x y f; rewrite [in f _](addnC x). (* put y when bound var will be OK *) +Qed. + +Lemma test3 : forall x y f, x + f (x + y) (f (y + x) x) = x + f (x + y) (f (x + y) x). +by move=> x y f; rewrite [in X in (f _ X)](addnC y). +Qed. + +Lemma test3' : forall x y f, x = y -> x + f (x + x) x + f (x + x) x = + x + f (x + y) x + f (y + x) x. +by move=> x y f E; rewrite {2 3}[in X in (f X _)]E. +Qed. + +Lemma test3'' : forall x y f, x = y -> x + f (x + y) x + f (x + y) x = + x + f (x + y) x + f (y + y) x. +by move=> x y f E; rewrite {2}[in X in (f X _)]E. +Qed. + +Lemma test4 : forall x y f, x = y -> x + f (fun _ : nat => x + x) x + f (fun _ => x + x) x = + x + f (fun _ => x + y) x + f (fun _ => y + x) x. +by move=> x y f E; rewrite {2 3}[in X in (f X _)]E. +Qed. + +Lemma test4' : forall x y f, x = y -> x + f (fun _ _ _ : nat => x + x) x = + x + f (fun _ _ _ => x + y) x. +by move=> x y f E; rewrite {2}[in X in (f X _)]E. +Qed. + +Lemma test5 : forall x y f, x = y -> x + f (y + x) x + f (y + x) x = + x + f (x + y) x + f (y + x) x. +by move=> x y f E; rewrite {1}[X in (f X _)]addnC. +Qed. + +Lemma test3''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = + x + f (x + y) x + f (y + y) (x + y). +by move=> x y f E; rewrite {1}[in X in (f X X)]E. +Qed. + +Lemma test3'''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = + x + f (x + y) x + f (y + y) (y + y). +by move=> x y f E; rewrite [in X in (f X X)]E. +Qed. + +Lemma test3x : forall x y f, y+y = x+y -> x + f (x + y) x + f (x + y) (x + y) = + x + f (x + y) x + f (y + y) (y + y). +by move=> x y f E; rewrite -[X in (f X X)]E. +Qed. + +Lemma test6 : forall x y (f : nat -> nat), f (x + y).+1 = f (y.+1 + x). +by move=> x y f; rewrite [(x + y) in X in (f X)]addnC. +Qed. + +Lemma test7 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1). +by move=> x y f; rewrite [(x.+1 + y) as X in (f X)]addnC. +Qed. + +Lemma manual x y z (f : nat -> nat -> nat) : (x + y).+1 + f (x.+1 + y) (z + (x + y).+1) = 0. +Proof. +rewrite [in f _]addSn. +match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 => idtac end. +rewrite -[X in _ = X]addn0. +match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + 0 => idtac end. +rewrite -{2}[in X in _ = X](addn0 0). +match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + (0 + 0) => idtac end. +rewrite [_.+1 in X in f _ X](addnC x.+1). +match goal with |- (x + y).+1 + f (x + y).+1 (z + (y + x.+1)) = 0 + (0 + 0) => idtac end. +rewrite [x.+1 + y as X in f X _]addnC. +match goal with |- (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0) => idtac end. +Admitted. + +Goal (exists x : 'I_3, x > 0). +apply: (ex_intro _ (@Ordinal _ 2 _)). +Admitted. + +Goal (forall y, 1 < y < 2 -> exists x : 'I_3, x > 0). +move=> y; case/andP=> y_gt1 y_lt2; apply: (ex_intro _ (@Ordinal _ y _)). + by apply: leq_trans y_lt2 _. +by move=> y_lt3; apply: leq_trans _ y_gt1. +Qed. + +Goal (forall x y : nat, forall P : nat -> Prop, x = y -> True). +move=> x y P E. +have: P x -> P y by suff: x = y by move=> ?; congr (P _). +Admitted. + +Goal forall a : bool, a -> true && a || false && a. +by move=> a ?; rewrite [true && _]/= [_ && a]/= orbC [_ || _]//=. +Qed. + +Goal forall a : bool, a -> true && a || false && a. +by move=> a ?; rewrite [X in X || _]/= [X in _ || X]/= orbC [false && a as X in X || _]//=. +Qed. + +Variable a : bool. +Definition f x := x || a. +Definition g x := f x. + +Goal a -> g false. +by move=> Ha; rewrite [g _]/f orbC Ha. +Qed. + +Goal a -> g false || g false. +move=> Ha; rewrite {2}[g _]/f orbC Ha. +match goal with |- (is_true (false || true || g false)) => done end. +Qed. + +Goal a -> (a && a || true && a) && true. +by move=> Ha; rewrite -[_ || _]/(g _) andbC /= Ha [g _]/f. +Qed. + +Goal a -> (a || a) && true. +by move=> Ha; rewrite -[in _ || _]/(f _) Ha andbC /f. +Qed. diff --git a/test-suite/ssr/set_lamda.v b/test-suite/ssr/set_lamda.v new file mode 100644 index 000000000..a012ec680 --- /dev/null +++ b/test-suite/ssr/set_lamda.v @@ -0,0 +1,27 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool ssrfun. +Require Import TestSuite.ssr_mini_mathcomp. + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +(* error 2 *) + +Goal (exists f: Set -> nat, f nat = 0). +Proof. set (f:= fun _:Set =>0). by exists f. Qed. + +Goal (exists f: Set -> nat, f nat = 0). +Proof. set f := (fun _:Set =>0). by exists f. Qed. diff --git a/test-suite/ssr/set_pattern.v b/test-suite/ssr/set_pattern.v new file mode 100644 index 000000000..3ce75e879 --- /dev/null +++ b/test-suite/ssr/set_pattern.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end. +Ltac T2 x := first [set t := (x in RHS)]. +Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac]. +Ltac T4 x := set t := (x in RHS); idtac. +Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end. + +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Open Scope nat_scope. + +Lemma foo x y : x.+1 = y + x.+1. +set t := (_.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end. +set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. +set t := (x in _ = x). match goal with |- x.+1 = t => rewrite /t {t} end. +set t := (x in X in _ = X). + match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. +set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. +set t := (y + (1 + x) as X in _ = X). + match goal with |- x.+1 = t => rewrite /t addSn add0n {t} end. +set t := x.+1. match goal with |- t = y + t => rewrite /t {t} end. +set t := (x).+1. match goal with |- t = y + t => rewrite /t {t} end. +set t := ((x).+1 in X in _ = X). + match goal with |- x.+1 = y + t => rewrite /t {t} end. +set t := (x.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end. +T1 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. +T2 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. +T3 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. +T4 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. +T5 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end. +rewrite [RHS]addnC. + match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end. +rewrite -[in RHS](@subnK 1 x.+1) //. + match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end. +have H : x.+1 = y by myadmit. +set t := _.+1 in H |- *. + match goal with H : t = y |- t = y + t => rewrite /t {t} in H * end. +set t := (_.+1 in X in _ + X) in H |- *. + match goal with H : x.+1 = y |- x.+1 = y + t => rewrite /t {t} in H * end. +set t := 0. match goal with t := 0 |- x.+1 = y + x.+1 => clear t end. +set t := y + _. match goal with |- x.+1 = t => rewrite /t {t} end. +set t : nat := 0. clear t. +set t : nat := (x in RHS). + match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end. +set t : nat := RHS. match goal with |- x.+1 = t => rewrite /t {t} end. +(* set t := 0 + _. *) +(* set t := (x).+1 in X in _ + X in H |-. *) +(* set t := (x).+1 in X in _ = X.*) +Admitted. diff --git a/test-suite/ssr/ssrsyntax2.v b/test-suite/ssr/ssrsyntax2.v new file mode 100644 index 000000000..af839fabd --- /dev/null +++ b/test-suite/ssr/ssrsyntax2.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import TestSuite.ssr_ssrsyntax1. +Require Import Arith. + +Goal (forall a b, a + b = b + a). +intros. +rewrite plus_comm, plus_comm. +split. +Qed. diff --git a/test-suite/ssr/tc.v b/test-suite/ssr/tc.v new file mode 100644 index 000000000..ae4589ef3 --- /dev/null +++ b/test-suite/ssr/tc.v @@ -0,0 +1,39 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + + +Class foo (A : Type) : Type := mkFoo { val : A }. +Instance foo_pair {A B} {f1 : foo A} {f2 : foo B} : foo (A * B) | 2 := + {| val := (@val _ f1, @val _ f2) |}. +Instance foo_nat : foo nat | 3 := {| val := 0 |}. + +Definition id {A} (x : A) := x. +Axiom E : forall A {f : foo A} (a : A), id a = (@val _ f). + +Lemma test (x : nat) : id true = true -> id x = 0. +Proof. +Fail move=> _; reflexivity. +Timeout 2 rewrite E => _; reflexivity. +Qed. + +Definition P {A} (x : A) : Prop := x = x. +Axiom V : forall A {f : foo A} (x:A), P x -> P (id x). + +Lemma test1 (x : nat) : P x -> P (id x). +Proof. +move=> px. +Timeout 2 Fail move/V: px. +Timeout 2 move/V : (px) => _. +move/(V nat) : px => H; exact H. +Qed. diff --git a/test-suite/ssr/typeof.v b/test-suite/ssr/typeof.v new file mode 100644 index 000000000..ca121fdb3 --- /dev/null +++ b/test-suite/ssr/typeof.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. + +Ltac mycut x := + let tx := type of x in + cut tx. + +Lemma test : True. +Proof. +by mycut I=> [ x | ]; [ exact x | exact I ]. +Qed. diff --git a/test-suite/ssr/unfold_Opaque.v b/test-suite/ssr/unfold_Opaque.v new file mode 100644 index 000000000..7c2b51de4 --- /dev/null +++ b/test-suite/ssr/unfold_Opaque.v @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssreflect. + +Definition x := 3. +Opaque x. + +Goal x = 3. +Fail rewrite /x. +Admitted. diff --git a/test-suite/ssr/unkeyed.v b/test-suite/ssr/unkeyed.v new file mode 100644 index 000000000..710941c30 --- /dev/null +++ b/test-suite/ssr/unkeyed.v @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp. + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Lemma test0 (a b : unit) f : a = f b. +Proof. by rewrite !unitE. Qed. + +Lemma phE T : all_equal_to (Phant T). Proof. by case. Qed. + +Lemma test1 (a b : phant nat) f : a = f b. +Proof. by rewrite !phE. Qed. + +Lemma eq_phE (T : eqType) : all_equal_to (Phant T). Proof. by case. Qed. + +Lemma test2 (a b : phant bool) f : a = locked (f b). +Proof. by rewrite !eq_phE. Qed. diff --git a/test-suite/ssr/view_case.v b/test-suite/ssr/view_case.v new file mode 100644 index 000000000..2721470c4 --- /dev/null +++ b/test-suite/ssr/view_case.v @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Axiom P : forall T, seq T -> Prop. + +Goal (forall T (s : seq T), P _ s). +move=> T s. +elim: s => [| x /lastP [| s] IH]. +Admitted. + +Goal forall x : 'I_1, x = 0 :> nat. +move=> /ord1 -> /=; exact: refl_equal. +Qed. + +Goal forall x : 'I_1, x = 0 :> nat. +move=> x. +move=> /ord1 -> in x |- *. +exact: refl_equal. +Qed. diff --git a/test-suite/ssr/wlog_suff.v b/test-suite/ssr/wlog_suff.v new file mode 100644 index 000000000..43a8f3b8b --- /dev/null +++ b/test-suite/ssr/wlog_suff.v @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. + +Lemma test b : b || ~~b. +wlog _ : b / b = true. + case: b; [ by apply | by rewrite orbC ]. +wlog suff: b / b || ~~b. + by case: b. +by case: b. +Qed. + +Lemma test2 b c (H : c = b) : b || ~~b. +wlog _ : b {c H} / b = true. + by case: b H. +by case: b. +Qed. diff --git a/test-suite/ssr/wlogletin.v b/test-suite/ssr/wlogletin.v new file mode 100644 index 000000000..64e1ea84f --- /dev/null +++ b/test-suite/ssr/wlogletin.v @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. +Require Import TestSuite.ssr_mini_mathcomp. + +Variable T : Type. +Variables P : T -> Prop. + +Definition f := fun x y : T => x. + +Lemma test1 : forall x y : T, P (f x y) -> P x. +Proof. +move=> x y; set fxy := f x y; move=> Pfxy. +wlog H : @fxy Pfxy / P x. + match goal with |- (let fxy0 := f x y in P fxy0 -> P x -> P x) -> P x => by auto | _ => fail end. +exact: H. +Qed. + +Lemma test2 : forall x y : T, P (f x y) -> P x. +Proof. +move=> x y; set fxy := f x y; move=> Pfxy. +wlog H : fxy Pfxy / P x. + match goal with |- (forall fxy, P fxy -> P x -> P x) -> P x => by auto | _ => fail end. +exact: H. +Qed. + +Lemma test3 : forall x y : T, P (f x y) -> P x. +Proof. +move=> x y; set fxy := f x y; move=> Pfxy. +move: {1}@fxy (Pfxy) (Pfxy). +match goal with |- (let fxy0 := f x y in P fxy0 -> P fxy -> P x) => by auto | _ => fail end. +Qed. + +Lemma test4 : forall n m z: bool, n = z -> let x := n in x = m && n -> x = m && n. +move=> n m z E x H. +case: true. + by rewrite {1 2}E in (x) H |- *. +by rewrite {1}E in x H |- *. +Qed. diff --git a/test-suite/ssr/wlong_intro.v b/test-suite/ssr/wlong_intro.v new file mode 100644 index 000000000..dd80f0435 --- /dev/null +++ b/test-suite/ssr/wlong_intro.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool. +Require Import TestSuite.ssr_mini_mathcomp. + +Goal (forall x y : nat, True). +move=> x y. +wlog suff: x y / x <= y. +Admitted. |