diff options
59 files changed, 1314 insertions, 716 deletions
diff --git a/default.nix b/default.nix index 6b0e396d23..df1c43101b 100644 --- a/default.nix +++ b/default.nix @@ -43,7 +43,7 @@ stdenv.mkDerivation rec { hostname python3 time # coq-makefile timing tools ] - ++ (with ocamlPackages; [ ocaml findlib num ]) + ++ (with ocamlPackages; [ ocaml findlib ]) ++ optionals buildIde [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook @@ -69,6 +69,12 @@ stdenv.mkDerivation rec { ++ [ dune_2 ] # Maybe the next build system ); + # Since #12604, ocamlfind looks for num when building plugins + # This follows a similar change in the nixpkgs repo (cf. NixOS/nixpkgs#94230) + propagatedBuildInputs = [ + ocamlPackages.num + ]; + src = if shell then null else diff --git a/dev/README.md b/dev/README.md index 0c6b8020f1..0a6b196ec0 100644 --- a/dev/README.md +++ b/dev/README.md @@ -22,14 +22,12 @@ | [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source | | [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files | | [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling | -| [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | -| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | -| [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | +| [`dev/doc/universes.md`](doc/universes.md) | Help for debugging universes | | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | +| [`dev/doc/parsing.md`](doc/parsing.md) | Grammar and parsing overview | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | | [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate | -| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 577ce35aae..fd6ea9bb09 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -55,7 +55,7 @@ IF DEFINED HTTP_PROXY ( )
REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
+SET CYGWIN_REPOSITORY=https://mirrors.kernel.org/sourceware/cygwin
REM see -cygcache in ReadMe.txt
SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh new file mode 100644 index 0000000000..e57f95ef19 --- /dev/null +++ b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then + + coqhammer_CI_REF=factor-class-hint-clenv + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md new file mode 100644 index 0000000000..f8b4537e77 --- /dev/null +++ b/dev/doc/parsing.md @@ -0,0 +1,397 @@ +# Parsing + +Coq's parser is based on Camlp5 using an extensible grammar. Somewhat helpful +Camlp5 documentation is available [here](http://camlp5.github.io/doc/htmlc/grammars.html). +However, the Camlp5 code has been copied into the Coq source tree and may differ +from the Camlp5 release. + +Notable attributes of the parser include: + +* The grammar is extensible at run time. This is essential for supporting notations + and optionally-loaded plugins that extend the grammar. + +* The grammar is split into multiple source files. Nonterminals can be local to a file + or global. + +* While 95% of the nonterminals and almost all the productions are defined in the grammar, + a few are defined directly in OCaml code. Since many developers have worked on the parser + over the years, this code can be idiosyncratic, reflecting various coding styles. + +* The parser is a recursive descent parser that, by default, only looks at the next token + to make a parsing decision. It's possible to hand-code additional lookahead where + necessary by writing OCaml code. + +* There's no code that checks whether a grammar is ambiguous or whether every production + can be recognized. Developers who modify the grammar may, in some cases, need to structure their + added productions in specific ways to ensure that their additions are parsable and that they + don't break existing productions. + +## Contents ## + +- [Grammars: `*.mlg` File Structure](#grammars-mlg-file-structure) +- [Grammars: Nonterminals and Productions](#grammars-nonterminals-and-productions) + - [Alternate production syntax](#alternate-production-syntax) +- [Usage notes](#usage-notes) + - [Other components](#other-components) + - [Parsing productions](#parsing-productions) + - [Lookahead](#lookahead) + +## Grammars: `*.mlg` File Structure ## + +Grammars are defined in `*.mlg` files, which `coqpp` compiles into `*.ml` files at build time. +`coqpp` code is in the `coqpp` directory. `coqpp` uses yacc and lex to parse the grammar files. +You can examine its yacc and lex input files in `coqpp_lex.mll` and `coqpp_parse.mly` for +details not fully covered here. + +In addition, there is a `doc_grammar` build utility that uses the `coqpp` parser to extract the +grammar, then edits and inserts it into the documentation. This is described in +[`doc/tools/docgram/README.md`](../../doc/tools/docgram/README.md). +`doc_grammar` generates +[`doc/tools/docgram/fullGrammar`](../../doc/tools/docgram/fullGrammar), +which has the full grammar for Coq +(not including some optionally-loaded plugins). This may be easier to read since everything is +in one file and the parser action routines and other OCaml code are omitted. + +`*.mlg` files contain the following types of nodes (See `node` in the yacc grammar). This part is +very specific to Coq (not so similar to Camlp5): + +* OCaml code - OCaml code enclosed in curly braces, which is copied verbatim to the generated `*.ml` file + +* Comments - comments in the `*.mlg` file in the form `(* … *)`, which are not copied + to the generated `*.ml` file. Comments in OCaml code are preserved. + +* `DECLARE_PLUGIN "*_plugin"` - associates the file with a specific plugin, for example "ltac_plugin" + +* `GRAMMAR EXTEND` - adds additional nonterminals and productions to the grammar and declares global + nonterminals referenced in the `GRAMMAR EXTEND`: + + ``` + GRAMMAR EXTEND Gram + GLOBAL: + bignat bigint …; + <nonterminal definitions> + END + ``` + + Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "Prim.bignat"`. + All the `*.mlg` files include `open Pcoq` and often its modules, e.g. `open Pcoq.Prim`. + + `GRAMMAR EXTEND` should be used only for large syntax additions. To add new commands + and tactics, use these instead: + + - `VERNAC COMMAND EXTEND` to add new commands + - `TACTIC EXTEND` to add new tactics + - `ARGUMENT EXTEND` to add new nonterminals + + These constructs provide essential semantic information that's provided in a more complex, + less readable way with `GRAMMAR EXTEND`. + +* `VERNAC COMMAND EXTEND` - adds new command syntax by adding productions to the + `command` nonterminal. For example: + + ``` + VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY + | [ "Extraction" "Library" ident(m) ] + -> { extraction_library false m } + END + ``` + + Productions here are represented with alternate syntax, described later. + + New commands should be added using this construct rather than `GRAMMAR EXTEND` so + they are correctly registered, such as having the correct command classifier. + + TODO: explain "ExtractionLibrary", CLASSIFIED AS, CLASSIFIED BY, "{ tactic_mode }", STATE + +* `VERNAC { … } EXTEND` - TODO. A variant. The `{ … }` is a block of OCaml code. + +* `TACTIC EXTEND` - adds new tactic syntax by adding productions to `simple_tactic`. + For example: + + ``` + TACTIC EXTEND btauto + | [ "btauto" ] -> { Refl_btauto.Btauto.tac } + END + ``` + + adds a new nonterminal `btauto`. + + New tactics should be added using this construct rather than `GRAMMAR EXTEND`. + + TODO: explain DEPRECATED, LEVEL (not shown) + +* `ARGUMENT EXTEND` - defines a new nonterminal + + ``` + ARGUMENT EXTEND ast_closure_term + PRINTED BY { pp_ast_closure_term } + INTERPRETED BY { interp_ast_closure_term } + GLOBALIZED BY { glob_ast_closure_term } + SUBSTITUTED BY { subst_ast_closure_term } + RAW_PRINTED BY { pp_ast_closure_term } + GLOB_PRINTED BY { pp_ast_closure_term } + | [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c } + END + ``` + + See comments in `tacentries.mli` for partial information on the various + arguments. + +* `VERNAC ARGUMENT EXTEND` - (part of `argument_extend` in the yacc grammar) defines + productions for a single nonterminal. For example: + + ``` + VERNAC ARGUMENT EXTEND language + PRINTED BY { pr_language } + | [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } + | [ "OCaml" ] -> { Ocaml } + | [ "Haskell" ] -> { Haskell } + | [ "Scheme" ] -> { Scheme } + | [ "JSON" ] -> { JSON } + END + ``` + + TODO: explain PRINTED BY, CODE + +* DOC_GRAMMAR - Used in `doc_grammar`-generated files to permit simplified syntax + +Note that you can reverse engineer many details by comparing the `.mlg` input file with +the `.ml` generated by `coqpp`. + +## Grammars: Nonterminals and Productions + +Here's a simple nonterminal definition in the Camlp5 format: + + ``` + universe: + [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids } + | u = universe_expr -> { [u] } ] ] + ; + ``` + +In which: +* `universe` is the nonterminal being defined +* productions are separated by `|` and, as a group, are enclosed in `[ [ … ] ];` +* `u = universe_expr` refers to the `universe_expr` nonterminal. `u` is bound to + the value returned by that nonterminal's action routine, which can be + referred to in the action routine. For `ids = LIST1 universe_expr SEP ","`, + `ids` is bound to the list of values returned by `universe_expr`. +* `-> { … }` contains the OCaml action routine, which is executed when the production is recognized + and returns a value +* Semicolons separate adjacent grammatical elements (nonterminals, strings or other constructs) + +Grammatical elements that appear in productions are: + +- nonterminal names - identifiers in the form `[a-zA-Z0-9_]*`. These correspond to variables in + the generated `.ml` code. In some cases a qualified name, such as `Prim.name`, is used. +- `"…"` - a literal string that becomes a keyword and cannot be used as an `ident`. + The string doesn't have to be a valid identifier; frequently the string will contain only + punctuation characters. Generally we try to avoid adding new keywords that are also valid + identifiers--though there is an unresolved debate among the developers about whether having more + such keywords in general is good (e.g. it makes it easier to highlight keywords in GUIs) + or bad (more keywords for the user to avoid and new keywords may require changes to existing + proof files). +- `IDENT "…"` - a literal string that has the form of an `ident` that doesn't become + a keyword +- `OPT element` - optionally include `element` (e.g. a nonterminal, IDENT "…" or "…"). + The value is of type `'a option`. +- `LIST1 element` - a list of one or more `element`s. The value is of type `'a list`. +- `LIST0 element` - an optional list of `element`s +- `LIST1 element SEP sep` - a list of `element`s separated by `sep` +- `LIST0 element SEP sep` - an optional list of `element`s separated by `sep` +- `( elements )` - grouping to represent a series of elements as a unit, + useful within `OPT` and `LIST*`. +- `[ elements1 | elements2 | … ]` - alternatives (either `elements1` or `elements2` or …), + actually nested productions, each of which can have its own action routines + +Nonterminals can also be defined with multiple levels to specify precedence and associativity +of its productions. This is described in the Coq documentation under the `Print Grammar` +command. The first square bracket around a nonterminal definition is for grouping +level definitions, which are separated with `|`, for example: + + ``` + tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] + | "4" LEFTA + : + ``` + +Grammar extensions can specify what level they are modifying, for example: + + ``` + tactic_expr: LEVEL "1" [ RIGHTA + [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + ] ]; + ``` + +### Alternate production syntax ### + +Except for `GRAMMAR EXTEND`, the `EXTEND` nodes in the `*.mlg`s use simplified syntax in +productions that's similar to what's used in the `Tactic Notation` and +`Ltac2 Notation` commands. For example: + + ``` + TACTIC EXTEND cc + | [ "congruence" ] -> { congruence_tac 1000 [] } + | [ "congruence" integer(n) ] -> { congruence_tac n [] } + | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } + | [ "congruence" integer(n) "with" ne_constr_list(l) ] -> + { congruence_tac n l } + END + ``` + +Nonterminals appearing in the alternate production syntax are accessed through `wit_*` symbols +defined in the OCaml code. Some commonly used symbols are defined in `stdarg.ml`. +Others are defined in the code generated by `ARGUMENT EXTEND` and `VERNAC ARGUMENT EXTEND` +constructs. References to nonterminals that don't have `wit_*` symbols cause +compilation errors. + +The differences are: +* The outer `: [ … ];` is omitted. Each production is enclosed in `| [ … ]`. +* The action routine is outside the square brackets +* Literal strings that are valid identifiers don't become reserved keywords +* No semicolons separating elements of the production +* `integer(n)` is used to bind a nonterminal value to a variable instead of `n = integer` +* Alternate forms of constructs are used: + * `ne_entry_list` for `LIST1 entry` + * `entry_list` for `LIST0 entry` + * `ne_entry_list_sep(var, sep)` for `LIST1 entry SEP sep` where the list is bound to `var` + * `entry_list_sep(var, sep)` for `LIST0 entry SEP sep` where the list is bound to `var` + * `entry_opt` for OPT entry +* There's no way to define `LEVEL`s +* There's no equivalent to `( elements )` or `[ elements1 | elements2 | … ]`, which may + require repeating similar syntax several times. For example, this single production + is equivalent to 8 productions in `TACTIC EXTEND` representing all possible expansions of + three `OPT`s: + + ``` + | IDENT "Add"; IDENT "Parametric"; IDENT "Relation"; LIST0 binder; ":"; constr; constr; + OPT [ IDENT "reflexivity"; IDENT "proved"; IDENT "by"; constr -> { … } ]; + OPT [ IDENT "symmetry"; IDENT "proved"; IDENT "by"; constr -> { … } ]; + OPT [ IDENT "transitivity"; IDENT "proved"; IDENT "by"; constr -> { … } ]; + IDENT "as"; ident -> { … } + ``` + +## Usage notes + +### Other components + +Coq's lexer is in `clexer.ml`. Its 10 token types are defined in `tok.ml`. + +The parser is in `grammar.ml`. The extensive use of GADT (generalized algebraic datatypes) +makes it harder for the uninitiated to understand it. + +When the parser is invoked, the call tells the parser which nonterminal to parse. `vernac_control` +is the start symbol for commands. `tactic_mode` is the start symbol for tactics. +Tactics give syntax errors if Coq is not in proof mode. There are additional details +not mentioned here. + +### Parsing productions + +Some thoughts, not to be taken as identifying all the issues: + +Since the parser examines only the next token to make a parsing decision (and perhaps +because of other potentially fixable limitations), some productions have to be ordered +or structured in a particular way to parse correctly in all cases. + +For example, consider these productions: + + ``` + command: [ [ + | IDENT "Print"; p = printable -> { VernacPrint p } + | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> { VernacPrint (PrintName (qid,l)) } + | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> + { VernacPrint (PrintModuleType qid) } + | IDENT "Print"; IDENT "Module"; qid = global -> + { VernacPrint (PrintModule qid) } + | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> + { VernacPrint (PrintNamespace ns) } + : + + printable: + [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> { PrintName (qid,l) } + | IDENT "All" -> { PrintFullContext } + | IDENT "Section"; s = global -> { PrintSectionContext s } + : + ``` + +Reversing the order of the first two productions in `command` causes the `All` in `Print All` to +be parsed incorrectly as a `smart_global`, making that command unavailable. `Print Namespace nat.` +still works correctly, though. + +Similarly, the production for `Print Module Type` has to appear before `Print Module <global>` +in order to be reachable. + +Internally, the parser generates a tree that represents the possible prefixes for the +productions of a nonterminal as described in +[the Camlp5 documentation](http://camlp5.github.io/doc/htmlc/grammars.html#b:Rules-insertion). + +Here's another example in which the way the productions are written matters. `OPT` at +the beginning of a production doesn't always work well: + + ``` + command: [ [ + | IDENT "Foo"; n = natural -> { VernacBack 1 } + | OPT (IDENT "ZZ"); IDENT "Foo" -> { VernacBack 1 } + : + ``` + +`Foo.` looks like it should be accepted, but it gives a parse error: + + ``` + Unnamed_thm < Foo. + Toplevel input, characters 3-4: + > Foo. + > ^ + Error: + Syntax error: [prim:natural] expected after 'Foo' (in [vernac:command]). + ``` + +Reversing the order of the productions doesn't help, but splitting +the 'OPT' production into 2 productions works: + + ``` + | IDENT "Foo" -> { VernacBack 1 } + | IDENT "ZZ"; IDENT "Foo" -> { VernacBack 1 } + | IDENT "Foo"; n = natural -> { VernacBack 1 } + + ``` + +On the other hand, `OPT` works just fine when the parser has already found the +right production. For example `Back` and `Back <natural>` can be combined using +an `OPT`: + + ``` + | IDENT "Back"; n = OPT natural -> { VernacBack (Option.default 1 n) } + ``` + +### Lookahead + +It's possible to look ahead more than one symbol using OCaml code. Generally we +avoid doing this unless there's a strong reason to do so. For example, this +code defines a new nonterminal `local_test_lpar_id_colon` that checks that +the next 3 tokens are `"("` `ident` and `":"` without consuming any input: + + ``` + let local_test_lpar_id_colon = + let open Pcoq.Lookahead in + to_entry "lpar_id_colon" begin + lk_kw "(" >> lk_ident >> lk_kw ":" + end + ``` + +This one checks that the next 2 tokens are `"["` and `"|"` with no space between. +This is a special case: intropatterns can have sequences like `"[|]"` that are +3 different tokens with empty nonterminals between them. Making `"[|"` a keyword +would break existing code with "[|]": + + ``` + let test_array_opening = + let open Pcoq.Lookahead in + to_entry "test_array_opening" begin + lk_kw "[" >> lk_kw "|" >> check_no_space + end + ``` + +TODO: how to add a tactic or command diff --git a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst new file mode 100644 index 0000000000..208855b4c8 --- /dev/null +++ b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + Int63 notations now match up with the rest of the standard library: :g:`a \% + m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced + with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. + The old notations are still available as deprecated notations. Additionally, + there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that + users can import to get the ``Int63`` notations without unqualifying the + various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes + `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst new file mode 100644 index 0000000000..1709cf1eae --- /dev/null +++ b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + <? n`, and :g:`m <=? n`. The old notations are still available as deprecated + notations. Additionally, there is now a + ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to + get the ``PrimFloat`` notations without unqualifying the various primitives + (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 + <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst new file mode 100644 index 0000000000..51b59e4a94 --- /dev/null +++ b/doc/changelog/10-standard-library/12716-curry.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12799-list-repeat.rst b/doc/changelog/10-standard-library/12799-list-repeat.rst new file mode 100644 index 0000000000..adfc48f67b --- /dev/null +++ b/doc/changelog/10-standard-library/12799-list-repeat.rst @@ -0,0 +1,4 @@ +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 <https://github.com/coq/coq/pull/12799>`_, + by Olivier Laurent). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index f9d24fde0e..c27eb216e8 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules ``Datatypes``, ``Specif``, ``Peano``, -``Wf`` and +``Wf`` and ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. @@ -175,7 +175,7 @@ Quantifiers Then we find first-order quantifiers: .. coqtop:: in - + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := ex_intro (x:A) (_:P x). @@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided. single: f_equal2 ... f_equal5 (term) The theorem ``f_equal`` is extended to functions with two to five -arguments. The theorem are names ``f_equal2``, ``f_equal3``, +arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. .. coqtop:: in abort - + Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), @@ -324,7 +324,7 @@ Programming Note that zero is the letter ``O``, and *not* the numeral ``0``. -The predicate ``identity`` is logically +The predicate ``identity`` is logically equivalent to equality but it lives in sort ``Type``. It is mainly maintained for compatibility. @@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``. Specification ~~~~~~~~~~~~~ -The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. +The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. They are available with the syntax shown in the previous section :ref:`datatypes`. For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct @@ -393,11 +393,11 @@ provided. .. coqtop:: in Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). - Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x). A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, -when the predicate ``P`` is now defined as a +when the predicate ``P`` is now defined as a constructor of types in ``Type``. .. index:: @@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: .. coqdoc:: - + Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := match n with @@ -628,7 +628,7 @@ induction principle. .. coqdoc:: Theorem nat_case : - forall (n:nat) (P:nat -> Prop), + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Theorem nat_double_ind : forall R:nat -> nat -> Prop, @@ -640,7 +640,7 @@ induction principle. Well-founded recursion ~~~~~~~~~~~~~~~~~~~~~~ -The basic library contains the basics of well-founded recursion and +The basic library contains the basics of well-founded recursion and well-founded induction, in module ``Wf.v``. .. index:: @@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``. forall P:A -> Prop, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. -The automatically generated scheme ``Acc_rect`` +The automatically generated scheme ``Acc_rect`` can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the @@ -741,7 +741,7 @@ The standard library Survey ~~~~~~ -The rest of the standard library is structured into the following +The rest of the standard library is structured into the following subdirectories: * **Logic** : Classical logic and dependent equality @@ -751,8 +751,8 @@ subdirectories: * **ZArith** : Basic relative integer arithmetic * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words) * **Bool** : Booleans (basic functions and results) - * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) - * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) + * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) + * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) @@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR :name: discrR - + Proves that two real integer constants are different. .. example:: @@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: split_Rmult :name: split_Rmult - + Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. @@ -963,7 +963,7 @@ List library single: fold_left (term) single: fold_right (term) -Some elementary operations on polymorphic lists are defined here. +Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module ``List``. It defines the following notions: @@ -1052,9 +1052,9 @@ Notation Interpretation ``_ + _`` ``add`` ``_ * _`` ``mul`` ``_ / _`` ``div`` -``_ == _`` ``eqb`` -``_ < _`` ``ltb`` -``_ <= _`` ``leb`` +``_ =? _`` ``eqb`` +``_ <? _`` ``ltb`` +``_ <=? _`` ``leb`` ``_ ?= _`` ``compare`` =========== ============== diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b4b80ca21..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1211,6 +1211,8 @@ The move tactic. :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. +.. _the_case_tactic_ssr: + The case tactic ``````````````` @@ -1235,7 +1237,17 @@ The case tactic x = 1 -> y = 2 -> G. - Note also that the case of |SSR| performs :g:`False` elimination, even + The :tacn:`case` can generate the following warning: + + .. warn:: SSReflect: cannot obtain new equations out of ... + + The tactic was run on an equation that cannot generate simpler equations, + for example `x = 1`. + + The warning can be silenced or made fatal by using the :opt:`Warnings` option + and the `spurious-ssr-injection` key. + + Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 25c4de7389..c5fab0983f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2227,9 +2227,6 @@ and an explanation of the underlying technique. then :n:`injection @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - .. exn:: Nothing to do, it is an equality between convertible terms. :undocumented: @@ -2237,7 +2234,8 @@ and an explanation of the underlying technique. :undocumented: .. exn:: Nothing to inject. - :undocumented: + + This error is given when one side of the equality is not a constructor. .. tacv:: injection @num diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 18149a690a..9e8e5e5fa5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -425,16 +425,98 @@ Displaying information about notations (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s - The first three of these give the precedence and associativity for each construct. - For example, these lines printed by `Print Grammar tactic` indicates that the `try` construct - is at level 3 and right-associative. `SELF` represents the `tactic_expr` nonterminal - at level 5 (the top level):: - + This command doesn't display all nonterminals of the grammar. For example, + productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` + and `tactic_then_gen` which are not shown and can't be printed. + + The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify + what part of the grammar a nonterminal is from. If you examine nonterminal definitions + in the source code, they are identified only by the name following the colon. + + Most of the grammar in the documentation was updated in 8.12 to make it accurate and + readable. This was done using a new developer tool that extracts the grammar from the + source code, edits it and inserts it into the documentation files. While the + edited grammar is equivalent to the original, for readability some nonterminals + have been renamed and others have been eliminated by substituting the nonterminal + definition where the nonterminal was referenced. This command shows the original grammar, + so it won't exactly match the documentation. + + The |Coq| parser is based on Camlp5. The documentation for + `Extensible grammars <http://camlp5.github.io/doc/htmlc/grammars.html>`_ is the + most relevant but it assumes considerable knowledge. Here are the essentials: + + Productions can contain the following elements: + + - nonterminal names - identifiers in the form `[a-zA-Z0-9_]*` + - `"…"` - a literal string that becomes a keyword and cannot be used as an :token:`ident`. + The string doesn't have to be a valid identifier; frequently the string will contain only + punctuation characters. + - `IDENT "…"` - a literal string that has the form of an :token:`ident` + - `OPT element` - optionally include `element` (e.g. a nonterminal, IDENT "…" or "…") + - `LIST1 element` - a list of one or more `element`\s + - `LIST0 element` - an optional list of `element`\s + - `LIST1 element SEP sep` - a list of `element`\s separated by `sep` + - `LIST0 element SEP sep` - an optional list of `element`\s separated by `sep` + - `[ elements1 | elements2 | … ]` - alternatives (either `elements1` or `elements2` or …) + + Nonterminals can have multiple **levels** to specify precedence and associativity + of its productions. This feature of grammars makes it simple to parse input + such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level. + + For example, this output from `Print Grammar tactic` shows the first 3 levels for + `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, + which applies to the productions within it, such as the `try` construct:: + + Entry tactic:tactic_expr is + [ "5" RIGHTA + [ tactic:binder_tactic ] + | "4" LEFTA + [ SELF; ";"; tactic:binder_tactic + | SELF; ";"; SELF + | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA [ IDENT "try"; SELF + : + + The interpretation of `SELF` depends on its position in the production and the + associativity of the level: + + - At the beginning of a production, `SELF` means the next level. In the + fragment shown above, the next level for `try` is "2". (This is defined by the order + of appearance in the grammar or output; the levels could just as well be + named "foo" and "bar".) + - In the middle of a production, `SELF` means the top level ("5" in the fragment) + - At the end of a production, `SELF` means the next level within + `LEFTA` levels and the current level within `RIGHTA` levels. + + `NEXT` always means the next level. `nonterminal LEVEL "…"` is a reference to the specified level + for `nonterminal`. + + `Associativity <http://camlp5.github.io/doc/htmlc/grammars.html#b:Associativity>`_ + explains `SELF` and `NEXT` in somewhat more detail. + + The output for `Print Grammar constr` includes :cmd:`Notation` definitions, + which are dynamically added to the grammar at run time. + For example, in the definition for `operconstr`, the production on the second line shown + here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: + + | "50" LEFTA + [ SELF; "||"; NEXT + + Similarly, `Print Grammar tactic` includes :cmd:`Tactic Notation`\s, such as :tacn:`dintuition`. + + The file + `doc/tools/docgram/fullGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar>`_ + in the source tree extracts the full grammar for + |Coq| (not including notations and tactic notations defined in `*.v` files nor some optionally-loaded plugins) + in a single file with minor changes to handle nonterminals using multiple levels (described in + `doc/tools/docgram/README.md <http://github.com/coq/coq/blob/master/doc/tools/docgram/README.md>`_). + This is complete and much easier to read than the grammar source files. + `doc/tools/docgram/orderedGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/orderedGrammar>`_ + has the edited grammar that's used in the documentation. - Note that the productions printed by this command are represented in the form used by - |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation. + Developer documentation for parsing is in + `dev/doc/parsing.md <http://github.com/coq/coq/blob/master/dev/doc/parsing.md>`_. .. _locating-notations: @@ -872,7 +954,7 @@ where ``x`` is any expression parsed in entry the given rule) and ``y`` is any expression parsed in entry ``expr`` at level strictly less than ``2``. -Rules associated to an entry can refer different sub-entries. The +Rules associated with an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar of term as in the rule @@ -958,7 +1040,7 @@ up to the insertion of a pair of curly brackets. .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar - This displays the state of the grammar for terms associated to + This displays the state of the grammar for terms associated with the custom entry :token:`ident`. .. _NotationSyntax: diff --git a/engine/evd.ml b/engine/evd.ml index c570f75c6b..e85cbc96b2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -987,11 +987,6 @@ let check_constraints evd csts = let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } -let refresh_undefined_universes evd = - let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in - let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in - evd', subst - let nf_univ_variables evd = let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in diff --git a/engine/evd.mli b/engine/evd.mli index 679173ca72..3f17e63034 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val fix_undefined_variables : evar_map -> evar_map -val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst - (** Universe minimization *) val minimize_universes : evar_map -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index d4cb59da26..ca0a21acf7 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -718,35 +718,6 @@ let fix_undefined_variables uctx = { uctx with univ_variables = vars'; univ_algebraic = algs' } -let refresh_undefined_univ_variables uctx = - let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in - let subst_fn u = subst_univs_level_level subst u in - let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc) - uctx.univ_algebraic LSet.empty - in - let vars = - LMap.fold - (fun u v acc -> - LMap.add (subst_fn u) - (Option.map (subst_univs_level_universe subst) v) acc) - uctx.univ_variables LMap.empty - in - let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in - let lbound = uctx.universes_lbound in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) - (ContextSet.levels ctx') g in - let initial = declare uctx.initial_universes in - let univs = declare UGraph.initial_universes in - let uctx' = {names = uctx.names; - local = ctx'; - seff_univs = uctx.seff_univs; - univ_variables = vars; univ_algebraic = alg; - universes = univs; - universes_lbound = lbound; - initial_universes = initial; - weak_constraints = weak; } in - uctx', subst - let minimize uctx = let open UnivMinim in let lbound = uctx.universes_lbound in diff --git a/engine/uState.mli b/engine/uState.mli index 45a0f9964e..607c6c9452 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t val fix_undefined_variables : t -> t -val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst - (** Universe minimization *) val minimize : t -> t diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 57cdccce6d..0e237b74fe 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -544,6 +544,7 @@ struct let coercions = BoolOpt ["Printing"; "Coercions"] let raw_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] + let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] let existential = BoolOpt ["Printing"; "Existential"; "Instances"] let universes = BoolOpt ["Printing"; "Universes"] @@ -558,7 +559,7 @@ struct { opts = [raw_matching]; init = true; label = "Display raw _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; - { opts = [notations]; init = true; label = "Display _parentheses" }; + { opts = [parentheses]; init = true; label = "Display _parentheses" }; { opts = [all_basic]; init = false; label = "Display _all basic low-level contents" }; { opts = [existential]; init = false; diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 9eeba614c7..148c1772bf 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1020,10 +1020,11 @@ let lia (can_enum : bool) (prfdepth : int) sys = p) sys end; + let bnd1 = bound_monomials sys in let sys = subst sys in - let bnd = bound_monomials sys in + let bnd2 = bound_monomials sys in (* To deal with non-linear monomials *) - let sys = bnd @ saturate_by_linear_equalities sys @ sys in + let sys = bnd1 @ bnd2 @ saturate_by_linear_equalities sys @ sys in let sys' = List.map (fun ((p, o), prf) -> (cstr_of_poly (p, o), prf)) sys in xlia (List.map fst sys) can_enum reduction_equations sys' diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 4e1f9a66ac..fa29e6080e 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) = let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in try - ignore (get_injection env evd (EConstr.of_constr ty)); - tac id.Context.binder_name (EConstr.of_constr t) - (EConstr.of_constr ty) + let x = id.Context.binder_name in + ignore + (let eq = Lazy.force eq in + find_option + (match_operator env evd eq + [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|]) + (HConstr.find_all eq !table_cache)); + tac x (EConstr.of_constr t) (EConstr.of_constr ty) with Not_found -> Tacticals.New.tclIDTAC) let iter_let_aux tac = diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 1c81fbc10b..1e182b52fa 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -485,17 +485,22 @@ let revtoptac n0 = Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) end -let equality_inj l b id c = - Proofview.V82.tactic begin fun gl -> - let msg = ref "" in - try Proofview.V82.of_tactic (Equality.inj None l b None c) gl - with - | CErrors.UserError (_,s) - when msg := Pp.string_of_ppcmds s; - !msg = "Not a projectable equality but a discriminable one." || - !msg = "Nothing to inject." -> - Feedback.msg_warning (Pp.str !msg); - discharge_hyp (id, (id, "")) gl +let nothing_to_inject = + CWarnings.create ~name:"spurious-ssr-injection" ~category:"ssr" + (fun (sigma, env, ty) -> + Pp.(str "SSReflect: cannot obtain new equations out of" ++ fnl() ++ + str" " ++ Printer.pr_econstr_env env sigma ty ++ fnl() ++ + str "Did you write an extra [] in the intro pattern?")) + +let equality_inj l b id c = Proofview.Goal.enter begin fun gl -> + Proofview.tclORELSE (Equality.inj None l b None c) + (function + | (Equality.NothingToInject,_) -> + let open Proofview.Notations in + Ssrcommon.tacTYPEOF (EConstr.mkVar id) >>= fun ty -> + nothing_to_inject (Proofview.Goal.sigma gl, Proofview.Goal.env gl, ty); + Proofview.V82.tactic (discharge_hyp (id, (id, ""))) + | (e,info) -> Proofview.tclZERO ~info e) end let injectidl2rtac id c = diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2c7b689c04..2661000a39 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -397,6 +397,10 @@ and apply_env env t = | _ -> map_with_binders subs_lift apply_env env t +let rec strip_app = function + | APP (args,st) -> APP (args,strip_app st) + | s -> TOP + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -442,7 +446,7 @@ let rec norm_head info env t stack = | Const sp -> Reductionops.reduction_effect_hook info.env info.sigma - (fst sp) (lazy (reify_stack t stack)); + (fst sp) (lazy (reify_stack t (strip_app stack))); norm_head_ref 0 info env stack (ConstKey sp) t | LetIn (_, b, _, c) -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fdc770dba6..aeb18ec322 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -499,13 +499,6 @@ let beta_applist sigma (c,l) = (* Iota reduction tools *) -type 'a miota_args = { - mP : constr; (* the result type *) - mconstr : constr; (* the constructor *) - mci : case_info; (* special info to re-build pattern *) - mcargs : 'a list; (* the constructor's arguments *) - mlf : 'a array } (* the branch code vector *) - let reducible_mind_case sigma c = match EConstr.kind sigma c with | Construct _ | CoFix _ -> true | _ -> false @@ -514,10 +507,7 @@ let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in - if Int.equal bodynum ind then mkCoFix (ind,typedbodies) - else - let bd = mkCoFix (ind,typedbodies) in - bd + mkCoFix (ind,typedbodies) in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -530,18 +520,6 @@ let reduce_and_refold_cofix recfun env sigma cofix sk = (fun _ (t,sk') -> recfun (t,sk')) [] sigma raw_answer sk -let reduce_mind_case sigma mia = - match EConstr.kind sigma mia.mconstr with - | Construct ((ind_sp,i),u) -> -(* let ncargs = (fst mia.mci).(i-1) in*) - let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in - applist (mia.mlf.(i-1),real_cargs) - | CoFix cofix -> - let cofix_def = contract_cofix sigma cofix in - (* XXX Is NoInvert OK here? *) - mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) - | _ -> assert false - (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) @@ -549,10 +527,7 @@ let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies) let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in - if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies) - else - let bd = mkFix ((recindices,ind),typedbodies) in - bd + mkFix ((recindices,ind),typedbodies) in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -757,7 +732,7 @@ let rec whd_state_gen flags env sigma = | None -> fold ()) | Const (c,u as const) -> reduction_effect_hook env sigma c - (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); + (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack))))); if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then let u' = EInstance.kind sigma u in match constant_value_in env (c, u') with diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 0f288cdd46..d404a7e414 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -217,22 +217,14 @@ val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr (** Raises [Invalid_argument] *) - -type 'a miota_args = { - mP : constr; (** the result type *) - mconstr : constr; (** the constructor *) - mci : case_info; (** special info to re-build pattern *) - mcargs : 'a list; (** the constructor's arguments *) - mlf : 'a array } (** the branch code vector *) - val reducible_mind_case : evar_map -> constr -> bool -val reduce_mind_case : evar_map -> constr miota_args -> constr val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool val contract_fix : evar_map -> fixpoint -> constr +val contract_cofix : evar_map -> cofixpoint -> constr (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : Environ.env -> Constant.t tableKey -> bool diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index e4b5dc1edf..9d15e98373 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -458,6 +458,25 @@ let contract_cofix_use_function env sigma f substl_checking_arity env (List.rev subbodies) sigma (nf_beta env sigma bodies.(bodynum)) +type 'a miota_args = { + mP : constr; (** the result type *) + mconstr : constr; (** the constructor *) + mci : case_info; (** special info to re-build pattern *) + mcargs : 'a list; (** the constructor's arguments *) + mlf : 'a array } (** the branch code vector *) + +let reduce_mind_case sigma mia = + match EConstr.kind sigma mia.mconstr with + | Construct ((ind_sp,i),u) -> +(* let ncargs = (fst mia.mci).(i-1) in*) + let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in + applist (mia.mlf.(i-1),real_cargs) + | CoFix cofix -> + let cofix_def = contract_cofix sigma cofix in + (* XXX Is NoInvert OK here? *) + mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) + | _ -> assert false + let reduce_mind_case_use_function func env sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((ind_sp,i),u) -> diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9bd7ccda5d..db76d08736 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp -let refresh_undefined_univs clenv = - match EConstr.kind clenv.evd clenv.templval.rebus with - | Var _ -> clenv, Univ.empty_level_subst - | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst - | _ -> - let evd', subst = Evd.refresh_undefined_universes clenv.evd in - let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in - { clenv with evd = evd'; templval = map_freelisted clenv.templval; - templtyp = map_freelisted clenv.templtyp }, subst - let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c diff --git a/proofs/clenv.mli b/proofs/clenv.mli index fd1e2fe593..43e808dac7 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -45,9 +45,6 @@ val mk_clenv_from_n : Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv -(** Refresh the universes in a clenv *) -val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst - (** {6 linking of clenvs } *) val clenv_fchain : diff --git a/tactics/auto.ml b/tactics/auto.ml index 3287c1c354..0931c3e61e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -12,11 +12,9 @@ open Pp open Util open Names open Termops -open EConstr open Environ open Genredexpr open Tactics -open Clenv open Locus open Proofview.Notations open Hints @@ -69,38 +67,7 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) -let connect_hint_clenv h gl = - let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in - (* [clenv] has been generated by a hint-making function, so the only relevant - data in its evarmap is the set of metas. The [evar_reset_evd] function - below just replaces the metas of sigma by those coming from the clenv. *) - let sigma = Tacmach.New.project gl in - let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in - (* Still, we need to update the universes *) - let clenv, c = - if h.hint_poly then - (* Refresh the instance of the hint *) - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let emap c = Vars.subst_univs_level_constr subst c in - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - (* Only metas are mentioning the old universes. *) - let clenv = { - templval = Evd.map_fl emap clenv.templval; - templtyp = Evd.map_fl emap clenv.templtyp; - evd = Evd.map_metas emap evd; - env = Proofview.Goal.env gl; - } in - clenv, emap c - else - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - { clenv with evd = evd ; env = Proofview.Goal.env gl }, c - in clenv, c - -let unify_resolve flags (h : hint) = - Proofview.Goal.enter begin fun gl -> - let clenv, c = connect_hint_clenv h gl in - Clenv.res_pf ~flags clenv - end +let unify_resolve flags h = Hints.hint_res_pf ~flags h let unify_resolve_nodelta h = unify_resolve auto_unif_flags h @@ -110,10 +77,10 @@ let unify_resolve_gen = function let exact h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (exact_check c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> exact_check c end (* Util *) diff --git a/tactics/auto.mli b/tactics/auto.mli index 903da143d2..bc2eee0e4c 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -12,7 +12,6 @@ open Names open EConstr -open Clenv open Pattern open Hints open Tactypes @@ -23,9 +22,6 @@ val default_search_depth : int ref val auto_flags_of_state : TransparentState.t -> Unification.unify_flags -val connect_hint_clenv - : hint -> Proofview.Goal.t -> clausenv * constr - (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index bb062bfc11..1f148e01fa 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -151,23 +151,15 @@ struct type t = Dn.t - let empty = Dn.empty + type pattern = Dn.pattern - let add = function - | None -> - (fun dn (c,v) -> - Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> - Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + let pattern st pat = match st with + | None -> Dn.pattern bounded_constr_pat_discr (pat, !dnet_depth) + | Some st -> Dn.pattern (bounded_constr_pat_discr_st st) (pat, !dnet_depth) - let rmv = function - | None -> - (fun dn (c,v) -> - Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> - Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + let empty = Dn.empty + let add = Dn.add + let rmv = Dn.rmv let lookup sigma = function | None -> diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 4358e5a8d9..2caa193202 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -28,10 +28,14 @@ module Make : sig type t + type pattern + + val pattern : TransparentState.t option -> constr_pattern -> pattern + val empty : t - val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t - val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t + val add : t -> pattern -> Z.t -> t + val rmv : t -> pattern -> Z.t -> t val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit diff --git a/tactics/cbn.ml b/tactics/cbn.ml index dfbcc9fbce..8f0966a486 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -571,7 +571,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | None -> fold ()) | Const (c,u as const) -> Reductionops.reduction_effect_hook env sigma c - (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); + (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack))))); if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then let u' = EInstance.kind sigma u in match constant_value_in env (c, u') with diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 63cafbf76d..36544883aa 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -144,61 +144,50 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st = } let e_give_exact flags h = - let { hint_term = c; hint_clnv = clenv } = h in let open Tacmach.New in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in - let c, sigma = - if h.hint_poly then - let clenv', subst = Clenv.refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in - let c = Vars.subst_univs_level_constr subst c in - c, evd - else c, sigma - in + let sigma, c = Hints.fresh_hint env sigma h in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> Clenv.unify ~flags t1 <*> exact_no_check c end -let unify_e_resolve flags = begin fun gls (h, _) -> - let clenv', c = connect_hint_clenv h gls in - Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv' - end - -let unify_resolve flags = begin fun gls (h, _) -> - let clenv', _ = connect_hint_clenv h gls in - Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv' +let unify_resolve ~with_evars flags h diff = match diff with +| None -> + Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h +| Some (diff, ty) -> + let () = assert (not h.hint_poly) in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let sigma, c = Hints.fresh_hint env sigma h in + let clenv = mk_clenv_from_env env sigma (Some diff) (c, ty) in + Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv end (** Application of a lemma using [refine] instead of the old [w_unify] *) -let unify_resolve_refine flags gls (h, n) = - let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in +let unify_resolve_refine flags h diff = + let len = match diff with None -> None | Some (diff, _) -> Some diff in + Proofview.Goal.enter begin fun gls -> let open Clenv in let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in Refine.refine ~typecheck:false begin fun sigma -> - let sigma, term, ty = - if h.hint_poly then - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let map c = Vars.subst_univs_level_constr subst c in - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - sigma, map c, map t - else - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - sigma, c, t - in - let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in - let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in - let sigma' = - Evarconv.(unify_leq_delay - ~flags:(default_flags_of flags.core_unify_flags.modulo_delta) - env sigma' cl.cl_concl concl) - in (sigma', term) end - -let unify_resolve_refine flags gl clenv = + let sigma, term = Hints.fresh_hint env sigma h in + let ty = Retyping.get_type_of env sigma term in + let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in + let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in + let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in + let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in + (sigma, term) + end + end + +let unify_resolve_refine flags h diff = Proofview.tclORELSE - (unify_resolve_refine flags gl clenv) + (unify_resolve_refine flags h diff) (fun (exn,info) -> match exn with | Evarconv.UnableToUnify _ -> @@ -211,35 +200,21 @@ let unify_resolve_refine flags gl clenv = (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. *) -let clenv_of_prods nprods h gl = - let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in - if poly || Int.equal nprods 0 then Some (None, clenv) - else - let sigma = Tacmach.New.project gl in - let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in - let diff = nb_prod sigma ty - nprods in - if (>=) diff 0 then - (* Was Some clenv... *) - Some (Some diff, - mk_clenv_from_n gl (Some diff) (c,ty)) - else None - let with_prods nprods h f = if get_typeclasses_limit_intros () then Proofview.Goal.enter begin fun gl -> - try match clenv_of_prods nprods h gl with - | None -> - let info = Exninfo.reify () in - Tacticals.New.tclZEROMSG ~info (str"Not enough premisses") - | Some (diff, clenv') -> - let h = { h with hint_clnv = clenv' } in - f gl (h, diff) - with e when CErrors.noncritical e -> - let e, info = Exninfo.capture e in - Proofview.tclZERO ~info e end + let { hint_term = c; hint_poly = poly } = h in + if poly || Int.equal nprods 0 then f None + else + let sigma = Tacmach.New.project gl in + let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in + let diff = nb_prod sigma ty - nprods in + if (>=) diff 0 then f (Some (diff, ty)) + else Tacticals.New.tclZEROMSG (str"Not enough premisses") + end else Proofview.Goal.enter begin fun gl -> - if Int.equal nprods 0 then f gl (h, None) + if Int.equal nprods 0 then f None else Tacticals.New.tclZEROMSG (str"Not enough premisses") end let matches_pattern concl pat = @@ -347,25 +322,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if get_typeclasses_filtered_unification () then let tac = with_prods nprods h - (fun gl clenv -> + (fun diff -> matches_pattern concl p <*> - unify_resolve_refine flags gl clenv) + unify_resolve_refine flags h diff) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = - with_prods nprods h (unify_resolve flags) in + with_prods nprods h (unify_resolve ~with_evars:false flags h) in Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | ERes_pf h -> if get_typeclasses_filtered_unification () then let tac = (with_prods nprods h - (fun gl clenv -> + (fun diff -> matches_pattern concl p <*> - unify_resolve_refine flags gl clenv)) in + unify_resolve_refine flags h diff)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = - with_prods nprods h (unify_e_resolve flags) in + with_prods nprods h (unify_resolve ~with_evars:true flags h) in Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | Give_exact h -> @@ -373,12 +348,12 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let tac = matches_pattern concl p <*> Proofview.Goal.enter - (fun gl -> unify_resolve_refine flags gl (h, None)) in + (fun gl -> unify_resolve_refine flags h None) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else e_give_exact flags h | Res_pf_THEN_trivial_fail h -> - let fst = with_prods nprods h (unify_e_resolve flags) in + let fst = with_prods nprods h (unify_resolve ~with_evars:true flags h) in let snd = if complete then Tacticals.New.tclIDTAC else e_trivial_fail_db only_classes db_list local_db secvars in Tacticals.New.tclTHEN fst snd @@ -1235,8 +1210,7 @@ let autoapply c i = (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in - unify_e_resolve flags gl (h, 0) <*> + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.make_unresolvables (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in diff --git a/tactics/dn.ml b/tactics/dn.ml index e1c9b7c0b5..07eb49442a 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -38,6 +38,8 @@ struct type t = Trie.t + type pattern = (Y.t * int) option list + let empty = Trie.empty (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in @@ -89,11 +91,13 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) in List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm)) - let add tm dna (pat,inf) = - let p = path_of dna pat in Trie.add p (ZSet.singleton inf) tm + let pattern dna pat = path_of dna pat + + let add tm p inf = + Trie.add p (ZSet.singleton inf) tm - let rmv tm dna (pat,inf) = - let p = path_of dna pat in Trie.remove p (ZSet.singleton inf) tm + let rmv tm p inf = + Trie.remove p (ZSet.singleton inf) tm let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm diff --git a/tactics/dn.mli b/tactics/dn.mli index 2a60c3eb82..287aa2b257 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -18,9 +18,13 @@ sig must decompose any tree into a label characterizing its root node and the list of its subtree *) - val add : t -> 'a decompose_fun -> 'a * Z.t -> t + type pattern - val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t + val pattern : 'a decompose_fun -> 'a -> pattern + + val add : t -> pattern -> Z.t -> t + + val rmv : t -> pattern -> Z.t -> t type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 686303a2ab..9a554b117e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -19,7 +19,6 @@ open Tacticals open Tacmach open Evd open Tactics -open Clenv open Auto open Genredexpr open Tactypes @@ -66,10 +65,7 @@ open Auto (***************************************************************************) let unify_e_resolve flags h = - Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv' - end + Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h let hintmap_of sigma secvars concl = (* Warning: for computation sharing, we need to return a closure *) @@ -87,10 +83,10 @@ let hintmap_of sigma secvars concl = let e_exact flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (e_give_exact c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c end let rec e_trivial_fail_db db_list local_db = diff --git a/tactics/equality.ml b/tactics/equality.ml index a2325b69cc..1689b0d3ad 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1416,6 +1416,11 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) +exception NothingToInject +let () = CErrors.register_handler (function + | NothingToInject -> Some (Pp.str "Nothing to inject.") + | _ -> None) + let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in let env = eq_clause.env in @@ -1429,7 +1434,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) | Inr [([],_,_)] -> - tclZEROMSG (str"Nothing to inject.") + Proofview.tclZERO NothingToInject | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) diff --git a/tactics/equality.mli b/tactics/equality.mli index e252eeab28..fdcbbc0e3c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -91,6 +91,7 @@ val discr_tac : evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic (* Below, if flag is [None], it takes the value from the dynamic value of the option *) +exception NothingToInject val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : inj_flags option -> intro_patterns option -> evars_flag -> diff --git a/tactics/hints.ml b/tactics/hints.ml index 386224824f..41b200bb83 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -258,7 +258,7 @@ let empty_se = { let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid -let add_tac pat t st se = +let add_tac pat t se = match pat with | None -> if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se @@ -267,12 +267,14 @@ let add_tac pat t st se = if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se else { se with sentry_pat = List.insert pri_order t se.sentry_pat; - sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); } + sentry_bnet = Bounded_net.add se.sentry_bnet pat t; } let rebuild_dn st se = let dn' = List.fold_left - (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) + (fun dn (id, t) -> + let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in + Bounded_net.add dn pat (id, t)) Bounded_net.empty se.sentry_pat in { se with sentry_bnet = dn' } @@ -636,8 +638,6 @@ struct is_unfold v.code.obj then None else Some gr | None -> None in - let dnst = if db.use_dn then Some db.hintdb_state else None in - let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in match k with | None -> let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in @@ -646,8 +646,14 @@ struct { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } else db | Some gr -> + let pat = + if not db.use_dn && is_exact v.code.obj then None + else + let dnst = if db.use_dn then Some db.hintdb_state else None in + Option.map (fun p -> Bounded_net.pattern dnst p) v.pat + in let oval = find gr db in - { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map } + { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map } let rebuild_db st' db = let db' = @@ -1593,3 +1599,45 @@ struct let repr (h : t) = h.code.obj end + +let connect_hint_clenv h gl = + let { hint_uctx = ctx; hint_clnv = clenv } = h in + (* [clenv] has been generated by a hint-making function, so the only relevant + data in its evarmap is the set of metas. The [evar_reset_evd] function + below just replaces the metas of sigma by those coming from the clenv. *) + let sigma = Tacmach.New.project gl in + let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in + (* Still, we need to update the universes *) + if h.hint_poly then + (* Refresh the instance of the hint *) + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let emap c = Vars.subst_univs_level_constr subst c in + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + (* Only metas are mentioning the old universes. *) + { + templval = Evd.map_fl emap clenv.templval; + templtyp = Evd.map_fl emap clenv.templtyp; + evd = Evd.map_metas emap evd; + env = Proofview.Goal.env gl; + } + else + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + { clenv with evd = evd ; env = Proofview.Goal.env gl } + +let fresh_hint env sigma h = + let { hint_term = c; hint_uctx = ctx } = h in + if h.hint_poly then + (* Refresh the instance of the hint *) + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let c = Vars.subst_univs_level_constr subst c in + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + sigma, c + else + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + sigma, c + +let hint_res_pf ?with_evars ?with_classes ?flags h = + Proofview.Goal.enter begin fun gl -> + let clenv = connect_hint_clenv h gl in + Clenv.res_pf ?with_evars ?with_classes ?flags clenv + end diff --git a/tactics/hints.mli b/tactics/hints.mli index 8243716624..f0fed75828 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -39,7 +39,7 @@ type 'a hint_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Genarg.glob_generic_argument (* Hint Extern *) -type hint = { +type hint = private { hint_term : constr; hint_type : types; hint_uctx : Univ.ContextSet.t; @@ -239,6 +239,11 @@ val wrap_hint_warning_fun : env -> evar_map -> (evar_map -> 'a * evar_map) -> 'a * evar_map (** Variant of the above for non-tactics *) +val fresh_hint : env -> evar_map -> hint -> evar_map * constr + +val hint_res_pf : ?with_evars:bool -> ?with_classes:bool -> + ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic + (** Printing hints *) val pr_searchtable : env -> evar_map -> Pp.t diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v index 0d034a65eb..ae46117e59 100644 --- a/test-suite/bugs/closed/bug_12483.v +++ b/test-suite/bugs/closed/bug_12483.v @@ -4,7 +4,7 @@ Goal False. Proof. cut (false = true). { intro H; discriminate H. } -change false with (1 <= 0)%float. +change false with (1 <=? 0)%float. rewrite leb_spec. Fail reflexivity. Abort. diff --git a/test-suite/micromega/bug_12790.v b/test-suite/micromega/bug_12790.v new file mode 100644 index 0000000000..39d640ebd9 --- /dev/null +++ b/test-suite/micromega/bug_12790.v @@ -0,0 +1,8 @@ +Require Import Lia. + +Goal forall (a b c d x: nat), +S c = a - b -> x <= x + (S c) * d. +Proof. +intros a b c d x H. +lia. +Qed. diff --git a/test-suite/micromega/bug_12791.v b/test-suite/micromega/bug_12791.v new file mode 100644 index 0000000000..8aec1904a4 --- /dev/null +++ b/test-suite/micromega/bug_12791.v @@ -0,0 +1,9 @@ +Require Import Lia. + +Definition t := nat. + +Goal forall (a b: t), let c := a in b = a -> b = c. +Proof. + intros a b c H. + lia. +Qed. diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v index 23d1e5bbae..75fd5c426f 100644 --- a/test-suite/primitive/float/compare.v +++ b/test-suite/primitive/float/compare.v @@ -6,380 +6,380 @@ Definition min_denorm := Eval compute in ldexp one (-1074)%Z. Definition min_norm := Eval compute in ldexp one (-1024)%Z. -Check (eq_refl false : nan == nan = false). -Check (eq_refl false : nan == nan = false). -Check (eq_refl false : nan < nan = false). -Check (eq_refl false : nan < nan = false). -Check (eq_refl false : nan <= nan = false). -Check (eq_refl false : nan <= nan = false). +Check (eq_refl false : nan =? nan = false). +Check (eq_refl false : nan =? nan = false). +Check (eq_refl false : nan <? nan = false). +Check (eq_refl false : nan <? nan = false). +Check (eq_refl false : nan <=? nan = false). +Check (eq_refl false : nan <=? nan = false). Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). -Check (eq_refl false <: nan == nan = false). -Check (eq_refl false <: nan == nan = false). -Check (eq_refl false <: nan < nan = false). -Check (eq_refl false <: nan < nan = false). -Check (eq_refl false <: nan <= nan = false). -Check (eq_refl false <: nan <= nan = false). +Check (eq_refl false <: nan =? nan = false). +Check (eq_refl false <: nan =? nan = false). +Check (eq_refl false <: nan <? nan = false). +Check (eq_refl false <: nan <? nan = false). +Check (eq_refl false <: nan <=? nan = false). +Check (eq_refl false <: nan <=? nan = false). Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). -Check (eq_refl false <<: nan == nan = false). -Check (eq_refl false <<: nan == nan = false). -Check (eq_refl false <<: nan < nan = false). -Check (eq_refl false <<: nan < nan = false). -Check (eq_refl false <<: nan <= nan = false). -Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl false <<: nan =? nan = false). +Check (eq_refl false <<: nan =? nan = false). +Check (eq_refl false <<: nan <? nan = false). +Check (eq_refl false <<: nan <? nan = false). +Check (eq_refl false <<: nan <=? nan = false). +Check (eq_refl false <<: nan <=? nan = false). Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). -Check (eq_refl false : nan == - nan = false). -Check (eq_refl false : - nan == nan = false). -Check (eq_refl false : nan < - nan = false). -Check (eq_refl false : - nan < nan = false). -Check (eq_refl false : nan <= - nan = false). -Check (eq_refl false : - nan <= nan = false). +Check (eq_refl false : nan =? - nan = false). +Check (eq_refl false : - nan =? nan = false). +Check (eq_refl false : nan <? - nan = false). +Check (eq_refl false : - nan <? nan = false). +Check (eq_refl false : nan <=? - nan = false). +Check (eq_refl false : - nan <=? nan = false). Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable). -Check (eq_refl false <: nan == - nan = false). -Check (eq_refl false <: - nan == nan = false). -Check (eq_refl false <: nan < - nan = false). -Check (eq_refl false <: - nan < nan = false). -Check (eq_refl false <: nan <= - nan = false). -Check (eq_refl false <: - nan <= nan = false). +Check (eq_refl false <: nan =? - nan = false). +Check (eq_refl false <: - nan =? nan = false). +Check (eq_refl false <: nan <? - nan = false). +Check (eq_refl false <: - nan <? nan = false). +Check (eq_refl false <: nan <=? - nan = false). +Check (eq_refl false <: - nan <=? nan = false). Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable). -Check (eq_refl false <<: nan == - nan = false). -Check (eq_refl false <<: - nan == nan = false). -Check (eq_refl false <<: nan < - nan = false). -Check (eq_refl false <<: - nan < nan = false). -Check (eq_refl false <<: nan <= - nan = false). -Check (eq_refl false <<: - nan <= nan = false). +Check (eq_refl false <<: nan =? - nan = false). +Check (eq_refl false <<: - nan =? nan = false). +Check (eq_refl false <<: nan <? - nan = false). +Check (eq_refl false <<: - nan <? nan = false). +Check (eq_refl false <<: nan <=? - nan = false). +Check (eq_refl false <<: - nan <=? nan = false). Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable). -Check (eq_refl true : one == one = true). -Check (eq_refl true : one == one = true). -Check (eq_refl false : one < one = false). -Check (eq_refl false : one < one = false). -Check (eq_refl true : one <= one = true). -Check (eq_refl true : one <= one = true). +Check (eq_refl true : one =? one = true). +Check (eq_refl true : one =? one = true). +Check (eq_refl false : one <? one = false). +Check (eq_refl false : one <? one = false). +Check (eq_refl true : one <=? one = true). +Check (eq_refl true : one <=? one = true). Check (eq_refl FEq : one ?= one = FEq). Check (eq_refl FEq : one ?= one = FEq). -Check (eq_refl true <: one == one = true). -Check (eq_refl true <: one == one = true). -Check (eq_refl false <: one < one = false). -Check (eq_refl false <: one < one = false). -Check (eq_refl true <: one <= one = true). -Check (eq_refl true <: one <= one = true). +Check (eq_refl true <: one =? one = true). +Check (eq_refl true <: one =? one = true). +Check (eq_refl false <: one <? one = false). +Check (eq_refl false <: one <? one = false). +Check (eq_refl true <: one <=? one = true). +Check (eq_refl true <: one <=? one = true). Check (eq_refl FEq <: one ?= one = FEq). Check (eq_refl FEq <: one ?= one = FEq). -Check (eq_refl true <<: one == one = true). -Check (eq_refl true <<: one == one = true). -Check (eq_refl false <<: one < one = false). -Check (eq_refl false <<: one < one = false). -Check (eq_refl true <<: one <= one = true). -Check (eq_refl true <<: one <= one = true). +Check (eq_refl true <<: one =? one = true). +Check (eq_refl true <<: one =? one = true). +Check (eq_refl false <<: one <? one = false). +Check (eq_refl false <<: one <? one = false). +Check (eq_refl true <<: one <=? one = true). +Check (eq_refl true <<: one <=? one = true). Check (eq_refl FEq <<: one ?= one = FEq). Check (eq_refl FEq <<: one ?= one = FEq). -Check (eq_refl true : zero == zero = true). -Check (eq_refl true : zero == zero = true). -Check (eq_refl false : zero < zero = false). -Check (eq_refl false : zero < zero = false). -Check (eq_refl true : zero <= zero = true). -Check (eq_refl true : zero <= zero = true). +Check (eq_refl true : zero =? zero = true). +Check (eq_refl true : zero =? zero = true). +Check (eq_refl false : zero <? zero = false). +Check (eq_refl false : zero <? zero = false). +Check (eq_refl true : zero <=? zero = true). +Check (eq_refl true : zero <=? zero = true). Check (eq_refl FEq : zero ?= zero = FEq). Check (eq_refl FEq : zero ?= zero = FEq). -Check (eq_refl true <: zero == zero = true). -Check (eq_refl true <: zero == zero = true). -Check (eq_refl false <: zero < zero = false). -Check (eq_refl false <: zero < zero = false). -Check (eq_refl true <: zero <= zero = true). -Check (eq_refl true <: zero <= zero = true). +Check (eq_refl true <: zero =? zero = true). +Check (eq_refl true <: zero =? zero = true). +Check (eq_refl false <: zero <? zero = false). +Check (eq_refl false <: zero <? zero = false). +Check (eq_refl true <: zero <=? zero = true). +Check (eq_refl true <: zero <=? zero = true). Check (eq_refl FEq <: zero ?= zero = FEq). Check (eq_refl FEq <: zero ?= zero = FEq). -Check (eq_refl true <<: zero == zero = true). -Check (eq_refl true <<: zero == zero = true). -Check (eq_refl false <<: zero < zero = false). -Check (eq_refl false <<: zero < zero = false). -Check (eq_refl true <<: zero <= zero = true). -Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl true <<: zero =? zero = true). +Check (eq_refl true <<: zero =? zero = true). +Check (eq_refl false <<: zero <? zero = false). +Check (eq_refl false <<: zero <? zero = false). +Check (eq_refl true <<: zero <=? zero = true). +Check (eq_refl true <<: zero <=? zero = true). Check (eq_refl FEq <<: zero ?= zero = FEq). Check (eq_refl FEq <<: zero ?= zero = FEq). -Check (eq_refl true : zero == - zero = true). -Check (eq_refl true : - zero == zero = true). -Check (eq_refl false : zero < - zero = false). -Check (eq_refl false : - zero < zero = false). -Check (eq_refl true : zero <= - zero = true). -Check (eq_refl true : - zero <= zero = true). +Check (eq_refl true : zero =? - zero = true). +Check (eq_refl true : - zero =? zero = true). +Check (eq_refl false : zero <? - zero = false). +Check (eq_refl false : - zero <? zero = false). +Check (eq_refl true : zero <=? - zero = true). +Check (eq_refl true : - zero <=? zero = true). Check (eq_refl FEq : zero ?= - zero = FEq). Check (eq_refl FEq : - zero ?= zero = FEq). -Check (eq_refl true <: zero == - zero = true). -Check (eq_refl true <: - zero == zero = true). -Check (eq_refl false <: zero < - zero = false). -Check (eq_refl false <: - zero < zero = false). -Check (eq_refl true <: zero <= - zero = true). -Check (eq_refl true <: - zero <= zero = true). +Check (eq_refl true <: zero =? - zero = true). +Check (eq_refl true <: - zero =? zero = true). +Check (eq_refl false <: zero <? - zero = false). +Check (eq_refl false <: - zero <? zero = false). +Check (eq_refl true <: zero <=? - zero = true). +Check (eq_refl true <: - zero <=? zero = true). Check (eq_refl FEq <: zero ?= - zero = FEq). Check (eq_refl FEq <: - zero ?= zero = FEq). -Check (eq_refl true <<: zero == - zero = true). -Check (eq_refl true <<: - zero == zero = true). -Check (eq_refl false <<: zero < - zero = false). -Check (eq_refl false <<: - zero < zero = false). -Check (eq_refl true <<: zero <= - zero = true). -Check (eq_refl true <<: - zero <= zero = true). +Check (eq_refl true <<: zero =? - zero = true). +Check (eq_refl true <<: - zero =? zero = true). +Check (eq_refl false <<: zero <? - zero = false). +Check (eq_refl false <<: - zero <? zero = false). +Check (eq_refl true <<: zero <=? - zero = true). +Check (eq_refl true <<: - zero <=? zero = true). Check (eq_refl FEq <<: zero ?= - zero = FEq). Check (eq_refl FEq <<: - zero ?= zero = FEq). -Check (eq_refl true : - zero == - zero = true). -Check (eq_refl true : - zero == - zero = true). -Check (eq_refl false : - zero < - zero = false). -Check (eq_refl false : - zero < - zero = false). -Check (eq_refl true : - zero <= - zero = true). -Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl true : - zero =? - zero = true). +Check (eq_refl true : - zero =? - zero = true). +Check (eq_refl false : - zero <? - zero = false). +Check (eq_refl false : - zero <? - zero = false). +Check (eq_refl true : - zero <=? - zero = true). +Check (eq_refl true : - zero <=? - zero = true). Check (eq_refl FEq : - zero ?= - zero = FEq). Check (eq_refl FEq : - zero ?= - zero = FEq). -Check (eq_refl true <: - zero == - zero = true). -Check (eq_refl true <: - zero == - zero = true). -Check (eq_refl false <: - zero < - zero = false). -Check (eq_refl false <: - zero < - zero = false). -Check (eq_refl true <: - zero <= - zero = true). -Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl true <: - zero =? - zero = true). +Check (eq_refl true <: - zero =? - zero = true). +Check (eq_refl false <: - zero <? - zero = false). +Check (eq_refl false <: - zero <? - zero = false). +Check (eq_refl true <: - zero <=? - zero = true). +Check (eq_refl true <: - zero <=? - zero = true). Check (eq_refl FEq <: - zero ?= - zero = FEq). Check (eq_refl FEq <: - zero ?= - zero = FEq). -Check (eq_refl true <<: - zero == - zero = true). -Check (eq_refl true <<: - zero == - zero = true). -Check (eq_refl false <<: - zero < - zero = false). -Check (eq_refl false <<: - zero < - zero = false). -Check (eq_refl true <<: - zero <= - zero = true). -Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl true <<: - zero =? - zero = true). +Check (eq_refl true <<: - zero =? - zero = true). +Check (eq_refl false <<: - zero <? - zero = false). +Check (eq_refl false <<: - zero <? - zero = false). +Check (eq_refl true <<: - zero <=? - zero = true). +Check (eq_refl true <<: - zero <=? - zero = true). Check (eq_refl FEq <<: - zero ?= - zero = FEq). Check (eq_refl FEq <<: - zero ?= - zero = FEq). -Check (eq_refl true : infinity == infinity = true). -Check (eq_refl true : infinity == infinity = true). -Check (eq_refl false : infinity < infinity = false). -Check (eq_refl false : infinity < infinity = false). -Check (eq_refl true : infinity <= infinity = true). -Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl true : infinity =? infinity = true). +Check (eq_refl true : infinity =? infinity = true). +Check (eq_refl false : infinity <? infinity = false). +Check (eq_refl false : infinity <? infinity = false). +Check (eq_refl true : infinity <=? infinity = true). +Check (eq_refl true : infinity <=? infinity = true). Check (eq_refl FEq : infinity ?= infinity = FEq). Check (eq_refl FEq : infinity ?= infinity = FEq). -Check (eq_refl true <: infinity == infinity = true). -Check (eq_refl true <: infinity == infinity = true). -Check (eq_refl false <: infinity < infinity = false). -Check (eq_refl false <: infinity < infinity = false). -Check (eq_refl true <: infinity <= infinity = true). -Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl true <: infinity =? infinity = true). +Check (eq_refl true <: infinity =? infinity = true). +Check (eq_refl false <: infinity <? infinity = false). +Check (eq_refl false <: infinity <? infinity = false). +Check (eq_refl true <: infinity <=? infinity = true). +Check (eq_refl true <: infinity <=? infinity = true). Check (eq_refl FEq <: infinity ?= infinity = FEq). Check (eq_refl FEq <: infinity ?= infinity = FEq). -Check (eq_refl true <<: infinity == infinity = true). -Check (eq_refl true <<: infinity == infinity = true). -Check (eq_refl false <<: infinity < infinity = false). -Check (eq_refl false <<: infinity < infinity = false). -Check (eq_refl true <<: infinity <= infinity = true). -Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl true <<: infinity =? infinity = true). +Check (eq_refl true <<: infinity =? infinity = true). +Check (eq_refl false <<: infinity <? infinity = false). +Check (eq_refl false <<: infinity <? infinity = false). +Check (eq_refl true <<: infinity <=? infinity = true). +Check (eq_refl true <<: infinity <=? infinity = true). Check (eq_refl FEq <<: infinity ?= infinity = FEq). Check (eq_refl FEq <<: infinity ?= infinity = FEq). -Check (eq_refl true : - infinity == - infinity = true). -Check (eq_refl true : - infinity == - infinity = true). -Check (eq_refl false : - infinity < - infinity = false). -Check (eq_refl false : - infinity < - infinity = false). -Check (eq_refl true : - infinity <= - infinity = true). -Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl true : - infinity =? - infinity = true). +Check (eq_refl true : - infinity =? - infinity = true). +Check (eq_refl false : - infinity <? - infinity = false). +Check (eq_refl false : - infinity <? - infinity = false). +Check (eq_refl true : - infinity <=? - infinity = true). +Check (eq_refl true : - infinity <=? - infinity = true). Check (eq_refl FEq : - infinity ?= - infinity = FEq). Check (eq_refl FEq : - infinity ?= - infinity = FEq). -Check (eq_refl true <: - infinity == - infinity = true). -Check (eq_refl true <: - infinity == - infinity = true). -Check (eq_refl false <: - infinity < - infinity = false). -Check (eq_refl false <: - infinity < - infinity = false). -Check (eq_refl true <: - infinity <= - infinity = true). -Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl true <: - infinity =? - infinity = true). +Check (eq_refl true <: - infinity =? - infinity = true). +Check (eq_refl false <: - infinity <? - infinity = false). +Check (eq_refl false <: - infinity <? - infinity = false). +Check (eq_refl true <: - infinity <=? - infinity = true). +Check (eq_refl true <: - infinity <=? - infinity = true). Check (eq_refl FEq <: - infinity ?= - infinity = FEq). Check (eq_refl FEq <: - infinity ?= - infinity = FEq). -Check (eq_refl true <<: - infinity == - infinity = true). -Check (eq_refl true <<: - infinity == - infinity = true). -Check (eq_refl false <<: - infinity < - infinity = false). -Check (eq_refl false <<: - infinity < - infinity = false). -Check (eq_refl true <<: - infinity <= - infinity = true). -Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl true <<: - infinity =? - infinity = true). +Check (eq_refl true <<: - infinity =? - infinity = true). +Check (eq_refl false <<: - infinity <? - infinity = false). +Check (eq_refl false <<: - infinity <? - infinity = false). +Check (eq_refl true <<: - infinity <=? - infinity = true). +Check (eq_refl true <<: - infinity <=? - infinity = true). Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). -Check (eq_refl false : min_denorm == min_norm = false). -Check (eq_refl false : min_norm == min_denorm = false). -Check (eq_refl true : min_denorm < min_norm = true). -Check (eq_refl false : min_norm < min_denorm = false). -Check (eq_refl true : min_denorm <= min_norm = true). -Check (eq_refl false : min_norm <= min_denorm = false). +Check (eq_refl false : min_denorm =? min_norm = false). +Check (eq_refl false : min_norm =? min_denorm = false). +Check (eq_refl true : min_denorm <? min_norm = true). +Check (eq_refl false : min_norm <? min_denorm = false). +Check (eq_refl true : min_denorm <=? min_norm = true). +Check (eq_refl false : min_norm <=? min_denorm = false). Check (eq_refl FLt : min_denorm ?= min_norm = FLt). Check (eq_refl FGt : min_norm ?= min_denorm = FGt). -Check (eq_refl false <: min_denorm == min_norm = false). -Check (eq_refl false <: min_norm == min_denorm = false). -Check (eq_refl true <: min_denorm < min_norm = true). -Check (eq_refl false <: min_norm < min_denorm = false). -Check (eq_refl true <: min_denorm <= min_norm = true). -Check (eq_refl false <: min_norm <= min_denorm = false). +Check (eq_refl false <: min_denorm =? min_norm = false). +Check (eq_refl false <: min_norm =? min_denorm = false). +Check (eq_refl true <: min_denorm <? min_norm = true). +Check (eq_refl false <: min_norm <? min_denorm = false). +Check (eq_refl true <: min_denorm <=? min_norm = true). +Check (eq_refl false <: min_norm <=? min_denorm = false). Check (eq_refl FLt <: min_denorm ?= min_norm = FLt). Check (eq_refl FGt <: min_norm ?= min_denorm = FGt). -Check (eq_refl false <<: min_denorm == min_norm = false). -Check (eq_refl false <<: min_norm == min_denorm = false). -Check (eq_refl true <<: min_denorm < min_norm = true). -Check (eq_refl false <<: min_norm < min_denorm = false). -Check (eq_refl true <<: min_denorm <= min_norm = true). -Check (eq_refl false <<: min_norm <= min_denorm = false). +Check (eq_refl false <<: min_denorm =? min_norm = false). +Check (eq_refl false <<: min_norm =? min_denorm = false). +Check (eq_refl true <<: min_denorm <? min_norm = true). +Check (eq_refl false <<: min_norm <? min_denorm = false). +Check (eq_refl true <<: min_denorm <=? min_norm = true). +Check (eq_refl false <<: min_norm <=? min_denorm = false). Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt). Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt). -Check (eq_refl false : min_denorm == one = false). -Check (eq_refl false : one == min_denorm = false). -Check (eq_refl true : min_denorm < one = true). -Check (eq_refl false : one < min_denorm = false). -Check (eq_refl true : min_denorm <= one = true). -Check (eq_refl false : one <= min_denorm = false). +Check (eq_refl false : min_denorm =? one = false). +Check (eq_refl false : one =? min_denorm = false). +Check (eq_refl true : min_denorm <? one = true). +Check (eq_refl false : one <? min_denorm = false). +Check (eq_refl true : min_denorm <=? one = true). +Check (eq_refl false : one <=? min_denorm = false). Check (eq_refl FLt : min_denorm ?= one = FLt). Check (eq_refl FGt : one ?= min_denorm = FGt). -Check (eq_refl false <: min_denorm == one = false). -Check (eq_refl false <: one == min_denorm = false). -Check (eq_refl true <: min_denorm < one = true). -Check (eq_refl false <: one < min_denorm = false). -Check (eq_refl true <: min_denorm <= one = true). -Check (eq_refl false <: one <= min_denorm = false). +Check (eq_refl false <: min_denorm =? one = false). +Check (eq_refl false <: one =? min_denorm = false). +Check (eq_refl true <: min_denorm <? one = true). +Check (eq_refl false <: one <? min_denorm = false). +Check (eq_refl true <: min_denorm <=? one = true). +Check (eq_refl false <: one <=? min_denorm = false). Check (eq_refl FLt <: min_denorm ?= one = FLt). Check (eq_refl FGt <: one ?= min_denorm = FGt). -Check (eq_refl false <<: min_denorm == one = false). -Check (eq_refl false <<: one == min_denorm = false). -Check (eq_refl true <<: min_denorm < one = true). -Check (eq_refl false <<: one < min_denorm = false). -Check (eq_refl true <<: min_denorm <= one = true). -Check (eq_refl false <<: one <= min_denorm = false). +Check (eq_refl false <<: min_denorm =? one = false). +Check (eq_refl false <<: one =? min_denorm = false). +Check (eq_refl true <<: min_denorm <? one = true). +Check (eq_refl false <<: one <? min_denorm = false). +Check (eq_refl true <<: min_denorm <=? one = true). +Check (eq_refl false <<: one <=? min_denorm = false). Check (eq_refl FLt <<: min_denorm ?= one = FLt). Check (eq_refl FGt <<: one ?= min_denorm = FGt). -Check (eq_refl false : min_norm == one = false). -Check (eq_refl false : one == min_norm = false). -Check (eq_refl true : min_norm < one = true). -Check (eq_refl false : one < min_norm = false). -Check (eq_refl true : min_norm <= one = true). -Check (eq_refl false : one <= min_norm = false). +Check (eq_refl false : min_norm =? one = false). +Check (eq_refl false : one =? min_norm = false). +Check (eq_refl true : min_norm <? one = true). +Check (eq_refl false : one <? min_norm = false). +Check (eq_refl true : min_norm <=? one = true). +Check (eq_refl false : one <=? min_norm = false). Check (eq_refl FLt : min_norm ?= one = FLt). Check (eq_refl FGt : one ?= min_norm = FGt). -Check (eq_refl false <: min_norm == one = false). -Check (eq_refl false <: one == min_norm = false). -Check (eq_refl true <: min_norm < one = true). -Check (eq_refl false <: one < min_norm = false). -Check (eq_refl true <: min_norm <= one = true). -Check (eq_refl false <: one <= min_norm = false). +Check (eq_refl false <: min_norm =? one = false). +Check (eq_refl false <: one =? min_norm = false). +Check (eq_refl true <: min_norm <? one = true). +Check (eq_refl false <: one <? min_norm = false). +Check (eq_refl true <: min_norm <=? one = true). +Check (eq_refl false <: one <=? min_norm = false). Check (eq_refl FLt <: min_norm ?= one = FLt). Check (eq_refl FGt <: one ?= min_norm = FGt). -Check (eq_refl false <<: min_norm == one = false). -Check (eq_refl false <<: one == min_norm = false). -Check (eq_refl true <<: min_norm < one = true). -Check (eq_refl false <<: one < min_norm = false). -Check (eq_refl true <<: min_norm <= one = true). -Check (eq_refl false <<: one <= min_norm = false). +Check (eq_refl false <<: min_norm =? one = false). +Check (eq_refl false <<: one =? min_norm = false). +Check (eq_refl true <<: min_norm <? one = true). +Check (eq_refl false <<: one <? min_norm = false). +Check (eq_refl true <<: min_norm <=? one = true). +Check (eq_refl false <<: one <=? min_norm = false). Check (eq_refl FLt <<: min_norm ?= one = FLt). Check (eq_refl FGt <<: one ?= min_norm = FGt). -Check (eq_refl false : one == infinity = false). -Check (eq_refl false : infinity == one = false). -Check (eq_refl true : one < infinity = true). -Check (eq_refl false : infinity < one = false). -Check (eq_refl true : one <= infinity = true). -Check (eq_refl false : infinity <= one = false). +Check (eq_refl false : one =? infinity = false). +Check (eq_refl false : infinity =? one = false). +Check (eq_refl true : one <? infinity = true). +Check (eq_refl false : infinity <? one = false). +Check (eq_refl true : one <=? infinity = true). +Check (eq_refl false : infinity <=? one = false). Check (eq_refl FLt : one ?= infinity = FLt). Check (eq_refl FGt : infinity ?= one = FGt). -Check (eq_refl false <: one == infinity = false). -Check (eq_refl false <: infinity == one = false). -Check (eq_refl true <: one < infinity = true). -Check (eq_refl false <: infinity < one = false). -Check (eq_refl true <: one <= infinity = true). -Check (eq_refl false <: infinity <= one = false). +Check (eq_refl false <: one =? infinity = false). +Check (eq_refl false <: infinity =? one = false). +Check (eq_refl true <: one <? infinity = true). +Check (eq_refl false <: infinity <? one = false). +Check (eq_refl true <: one <=? infinity = true). +Check (eq_refl false <: infinity <=? one = false). Check (eq_refl FLt <: one ?= infinity = FLt). Check (eq_refl FGt <: infinity ?= one = FGt). -Check (eq_refl false <<: one == infinity = false). -Check (eq_refl false <<: infinity == one = false). -Check (eq_refl true <<: one < infinity = true). -Check (eq_refl false <<: infinity < one = false). -Check (eq_refl true <<: one <= infinity = true). -Check (eq_refl false <<: infinity <= one = false). +Check (eq_refl false <<: one =? infinity = false). +Check (eq_refl false <<: infinity =? one = false). +Check (eq_refl true <<: one <? infinity = true). +Check (eq_refl false <<: infinity <? one = false). +Check (eq_refl true <<: one <=? infinity = true). +Check (eq_refl false <<: infinity <=? one = false). Check (eq_refl FLt <<: one ?= infinity = FLt). Check (eq_refl FGt <<: infinity ?= one = FGt). -Check (eq_refl false : - infinity == infinity = false). -Check (eq_refl false : infinity == - infinity = false). -Check (eq_refl true : - infinity < infinity = true). -Check (eq_refl false : infinity < - infinity = false). -Check (eq_refl true : - infinity <= infinity = true). -Check (eq_refl false : infinity <= - infinity = false). +Check (eq_refl false : - infinity =? infinity = false). +Check (eq_refl false : infinity =? - infinity = false). +Check (eq_refl true : - infinity <? infinity = true). +Check (eq_refl false : infinity <? - infinity = false). +Check (eq_refl true : - infinity <=? infinity = true). +Check (eq_refl false : infinity <=? - infinity = false). Check (eq_refl FLt : - infinity ?= infinity = FLt). Check (eq_refl FGt : infinity ?= - infinity = FGt). -Check (eq_refl false <: - infinity == infinity = false). -Check (eq_refl false <: infinity == - infinity = false). -Check (eq_refl true <: - infinity < infinity = true). -Check (eq_refl false <: infinity < - infinity = false). -Check (eq_refl true <: - infinity <= infinity = true). -Check (eq_refl false <: infinity <= - infinity = false). +Check (eq_refl false <: - infinity =? infinity = false). +Check (eq_refl false <: infinity =? - infinity = false). +Check (eq_refl true <: - infinity <? infinity = true). +Check (eq_refl false <: infinity <? - infinity = false). +Check (eq_refl true <: - infinity <=? infinity = true). +Check (eq_refl false <: infinity <=? - infinity = false). Check (eq_refl FLt <: - infinity ?= infinity = FLt). Check (eq_refl FGt <: infinity ?= - infinity = FGt). -Check (eq_refl false <<: - infinity == infinity = false). -Check (eq_refl false <<: infinity == - infinity = false). -Check (eq_refl true <<: - infinity < infinity = true). -Check (eq_refl false <<: infinity < - infinity = false). -Check (eq_refl true <<: - infinity <= infinity = true). -Check (eq_refl false <<: infinity <= - infinity = false). +Check (eq_refl false <<: - infinity =? infinity = false). +Check (eq_refl false <<: infinity =? - infinity = false). +Check (eq_refl true <<: - infinity <? infinity = true). +Check (eq_refl false <<: infinity <? - infinity = false). +Check (eq_refl true <<: - infinity <=? infinity = true). +Check (eq_refl false <<: infinity <=? - infinity = false). Check (eq_refl FLt <<: - infinity ?= infinity = FLt). Check (eq_refl FGt <<: infinity ?= - infinity = FGt). -Check (eq_refl false : - infinity == one = false). -Check (eq_refl false : one == - infinity = false). -Check (eq_refl true : - infinity < one = true). -Check (eq_refl false : one < - infinity = false). -Check (eq_refl true : - infinity <= one = true). -Check (eq_refl false : one <= - infinity = false). +Check (eq_refl false : - infinity =? one = false). +Check (eq_refl false : one =? - infinity = false). +Check (eq_refl true : - infinity <? one = true). +Check (eq_refl false : one <? - infinity = false). +Check (eq_refl true : - infinity <=? one = true). +Check (eq_refl false : one <=? - infinity = false). Check (eq_refl FLt : - infinity ?= one = FLt). Check (eq_refl FGt : one ?= - infinity = FGt). -Check (eq_refl false <: - infinity == one = false). -Check (eq_refl false <: one == - infinity = false). -Check (eq_refl true <: - infinity < one = true). -Check (eq_refl false <: one < - infinity = false). -Check (eq_refl true <: - infinity <= one = true). -Check (eq_refl false <: one <= - infinity = false). +Check (eq_refl false <: - infinity =? one = false). +Check (eq_refl false <: one =? - infinity = false). +Check (eq_refl true <: - infinity <? one = true). +Check (eq_refl false <: one <? - infinity = false). +Check (eq_refl true <: - infinity <=? one = true). +Check (eq_refl false <: one <=? - infinity = false). Check (eq_refl FLt <: - infinity ?= one = FLt). Check (eq_refl FGt <: one ?= - infinity = FGt). -Check (eq_refl false <<: - infinity == one = false). -Check (eq_refl false <<: one == - infinity = false). -Check (eq_refl true <<: - infinity < one = true). -Check (eq_refl false <<: one < - infinity = false). -Check (eq_refl true <<: - infinity <= one = true). -Check (eq_refl false <<: one <= - infinity = false). +Check (eq_refl false <<: - infinity =? one = false). +Check (eq_refl false <<: one =? - infinity = false). +Check (eq_refl true <<: - infinity <? one = true). +Check (eq_refl false <<: one <? - infinity = false). +Check (eq_refl true <<: - infinity <=? one = true). +Check (eq_refl false <<: one <=? - infinity = false). Check (eq_refl FLt <<: - infinity ?= one = FLt). Check (eq_refl FGt <<: one ?= - infinity = FGt). diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh index cd87eb4e5b..6e3dd6d04b 100755 --- a/test-suite/primitive/float/gen_compare.sh +++ b/test-suite/primitive/float/gen_compare.sh @@ -20,7 +20,7 @@ genTest() { echo >&2 "genTest expects 10 arguments" fi TACTICS=(":" "<:" "<<:") - OPS=("==" "<" "<=" "?=") + OPS=("=?" "<?" "<=?" "?=") x="$1" y="$2" OPS1=("$3" "$4" "$5" "$6") # for x y diff --git a/test-suite/primitive/uint63/eqb.v b/test-suite/primitive/uint63/eqb.v index dcc0b71f6d..43c98e2b6f 100644 --- a/test-suite/primitive/uint63/eqb.v +++ b/test-suite/primitive/uint63/eqb.v @@ -4,14 +4,14 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 == 1 = true). -Check (eq_refl true <: 1 == 1 = true). -Check (eq_refl true <<: 1 == 1 = true). -Definition compute1 := Eval compute in 1 == 1. +Check (eq_refl : 1 =? 1 = true). +Check (eq_refl true <: 1 =? 1 = true). +Check (eq_refl true <<: 1 =? 1 = true). +Definition compute1 := Eval compute in 1 =? 1. Check (eq_refl compute1 : true = true). -Check (eq_refl : 9223372036854775807 == 0 = false). -Check (eq_refl false <: 9223372036854775807 == 0 = false). -Check (eq_refl false <<: 9223372036854775807 == 0 = false). -Definition compute2 := Eval compute in 9223372036854775807 == 0. +Check (eq_refl : 9223372036854775807 =? 0 = false). +Check (eq_refl false <: 9223372036854775807 =? 0 = false). +Check (eq_refl false <<: 9223372036854775807 =? 0 = false). +Definition compute2 := Eval compute in 9223372036854775807 =? 0. Check (eq_refl compute2 : false = false). diff --git a/test-suite/primitive/uint63/leb.v b/test-suite/primitive/uint63/leb.v index 5354919978..e5142282ae 100644 --- a/test-suite/primitive/uint63/leb.v +++ b/test-suite/primitive/uint63/leb.v @@ -4,20 +4,20 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 <= 1 = true). -Check (eq_refl true <: 1 <= 1 = true). -Check (eq_refl true <<: 1 <= 1 = true). -Definition compute1 := Eval compute in 1 <= 1. +Check (eq_refl : 1 <=? 1 = true). +Check (eq_refl true <: 1 <=? 1 = true). +Check (eq_refl true <<: 1 <=? 1 = true). +Definition compute1 := Eval compute in 1 <=? 1. Check (eq_refl compute1 : true = true). -Check (eq_refl : 1 <= 2 = true). -Check (eq_refl true <: 1 <= 2 = true). -Check (eq_refl true <<: 1 <= 2 = true). -Definition compute2 := Eval compute in 1 <= 2. +Check (eq_refl : 1 <=? 2 = true). +Check (eq_refl true <: 1 <=? 2 = true). +Check (eq_refl true <<: 1 <=? 2 = true). +Definition compute2 := Eval compute in 1 <=? 2. Check (eq_refl compute2 : true = true). -Check (eq_refl : 9223372036854775807 <= 0 = false). -Check (eq_refl false <: 9223372036854775807 <= 0 = false). -Check (eq_refl false <<: 9223372036854775807 <= 0 = false). -Definition compute3 := Eval compute in 9223372036854775807 <= 0. +Check (eq_refl : 9223372036854775807 <=? 0 = false). +Check (eq_refl false <: 9223372036854775807 <=? 0 = false). +Check (eq_refl false <<: 9223372036854775807 <=? 0 = false). +Definition compute3 := Eval compute in 9223372036854775807 <=? 0. Check (eq_refl compute3 : false = false). diff --git a/test-suite/primitive/uint63/ltb.v b/test-suite/primitive/uint63/ltb.v index 7ae5ac6493..50cef6be66 100644 --- a/test-suite/primitive/uint63/ltb.v +++ b/test-suite/primitive/uint63/ltb.v @@ -4,20 +4,20 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 < 1 = false). -Check (eq_refl false <: 1 < 1 = false). -Check (eq_refl false <<: 1 < 1 = false). -Definition compute1 := Eval compute in 1 < 1. +Check (eq_refl : 1 <? 1 = false). +Check (eq_refl false <: 1 <? 1 = false). +Check (eq_refl false <<: 1 <? 1 = false). +Definition compute1 := Eval compute in 1 <? 1. Check (eq_refl compute1 : false = false). -Check (eq_refl : 1 < 2 = true). -Check (eq_refl true <: 1 < 2 = true). -Check (eq_refl true <<: 1 < 2 = true). -Definition compute2 := Eval compute in 1 < 2. +Check (eq_refl : 1 <? 2 = true). +Check (eq_refl true <: 1 <? 2 = true). +Check (eq_refl true <<: 1 <? 2 = true). +Definition compute2 := Eval compute in 1 <? 2. Check (eq_refl compute2 : true = true). -Check (eq_refl : 9223372036854775807 < 0 = false). -Check (eq_refl false <: 9223372036854775807 < 0 = false). -Check (eq_refl false <<: 9223372036854775807 < 0 = false). -Definition compute3 := Eval compute in 9223372036854775807 < 0. +Check (eq_refl : 9223372036854775807 <? 0 = false). +Check (eq_refl false <: 9223372036854775807 <? 0 = false). +Check (eq_refl false <<: 9223372036854775807 <? 0 = false). +Definition compute3 := Eval compute in 9223372036854775807 <? 0. Check (eq_refl compute3 : false = false). diff --git a/test-suite/primitive/uint63/mod.v b/test-suite/primitive/uint63/mod.v index 5307eed493..3ad6312c2c 100644 --- a/test-suite/primitive/uint63/mod.v +++ b/test-suite/primitive/uint63/mod.v @@ -4,14 +4,14 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 6 \% 3 = 0). -Check (eq_refl 0 <: 6 \% 3 = 0). -Check (eq_refl 0 <<: 6 \% 3 = 0). -Definition compute1 := Eval compute in 6 \% 3. +Check (eq_refl : 6 mod 3 = 0). +Check (eq_refl 0 <: 6 mod 3 = 0). +Check (eq_refl 0 <<: 6 mod 3 = 0). +Definition compute1 := Eval compute in 6 mod 3. Check (eq_refl compute1 : 0 = 0). -Check (eq_refl : 5 \% 3 = 2). -Check (eq_refl 2 <: 5 \% 3 = 2). -Check (eq_refl 2 <<: 5 \% 3 = 2). -Definition compute2 := Eval compute in 5 \% 3. +Check (eq_refl : 5 mod 3 = 2). +Check (eq_refl 2 <: 5 mod 3 = 2). +Check (eq_refl 2 <<: 5 mod 3 = 2). +Definition compute2 := Eval compute in 5 mod 3. Check (eq_refl compute2 : 2 = 2). diff --git a/test-suite/primitive/uint63/unsigned.v b/test-suite/primitive/uint63/unsigned.v index 82920bd201..6224e9d15b 100644 --- a/test-suite/primitive/uint63/unsigned.v +++ b/test-suite/primitive/uint63/unsigned.v @@ -11,8 +11,8 @@ Check (eq_refl 0 <<: 1/(0-1) = 0). Definition compute1 := Eval compute in 1/(0-1). Check (eq_refl compute1 : 0 = 0). -Check (eq_refl : 3 \% (0-1) = 3). -Check (eq_refl 3 <: 3 \% (0-1) = 3). -Check (eq_refl 3 <<: 3 \% (0-1) = 3). -Definition compute2 := Eval compute in 3 \% (0-1). +Check (eq_refl : 3 mod (0-1) = 3). +Check (eq_refl 3 <: 3 mod (0-1) = 3). +Check (eq_refl 3 <<: 3 mod (0-1) = 3). +Definition compute2 := Eval compute in 3 mod (0-1). Check (eq_refl compute2 : 3 = 3). diff --git a/test-suite/ssr/noting_to_inject.v b/test-suite/ssr/noting_to_inject.v new file mode 100644 index 0000000000..95bbd3e777 --- /dev/null +++ b/test-suite/ssr/noting_to_inject.v @@ -0,0 +1,9 @@ +Require Import ssreflect ssrfun ssrbool. + + +Goal forall b : bool, b -> False. +Set Warnings "+spurious-ssr-injection". +Fail move=> b []. +Set Warnings "-spurious-ssr-injection". +move=> b []. +Abort. diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v index 282f56267c..3511ba0918 100644 --- a/theories/Array/PArray.v +++ b/theories/Array/PArray.v @@ -45,19 +45,19 @@ Local Open Scope array_scope. Primitive max_length := #array_max_length. (** Axioms *) -Axiom get_out_of_bounds : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t. +Axiom get_out_of_bounds : forall A (t:array A) i, (i <? length t) = false -> t.[i] = default t. -Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. +Axiom get_set_same : forall A t i (a:A), (i <? length t) = true -> t.[i<-a].[i] = a. Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. Axiom default_set : forall A t i (a:A), default t.[i<-a] = default t. Axiom get_make : forall A (a:A) size i, (make size a).[i] = a. -Axiom leb_length : forall A (t:array A), length t <= max_length = true. +Axiom leb_length : forall A (t:array A), length t <=? max_length = true. Axiom length_make : forall A size (a:A), - length (make size a) = if size <= max_length then size else max_length. + length (make size a) = if size <=? max_length then size else max_length. Axiom length_set : forall A t i (a:A), length t.[i<-a] = length t. @@ -69,7 +69,7 @@ Axiom length_reroot : forall A (t:array A), length (reroot t) = length t. Axiom array_ext : forall A (t1 t2:array A), length t1 = length t2 -> - (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> + (forall i, i <? length t1 = true -> t1.[i] = t2.[i]) -> default t1 = default t2 -> t1 = t2. @@ -77,7 +77,7 @@ Axiom array_ext : forall A (t1 t2:array A), Lemma default_copy A (t:array A) : default (copy t) = default t. Proof. - assert (irr_lt : length t < length t = false). + assert (irr_lt : length t <? length t = false). destruct (Int63.ltbP (length t) (length t)); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. assert (get_copy := get_copy A t (length t)). @@ -87,7 +87,7 @@ Qed. Lemma default_make A (a : A) size : default (make size a) = a. Proof. - assert (irr_lt : length (make size a) < length (make size a) = false). + assert (irr_lt : length (make size a) <? length (make size a) = false). destruct (Int63.ltbP (length (make size a)) (length (make size a))); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. assert (get_make := get_make A a size (length (make size a))). @@ -96,7 +96,7 @@ Qed. Lemma default_reroot A (t:array A) : default (reroot t) = default t. Proof. - assert (irr_lt : length t < length t = false). + assert (irr_lt : length t <? length t = false). destruct (Int63.ltbP (length t) (length t)); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. assert (get_reroot := get_reroot A t (length t)). @@ -107,16 +107,16 @@ Qed. Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t. Proof. - case_eq (i < length t); intros. + case_eq (i <? length t); intros. rewrite get_set_same; trivial. rewrite get_out_of_bounds, default_set; trivial. rewrite length_set; trivial. Qed. Lemma get_not_default_lt A (t:array A) x : - t.[x] <> default t -> (x < length t) = true. + t.[x] <> default t -> (x <? length t) = true. Proof. intros Hd. - case_eq (x < length t); intros Heq; [trivial | ]. + case_eq (x <? length t); intros Heq; [trivial | ]. elim Hd; rewrite get_out_of_bounds; trivial. Qed. diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v index f4aa1f81c6..78df357c0f 100644 --- a/theories/Floats/FloatAxioms.v +++ b/theories/Floats/FloatAxioms.v @@ -38,9 +38,9 @@ Qed. Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x). Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x). -Axiom eqb_spec : forall x y, (x == y)%float = SFeqb (Prim2SF x) (Prim2SF y). -Axiom ltb_spec : forall x y, (x < y)%float = SFltb (Prim2SF x) (Prim2SF y). -Axiom leb_spec : forall x y, (x <= y)%float = SFleb (Prim2SF x) (Prim2SF y). +Axiom eqb_spec : forall x y, (x =? y)%float = SFeqb (Prim2SF x) (Prim2SF y). +Axiom ltb_spec : forall x y, (x <? y)%float = SFltb (Prim2SF x) (Prim2SF y). +Axiom leb_spec : forall x y, (x <=? y)%float = SFleb (Prim2SF x) (Prim2SF y). Definition flatten_cmp_opt c := match c with diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v index e5a9748481..ed7947aa63 100644 --- a/theories/Floats/PrimFloat.v +++ b/theories/Floats/PrimFloat.v @@ -27,9 +27,11 @@ Register float_class as kernel.ind_f_class. Primitive float := #float64_type. (** ** Syntax support *) +Module Import PrimFloatNotationsInternalA. Declare Scope float_scope. Delimit Scope float_scope with float. Bind Scope float_scope with float. +End PrimFloatNotationsInternalA. Declare ML Module "float_syntax_plugin". @@ -41,31 +43,34 @@ Primitive abs := #float64_abs. Primitive sqrt := #float64_sqrt. Primitive opp := #float64_opp. -Notation "- x" := (opp x) : float_scope. Primitive eqb := #float64_eq. -Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope. Primitive ltb := #float64_lt. -Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope. Primitive leb := #float64_le. -Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope. Primitive compare := #float64_compare. -Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope. Primitive mul := #float64_mul. -Notation "x * y" := (mul x y) : float_scope. Primitive add := #float64_add. -Notation "x + y" := (add x y) : float_scope. Primitive sub := #float64_sub. -Notation "x - y" := (sub x y) : float_scope. Primitive div := #float64_div. + +Module Import PrimFloatNotationsInternalB. +Notation "- x" := (opp x) : float_scope. +Notation "x =? y" := (eqb x y) (at level 70, no associativity) : float_scope. +Notation "x <? y" := (ltb x y) (at level 70, no associativity) : float_scope. +Notation "x <=? y" := (leb x y) (at level 70, no associativity) : float_scope. +Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope. +Notation "x * y" := (mul x y) : float_scope. +Notation "x + y" := (add x y) : float_scope. +Notation "x - y" := (sub x y) : float_scope. Notation "x / y" := (div x y) : float_scope. +End PrimFloatNotationsInternalB. (** ** Conversions *) @@ -114,15 +119,27 @@ Definition neg_zero := Eval compute in (-zero)%float. Definition two := Eval compute in (of_int63 2). (** ** Predicates and helper functions *) -Definition is_nan f := negb (f == f)%float. +Definition is_nan f := negb (f =? f)%float. -Definition is_zero f := (f == zero)%float. (* note: 0 == -0 with floats *) +Definition is_zero f := (f =? zero)%float. (* note: 0 =? -0 with floats *) -Definition is_infinity f := (abs f == infinity)%float. +Definition is_infinity f := (abs f =? infinity)%float. Definition is_finite (x : float) := negb (is_nan x || is_infinity x). (** [get_sign]: return [true] for [-] sign, [false] for [+] sign. *) Definition get_sign f := let f := if is_zero f then (one / f)%float else f in - (f < zero)%float. + (f <? zero)%float. + +Module Export PrimFloatNotations. + Local Open Scope float_scope. + #[deprecated(since="8.13",note="use infix <? instead")] + Notation "x < y" := (x <? y) (at level 70, no associativity) : float_scope. + #[deprecated(since="8.13",note="use infix <=? instead")] + Notation "x <= y" := (x <=? y) (at level 70, no associativity) : float_scope. + #[deprecated(since="8.13",note="use infix =? instead")] + Notation "x == y" := (x =? y) (at level 70, no associativity) : float_scope. + Export PrimFloatNotationsInternalA. + Export PrimFloatNotationsInternalB. +End PrimFloatNotations. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 8ab12ae534..77be679070 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -272,12 +272,18 @@ Proof with auto. - destruct H; subst... Qed. -Definition prod_uncurry (A B C:Type) (f:A * B -> C) +Definition curry {A B C:Type} (f:A * B -> C) (x:A) (y:B) : C := f (x,y). -Definition prod_curry (A B C:Type) (f:A -> B -> C) +Definition uncurry {A B C:Type} (f:A -> B -> C) (p:A * B) : C := match p with (x, y) => f x y end. +#[deprecated(since = "8.13", note = "Use curry instead.")] +Definition prod_uncurry (A B C:Type) : (A * B -> C) -> A -> B -> C := curry. + +#[deprecated(since = "8.13", note = "Use uncurry instead.")] +Definition prod_curry (A B C:Type) : (A -> B -> C) -> A * B -> C := uncurry. + Import EqNotations. Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2), diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c3c69f46f3..e0eae7c287 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -3157,6 +3157,44 @@ Section Repeat. - f_equal; apply IHn. Qed. + Lemma repeat_app x n m : + repeat x (n + m) = repeat x n ++ repeat x m. + Proof. + induction n as [|n IHn]; simpl; auto. + now rewrite IHn. + Qed. + + Lemma repeat_eq_app x n l1 l2 : + repeat x n = l1 ++ l2 -> repeat x (length l1) = l1 /\ repeat x (length l2) = l2. + Proof. + revert n; induction l1 as [|a l1 IHl1]; simpl; intros n Hr; subst. + - repeat split; now rewrite repeat_length. + - destruct n; inversion Hr as [ [Heq Hr0] ]; subst. + now apply IHl1 in Hr0 as [-> ->]. + Qed. + + Lemma repeat_eq_cons x y n l : + repeat x n = y :: l -> x = y /\ repeat x (pred n) = l. + Proof. + intros Hr. + destruct n; inversion_clear Hr; auto. + Qed. + + Lemma repeat_eq_elt x y n l1 l2 : + repeat x n = l1 ++ y :: l2 -> x = y /\ repeat x (length l1) = l1 /\ repeat x (length l2) = l2. + Proof. + intros Hr; apply repeat_eq_app in Hr as [Hr1 Hr2]; subst. + apply repeat_eq_cons in Hr2; intuition. + Qed. + + Lemma Forall_eq_repeat x l : + Forall (eq x) l -> l = repeat x (length l). + Proof. + induction l as [|a l IHl]; simpl; intros HF; auto. + inversion_clear HF as [ | ? ? ? HF']; subst. + now rewrite (IHl HF') at 1. + Qed. + End Repeat. Lemma repeat_to_concat A n (a:A) : diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 5f903c41cb..2a26b6b12a 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -48,7 +48,7 @@ Definition mulc_WW x y := Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : int63_scope. Definition pos_mod p x := - if p <= digits then + if p <=? digits then let p := digits - p in (x << p) >> p else x. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 2c112c3469..383c0aff3a 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -31,56 +31,61 @@ Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. Declare ML Module "int63_syntax_plugin". +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. +End Int63NotationsInternalA. (* Logical operations *) Primitive lsl := #int63_lsl. -Infix "<<" := lsl (at level 30, no associativity) : int63_scope. Primitive lsr := #int63_lsr. -Infix ">>" := lsr (at level 30, no associativity) : int63_scope. Primitive land := #int63_land. -Infix "land" := land (at level 40, left associativity) : int63_scope. Primitive lor := #int63_lor. -Infix "lor" := lor (at level 40, left associativity) : int63_scope. Primitive lxor := #int63_lxor. -Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. (* Arithmetic modulo operations *) Primitive add := #int63_add. -Notation "n + m" := (add n m) : int63_scope. Primitive sub := #int63_sub. -Notation "n - m" := (sub n m) : int63_scope. Primitive mul := #int63_mul. -Notation "n * m" := (mul n m) : int63_scope. Primitive mulc := #int63_mulc. Primitive div := #int63_div. -Notation "n / m" := (div n m) : int63_scope. Primitive mod := #int63_mod. -Notation "n '\%' m" := (mod n m) (at level 40, left associativity) : int63_scope. (* Comparisons *) Primitive eqb := #int63_eq. -Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. Primitive ltb := #int63_lt. -Notation "m < n" := (ltb m n) : int63_scope. Primitive leb := #int63_le. -Notation "m <= n" := (leb m n) : int63_scope. -Notation "m ≤ n" := (leb m n) (at level 70, no associativity) : int63_scope. Local Open Scope int63_scope. +Module Import Int63NotationsInternalB. +Infix "<<" := lsl (at level 30, no associativity) : int63_scope. +Infix ">>" := lsr (at level 30, no associativity) : int63_scope. +Infix "land" := land (at level 40, left associativity) : int63_scope. +Infix "lor" := lor (at level 40, left associativity) : int63_scope. +Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. +Infix "+" := add : int63_scope. +Infix "-" := sub : int63_scope. +Infix "*" := mul : int63_scope. +Infix "/" := div : int63_scope. +Infix "mod" := mod (at level 40, no associativity) : int63_scope. +Infix "=?" := eqb (at level 70, no associativity) : int63_scope. +Infix "<?" := ltb (at level 70, no associativity) : int63_scope. +Infix "<=?" := leb (at level 70, no associativity) : int63_scope. +Infix "≤?" := leb (at level 70, no associativity) : int63_scope. +End Int63NotationsInternalB. + (** The number of digits as a int *) Definition digits := 63. @@ -89,16 +94,16 @@ Definition max_int := Eval vm_compute in 0 - 1. Register Inline max_int. (** Access to the nth digits *) -Definition get_digit x p := (0 < (x land (1 << p))). +Definition get_digit x p := (0 <? (x land (1 << p))). Definition set_digit x p (b:bool) := - if if 0 <= p then p < digits else false then + if if 0 <=? p then p <? digits else false then if b then x lor (1 << p) else x land (max_int lxor (1 << p)) else x. (** Equality to 0 *) -Definition is_zero (i:int) := i == 0. +Definition is_zero (i:int) := i =? 0. Register Inline is_zero. (** Parity *) @@ -113,7 +118,6 @@ Definition bit i n := negb (is_zero ((i >> n) << (digits - 1))). (** Extra modulo operations *) Definition opp (i:int) := 0 - i. Register Inline opp. -Notation "- x" := (opp x) : int63_scope. Definition oppcarry i := max_int - i. Register Inline oppcarry. @@ -134,29 +138,27 @@ Register Inline subcarry. Definition addc_def x y := let r := x + y in - if r < x then C1 r else C0 r. + if r <? x then C1 r else C0 r. (* the same but direct implementation for efficiency *) Primitive addc := #int63_addc. -Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. Definition addcarryc_def x y := let r := addcarry x y in - if r <= x then C1 r else C0 r. + if r <=? x then C1 r else C0 r. (* the same but direct implementation for efficiency *) Primitive addcarryc := #int63_addcarryc. Definition subc_def x y := - if y <= x then C0 (x - y) else C1 (x - y). + if y <=? x then C0 (x - y) else C1 (x - y). (* the same but direct implementation for efficiency *) Primitive subc := #int63_subc. -Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. Definition subcarryc_def x y := - if y < x then C0 (x - y - 1) else C1 (x - y - 1). + if y <? x then C0 (x - y - 1) else C1 (x - y - 1). (* the same but direct implementation for efficiency *) Primitive subcarryc := #int63_subcarryc. -Definition diveucl_def x y := (x/y, x\%y). +Definition diveucl_def x y := (x/y, x mod y). (* the same but direct implementation for efficiency *) Primitive diveucl := #int63_diveucl. @@ -166,6 +168,12 @@ Definition addmuldiv_def p x y := (x << p) lor (y >> (digits - p)). Primitive addmuldiv := #int63_addmuldiv. +Module Import Int63NotationsInternalC. +Notation "- x" := (opp x) : int63_scope. +Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. +Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. +End Int63NotationsInternalC. + Definition oppc (i:int) := 0 -c i. Register Inline oppc. @@ -177,11 +185,10 @@ Register Inline predc. (** Comparison *) Definition compare_def x y := - if x < y then Lt - else if (x == y) then Eq else Gt. + if x <? y then Lt + else if (x =? y) then Eq else Gt. Primitive compare := #int63_compare. -Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. Import Bool ZArith. (** Translation to Z *) @@ -194,8 +201,6 @@ Fixpoint to_Z_rec (n:nat) (i:int) := Definition to_Z := to_Z_rec size. -Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. - Fixpoint of_pos_rec (n:nat) (p:positive) := match n, p with | O, _ => 0 @@ -215,8 +220,12 @@ Definition of_Z z := Definition wB := (2 ^ (Z.of_nat size))%Z. +Module Import Int63NotationsInternalD. +Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. +Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. Notation "'Φ' x" := (zn2z_to_Z wB to_Z x) (at level 0) : int63_scope. +End Int63NotationsInternalD. Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z. Proof. @@ -347,16 +356,16 @@ Axiom mulc_spec : forall x y, φ x * φ y = φ (fst (mulc x y)) * wB + φ (snd ( Axiom div_spec : forall x y, φ (x / y) = φ x / φ y. -Axiom mod_spec : forall x y, φ (x \% y) = φ x mod φ y. +Axiom mod_spec : forall x y, φ (x mod y) = φ x mod φ y. (* Comparisons *) -Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. +Axiom eqb_correct : forall i j, (i =? j)%int63 = true -> i = j. -Axiom eqb_refl : forall x, (x == x)%int63 = true. +Axiom eqb_refl : forall x, (x =? x)%int63 = true. -Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> φ x < φ y. +Axiom ltb_spec : forall x y, (x <? y)%int63 = true <-> φ x < φ y. -Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> φ x <= φ y. +Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y. (** Exotic operations *) @@ -397,7 +406,7 @@ Local Open Scope int63_scope. Definition sqrt_step (rec: int -> int -> int) (i j: int) := let quo := i / j in - if quo < j then rec i ((j + quo) >> 1) + if quo <? j then rec i ((j + quo) >> 1) else j. Definition iter_sqrt := @@ -421,9 +430,9 @@ Definition high_bit := 1 << (digits - 1). Definition sqrt2_step (rec: int -> int -> int -> int) (ih il j: int) := - if ih < j then + if ih <? j then let (quo,_) := diveucl_21 ih il j in - if quo < j then + if quo <? j then match j +c quo with | C0 m1 => rec ih il (m1 >> 1) | C1 m1 => rec ih il ((m1 >> 1) + high_bit) @@ -448,48 +457,48 @@ Definition sqrt2 ih il := let (ih1, il1) := mulc s s in match il -c il1 with | C0 il2 => - if ih1 < ih then (s, C1 il2) else (s, C0 il2) + if ih1 <? ih then (s, C1 il2) else (s, C0 il2) | C1 il2 => - if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2) + if ih1 <? (ih - 1) then (s, C1 il2) else (s, C0 il2) end. (** Gcd **) Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} := match guard with | O => 1 - | S p => if j == 0 then i else gcd_rec p j (i \% j) + | S p => if j =? 0 then i else gcd_rec p j (i mod j) end. Definition gcd := gcd_rec (2*size). (** equality *) -Lemma eqb_complete : forall x y, x = y -> (x == y) = true. +Lemma eqb_complete : forall x y, x = y -> (x =? y) = true. Proof. intros x y H; rewrite -> H, eqb_refl;trivial. Qed. -Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. +Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y. Proof. split;auto using eqb_correct, eqb_complete. Qed. -Lemma eqb_false_spec : forall x y, (x == y) = false <-> x <> y. +Lemma eqb_false_spec : forall x y, (x =? y) = false <-> x <> y. Proof. intros;rewrite <- not_true_iff_false, eqb_spec;split;trivial. Qed. -Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false. +Lemma eqb_false_complete : forall x y, x <> y -> (x =? y) = false. Proof. intros x y;rewrite eqb_false_spec;trivial. Qed. -Lemma eqb_false_correct : forall x y, (x == y) = false -> x <> y. +Lemma eqb_false_correct : forall x y, (x =? y) = false -> x <> y. Proof. intros x y;rewrite eqb_false_spec;trivial. Qed. Definition eqs (i j : int) : {i = j} + { i <> j } := - (if i == j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) + (if i =? j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true)) else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false))) (eqb_correct i j) @@ -503,7 +512,7 @@ Qed. (* Extra function on equality *) Definition cast i j := - (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) + (if i =? j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) then fun Heq : true = true -> i = j => Some (fun (P : int -> Type) (Hi : P i) => @@ -520,14 +529,14 @@ Proof. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. -Lemma cast_diff : forall i j, i == j = false -> cast i j = None. +Lemma cast_diff : forall i j, i =? j = false -> cast i j = None. Proof. intros;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed. Definition eqo i j := - (if i == j as b return ((b = true -> i = j) -> option (i=j)) + (if i =? j as b return ((b = true -> i = j) -> option (i=j)) then fun Heq : true = true -> i = j => Some (Heq (eq_refl true)) else fun _ : false = true -> i = j => None) (eqb_correct i j). @@ -540,7 +549,7 @@ Proof. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. -Lemma eqo_diff : forall i j, i == j = false -> eqo i j = None. +Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None. Proof. unfold eqo;intros; generalize (eqb_correct i j). rewrite H;trivial. @@ -548,13 +557,13 @@ Qed. (** Comparison *) -Lemma eqbP x y : reflect (φ x = φ y ) (x == y). +Lemma eqbP x y : reflect (φ x = φ y ) (x =? y). Proof. apply iff_reflect; rewrite eqb_spec; split; [ apply to_Z_inj | apply f_equal ]. Qed. -Lemma ltbP x y : reflect (φ x < φ y )%Z (x < y). +Lemma ltbP x y : reflect (φ x < φ y )%Z (x <? y). Proof. apply iff_reflect; symmetry; apply ltb_spec. Qed. -Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤ y). +Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤? y). Proof. apply iff_reflect; symmetry; apply leb_spec. Qed. Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z. @@ -742,7 +751,7 @@ Proof. Qed. Lemma add_le_r m n: - if (n <= m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. + if (n <=? m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. @@ -753,11 +762,11 @@ Proof. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. apply f_equal2 with (f := Zmod); auto with zarith. - case_eq (n <= m + n)%int63; auto. + case_eq (n <=? m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. assert (H1: (φ (m + n) = φ m + φ n)%Z). rewrite add_spec, Zmod_small; auto with zarith. - replace (n <= m + n)%int63 with true; auto. + replace (n <=? m + n)%int63 with true; auto. apply sym_equal; rewrite leb_spec, H1; auto with zarith. Qed. @@ -783,7 +792,7 @@ Proof. apply to_Z_inj; rewrite lsr_spec; reflexivity. Qed. Lemma lsr_0_r i: i >> 0 = i. Proof. apply to_Z_inj; rewrite lsr_spec, Zdiv_1_r; exact eq_refl. Qed. -Lemma lsr_1 n : 1 >> n = (n == 0). +Lemma lsr_1 n : 1 >> n = (n =? 0)%int63. Proof. case eqbP. intros h; rewrite (to_Z_inj _ _ h), lsr_0_r; reflexivity. @@ -798,12 +807,12 @@ Proof. lia. Qed. -Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int63. +Lemma lsr_add i m n: ((i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%int63. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. case (to_Z_bounded i); intros H1i H2i. - generalize (add_le_r m n); case (n <= m + n)%int63; intros H. + generalize (add_le_r m n); case (n <=? m + n)%int63; intros H. apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. rewrite add_spec, Zmod_small; auto with zarith. apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. @@ -833,7 +842,7 @@ Proof. apply f_equal2 with (f := Zmod); auto with zarith. Qed. -Lemma lsr_M_r x i (H: (digits <= i = true)%int63) : x >> i = 0%int63. +Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63. Proof. apply to_Z_inj. rewrite lsr_spec, to_Z_0. @@ -889,22 +898,22 @@ Proof. Qed. Lemma bit_lsr x i j : - (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63. + (bit (x >> i) j = if j <=? i + j then bit x (i + j) else false)%int63. Proof. - unfold bit; rewrite lsr_add; case (_ ≤ _); auto. + unfold bit; rewrite lsr_add; case (_ ≤? _); auto. Qed. -Lemma bit_b2i (b: bool) i : bit b i = (i == 0) && b. +Lemma bit_b2i (b: bool) i : bit b i = (i =? 0)%int63 && b. Proof. case b; unfold bit; simpl b2i. - rewrite lsr_1; case (i == 0); auto. + rewrite lsr_1; case (i =? 0)%int63; auto. rewrite lsr0, lsl0, andb_false_r; auto. Qed. -Lemma bit_1 n : bit 1 n = (n == 0). +Lemma bit_1 n : bit 1 n = (n =? 0)%int63. Proof. unfold bit; rewrite lsr_1. - case (_ == _); simpl; auto. + case (_ =? _)%int63; simpl; auto. Qed. Local Hint Resolve Z.lt_gt Z.div_pos : zarith. @@ -929,14 +938,14 @@ Proof. case bit; discriminate. Qed. -Lemma bit_M i n (H: (digits <= n = true)%int63): bit i n = false. +Lemma bit_M i n (H: (digits <=? n = true)%int63): bit i n = false. Proof. unfold bit; rewrite lsr_M_r; auto. Qed. -Lemma bit_half i n (H: (n < digits = true)%int63) : bit (i>>1) n = bit i (n+1). +Lemma bit_half i n (H: (n <? digits = true)%int63) : bit (i>>1) n = bit i (n+1). Proof. unfold bit. rewrite lsr_add. - case_eq (n <= (1 + n))%int63. + case_eq (n <=? (1 + n))%int63. replace (1+n)%int63 with (n+1)%int63; [auto|idtac]. apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto. intros H1; assert (H2: n = max_int). @@ -968,10 +977,10 @@ Proof. Qed. Lemma bit_lsl x i j : bit (x << i) j = -(if (j < i) || (digits <= j) then false else bit x (j - i))%int63. +(if (j <? i) || (digits <=? j) then false else bit x (j - i))%int63. Proof. assert (F1: 1 >= 0) by discriminate. - case_eq (digits <= j)%int63; intros H. + case_eq (digits <=? j)%int63; intros H. rewrite orb_true_r, bit_M; auto. set (d := φ digits). case (Zle_or_lt d (φ j)); intros H1. @@ -1039,10 +1048,10 @@ Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i). Proof. apply bit_ext; intros n. rewrite -> lor_spec, !bit_lsr, lor_spec. - case (_ <= _)%int63; auto. + case (_ <=? _)%int63; auto. Qed. -Lemma lor_le x y : (y <= x lor y)%int63 = true. +Lemma lor_le x y : (y <=? x lor y)%int63 = true. Proof. generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. unfold wB; elim size. @@ -1092,7 +1101,7 @@ Proof. rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. intros m H1 H2. - case_eq (digits <= m)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (digits <=? m)%int63; [idtac | rewrite <- not_true_iff_false]; intros Heq. rewrite bit_M in H1; auto; discriminate. rewrite leb_spec in Heq. @@ -1131,7 +1140,7 @@ Proof. rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. intros _ HH m; case (to_Z_bounded m); intros H1m H2m. - case_eq (digits <= m)%int63. + case_eq (digits <=? m)%int63. intros Hlm; rewrite bit_M; auto; discriminate. rewrite <- not_true_iff_false, leb_spec; intros Hlm. case (Zle_lt_or_eq 0 φ m); auto; intros Hm. @@ -1177,11 +1186,11 @@ Proof. rewrite (fun x y => Zmod_small (x - y)); auto with zarith. intros n; rewrite -> bit_lsl, bit_lsr. generalize (add_le_r (digits - p) n). - case (_ ≤ _); try discriminate. + case (_ ≤? _); try discriminate. rewrite -> sub_spec, Zmod_small; auto with zarith; intros H1. - case_eq (n < p)%int63; try discriminate. + case_eq (n <? p)%int63; try discriminate. rewrite <- not_true_iff_false, ltb_spec; intros H2. - case (_ ≤ _); try discriminate. + case (_ ≤? _); try discriminate. intros _; rewrite bit_M; try discriminate. rewrite -> leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith. rewrite -> sub_spec, Zmod_small; auto with zarith. @@ -1196,7 +1205,7 @@ Proof. apply bit_ext; intros n. rewrite bit_b2i, land_spec, bit_1. generalize (eqb_spec n 0). - case (n == 0); auto. + case (n =? 0)%int63; auto. intros(H,_); rewrite andb_true_r, H; auto. rewrite andb_false_r; auto. Qed. @@ -1373,9 +1382,9 @@ Qed. (* sqrt2 *) Lemma sqrt2_step_def rec ih il j: sqrt2_step rec ih il j = - if (ih < j)%int63 then + if (ih <? j)%int63 then let quo := fst (diveucl_21 ih il j) in - if (quo < j)%int63 then + if (quo <? j)%int63 then let m := match j +c quo with | C0 m1 => m1 >> 1 @@ -1453,7 +1462,7 @@ Proof. apply Zmult_lt_0_compat; auto with zarith. refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } cbv zeta. - case_eq (ih < j)%int63;intros Heq. + case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. 2: rewrite <-not_true_iff_false, ltb_spec in Heq. 2: split; auto. @@ -1462,7 +1471,7 @@ Proof. 2: assert (0 <= φ il/φ j) by (apply Z_div_pos; auto with zarith). 2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. case (Zle_or_lt (2^(Z_of_nat size -1)) φ j); intros Hjj. - case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0. + case_eq (fst (diveucl_21 ih il j) <? j)%int63;intros Heq0. 2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. 2: split; auto; apply sqrt_test_true; auto with zarith. rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. @@ -1557,7 +1566,7 @@ Lemma sqrt2_spec : forall x y, generalize (subc_spec il il1). case subc; intros il2 Hil2. simpl interp_carry in Hil2. - case_eq (ih1 < ih)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (ih1 <? ih)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec; intros Heq. unfold interp_carry; rewrite Zmult_1_l. rewrite -> Z.pow_2_r, Hihl1, Hil2. @@ -1602,7 +1611,7 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded ih); intros H1 H2. split; auto with zarith. apply Z.le_trans with (wB/4 - 1); auto with zarith. - case_eq (ih1 < ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (ih1 <? ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec, Hsih; intros Heq. rewrite Z.pow_2_r, Hihl1. case (Zle_lt_or_eq (φ ih1 + 2) φ ih); auto with zarith. @@ -1927,3 +1936,21 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. + +Module Export Int63Notations. + Local Open Scope int63_scope. + #[deprecated(since="8.13",note="use infix mod instead")] + Notation "a \% m" := (a mod m) (at level 40, left associativity) : int63_scope. + #[deprecated(since="8.13",note="use infix =? instead")] + Notation "m '==' n" := (m =? n) (at level 70, no associativity) : int63_scope. + #[deprecated(since="8.13",note="use infix <? instead")] + Notation "m < n" := (m <? n) : int63_scope. + #[deprecated(since="8.13",note="use infix <=? instead")] + Notation "m <= n" := (m <=? n) : int63_scope. + #[deprecated(since="8.13",note="use infix ≤? instead")] + Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope. + Export Int63NotationsInternalA. + Export Int63NotationsInternalB. + Export Int63NotationsInternalC. + Export Int63NotationsInternalD. +End Int63Notations. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 026cf32ceb..2f445c341a 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -522,6 +522,18 @@ Proof. repeat red; eauto using Permutation_NoDup. Qed. +Lemma Permutation_repeat x n l : + Permutation l (repeat x n) -> l = repeat x n. +Proof. + revert n; induction l as [|y l IHl] ; simpl; intros n HP; auto. + - now apply Permutation_nil in HP; inversion HP. + - assert (y = x) as Heq by (now apply repeat_spec with n, (Permutation_in _ HP); left); subst. + destruct n; simpl; simpl in HP. + + symmetry in HP; apply Permutation_nil in HP; inversion HP. + + f_equal; apply IHl. + now apply Permutation_cons_inv with x. +Qed. + End Permutation_properties. Section Permutation_map. |