diff options
36 files changed, 766 insertions, 615 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 46f8572b94..492b658d98 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -337,6 +337,9 @@ ci-fcsl-pcm: ci-fiat-crypto: <<: *ci-template-flambda +ci-fiat-crypto-legacy: + <<: *ci-template-flambda + ci-fiat-parsers: <<: *ci-template @@ -48,6 +48,12 @@ Tactics may need to add `Require Import Lra` to your developments. For compatibility, we now define `fourier` as a deprecated alias of `lra`. +Focusing + +- Focusing bracket `{` now supports named goal selectors, + e.g. `[x]: {` will focus on a goal (existential variable) named `x`. + As usual, unfocus with `}` once the sub-goal is fully solved. + Standard Library - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them, @@ -76,6 +82,11 @@ Tools please open an issue. We can help set up external maintenance as part of Proof-General, or independently as part of coq-community. +- The targets `print-pretty-timed`, `print-pretty-timed-diff`, and + `print-pretty-single-time-diff` now correctly label the "before" and + "after" columns, rather than swapping them. + + Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments @@ -81,7 +81,7 @@ export ML4FILES := $(call find, '*.ml4') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') -export MERLININFILES := $(call find, '.merlin.in') +MERLININFILES := $(call find, '.merlin.in') export MERLINFILES := $(MERLININFILES:.in=) # NB: The lists of currently existing .ml and .mli files will change @@ -116,7 +116,7 @@ include Makefile.common NOARG: world -.PHONY: NOARG help noconfig submake +.PHONY: NOARG help noconfig submake camldevfiles help: @echo "Please use either:" @@ -143,12 +143,13 @@ Then, you may want to consider whether you want to restore the autosaves) #run. endif -# Apart from clean and tags, everything will be done in a sub-call to make -# on Makefile.build. This way, we avoid doing here the -include of .d : -# since they trigger some compilations, we do not want them for a mere clean. -# Moreover, we regroup this sub-call in a common target named 'submake'. -# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't -# trigger multiple (possibly parallel) make sub-calls +# Apart from clean and a few misc files, everything will be done in a +# sub-call to make on Makefile.build. This way, we avoid doing here +# the -include of .d : since they trigger some compilations, we do not +# want them for a mere clean. Moreover, we regroup this sub-call in a +# common target named 'submake'. This way, multiple user-given goals +# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly +# parallel) make sub-calls ifdef COQ_CONFIGURED %:: submake ; @@ -161,7 +162,7 @@ MAKE_OPTS := --warn-undefined-variable --no-builtin-rules bin: mkdir bin -submake: alienclean | bin +submake: alienclean camldevfiles | bin $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) noconfig: @@ -172,6 +173,20 @@ noconfig: Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### +# OCaml dev files +########################################################################### +camldevfiles: $(MERLINFILES) META.coq + +.merlin: .merlin.in + cp -a "$<" "$@" + +%/.merlin: %/.merlin.in + cp -a "$<" "$@" + +META.coq: META.coq.in + cp -a "$<" "$@" + +########################################################################### # Cleaning ########################################################################### diff --git a/Makefile.build b/Makefile.build index 05633cecc8..c100eda400 100644 --- a/Makefile.build +++ b/Makefile.build @@ -64,7 +64,7 @@ AFTER ?= # build the different subsystems: -world: camldevfiles coq coqide documentation revision +world: coq coqide documentation revision coq: coqlib coqbinaries tools diff --git a/Makefile.ci b/Makefile.ci index fce16906c4..306471d1d0 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -22,6 +22,7 @@ CI_TARGETS=ci-bedrock2 \ ci-equations \ ci-fcsl-pcm \ ci-fiat-crypto \ + ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ ci-formal-topology \ diff --git a/Makefile.dev b/Makefile.dev index ea1a3d40a2..68e96a57b7 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,7 +15,7 @@ # Debug printers in dev/ ######################### -.PHONY: devel printers camldevfiles +.PHONY: devel printers DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo @@ -85,20 +85,6 @@ endif # But these partial targets could be quite handy for quick builds # of specific components of Coq. -########################################################################### -# OCaml dev files -########################################################################### -camldevfiles: $(MERLINFILES) META.coq - -.merlin: .merlin.in - cp -a "$<" "$@" - -%/.merlin: %/.merlin.in - cp -a "$<" "$@" - -META.coq: META.coq.in - cp -a "$<" "$@" - ############################### ### 1) general-purpose targets ############################### diff --git a/clib/cList.ml b/clib/cList.ml index de42886dcb..dc59ff2970 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -60,6 +60,7 @@ sig val extend : bool list -> 'a -> 'a list -> 'a list val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int + val safe_index : 'a eq -> 'a -> 'a list -> int option val index0 : 'a eq -> 'a -> 'a list -> int val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b @@ -538,6 +539,8 @@ let rec index_f f x l n = match l with let index f x l = index_f f x l 1 +let safe_index f x l = try Some (index f x l) with Not_found -> None + let index0 f x l = index_f f x l 0 (** {6 Folding} *) diff --git a/clib/cList.mli b/clib/cList.mli index 42fae5ed39..ed468cb977 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -155,6 +155,10 @@ sig val index : 'a eq -> 'a -> 'a list -> int (** [index] returns the 1st index of an element in a list (counting from 1). *) + val safe_index : 'a eq -> 'a -> 'a list -> int option + (** [safe_index] returns the 1st index of an element in a list (counting from 1) + and None otherwise. *) + val index0 : 'a eq -> 'a -> 'a list -> int (** [index0] behaves as [index] except that it starts counting at 0. *) diff --git a/configure.ml b/configure.ml index 7fd900d995..7e0fd4c8ac 100644 --- a/configure.ml +++ b/configure.ml @@ -1214,8 +1214,8 @@ let write_configml f = pr_s "browser" browser; pr_s "wwwcoq" !prefs.coqwebsite; pr_s "wwwbugtracker" (!prefs.coqwebsite ^ "bugs/"); - pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); - pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); + pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/refman/"); + pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "bytecode_compiler" !prefs.bytecodecompiler; pr_b "native_compiler" !prefs.nativecompiler; diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh new file mode 100755 index 0000000000..9429344159 --- /dev/null +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" + +git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" + +( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) + +fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" +fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" +( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 48a1366aba..c6d2f0cfd9 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -9,6 +9,7 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) -fiat_crypto_CI_TARGETS1="printlite lite lite-display" -fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) +# We need a larger stack size to not overflow ocamlopt+flambda when +# building the executables. +# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +( cd "${fiat_crypto_CI_DIR}" && ulimit -s 32768 && make new-pipeline c-files ) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index a63400103f..b0ba2bcc31 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -781,7 +781,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is .. coqtop:: in - Inductive even : nat -> prop := + Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) with odd : nat -> prop := diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 88da58c27d..4e42bddee2 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -90,8 +90,8 @@ not set, they look for the commands in the executable path. The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated -list of assignments of the form ``name=``:n:``{*; attr}`` where -``name`` is the name of the corresponding highlight tag and each ``attrᵢ`` is an +list of assignments of the form :n:`name={*; attr}` where +``name`` is the name of the corresponding highlight tag and each ``attr`` is an ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index e9aacba3a5..b49d0f0504 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -329,20 +329,47 @@ Navigation in the proof tree .. cmdv:: @num: %{ - This focuses on the :token:`num` th subgoal to prove. + This focuses on the :token:`num`\-th subgoal to prove. - Error messages: + .. cmdv:: [@ident]: %{ + + This focuses on the named goal :token:`ident`. + + .. note:: + + Goals are just existential variables and existential variables do not + get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + + .. seealso:: :ref:`existential-variables` + + .. example:: + + This can also be a way of focusing on a shelved goal, for instance: + + .. coqtop:: all + + Goal exists n : nat, n = n. + eexists ?[x]. + reflexivity. + [x]: exact 0. + Qed. .. exn:: This proof is focused, but cannot be unfocused this way. You are trying to use ``}`` but the current subproof has not been fully solved. - .. exn:: No such goal. - :name: No such goal. (Focusing) + .. exn:: No such goal (@num). + :undocumented: + + .. exn:: No such goal (@ident). + :undocumented: + + .. exn:: Brackets do not support multi-goal selectors. - .. exn:: Brackets only support the single numbered goal selector. + Brackets are used to focus on a single goal given either by its position + or by its name if it has one. - See also error messages about bullets below. + .. seealso:: The error messages about bullets below. .. _bullets: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fdb04bf9a0..fcb52cf275 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -113,26 +113,26 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: -.. _tactic_occurence_grammar: - .. productionlist:: `sentence` - occurence_clause : in `goal_occurences` - goal_occurences : [ident [`at_occurences`], ... , ident [`at_occurences`] [|- [* [`at_occurences`]]]] - :| * |- [* [`at_occurences`]] + occurrence_clause : in `goal_occurrences` + goal_occurrences : [`ident` [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]] + :| * |- [* [`at_occurrences`]] :| * at_occurrences : at `occurrences` - occurences : [-] `num` ... `num` - -The role of an occurrence clause is to select a set of occurrences of a term in -a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that -occurrences have to be selected in the hypotheses named :n:`@ident`. If no -numbers are given for hypothesis :n:`@ident`, then all the occurrences of `term` -in the hypothesis are selected. If numbers are given, they refer to occurrences -of `term` when the term is printed using option :opt:`Printing All`, counting -from left to right. In particular, occurrences of `term` in implicit arguments -(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. - -If a minus sign is given between at and the list of occurrences, it + occurrences : [-] `num` ... `num` + +The role of an occurrence clause is to select a set of occurrences of a term +in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate +that occurrences have to be selected in the hypotheses named :token:`ident`. +If no numbers are given for hypothesis :token:`ident`, then all the +occurrences of :token:`term` in the hypothesis are selected. If numbers are +given, they refer to occurrences of :token:`term` when the term is printed +using option :opt:`Printing All`, counting from left to right. In particular, +occurrences of :token:`term` in implicit arguments +(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are +counted. + +If a minus sign is given between ``at`` and the list of occurrences, it negates the condition so that the clause denotes all the occurrences except the ones explicitly mentioned after the minus sign. @@ -146,18 +146,20 @@ of term are selected in every hypothesis. In the first and second case, if ``*`` is mentioned on the right of ``|-``, the occurrences of the conclusion of the goal have to be selected. If some numbers are given, then only the occurrences denoted by these numbers are selected. If -no numbers are given, all occurrences of :n:`@term` in the goal are selected. +no numbers are given, all occurrences of :token:`term` in the goal are selected. Finally, the last notation is an abbreviation for ``* |- *``. Note also that ``|-`` is optional in the first case when no ``*`` is given. -Here are some tactics that understand occurrence clauses: :tacn:`set`, :tacn:`remember` -, :tacn:`induction`, :tacn:`destruct`. +Here are some tactics that understand occurrence clauses: :tacn:`set`, +:tacn:`remember`, :tacn:`induction`, :tacn:`destruct`. + +.. seealso:: + + :ref:`Managingthelocalcontext`, :ref:`caseanalysisandinduction`, + :ref:`printing_constructions_full`. -See also: :ref:`Managingthelocalcontext`, -:ref:`caseanalysisandinduction`, -:ref:`printing_constructions_full`. .. _applyingtheorems: @@ -173,35 +175,39 @@ Applying theorems :ref:`Conversion-rules`). .. exn:: Not an exact proof. + :undocumented: .. tacv:: eexact @term. :name: eexact - This tactic behaves like exact but is able to handle terms and goals with - meta-variables. + This tactic behaves like :tacn:`exact` but is able to handle terms and + goals with existential variables. .. tacn:: assumption :name: assumption - This tactic looks in the local context for an hypothesis which type is equal to - the goal. If it is the case, the subgoal is proved. Otherwise, it fails. + This tactic looks in the local context for an hypothesis whose type is + convertible to the goal. If it is the case, the subgoal is proved. + Otherwise, it fails. .. exn:: No such assumption. + :undocumented: .. tacv:: eassumption :name: eassumption - This tactic behaves like assumption but is able to handle goals with - meta-variables. + This tactic behaves like :tacn:`assumption` but is able to handle + goals with existential variables. .. tacn:: refine @term :name: refine This tactic applies to any goal. It behaves like :tacn:`exact` with a big - difference: the user can leave some holes (denoted by ``_`` or ``(_:type)``) in - the term. :tacn:`refine` will generate as many subgoals as there are holes in - the term. The type of holes must be either synthesized by the system - or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that + difference: the user can leave some holes (denoted by ``_`` + or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many + subgoals as there are holes in the term. The type of holes must be either + synthesized by the system or declared by an explicit cast + like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling :tacn:`shelve_unifiable`. This low-level tactic can be useful to advanced users. @@ -215,16 +221,13 @@ Applying theorems | Ok : bool -> Option. Definition get : forall x:Option, x <> Fail -> bool. - - refine - (fun x:Option => - match x return x <> Fail -> bool with - | Fail => _ - | Ok b => fun _ => b - end). - - intros; absurd (Fail = Fail); trivial. - + refine + (fun x:Option => + match x return x <> Fail -> bool with + | Fail => _ + | Ok b => fun _ => b + end). + intros; absurd (Fail = Fail); trivial. Defined. .. exn:: Invalid argument. @@ -264,29 +267,31 @@ Applying theorems .. tacn:: apply @term :name: apply - This tactic applies to any goal. The argument term is a term well-formed in the - local context. The tactic apply tries to match the current goal against the - conclusion of the type of term. If it succeeds, then the tactic returns as many - subgoals as the number of non-dependent premises of the type of term. If the - conclusion of the type of term does not match the goal *and* the conclusion is - an inductive type isomorphic to a tuple type, then each component of the tuple - is recursively matched to the goal in the left-to-right order. - - The tactic :tacn:`apply` relies on first-order unification with dependent types - unless the conclusion of the type of :token:`term` is of the form :g:`P (t`:sub:`1` - :g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior - depends on the form of the goal. If the goal is of the form - :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and - :g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, - :tacn:`apply` tries to define :g:`P` by abstracting over :g:`t`:sub:`1` :g:`...` - :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it - gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. + This tactic applies to any goal. The argument term is a term well-formed in + the local context. The tactic :tacn:`apply` tries to match the current goal + against the conclusion of the type of :token:`term`. If it succeeds, then + the tactic returns as many subgoals as the number of non-dependent premises + of the type of term. If the conclusion of the type of :token:`term` does + not match the goal *and* the conclusion is an inductive type isomorphic to + a tuple type, then each component of the tuple is recursively matched to + the goal in the left-to-right order. + + The tactic :tacn:`apply` relies on first-order unification with dependent + types unless the conclusion of the type of :token:`term` is of the form + :n:`P (t__1 ... t__n)` with ``P`` to be instantiated. In the latter case, + the behavior depends on the form of the goal. If the goal is of the form + :n:`(fun x => Q) u__1 ... u__n` and the :n:`t__i` and :n:`u__i` unify, + then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, :tacn:`apply` + tries to define :g:`P` by abstracting over :g:`t_1 ... t__n` in the goal. + See :tacn:`pattern` to transform the goal so that it + gets the form :n:`(fun x => Q) u__1 ... u__n`. .. exn:: Unable to unify @term with @term. - The apply tactic failed to match the conclusion of :token:`term` and the - current goal. You can help the apply tactic by transforming your goal with - the :tacn:`change` or :tacn:`pattern` tactics. + The :tacn:`apply` tactic failed to match the conclusion of :token:`term` + and the current goal. You can help the :tacn:`apply` tactic by + transforming your goal with the :tacn:`change` or :tacn:`pattern` + tactics. .. exn:: Unable to find an instance for the variables {+ @ident}. @@ -302,6 +307,7 @@ Applying theorems according to the order of these dependent premises of the type of term. .. exn:: Not the right number of missing arguments. + :undocumented: .. tacv:: apply @term with @bindings_list @@ -311,11 +317,9 @@ Applying theorems .. tacv:: apply {+, @term} - This is a shortcut for :n:`apply @term`:sub:`1` - :n:`; [.. | ... ; [ .. | apply @term`:sub:`n` :n:`] ... ]`, - i.e. for the successive applications of :token:`term`:sub:`i+1` on the last subgoal - generated by :n:`apply @term`:sub:`i` , starting from the application of - :token:`term`:sub:`1`. + This is a shortcut for :n:`apply @term__1; [.. | ... ; [ .. | apply @term__n] ... ]`, + i.e. for the successive applications of :n:`@term`:sub:`i+1` on the last subgoal + generated by :n:`apply @term__i` , starting from the application of :n:`@term__1`. .. tacv:: eapply @term :name: eapply @@ -327,7 +331,6 @@ Applying theorems intended to be found later in the proof. .. tacv:: simple apply @term. - :name: simple apply This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example @@ -349,8 +352,8 @@ Applying theorems does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} - .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} - :name: simple eapply + {? simple} eapply {+, @term {? with @bindings_list}} + :name: simple apply; simple eapply This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`. @@ -365,6 +368,7 @@ Applying theorems sequence ``cut B. 2:apply H.`` where ``cut`` is described below. .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. + :undocumented: .. example:: @@ -455,164 +459,151 @@ Applying theorems .. tacn:: apply @term in @ident :name: apply ... in - This tactic applies to any goal. The argument ``term`` is a term well-formed in - the local context and the argument :n:`@ident` is an hypothesis of the context. - The tactic ``apply term in ident`` tries to match the conclusion of the type - of :n:`@ident` against a non-dependent premise of the type of ``term``, trying - them from right to left. If it succeeds, the statement of hypothesis - :n:`@ident` is replaced by the conclusion of the type of ``term``. The tactic - also returns as many subgoals as the number of other non-dependent premises - in the type of ``term`` and of the non-dependent premises of the type of - :n:`@ident`. If the conclusion of the type of ``term`` does not match the goal - *and* the conclusion is an inductive type isomorphic to a tuple type, then + This tactic applies to any goal. The argument :token:`term` is a term + well-formed in the local context and the argument :token:`ident` is an + hypothesis of the context. + The tactic :n:`apply @term in @ident` tries to match the conclusion of the + type of :token:`ident` against a non-dependent premise of the type + of :token:`term`, trying them from right to left. If it succeeds, the + statement of hypothesis :token:`ident` is replaced by the conclusion of + the type of :token:`term`. The tactic also returns as many subgoals as the + number of other non-dependent premises in the type of :token:`term` and of + the non-dependent premises of the type of :token:`ident`. If the conclusion + of the type of :token:`term` does not match the goal *and* the conclusion + is an inductive type isomorphic to a tuple type, then the tuple is (recursively) decomposed and the first component of the tuple of which a non-dependent premise matches the conclusion of the type of - :n:`@ident`. Tuples are decomposed in a width-first left-to-right order (for - instance if the type of :g:`H1` is :g:`A <-> B` and the type of - :g:`H2` is :g:`A` then ``apply H1 in H2`` transforms the type of :g:`H2` - into :g:`B`). The tactic ``apply`` relies on first-order pattern-matching + :token:`ident`. Tuples are decomposed in a width-first left-to-right order + (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of + :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2` + into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern-matching with dependent types. -.. exn:: Statement without assumptions. - - This happens if the type of ``term`` has no non dependent premise. - -.. exn:: Unable to apply. + .. exn:: Statement without assumptions. - This happens if the conclusion of :n:`@ident` does not match any of the non - dependent premises of the type of ``term``. + This happens if the type of :token:`term` has no non-dependent premise. -.. tacv:: apply {+, @term} in @ident + .. exn:: Unable to apply. - This applies each of ``term`` in sequence in :n:`@ident`. + This happens if the conclusion of :token:`ident` does not match any of + the non-dependent premises of the type of :token:`term`. -.. tacv:: apply {+, @term with @bindings_list} in @ident + .. tacv:: apply {+, @term} in @ident - This does the same but uses the bindings in each :n:`(@id := @ val)` to - instantiate the parameters of the corresponding type of ``term`` (see - :ref:`bindings list <bindingslist>`). + This applies each :token:`term` in sequence in :token:`ident`. -.. tacv:: eapply {+, @term with @bindings_list} in @ident + .. tacv:: apply {+, @term with @bindings_list} in @ident - This works as :tacn:`apply ... in` but turns unresolved bindings into - existential variables, if any, instead of failing. + This does the same but uses the bindings in each :n:`(@ident := @term)` to + instantiate the parameters of the corresponding type of :token:`term` + (see :ref:`bindings list <bindingslist>`). -.. tacv:: apply {+, @term with @bindings_list} in @ident as @intro_pattern - :name: apply ... in ... as + .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident - This works as :tacn:`apply ... in` then applies the - :n:`@intro_pattern` to the hypothesis :n:`@ident`. + This works as :tacn:`apply ... in` but turns unresolved bindings into + existential variables, if any, instead of failing. -.. tacv:: eapply {+, @term with @bindings_list} in @ident as @intro_pattern. + .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @intro_pattern + :name: apply ... in ... as - This works as :tacn:`apply ... in ... as` but using ``eapply``. + This works as :tacn:`apply ... in` then applies the :token:`intro_pattern` + to the hypothesis :token:`ident`. -.. tacv:: simple apply @term in @ident + .. tacv:: simple apply @term in @ident - This behaves like :tacn:`apply ... in` but it reasons modulo conversion only - on subterms that contain no variables to instantiate. For instance, if - :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and - :g:`H0 : O = O` then ``simple apply H in H0`` does not succeed because it - would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is - an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not - either traverse tuples as :n:`apply @term in @ident` does. + This behaves like :tacn:`apply ... in` but it reasons modulo conversion + only on subterms that contain no variables to instantiate. For instance, + if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and + :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it + would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is + an existential variable to instantiate. + Tactic :n:`simple apply @term in @ident` does not + either traverse tuples as :n:`apply @term in @ident` does. -.. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} -.. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} + .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} + {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - This summarizes the different syntactic variants of :n:`apply @term in @ident` - and :n:`eapply @term in @ident`. + This summarizes the different syntactic variants of :n:`apply @term in @ident` + and :n:`eapply @term in @ident`. .. tacn:: constructor @num :name: constructor This tactic applies to a goal such that its conclusion is an inductive - type (say :g:`I`). The argument :n:`@num` must be less or equal to the - numbers of constructor(s) of :g:`I`. Let :g:`c`:sub:`i` be the i-th - constructor of :g:`I`, then ``constructor i`` is equivalent to - ``intros; apply c``:sub:`i`. + type (say :g:`I`). The argument :token:`num` must be less or equal to the + numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th + constructor of :g:`I`, then :g:`constructor i` is equivalent to + :n:`intros; apply c__i`. -.. exn:: Not an inductive product. -.. exn:: Not enough constructors. - -.. tacv:: constructor - - This tries :g:`constructor`:sub:`1` then :g:`constructor`:sub:`2`, ..., then - :g:`constructor`:sub:`n` where `n` is the number of constructors of the head - of the goal. - -.. tacv:: constructor @num with @bindings_list + .. exn:: Not an inductive product. + :undocumented: - Let ``c`` be the i-th constructor of :g:`I`, then - :n:`constructor i with @bindings_list` is equivalent to - :n:`intros; apply c with @bindings_list`. + .. exn:: Not enough constructors. + :undocumented: - .. warn:: - The terms in the @bindings_list are checked in the context where constructor is executed and not in the context where @apply is executed (the introductions are not taken into account). + .. tacv:: constructor -.. tacv:: split - :name: split + This tries :g:`constructor 1` then :g:`constructor 2`, ..., then + :g:`constructor n` where ``n`` is the number of constructors of the head + of the goal. - This applies only if :g:`I` has a single constructor. It is then - equivalent to :n:`constructor 1.`. It is typically used in the case of a - conjunction :g:`A` :math:`\wedge` :g:`B`. + .. tacv:: constructor @num with @bindings_list -.. exn:: Not an inductive goal with 1 constructor + Let ``c`` be the i-th constructor of :g:`I`, then + :n:`constructor i with @bindings_list` is equivalent to + :n:`intros; apply c with @bindings_list`. -.. tacv:: exists @val - :name: exists - - This applies only if :g:`I` has a single constructor. It is then equivalent - to :n:`intros; constructor 1 with @bindings_list.` It is typically used in - the case of an existential quantification :math:`\exists`:g:`x, P(x).` - -.. exn:: Not an inductive goal with 1 constructor. - -.. tacv:: exists @bindings_list + .. warning:: - This iteratively applies :n:`exists @bindings_list`. + The terms in the :token:`bindings_list` are checked in the context + where constructor is executed and not in the context where :tacn:`apply` + is executed (the introductions are not taken into account). -.. tacv:: left - :name: left + .. tacv:: split {? with @bindings_list } + :name: split -.. tacv:: right - :name: right + This applies only if :g:`I` has a single constructor. It is then + equivalent to :n:`constructor 1 {? with @bindings_list }`. It is + typically used in the case of a conjunction :math:`A \wedge B`. - These tactics apply only if :g:`I` has two constructors, for - instance in the case of a disjunction :g:`A` :math:`\vee` :g:`B`. - Then, they are respectively equivalent to ``constructor 1`` and - ``constructor 2``. + .. tacv:: exists @bindings_list + :name: exists -.. exn:: Not an inductive goal with 2 constructors. + This applies only if :g:`I` has a single constructor. It is then equivalent + to :n:`intros; constructor 1 with @bindings_list.` It is typically used in + the case of an existential quantification :math:`\exists x, P(x).` -.. tacv:: left with @bindings_list -.. tacv:: right with @bindings_list -.. tacv:: split with @bindings_list + .. tacv:: exists {+, @bindings_list } - As soon as the inductive type has the right number of constructors, these - expressions are equivalent to calling :n:`constructor i with @bindings_list` - for the appropriate ``i``. + This iteratively applies :n:`exists @bindings_list`. -.. tacv:: econstructor - :name: econstructor + .. exn:: Not an inductive goal with 1 constructor. + :undocumented: -.. tacv:: eexists - :name: eexists + .. tacv:: left {? with @bindings_list } + right {? with @bindings_list } + :name: left; right -.. tacv:: esplit - :name: esplit + These tactics apply only if :g:`I` has two constructors, for + instance in the case of a disjunction :math:`A \vee B`. + Then, they are respectively equivalent to + :n:`constructor 1 {? with @bindings_list }` and + :n:`constructor 2 {? with @bindings_list }`. -.. tacv:: eleft - :name: eleft + .. exn:: Not an inductive goal with 2 constructors. -.. tacv:: eright - :name: eright + .. tacv:: econstructor + eexists + esplit + eleft + eright + :name: econstructor; eexists; esplit; eleft; eright - These tactics and their variants behave like :tacn:`constructor`, - :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their variants - but they introduce existential variables instead of failing when the - instantiation of a variable cannot be found (cf. :tacn:`eapply` and - :tacn:`apply`). + These tactics and their variants behave like :tacn:`constructor`, + :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their + variants but they introduce existential variables instead of failing + when the instantiation of a variable cannot be found + (cf. :tacn:`eapply` and :tacn:`apply`). .. _managingthelocalcontext: @@ -623,101 +614,107 @@ Managing the local context .. tacn:: intro :name: intro -This tactic applies to a goal that is either a product or starts with a let -binder. If the goal is a product, the tactic implements the "Lam" rule given in -:ref:`Typing-rules` [1]_. If the goal starts with a let binder, then the -tactic implements a mix of the "Let" and "Conv". + This tactic applies to a goal that is either a product or starts with a + let-binder. If the goal is a product, the tactic implements the "Lam" rule + given in :ref:`Typing-rules` [1]_. If the goal starts with a let-binder, + then the tactic implements a mix of the "Let" and "Conv". -If the current goal is a dependent product :g:`forall x:T, U` (resp -:g:`let x:=t in U`) then ``intro`` puts :g:`x:T` (resp :g:`x:=t`) in the local -context. The new subgoal is :g:`U`. + If the current goal is a dependent product :g:`forall x:T, U` + (resp :g:`let x:=t in U`) then :tacn:`intro` puts :g:`x:T` (resp :g:`x:=t`) + in the local context. The new subgoal is :g:`U`. -If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it -puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or -:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index -``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the -new subgoal is :g:`U`. + If the goal is a non-dependent product :math:`T \rightarrow U`, then it + puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` + or :g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). + The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh + identifier. In both cases, the new subgoal is :g:`U`. -If the goal is an existential variable, ``intro`` forces the resolution of the -existential variable into a dependent product :math:`forall`:g:`x:?X, ?Y`, puts -:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to -depend on :g:`x`. + If the goal is an existential variable, :tacn:`intro` forces the resolution + of the existential variable into a dependent product :math:`\forall`\ :g:`x:?X, ?Y`, + puts :g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal + allowed to depend on :g:`x`. -the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can -be applied or the goal is not head-reducible. + The tactic :tacn:`intro` applies the tactic :tacn:`hnf` + until :tacn:`intro` can be applied or the goal is not head-reducible. -.. exn:: No product even after head-reduction. -.. exn:: @ident is already used. + .. exn:: No product even after head-reduction. + :undocumented: -.. tacv:: intros - :name: intros + .. tacv:: intro @ident - This repeats ``intro`` until it meets the head-constant. It never - reduces head-constants and it never fails. + This applies :tacn:`intro` but forces :token:`ident` to be the name of + the introduced hypothesis. -.. tacn:: intro @ident + .. exn:: @ident is already used. + :undocumented: - This applies ``intro`` but forces :n:`@ident` to be the name of the - introduced hypothesis. + .. note:: -.. exn:: Name @ident is already used. + If a name used by intro hides the base name of a global constant then + the latter can still be referred to by a qualified name + (see :ref:`Qualified-names`). -.. note:: If a name used by intro hides the base name of a global - constant then the latter can still be referred to by a qualified name - (see :ref:`Qualified-names`). -.. tacv:: intros {+ @ident}. + .. tacv:: intros + :name: intros - This is equivalent to the composed tactic - :n:`intro @ident; ... ; intro @ident`. More generally, the ``intros`` tactic - takes a pattern as argument in order to introduce names for components - of an inductive definition or to clear introduced hypotheses. This is - explained in :ref:`Managingthelocalcontext`. + This repeats :tacn:`intro` until it meets the head-constant. It never + reduces head-constants and it never fails. -.. tacv:: intros until @ident + .. tacv:: intros {+ @ident}. - This repeats intro until it meets a premise of the goal having form - `(@ident:term)` and discharges the variable named `ident` of the current - goal. + This is equivalent to the composed tactic :n:`intro @ident; ... ; intro @ident`. -.. exn:: No such hypothesis in current goal. + .. tacv:: intros until @ident -.. tacv:: intros until @num + This repeats intro until it meets a premise of the goal having the + form :n:`(@ident : @type)` and discharges the variable + named :token:`ident` of the current goal. - This repeats intro until the `num`-th non-dependent product. For instance, - on the subgoal :g:`forall x y:nat, x=y -> y=x` the tactic - :n:`intros until 1` is equivalent to :n:`intros x y H`, as :g:`x=y -> y=x` - is the first non-dependent product. And on the subgoal :g:`forall x y - z:nat, x=y -> y=x` the tactic :n:`intros until 1` is equivalent to - :n:`intros x y z` as the product on :g:`z` can be rewritten as a - non-dependent product: :g:`forall x y:nat, nat -> x=y -> y=x` + .. exn:: No such hypothesis in current goal. + :undocumented: -.. exn:: No such hypothesis in current goal. + .. tacv:: intros until @num - This happens when `num` is 0 or is greater than the number of non-dependent - products of the goal. + This repeats :tacn:`intro` until the :token:`num`\-th non-dependent + product. -.. tacv:: intro after @ident -.. tacv:: intro before @ident -.. tacv:: intro at top -.. tacv:: intro at bottom + .. example:: - These tactics apply :n:`intro` and move the freshly introduced hypothesis - respectively after the hypothesis :n:`@ident`, before the hypothesis - :n:`@ident`, at the top of the local context, or at the bottom of the local - context. All hypotheses on which the new hypothesis depends are moved - too so as to respect the order of dependencies between hypotheses. - Note that :n:`intro at bottom` is a synonym for :n:`intro` with no argument. + On the subgoal :g:`forall x y : nat, x = y -> y = x` the + tactic :n:`intros until 1` is equivalent to :n:`intros x y H`, + as :g:`x = y -> y = x` is the first non-dependent product. -.. exn:: No such hypothesis: @ident. + On the subgoal :g:`forall x y z : nat, x = y -> y = x` the + tactic :n:`intros until 1` is equivalent to :n:`intros x y z` + as the product on :g:`z` can be rewritten as a non-dependent + product: :g:`forall x y : nat, nat -> x = y -> y = x`. + + .. exn:: No such hypothesis in current goal. + + This happens when :token:`num` is 0 or is greater than the number of + non-dependent products of the goal. + + .. tacv:: intro {? @ident__1 } after @ident__2 + intro {? @ident__1 } before @ident__2 + intro {? @ident__1 } at top + intro {? @ident__1 } at bottom + + These tactics apply :n:`intro {? @ident__1}` and move the freshly + introduced hypothesis respectively after the hypothesis :n:`@ident__2`, + before the hypothesis :n:`@ident__2`, at the top of the local context, + or at the bottom of the local context. All hypotheses on which the new + hypothesis depends are moved too so as to respect the order of + dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` + followed by the appropriate call to :tacn:`move ... after ...`, + :tacn:`move ... before ...`, :tacn:`move ... at top`, + or :tacn:`move ... at bottom`. -.. tacv:: intro @ident after @ident -.. tacv:: intro @ident before @ident -.. tacv:: intro @ident at top -.. tacv:: intro @ident at bottom + .. note:: - These tactics behave as previously but naming the introduced hypothesis - :n:`@ident`. It is equivalent to :n:`intro @ident` followed by the - appropriate call to ``move`` (see :tacn:`move ... after ...`). + :n:`intro at bottom` is a synonym for :n:`intro` with no argument. + + .. exn:: No such hypothesis: @ident. + :undocumented: .. tacn:: intros @intro_pattern_list :name: intros ... @@ -766,24 +763,22 @@ be applied or the goal is not head-reducible. :n:`intros p` is defined inductively over the structure of the introduction pattern :n:`p`: -Introduction on :n:`?` performs the introduction, and lets Coq choose a fresh -name for the variable; - -Introduction on :n:`?ident` performs the introduction, and lets Coq choose a -fresh name for the variable based on :n:`@ident`; + Introduction on :n:`?` performs the introduction, and lets Coq choose a fresh + name for the variable; -Introduction on :n:`@ident` behaves as described in :tacn:`intro` + Introduction on :n:`?@ident` performs the introduction, and lets Coq choose a + fresh name for the variable based on :n:`@ident`; -Introduction over a disjunction of list of patterns -:n:`[@intro_pattern_list | ... | @intro_pattern_list ]` expects the product -to be over an inductive type whose number of constructors is `n` (or more -generally over a type of conclusion an inductive type built from `n` -constructors, e.g. :g:`C -> A\/B` with `n=2` since :g:`A\/B` has `2` -constructors): it destructs the introduced hypothesis as :n:`destruct` (see -:tacn:`destruct`) would and applies on each generated subgoal the -corresponding tactic; + Introduction on :n:`@ident` behaves as described in :tacn:`intro` -.. tacv:: intros @intro_pattern_list + Introduction over a disjunction of list of patterns + :n:`[@intro_pattern_list | ... | @intro_pattern_list ]` expects the product + to be over an inductive type whose number of constructors is `n` (or more + generally over a type of conclusion an inductive type built from `n` + constructors, e.g. :g:`C -> A\/B` with `n=2` since :g:`A\/B` has `2` + constructors): it destructs the introduced hypothesis as :n:`destruct` (see + :tacn:`destruct`) would and applies on each generated subgoal the + corresponding tactic; The introduction patterns in :n:`@intro_pattern_list` are expected to consume no more than the number of arguments of the `i`-th constructor. If it @@ -792,60 +787,59 @@ corresponding tactic; list of patterns :n:`[ | ] H` applied on goal :g:`forall x:nat, x=0 -> 0=x` behaves the same as the list of patterns :n:`[ | ? ] H`); -Introduction over a conjunction of patterns :n:`({+, p})` expects -the goal to be a product over an inductive type :g:`I` with a single -constructor that itself has at least `n` arguments: It performs a case -analysis over the hypothesis, as :n:`destruct` would, and applies the -patterns :n:`{+ p}` to the arguments of the constructor of :g:`I` (observe -that :n:`({+ p})` is an alternative notation for :n:`[{+ p}]`); - -Introduction via :n:`({+& p})` is a shortcut for introduction via -:n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of -right-associative binary inductive constructors such as :g:`conj` or -:g:`ex_intro`; for instance, an hypothesis with type -:g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern -:n:`(a & x & b & c & d)`; - -If the product is over an equality type, then a pattern of the form -:n:`[= {+ p}]` applies either :tacn:`injection` or :tacn:`discriminate` -instead of :tacn:`destruct`; if :tacn:`injection` is applicable, the patterns -:n:`{+, p}` are used on the hypotheses generated by :tacn:`injection`; if the -number of patterns is smaller than the number of hypotheses generated, the -pattern :n:`?` is used to complete the list; - -.. tacv:: introduction over -> -.. tacv:: introduction over <- - + Introduction over a conjunction of patterns :n:`({+, p})` expects + the goal to be a product over an inductive type :g:`I` with a single + constructor that itself has at least `n` arguments: It performs a case + analysis over the hypothesis, as :n:`destruct` would, and applies the + patterns :n:`{+ p}` to the arguments of the constructor of :g:`I` (observe + that :n:`({+ p})` is an alternative notation for :n:`[{+ p}]`); + + Introduction via :n:`({+& p})` is a shortcut for introduction via + :n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of + right-associative binary inductive constructors such as :g:`conj` or + :g:`ex_intro`; for instance, an hypothesis with type + :g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern + :n:`(a & x & b & c & d)`; + + If the product is over an equality type, then a pattern of the form + :n:`[= {+ p}]` applies either :tacn:`injection` or :tacn:`discriminate` + instead of :tacn:`destruct`; if :tacn:`injection` is applicable, the patterns + :n:`{+, p}` are used on the hypotheses generated by :tacn:`injection`; if the + number of patterns is smaller than the number of hypotheses generated, the + pattern :n:`?` is used to complete the list. + + Introduction over ``->`` (respectively over ``<-``) expects the hypothesis to be an equality and the right-hand-side (respectively the left-hand-side) is replaced by the left-hand-side (respectively the right-hand-side) in the conclusion of the goal; the hypothesis itself is erased; if the term to substitute is a variable, it - is substituted also in the context of goal and the variable is removed too; + is substituted also in the context of goal and the variable is removed too. -Introduction over a pattern :n:`p{+ %term}` first applies :n:`{+ term}` -on the hypothesis to be introduced (as in :n:`apply {+, term}`) prior to the -application of the introduction pattern :n:`p`; + Introduction over a pattern :n:`p{+ %term}` first applies :n:`{+ term}` + on the hypothesis to be introduced (as in :n:`apply {+, term}`) prior to the + application of the introduction pattern :n:`p`; -Introduction on the wildcard depends on whether the product is dependent or not: -in the non-dependent case, it erases the corresponding hypothesis (i.e. it -behaves as an :tacn:`intro` followed by a :tacn:`clear`) while in the -dependent case, it succeeds and erases the variable only if the wildcard is part -of a more complex list of introduction patterns that also erases the hypotheses -depending on this variable; + Introduction on the wildcard depends on whether the product is dependent or not: + in the non-dependent case, it erases the corresponding hypothesis (i.e. it + behaves as an :tacn:`intro` followed by a :tacn:`clear`) while in the + dependent case, it succeeds and erases the variable only if the wildcard is part + of a more complex list of introduction patterns that also erases the hypotheses + depending on this variable; -Introduction over :n:`*` introduces all forthcoming quantified variables -appearing in a row; introduction over :n:`**` introduces all forthcoming -quantified variables or hypotheses until the goal is not any more a -quantification or an implication. + Introduction over :n:`*` introduces all forthcoming quantified variables + appearing in a row; introduction over :n:`**` introduces all forthcoming + quantified variables or hypotheses until the goal is not any more a + quantification or an implication. -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: reset all - Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. - intros * [a | (_,c)] f. + Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. + intros * [a | (_,c)] f. .. note:: + :n:`intros {+ p}` is not equivalent to :n:`intros p; ... ; intros p` for the following reason: If one of the :n:`p` is a wildcard pattern, it might succeed in the first case because the further hypotheses it @@ -854,6 +848,7 @@ quantification or an implication. introduced (and a fortiori not yet erased). .. note:: + In :n:`intros @intro_pattern_list`, if the last introduction pattern is a disjunctive or conjunctive pattern :n:`[{+| @intro_pattern_list}]`, the completion of :n:`@intro_pattern_list` @@ -872,38 +867,42 @@ quantification or an implication. the current goal. As a consequence, :n:`@ident` is no more displayed and no more usable in the proof development. -.. exn:: No such hypothesis. + .. exn:: No such hypothesis. + :undocumented: -.. exn:: @ident is used in the conclusion. + .. exn:: @ident is used in the conclusion. + :undocumented: -.. exn:: @ident is used in the hypothesis @ident. + .. exn:: @ident is used in the hypothesis @ident. + :undocumented: -.. tacv:: clear {+ @ident} + .. tacv:: clear {+ @ident} - This is equivalent to :n:`clear @ident. ... clear @ident.` + This is equivalent to :n:`clear @ident. ... clear @ident.` -.. tacv:: clear - {+ @ident} + .. tacv:: clear - {+ @ident} - This tactic clears all the hypotheses except the ones depending in the - hypotheses named :n:`{+ @ident}` and in the goal. + This variant clears all the hypotheses except the ones depending in the + hypotheses named :n:`{+ @ident}` and in the goal. -.. tacv:: clear + .. tacv:: clear - This tactic clears all the hypotheses except the ones the goal depends on. + This variants clears all the hypotheses except the ones the goal depends on. -.. tacv:: clear dependent @ident + .. tacv:: clear dependent @ident - This clears the hypothesis :n:`@ident` and all the hypotheses that depend on - it. + This clears the hypothesis :token:`ident` and all the hypotheses that + depend on it. -.. tacv:: clearbody {+ @ident} - :name: clearbody + .. tacv:: clearbody {+ @ident} + :name: clearbody - This tactic expects :n:`{+ @ident}` to be local definitions and clears their - respective bodies. - In other words, it turns the given definitions into assumptions. + This tactic expects :n:`{+ @ident}` to be local definitions and clears + their respective bodies. + In other words, it turns the given definitions into assumptions. -.. exn:: @ident is not a local definition. + .. exn:: @ident is not a local definition. + :undocumented: .. tacn:: revert {+ @ident} :name: revert @@ -912,172 +911,184 @@ quantification or an implication. (possibly defined) to the goal, if this respects dependencies. This tactic is the inverse of :tacn:`intro`. -.. exn:: No such hypothesis. + .. exn:: No such hypothesis. + :undocumented: -.. exn:: @ident is used in the hypothesis @ident. + .. exn:: @ident__1 is used in the hypothesis @ident__2. + :undocumented: -.. tacn:: revert dependent @ident + .. tacv:: revert dependent @ident + :name: revert dependent - This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that - depend on it. + This moves to the goal the hypothesis :token:`ident` and all the + hypotheses that depend on it. -.. tacn:: move @ident after @ident +.. tacn:: move @ident__1 after @ident__2 :name: move ... after ... - This moves the hypothesis named :n:`@ident` in the local context after the - hypothesis named :n:`@ident`, where “after” is in reference to the + This moves the hypothesis named :n:`@ident__1` in the local context after + the hypothesis named :n:`@ident__2`, where “after” is in reference to the direction of the move. The proof term is not changed. - If :n:`@ident` comes before :n:`@ident` in the order of dependencies, then - all the hypotheses between :n:`@ident` and :n:`ident@` that (possibly - indirectly) depend on :n:`@ident` are moved too, and all of them are thus - moved after :n:`@ident` in the order of dependencies. + If :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies, + then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that + (possibly indirectly) depend on :n:`@ident__1` are moved too, and all of + them are thus moved after :n:`@ident__2` in the order of dependencies. - If :n:`@ident` comes after :n:`@ident` in the order of dependencies, then all - the hypotheses between :n:`@ident` and :n:`@ident` that (possibly indirectly) - occur in the type of :n:`@ident` are moved too, and all of them are thus - moved before :n:`@ident` in the order of dependencies. + If :n:`@ident__1` comes after :n:`@ident__2` in the order of dependencies, + then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that + (possibly indirectly) occur in the type of :n:`@ident__1` are moved too, + and all of them are thus moved before :n:`@ident__2` in the order of + dependencies. -.. tacv:: move @ident before @ident + .. tacv:: move @ident__1 before @ident__2 + :name: move ... before ... - This moves :n:`@ident` towards and just before the hypothesis named - :n:`@ident`. As for :tacn:`move ... after ...`, dependencies over - :n:`@ident` (when :n:`@ident` comes before :n:`@ident` in the order of - dependencies) or in the type of :n:`@ident` (when :n:`@ident` comes after - :n:`@ident` in the order of dependencies) are moved too. + This moves :n:`@ident__1` towards and just before the hypothesis + named :n:`@ident__2`. As for :tacn:`move ... after ...`, dependencies + over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in + the order of dependencies) or in the type of :n:`@ident__1` + (when :n:`@ident__1` comes after :n:`@ident__2` in the order of + dependencies) are moved too. -.. tacv:: move @ident at top + .. tacv:: move @ident at top + :name: move ... at top - This moves :n:`@ident` at the top of the local context (at the beginning of - the context). + This moves :token:`ident` at the top of the local context (at the beginning + of the context). -.. tacv:: move @ident at bottom + .. tacv:: move @ident at bottom + :name: move ... at bottom - This moves ident at the bottom of the local context (at the end of the - context). + This moves :token:`ident` at the bottom of the local context (at the end of + the context). -.. exn:: No such hypothesis. -.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident. -.. exn:: Cannot move @ident after @ident : it depends on @ident. + .. exn:: No such hypothesis. + :undocumented: -.. example:: + .. exn:: Cannot move @ident__1 after @ident__2: it occurs in the type of @ident__2. + :undocumented: - .. coqtop:: all + .. exn:: Cannot move @ident__1 after @ident__2: it depends on @ident__2. + :undocumented: + + .. example:: + + .. coqtop:: reset all - Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. - intros x H z y H0. - move x after H0. - Undo. - move x before H0. - Undo. - move H0 after H. - Undo. - move H0 before H. - -.. tacn:: rename @ident into @ident + Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. + intros x H z y H0. + move x after H0. + Undo. + move x before H0. + Undo. + move H0 after H. + Undo. + move H0 before H. + +.. tacn:: rename @ident__1 into @ident__2 :name: rename -This renames hypothesis :n:`@ident` into :n:`@ident` in the current context. -The name of the hypothesis in the proof-term, however, is left unchanged. + This renames hypothesis :n:`@ident__1` into :n:`@ident__2` in the current + context. The name of the hypothesis in the proof-term, however, is left + unchanged. -.. tacv:: rename {+, @ident into @ident} + .. tacv:: rename {+, @ident__i into @ident__j} - This renames the variables :n:`@ident` into :n:`@ident` in parallel. In - particular, the target identifiers may contain identifiers that exist in the - source context, as long as the latter are also renamed by the same tactic. + This renames the variables :n:`@ident__i` into :n:`@ident__j` in parallel. + In particular, the target identifiers may contain identifiers that exist in + the source context, as long as the latter are also renamed by the same + tactic. -.. exn:: No such hypothesis. -.. exn:: @ident is already used. + .. exn:: No such hypothesis. + :undocumented: + + .. exn:: @ident is already used. + :undocumented: .. tacn:: set (@ident := @term) :name: set - This replaces :n:`@term` by :n:`@ident` in the conclusion of the current goal - and adds the new definition :g:`ident := term` to the local context. - - If :n:`@term` has holes (i.e. subexpressions of the form “`_`”), the tactic - first checks that all subterms matching the pattern are compatible before - doing the replacement using the leftmost subterm matching the pattern. + This replaces :token:`term` by :token:`ident` in the conclusion of the + current goal and adds the new definition :n:`@ident := @term` to the + local context. -.. exn:: The variable @ident is already defined. + If :token:`term` has holes (i.e. subexpressions of the form “`_`”), the + tactic first checks that all subterms matching the pattern are compatible + before doing the replacement using the leftmost subterm matching the + pattern. -.. tacv:: set (@ident := @term ) in @goal_occurrences + .. exn:: The variable @ident is already defined. + :undocumented: - This notation allows specifying which occurrences of :n:`@term` have to be - substituted in the context. The :n:`in @goal_occurrences` clause is an - occurrence clause whose syntax and behavior are described in - :ref:`goal occurences <occurencessets>`. + .. tacv:: set (@ident := @term) in @goal_occurrences -.. tacv:: set (@ident {+ @binder} := @term ) + This notation allows specifying which occurrences of :token:`term` have + to be substituted in the context. The :n:`in @goal_occurrences` clause + is an occurrence clause whose syntax and behavior are described in + :ref:`goal occurences <occurencessets>`. - This is equivalent to :n:`set (@ident := funbinder {+ binder} => @term )`. + .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } -.. tacv:: set term - This behaves as :n:`set(@ident := @term)` but :n:`@ident` is generated by - Coq. This variant also supports an occurrence clause. + This is equivalent to :n:`set (@ident := fun @binders => @term) {? in @goal_occurrences }`. -.. tacv:: set (@ident {+ @binder} := @term) in @goal_occurrences -.. tacv:: set @term in @goal_occurrences + .. tacv:: set @term {? in @goal_occurrences } - These are the general forms that combine the previous possibilities. + This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` + but :token:`ident` is generated by Coq. -.. tacv:: eset (@ident {+ @binder} := @term ) in @goal_occurrences -.. tacv:: eset @term in @goal_occurrences - :name: eset + .. tacv:: eset (@ident {? @binders } := @term) {? in @goal_occurrences } + eset @term {? in @goal_occurrences } + :name: eset; _ - While the different variants of :tacn:`set` expect that no existential - variables are generated by the tactic, :n:`eset` removes this constraint. In - practice, this is relevant only when :n:`eset` is used as a synonym of - :tacn:`epose`, i.e. when the :`@term` does not occur in the goal. + While the different variants of :tacn:`set` expect that no existential + variables are generated by the tactic, :tacn:`eset` removes this + constraint. In practice, this is relevant only when :tacn:`eset` is + used as a synonym of :tacn:`epose`, i.e. when the :token:`term` does + not occur in the goal. -.. tacv:: remember @term as @ident +.. tacn:: remember @term as @ident__1 {? eqn:@ident__2 } :name: remember - This behaves as :n:`set (@ident:= @term ) in *` and using a logical + This behaves as :n:`set (@ident__1 := @term) in *`, using a logical (Leibniz’s) equality instead of a local definition. + If :n:`@ident__2` is provided, it will be the name of the new equation. -.. tacv:: remember @term as @ident eqn:@ident - - This behaves as :n:`remember @term as @ident`, except that the name of the - generated equality is also given. + .. tacv:: remember @term as @ident__1 {? eqn:@ident__2 } in @goal_occurrences -.. tacv:: remember @term as @ident in @goal_occurrences + This is a more general form of :tacn:`remember` that remembers the + occurrences of :token:`term` specified by an occurrence set. - This is a more general form of :n:`remember` that remembers the occurrences - of term specified by an occurrence set. + .. tacv:: eremember @term as @ident__1 {? eqn:@ident__2 } {? in @goal_occurrences } + :name: eremember -.. tacv:: eremember @term as @ident -.. tacv:: eremember @term as @ident in @goal_occurrences -.. tacv:: eremember @term as @ident eqn:@ident - :name: eremember + While the different variants of :tacn:`remember` expect that no + existential variables are generated by the tactic, :tacn:`eremember` + removes this constraint. - While the different variants of :n:`remember` expect that no existential - variables are generated by the tactic, :n:`eremember` removes this constraint. - -.. tacv:: pose ( @ident := @term ) +.. tacn:: pose (@ident := @term) :name: pose This adds the local definition :n:`@ident := @term` to the current context without performing any replacement in the goal or in the hypotheses. It is - equivalent to :n:`set ( @ident := @term ) in |-`. + equivalent to :n:`set (@ident := @term) in |-`. -.. tacv:: pose ( @ident {+ @binder} := @term ) + .. tacv:: pose (@ident @binders := @term) - This is equivalent to :n:`pose (@ident := funbinder {+ binder} => @term)`. + This is equivalent to :n:`pose (@ident := fun @binders => @term)`. -.. tacv:: pose @term + .. tacv:: pose @term - This behaves as :n:`pose (@ident := @term )` but :n:`@ident` is generated by - Coq. + This behaves as :n:`pose (@ident := @term)` but :token:`ident` is + generated by Coq. -.. tacv:: epose (@ident := @term ) -.. tacv:: epose (@ident {+ @binder} := @term ) -.. tacv:: epose term - :name: epose + .. tacv:: epose (@ident {? @binders} := @term) + .. tacv:: epose term + :name: epose - While the different variants of :tacn:`pose` expect that no - existential variables are generated by the tactic, epose removes this - constraint. + While the different variants of :tacn:`pose` expect that no + existential variables are generated by the tactic, :tacn:`epose` + removes this constraint. .. tacn:: decompose [{+ @qualid}] @term :name: decompose @@ -1085,25 +1096,30 @@ The name of the hypothesis in the proof-term, however, is left unchanged. This tactic recursively decomposes a complex proposition in order to obtain atomic ones. -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: reset all - Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. - intros A B C H; decompose [and or] H; assumption. - Qed. + Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. + intros A B C H; decompose [and or] H. + all: assumption. + Qed. -:n:`decompose` does not work on right-hand sides of implications or products. + .. note:: + + :tacn:`decompose` does not work on right-hand sides of implications or + products. -.. tacv:: decompose sum @term + .. tacv:: decompose sum @term - This decomposes sum types (like or). + This decomposes sum types (like :g:`or`). -.. tacv:: decompose record @term + .. tacv:: decompose record @term + + This decomposes record types (inductive types with one constructor, + like :g:`and` and :g:`exists` and those defined with the :cmd:`Record` + command. - This decomposes record types (inductive types with one constructor, like - "and" and "exists" and those defined with the Record macro, see - :ref:`record-types`). .. _controllingtheproofflow: @@ -1410,94 +1426,101 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. tacn:: destruct @term :name: destruct - This tactic applies to any goal. The argument :n:`@term` must be of + This tactic applies to any goal. The argument :token:`term` must be of inductive or co-inductive type and the tactic generates subgoals, one - for each possible form of :n:`@term`, i.e. one for each constructor of the - inductive or co-inductive type. Unlike :n:`induction`, no induction - hypothesis is generated by :n:`destruct`. + for each possible form of :token:`term`, i.e. one for each constructor of the + inductive or co-inductive type. Unlike :tacn:`induction`, no induction + hypothesis is generated by :tacn:`destruct`. - There are special cases: + .. tacv:: destruct @ident - + If :n:`@term` is an identifier :n:`@ident` denoting a quantified variable - of the conclusion of the goal, then :n:`destruct @ident` behaves as - :n:`intros until @ident; destruct @ident`. If :n:`@ident` is not anymore - dependent in the goal after application of :n:`destruct`, it is erased - (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). + If :token:`ident` denotes a quantified variable of the conclusion + of the goal, then :n:`destruct @ident` behaves + as :n:`intros until @ident; destruct @ident`. If :token:`ident` is not + anymore dependent in the goal after application of :tacn:`destruct`, it + is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - + If term is a num, then destruct num behaves as intros until num - followed by destruct applied to the last introduced hypothesis. + If :token:`ident` is an hypothesis of the context, and :token:`ident` + is not anymore dependent in the goal after application + of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as + in :n:`destruct (@ident)`). + + .. tacv:: destruct @num + + :n:`destruct @num` behaves as :n:`intros until @num` + followed by destruct applied to the last introduced hypothesis. .. note:: - For destruction of a numeral, use syntax destruct (num) (not + For destruction of a numeral, use syntax :n:`destruct (@num)` (not very interesting anyway). - + In case term is an hypothesis :n:`@ident` of the context, and :n:`@ident` - is not anymore dependent in the goal after application of :n:`destruct`, it - is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). + .. tacv:: destruct @pattern - + The argument :n:`@term` can also be a pattern of which holes are denoted - by “_”. In this case, the tactic checks that all subterms matching the - pattern in the conclusion and the hypotheses are compatible and - performs case analysis using this subterm. + The argument of :tacn:`destruct` can also be a pattern of which holes are + denoted by “_”. In this case, the tactic checks that all subterms + matching the pattern in the conclusion and the hypotheses are compatible + and performs case analysis using this subterm. -.. tacv:: destruct {+, @term} + .. tacv:: destruct {+, @term} - This is a shortcut for :n:`destruct term; ...; destruct term`. + This is a shortcut for :n:`destruct @term; ...; destruct @term`. -.. tacv:: destruct @term as @disj_conj_intro_pattern + .. tacv:: destruct @term as @disj_conj_intro_pattern - This behaves as :n:`destruct @term` but uses the names in :n:`@intro_pattern` - to name the variables introduced in the context. The :n:`@intro_pattern` must - have the form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with `m` being the - number of constructors of the type of :n:`@term`. Each variable introduced - by :n:`destruct` in the context of the `i`-th goal gets its name from the - list :n:`pi1 ... pin` in order. If there are not enough names, - :n:`@destruct` invents names for the remaining variables to introduce. More - generally, the :n:`pij` can be any introduction pattern (see - :tacn:`intros`). This provides a concise notation for chaining destruction of - an hypothesis. + This behaves as :n:`destruct @term` but uses the names + in :token:`disj_conj_intro_pattern` to name the variables introduced in the + context. The :token:`disj_conj_intro_pattern` must have the + form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with ``m`` being the + number of constructors of the type of :token:`term`. Each variable + introduced by :tacn:`destruct` in the context of the ``i``-th goal + gets its name from the list :n:`pi1 ... pin` in order. If there are not + enough names, :tacn:`destruct` invents names for the remaining variables + to introduce. More generally, the :n:`pij` can be any introduction + pattern (see :tacn:`intros`). This provides a concise notation for + chaining destruction of an hypothesis. -.. tacv:: destruct @term eqn:@naming_intro_pattern + .. tacv:: destruct @term eqn:@naming_intro_pattern + :name: destruct ... eqn: - This behaves as :n:`destruct @term` but adds an equation between :n:`@term` - and the value that :n:`@term` takes in each of the possible cases. The name - of the equation is specified by :n:`@naming_intro_pattern` (see - :tacn:`intros`), in particular `?` can be used to let Coq generate a fresh - name. + This behaves as :n:`destruct @term` but adds an equation + between :token:`term` and the value that it takes in each of the + possible cases. The name of the equation is specified + by :token:`naming_intro_pattern` (see :tacn:`intros`), + in particular ``?`` can be used to let Coq generate a fresh name. -.. tacv:: destruct @term with @bindings_list + .. tacv:: destruct @term with @bindings_list - This behaves like :n:`destruct @term` providing explicit instances for the - dependent premises of the type of :n:`@term` (see :ref:`syntax of bindings <bindingslist>`). + This behaves like :n:`destruct @term` providing explicit instances for + the dependent premises of the type of :token:`term`. -.. tacv:: edestruct @term - :name: edestruct + .. tacv:: edestruct @term + :name: edestruct - This tactic behaves like :n:`destruct @term` except that it does not fail if - the instance of a dependent premises of the type of :n:`@term` is not - inferable. Instead, the unresolved instances are left as existential - variables to be inferred later, in the same way as :tacn:`eapply` does. + This tactic behaves like :n:`destruct @term` except that it does not + fail if the instance of a dependent premises of the type + of :token:`term` is not inferable. Instead, the unresolved instances + are left as existential variables to be inferred later, in the same way + as :tacn:`eapply` does. -.. tacv:: destruct @term using @term -.. tacv:: destruct @term using @term with @bindings_list + .. tacv:: destruct @term using @term {? with @bindings_list } - These are synonyms of :n:`induction @term using @term` and - :n:`induction @term using @term with @bindings_list`. + This is synonym of :n:`induction @term using @term {? with @bindings_list }`. -.. tacv:: destruct @term in @goal_occurrences + .. tacv:: destruct @term in @goal_occurrences - This syntax is used for selecting which occurrences of :n:`@term` the case - analysis has to be done on. The :n:`in @goal_occurrences` clause is an - occurrence clause whose syntax and behavior is described in - :ref:`occurences sets <occurencessets>`. + This syntax is used for selecting which occurrences of :token:`term` + the case analysis has to be done on. The :n:`in @goal_occurrences` + clause is an occurrence clause whose syntax and behavior is described + in :ref:`occurences sets <occurencessets>`. -.. tacv:: destruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences -.. tacv:: edestruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences + .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - These are the general forms of :n:`destruct` and :n:`edestruct`. They combine - the effects of the `with`, `as`, `eqn:`, `using`, and `in` clauses. + These are the general forms of :tacn:`destruct` and :tacn:`edestruct`. + They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, + and ``in`` clauses. -.. tacv:: case term +.. tacn:: case term :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 1fdd7317b5..b6654f6d7a 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -23,7 +23,11 @@ let number = [ '0'-'9' ]+ let string = "\"" _+ "\"" -let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ +let alpha = ['a'-'z' 'A'-'Z'] + +let ident = alpha (alpha | number | '_' | "'")* + +let undotted_sep = ((number | '[' ident ']') space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number diff --git a/ide/coqide.ml b/ide/coqide.ml index 09a82ba91e..00d43e6e64 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1046,16 +1046,24 @@ let build_ui () = ~accel:"F1" ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane); GAction.group_radio_actions - ~callback:begin function - | 0 -> List.iter (fun o -> Opt.set o "off") Opt.diff_item.Opt.opts - | 1 -> List.iter (fun o -> Opt.set o "on") Opt.diff_item.Opt.opts - | 2 -> List.iter (fun o -> Opt.set o "removed") Opt.diff_item.Opt.opts - | _ -> assert false + ~init_value:( + let v = diffs#get in + List.iter (fun o -> Opt.set o v) Opt.diff_item.Opt.opts; + if v = "on" then 1 + else if v = "removed" then 2 + else 0) + ~callback:begin fun n -> + (match n with + | 0 -> List.iter (fun o -> Opt.set o "off"; diffs#set "off") Opt.diff_item.Opt.opts + | 1 -> List.iter (fun o -> Opt.set o "on"; diffs#set "on") Opt.diff_item.Opt.opts + | 2 -> List.iter (fun o -> Opt.set o "removed"; diffs#set "removed") Opt.diff_item.Opt.opts + | _ -> assert false); + send_to_coq (fun sn -> sn.coqops#show_goals) end [ - radio "Unset diff" 0 ~label:"Unset _Diff"; - radio "Set diff" 1 ~label:"Set Di_ff"; - radio "Set removed diff" 2 ~label:"Set _Removed Diff"; + radio "Unset diff" 0 ~label:"_Don't show diffs"; + radio "Set diff" 1 ~label:"Show diffs: only _added"; + radio "Set removed diff" 2 ~label:"Show diffs: added and _removed"; ]; ]; toggle_items view_menu Coq.PrintOpt.bool_items; diff --git a/ide/idetop.ml b/ide/idetop.ml index 417ade51fd..d846b3abb5 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -53,10 +53,12 @@ let coqide_known_option table = List.mem table [ ["Printing";"Records"]; ["Printing";"Existential";"Instances"]; ["Printing";"Universes"]; - ["Printing";"Unfocused"]] + ["Printing";"Unfocused"]; + ["Diffs"]] let is_known_option cmd = match Vernacprop.under_control cmd with | VernacSetOption (_, o, BoolValue true) + | VernacSetOption (_, o, StringValue _) | VernacUnsetOption (_, o) -> coqide_known_option o | _ -> false diff --git a/ide/preferences.ml b/ide/preferences.ml index 526d94a939..955ee87840 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -565,6 +565,9 @@ let nanoPG = let user_queries = new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$') +let diffs = + new preference ~name:["diffs"] ~init:"off" ~repr:Repr.(string) + class tag_button (box : Gtk.box Gtk.obj) = object (self) diff --git a/ide/preferences.mli b/ide/preferences.mli index f3882d486d..dd2976efc2 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -102,6 +102,7 @@ val tab_length : int preference val highlight_current_line : bool preference val nanoPG : bool preference val user_queries : (string * string) list preference +val diffs : string preference val save_pref : unit -> unit val load_pref : unit -> unit diff --git a/proofs/proof.ml b/proofs/proof.ml index 51e0a1d614..0d355890c5 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -63,6 +63,7 @@ exception CannotUnfocusThisWay (* Cannot focus on non-existing subgoals *) exception NoSuchGoals of int * int +exception NoSuchGoal of Names.Id.t exception FullyUnfocused @@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) + | NoSuchGoal id -> + CErrors.user_err + ~hdr:"Focus" + Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -230,6 +235,37 @@ let focus cond inf i pr = try _focus cond (Obj.repr inf) i i pr with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i)) +(* Focus on the goal named id *) +let focus_id cond inf id pr = + let (focused_goals, evar_map) = Proofview.proofview pr.proofview in + begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with + | Some ev -> + begin match CList.safe_index Evar.equal ev focused_goals with + | Some i -> + (* goal is already under focus *) + _focus cond (Obj.repr inf) i i pr + | None -> + if CList.mem_f Evar.equal ev pr.shelf then + (* goal is on the shelf, put it in focus *) + let proofview = Proofview.unshelve [ev] pr.proofview in + let shelf = + CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf + in + let pr = { pr with proofview; shelf } in + let (focused_goals, _) = Proofview.proofview pr.proofview in + let i = + (* Now we know that this will succeed *) + try CList.index Evar.equal ev focused_goals + with Not_found -> assert false + in + _focus cond (Obj.repr inf) i i pr + else + raise CannotUnfocusThisWay + end + | None -> + raise (NoSuchGoal id) + end + let rec unfocus kind pr () = let cond = cond_of_focus pr in match test_cond cond kind pr.proofview with diff --git a/proofs/proof.mli b/proofs/proof.mli index c0e832fb8c..33addf13d7 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition a need for it? *) val focus : 'a focus_condition -> 'a -> int -> t -> t +(* focus on goal named id *) +val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t + exception FullyUnfocused exception CannotUnfocusThisWay diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 56815d241e..72c520218c 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -1,6 +1,6 @@ After | File Name | Before || Change | % Change -------------------------------------------------------- -0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61% -------------------------------------------------------- -0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% -0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file +0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00% +0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired index 18f0f34b28..74dad73332 100644 --- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -1,9 +1,9 @@ -After | Code | Before || Change | % Change ---------------------------------------------------------------------------------------------------- -0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% ---------------------------------------------------------------------------------------------------- -0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% -0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% - N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A -0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A -0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file +After | Code | Before || Change | % Change +---------------------------------------------------------------------------------------------------- +0m04.35s | Total | 0m00.58s || +0m03.77s | +649.05% +---------------------------------------------------------------------------------------------------- +0m03.87s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.246s || +0m03.62s | +1473.17% +0m00.322s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.189s || +0m00.13s | +70.37% +0m00.16s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.146s || +0m00.01s | +9.58% +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 6737197ee4..78a3f7c63a 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -5,6 +5,10 @@ set -e . ../template/path-init.sh +# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues + +MAKEFLAGS= + cd precomputed-time-tests ./run.sh || exit $? diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v index ed035f5213..2f7425bce6 100644 --- a/test-suite/success/BracketsWithGoalSelector.v +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -14,3 +14,12 @@ Proof. Fail Qed. } Qed. + +Lemma foo (n: nat) (P : nat -> Prop): + P n. +Proof. + intros. + refine (nat_ind _ ?[Base] ?[Step] _). + [Base]: { admit. } + [Step]: { admit. } +Abort. diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 56844f4773..59b2f789ab 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -333,7 +333,7 @@ Proof. auto with set. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma union_subset_1: subset s (union s s')=true. Proof. @@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma inter_subset_1: subset (inter s s') s=true. Proof. diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 1ee098cb07..4f2fdcf94c 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -333,7 +333,7 @@ Proof. auto with set. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma union_subset_1: subset s (union s s')=true. Proof. @@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma inter_subset_1: subset (inter s s') s=true. Proof. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 2da4452819..4aabda77ee 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -80,7 +80,7 @@ Proof. now apply testbit_even_succ. Qed. -(** Alternative caracterisations of [testbit] *) +(** Alternative characterisations of [testbit] *) (** This concise equation could have been taken as specification for testbit in the interface, but it would have been hard to @@ -102,10 +102,10 @@ Proof. left. destruct b; split; simpl; order'. Qed. -(** This caracterisation that uses only basic operations and +(** This characterisation that uses only basic operations and power was initially taken as specification for testbit. We describe [a] as having a low part and a high part, with - the corresponding bit in the middle. This caracterisation + the corresponding bit in the middle. This characterisation is moderatly complex to implement, but also moderately usable... *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index e1391f5990..90663de3f2 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -78,7 +78,7 @@ Proof. apply testbit_even_succ, le_0_l. Qed. -(** Alternative caracterisations of [testbit] *) +(** Alternative characterisations of [testbit] *) (** This concise equation could have been taken as specification for testbit in the interface, but it would have been hard to @@ -99,10 +99,10 @@ Proof. destruct b; order'. Qed. -(** This caracterisation that uses only basic operations and +(** This characterisation that uses only basic operations and power was initially taken as specification for testbit. We describe [a] as having a low part and a high part, with - the corresponding bit in the middle. This caracterisation + the corresponding bit in the middle. This characterisation is moderatly complex to implement, but also moderately usable... *) diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 6a3dd97656..9b8dd1db0b 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -392,7 +392,7 @@ Definition cond_positivity (x:R) : bool := | right _ => false end. -(** Sequential caracterisation of continuity *) +(** Sequential characterisation of continuity *) Lemma continuity_seq : forall (f:R -> R) (Un:nat -> R) (l:R), continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l). diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 05edc6ccde..4d04667c01 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -83,7 +83,7 @@ End GenericMinMax. Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). Module Import Private_Tac := !MakeOrderTac O O. -(** An alternative caracterisation of [max], equivalent to +(** An alternative characterisation of [max], equivalent to [max_l /\ max_r] *) Lemma max_spec n m : diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8b6822a4ed..403ad61798 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -343,19 +343,19 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: print-pretty-timed:: $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else ifeq (,$(AFTER)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ad489da822..c3bdf656d1 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -31,8 +31,19 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage_common () = +let usage_coq_makefile () = + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n"; output_string stderr "\ +\nFull list of options:\ +\n\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ \n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ @@ -61,25 +72,6 @@ let usage_common () = \n[-install opt]: where opt is \"user\" to force install into user directory,\ \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ -\n" - -let usage_coq_project () = - output_string stderr "Available arguments:"; - usage_common (); - exit 1 - -let usage_coq_makefile () = - output_string stderr "Usage summary:\ -\n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ -\n ... [any] ... [-extra[-phony] result dependencies command]\ -\n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ -\n [-h] [--help]\ -\n"; - usage_common (); - output_string stderr "\ \n[-f file]: take the contents of file as arguments\ \n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ @@ -405,7 +397,7 @@ let _ = let project = try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage_coq_project () in + with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin destination_of project (Option.get only_destination); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 96b8a23dd9..8cd262c6d6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -384,7 +384,7 @@ let print_style_tags opts = (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the - minor heap is heavily sollicited. Unfortunately, the default size is far too + minor heap is heavily solicited. Unfortunately, the default size is far too small, so we enlarge it a lot (128 times larger). To better handle huge memory consumers, we also augment the default major diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9824172315..5258ab2ea4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1987,8 +1987,9 @@ let vernac_subproof gln = match gln with | None -> Proof.focus subproof_cond () 1 p | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p | _ -> user_err ~hdr:"bracket_selector" - (str "Brackets only support the single numbered goal selector.")) + (str "Brackets do not support multi-goal selectors.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> |