diff options
42 files changed, 1201 insertions, 653 deletions
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/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/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/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/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/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/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. |