diff options
| -rw-r--r-- | .gitlab-ci.yml | 35 | ||||
| -rw-r--r-- | dev/bench/gitlab-bench.yml | 32 | ||||
| -rwxr-xr-x | dev/bench/gitlab.sh | 42 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 9 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 14 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 192 | ||||
| -rw-r--r-- | tactics/elim.ml | 8 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.mli | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12676.v | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12860.v | 10 | ||||
| -rw-r--r-- | theories/nsatz/Nsatz.v | 40 | ||||
| -rw-r--r-- | theories/nsatz/NsatzTactic.v | 40 |
17 files changed, 251 insertions, 227 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ab06123aed..51d39936d0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -27,6 +27,9 @@ variables: OPAM_VARIANT: "" GIT_DEPTH: "10" +include: + - local: '/dev/bench/gitlab-bench.yml' + docker-boot: stage: docker image: docker:stable @@ -921,35 +924,3 @@ plugin:ci-rewriter: name: "$CI_JOB_NAME" paths: - _build_ci - -bench: - stage: stage-1 - when: manual - before_script: - - printenv -0 | sort -z | tr '\0' '\n' - script: - - . ~/.opam/opam-init/init.sh - - ./dev/bench/gitlab.sh - tags: - - timing - variables: - GIT_DEPTH: "" - coq_pr_number: "" - coq_pr_comment_id: "" - new_ocaml_switch: "ocaml-base-compiler.4.07.1" - old_ocaml_switch: "ocaml-base-compiler.4.07.1" - new_coq_repository: "https://gitlab.com/coq/coq.git" - old_coq_repository: "https://gitlab.com/coq/coq.git" - new_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" - old_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" - new_coq_opam_archive_git_branch: "master" - old_coq_opam_archive_git_branch: "master" - num_of_iterations: 1 - coq_opam_packages: "coq-performance-tests coq-engine-bench coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast" - artifacts: - name: "$CI_JOB_NAME" - paths: - - _bench/html/**/*.v.html - - _bench/logs - when: always - expire_in: 1 year diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml new file mode 100644 index 0000000000..2246d4047a --- /dev/null +++ b/dev/bench/gitlab-bench.yml @@ -0,0 +1,32 @@ + +bench: + stage: stage-1 + when: manual + before_script: + - printenv -0 | sort -z | tr '\0' '\n' + script: + - . ~/.opam/opam-init/init.sh + - ./dev/bench/gitlab.sh + tags: + - timing + variables: + GIT_DEPTH: "" + coq_pr_number: "" + coq_pr_comment_id: "" + new_ocaml_switch: "ocaml-base-compiler.4.07.1" + old_ocaml_switch: "ocaml-base-compiler.4.07.1" + new_coq_repository: "https://gitlab.com/coq/coq.git" + old_coq_repository: "https://gitlab.com/coq/coq.git" + new_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" + old_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" + new_coq_opam_archive_git_branch: "master" + old_coq_opam_archive_git_branch: "master" + num_of_iterations: 1 + coq_opam_packages: "coq-performance-tests coq-engine-bench coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast" + artifacts: + name: "$CI_JOB_NAME" + paths: + - _bench/html/**/*.v.html + - _bench/logs + when: always + expire_in: 1 year diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 15f5c01ac6..38b4e25bde 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -52,15 +52,6 @@ check_variable "coq_opam_packages" new_coq_commit=$(git rev-parse HEAD^2) old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit) -if which jq > /dev/null; then - : -else - echo > /dev/stderr - echo "ERROR: \"jq\" program is not available." > /dev/stderr - echo > /dev/stderr - exit 1 -fi - if echo "$num_of_iterations" | grep '^[1-9][0-9]*$' 2> /dev/null > /dev/null; then : else @@ -76,39 +67,6 @@ working_dir="$PWD/_bench" log_dir=$working_dir/logs mkdir "$log_dir" -if [ ! -z "${coq_pr_number}" ]; then - github_response="$(curl "https://api.github.com/repos/coq/coq/pulls/${coq_pr_number}")" - new_coq_repository="$(echo "${github_response}" | jq -r '.head.repo.clone_url')" - new_coq_commit="$(echo "${github_response}" | jq -r '.head.sha')" - old_coq_repository="$(echo "${github_response}" | jq -r '.base.repo.clone_url')" - old_coq_commit="$(echo "${github_response}" | jq -r '.base.sha')" - coq_pr_title="$(echo "${github_response}" | jq -r '.title')" - # for coqbot parsing purposes, coq_pr_number and coq_pr_comment_id must not have newlines - coq_pr_number="$(echo "${coq_pr_number}" | tr -d '\n' | tr -d '\r')" - coq_pr_comment_id="$(echo "${coq_pr_comment_id}" | tr -d '\n' | tr -d '\r')" - - for val in "${new_coq_repository}" "${new_coq_commit}" "${old_coq_repository}" "${old_coq_commit}" "${coq_pr_title}"; do - if [ -z "$val" ] || [ "val" == "null" ]; then - echo 'ERROR: Invalid Response:' > /dev/stderr - echo "${github_response}" > /dev/stderr - echo "Info:" > /dev/stderr - curl -i "https://api.github.com/repos/coq/coq/pulls/${coq_pr_number}" > /dev/stderr - exit 1 - fi - done - - if [ -z "$BENCH_DEBUG" ]; then # if it's non-empty, this'll get - # printed later anyway. But we - # want to see it always if we're - # automatically computing values - echo "DEBUG: new_coq_repository = $new_coq_repository" - echo "DEBUG: new_coq_commit = $new_coq_commit" - echo "DEBUG: old_coq_repository = $old_coq_repository" - echo "DEBUG: old_coq_commit = $old_coq_commit" - fi - -fi - if [ ! -z "$BENCH_DEBUG" ] then echo "DEBUG: ocaml -version = `ocaml -version`" diff --git a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst new file mode 100644 index 0000000000..41359098e3 --- /dev/null +++ b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst @@ -0,0 +1,7 @@ +- **Changed:** + ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` + with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which + transitively requires unneeded files declaring axioms used in the reals + (`#12861 <https://github.com/coq/coq/pull/12861>`_, + fixes `#12860 <https://github.com/coq/coq/issues/12860>`_, + by Jason Gross). diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ed2e1ea58c..ed93145622 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -34,6 +34,12 @@ Nsatz: tactics for proving equalities in integral domains You can load the ``Nsatz`` module with the command ``Require Import Nsatz``. + Alternatively, if you prefer not to transitively depend on the + files declaring the axioms used to define the real numbers, you can + ``Require Import NsatzTactic`` instead; this will still allow + :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`, + :math:`\mathbb{Q}` and any user-registered rings. + More about `nsatz` --------------------- @@ -85,4 +91,4 @@ performed using :ref:`typeclasses`. then `lvar` is replaced by all the variables which are not in `parameters`. -See the file `Nsatz.v` for many examples, especially in geometry. +See the test-suite file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_ for many examples, especially in geometry. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index d9992029ba..daae46ad11 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -89,10 +89,11 @@ invoking ``coq_makefile`` is the following one: Such command generates the following files: CoqMakefile - is a generic makefile for ``GNU Make`` that provides - targets to build the project (both ``.v`` and ``.ml*`` files), to install it - system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed) - as well as to invoke coqdoc to generate HTML documentation. + is a makefile for ``GNU Make`` with targets to build the project + (e.g. generate .vo or .html files from .v or compile .ml* files) + and install it in the ``user-contrib`` directory where the |Coq| + library is installed. Run ``make`` with the ``-f CoqMakefile`` + option to use ``CoqMakefile``. CoqMakefile.conf contains make variables assignments that reflect diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 743afe4177..72e6006b7e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -483,7 +483,10 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g = (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))) ; (* Then the equation itself *) - Proofview.V82.of_tactic (intro_using heq_id) + Proofview.V82.of_tactic + (intro_using_then heq_id + (* we get the fresh name with onLastHypId *) + (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) @@ -1113,16 +1116,18 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num in let first_tac : tactic = (* every operations until fix creations *) + (* names are already refreshed *) tclTHENLIST [ observe_tac "introducing params" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.params))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))) ; observe_tac "introducing predictes" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.predicates))) + (intros_mustbe_force + (List.rev_map id_of_decl princ_info.predicates))) ; observe_tac "introducing branches" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.branches))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches))) ; observe_tac "building fixes" mk_fixes ] in let intros_after_fixes : tactic = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 253c95fa67..066ade07d2 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -414,7 +414,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ h_intros (List.rev rev_ids) - ; Proofview.V82.of_tactic (intro_using teq_id) + ; Proofview.V82.of_tactic + (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq -> observe_tclTHENLIST (fun _ _ -> str "treat_case2") @@ -601,7 +602,11 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g = (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ observe_tclTHENLIST (fun _ _ -> str "") - [ Proofview.V82.of_tactic (intro_using h_id) + [ Proofview.V82.of_tactic + (intro_using_then h_id + (* We don't care about the refreshed name, + accessed only through auto? *) + (fun _ -> Proofview.tclUNIT ())) ; Proofview.V82.of_tactic (simplest_elim (mkApp (delayed_force lt_n_O, [|s_max|]))) @@ -865,7 +870,10 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g = (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))) [ observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2") - [ Proofview.V82.of_tactic (intro_using rec_res_id) + [ Proofview.V82.of_tactic + (intro_using_then rec_res_id + (* refreshed name gotten from onNthHypId *) + (fun _ -> Proofview.tclUNIT ())) ; Proofview.V82.of_tactic intro ; onNthHypId 1 (fun v_bound -> onNthHypId 2 (fun v -> diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 3ba6365783..cd5b747d75 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1055,6 +1055,9 @@ let rec clear_zero p = function let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t) | t -> [],t +open Proofview +open Proofview.Notations + let replay_history tactic_normalisation = let aux = Id.of_string "auxiliary" in let aux1 = Id.of_string "auxiliary_1" in @@ -1085,8 +1088,8 @@ let replay_history tactic_normalisation = mk_integer k; mkVar id1; mkVar id2 |])]; mk_then tac; - (intros_using [aux]); - resolve_id aux; + intro_using_then aux (fun aux -> + resolve_id aux); reflexivity ] | CONTRADICTION (e1,e2) :: l -> @@ -1128,24 +1131,25 @@ let replay_history tactic_normalisation = tclTHENS (cut state_eg) [ tclTHENS - (tclTHENLIST [ - (intros_using [aux]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA1, - [| eq1; rhs; mkVar aux; mkVar id |])]); - (clear [aux;id]); - (intros_using [id]); - (cut (mk_gt kk dd)) ]) + (intro_using_then aux (fun aux -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_OMEGA1, + [| eq1; rhs; mkVar aux; mkVar id |])]); + (clear [aux;id]); + (intro_mustbe_force id); + (cut (mk_gt kk dd)) ])) [ tclTHENS (cut (mk_gt kk izero)) - [ tclTHENLIST [ - (intros_using [aux1; aux2]); + [ intro_using_then aux1 (fun aux1 -> + intro_using_then aux2 (fun aux2 -> + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); (clear [aux1;aux2;id]); - (intros_using [id]); - (loop l) ]; + (intro_mustbe_force id); + (loop l) ])); tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; @@ -1166,21 +1170,24 @@ let replay_history tactic_normalisation = tclTHENS (cut (mk_gt dd izero)) [ tclTHENS (cut (mk_gt kk dd)) - [tclTHENLIST [ - (intros_using [aux2;aux1]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA4, - [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); - (clear [aux1;aux2]); - unfold sp_not; - (intros_using [aux]); - resolve_id aux; - mk_then tac; - assumption ] ; - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ]; + [ intro_using_then aux2 (fun aux2 -> + intro_using_then aux1 (fun aux1 -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_OMEGA4, + [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); + (clear [aux1;aux2]); + unfold sp_not; + intro_using_then aux (fun aux -> + tclTHENLIST [ + resolve_id aux; + mk_then tac; + assumption + ])])) ; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ]; tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; @@ -1196,29 +1203,30 @@ let replay_history tactic_normalisation = let tac = scalar_norm [P_APP 3] e2.body in tclTHENS (cut state_eq) - [tclTHENLIST [ - (intros_using [aux1]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA18, - [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); - (clear [aux1;id]); - (intros_using [id]); - (loop l) ]; - tclTHEN (mk_then tac) reflexivity ] + [ intro_using_then aux1 (fun aux1 -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_OMEGA18, + [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); + (clear [aux1;id]); + (intro_mustbe_force id); + (loop l) ]); + tclTHEN (mk_then tac) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in tclTHENS (cut state_eq) [ tclTHENS (cut (mk_gt kk izero)) - [tclTHENLIST [ - (intros_using [aux2;aux1]); - (generalize_tac + [ intro_using_then aux2 (fun aux2 -> + intro_using_then aux1 (fun aux1 -> + tclTHENLIST [ + (generalize_tac [mkApp (Lazy.force coq_OMEGA3, [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); (clear [aux1;aux2;id]); - (intros_using [id]); - (loop l) ]; + (intro_mustbe_force id); + (loop l) ])); tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; @@ -1238,13 +1246,13 @@ let replay_history tactic_normalisation = in tclTHENS (cut (mk_eq eq1 (mk_inv eq2))) - [tclTHENLIST [ - (intros_using [aux]); - (generalize_tac [mkApp (Lazy.force coq_OMEGA8, - [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); - (clear [id1;id2;aux]); - (intros_using [id]); - (loop l) ]; + [ intro_using_then aux (fun aux -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); + (clear [id1;id2;aux]); + (intro_mustbe_force id); + (loop l) ]); tclTHEN (mk_then tac) reflexivity] | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> @@ -1271,18 +1279,19 @@ let replay_history tactic_normalisation = orig.body m ({c= negone;v= v}::def.body) in tclTHENS (cut theorem) - [tclTHENLIST [ - (intros_using [aux]); - (elim_id aux); - (clear [aux]); - (intros_using [vid; aux]); - (generalize_tac + [ tclTHENLIST [ intro_using_then aux (fun aux -> + (elim_id aux) <*> + (clear [aux])); + intro_using_then vid (fun vid -> + intro_using_then aux (fun aux -> + tclTHENLIST [ + (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); mk_then tac; (clear [aux]); - (intros_using [id]); - (loop l) ]; + (intro_mustbe_force id); + (loop l) ]))]; tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () @@ -1294,8 +1303,8 @@ let replay_history tactic_normalisation = let eq = val_of(decompile e) in tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ]; - tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]] + [tclTHENLIST [ mk_then tac1; (intro_mustbe_force id1); (loop act1) ]; + tclTHENLIST [ mk_then tac2; (intro_mustbe_force id2); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1318,7 +1327,7 @@ let replay_history tactic_normalisation = (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); mk_then tac; - (intros_using [id]); + (intro_mustbe_force id); (loop l) ] else @@ -1329,25 +1338,26 @@ let replay_history tactic_normalisation = tclTHENS (cut (mk_gt kk1 izero)) [tclTHENS (cut (mk_gt kk2 izero)) - [tclTHENLIST [ - (intros_using [aux2;aux1]); - (generalize_tac - [mkApp (Lazy.force coq_OMEGA7, [| - eq1;eq2;kk1;kk2; - mkVar aux1;mkVar aux2; - mkVar id1;mkVar id2 |])]); - (clear [aux1;aux2]); - mk_then tac; - (intros_using [id]); - (loop l) ]; - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ]; - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ] + [ intro_using_then aux2 (fun aux2 -> + intro_using_then aux1 (fun aux1 -> + tclTHENLIST [ + (generalize_tac + [mkApp (Lazy.force coq_OMEGA7, [| + eq1;eq2;kk1;kk2; + mkVar aux1;mkVar aux2; + mkVar id1;mkVar id2 |])]); + (clear [aux1;aux2]); + mk_then tac; + (intro_mustbe_force id); + (loop l) ])); + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ]; + tclTHENLIST [ + unfold sp_Zgt; + simpl_in_concl; + reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> @@ -1358,9 +1368,8 @@ let replay_history tactic_normalisation = unfold sp_Zle; simpl_in_concl; unfold sp_not; - (intros_using [aux]); - resolve_id aux; - reflexivity + intro_using_then aux (fun aux -> + resolve_id aux <*> reflexivity) ] | _ -> Proofview.tclUNIT () in @@ -1382,7 +1391,7 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = in if not (List.is_empty tac) then let id' = new_identifier () in - ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ])) + ((id',(tclTHENLIST [ shift_left; mk_then tac; (intro_mustbe_force id') ])) :: tactic, compile id' flag t' :: defs) else @@ -1423,10 +1432,7 @@ let destructure_omega env sigma tac_def (id,c) = let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - tclTHEN (tclTRY (clear [id])) (intro_using id) - - -open Proofview.Notations + tclTHEN (tclTRY (clear [id])) (intro_using_then id (fun _ -> tclUNIT())) let coq_omega = Proofview.Goal.enter begin fun gl -> @@ -1444,10 +1450,10 @@ let coq_omega = tag_hypothesis id i; (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); - (intros_using [v; id]); + (intros_mustbe_force [v; id]); (elim_id id); (clear [id]); - (intros_using [th;id]); + (intros_mustbe_force [th;id]); tac ]), {kind = INEQ; body = [{v=intern_id v; c=one}]; @@ -1455,7 +1461,7 @@ let coq_omega = else (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_new_var, [t]))); - (intros_using [v;th]); + (intros_mustbe_force [v;th]); tac ]), sys) (Proofview.tclUNIT (),[]) (dump_tables ()) @@ -1508,7 +1514,7 @@ let nat_inject = tclTHENS (tclTHEN (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) - (intros_using [id])) + (intro_mustbe_force id)) [ tclTHENLIST [ (clever_rewrite_gen p @@ -1703,7 +1709,7 @@ let onClearedName2 id tac = (tclTRY (clear [id])) (Proofview.Goal.enter begin fun gl -> let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in - let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in + let id2 = fresh_id (Id.Set.singleton id1) (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end) diff --git a/tactics/elim.ml b/tactics/elim.ml index 415c980c2a..274ebc9f60 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -82,10 +82,10 @@ let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> let typc = pf_get_type_of gl c in tclTHENS (cut typc) - [ tclTHEN (intro_using tmphyp_name) - (onLastHypId - (ifOnHyp recognizer (general_decompose_aux recognizer) - (fun id -> clear [id]))); + [ intro_using_then tmphyp_name (fun id -> + ifOnHyp recognizer (general_decompose_aux recognizer) + (fun id -> clear [id]) + id); exact_no_check c ] end diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 57d793b2a5..d4cc193eb3 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -150,12 +150,12 @@ let injHyp id = let diseqCase hyps eqonleft = let diseq = Id.of_string "diseq" in let absurd = Id.of_string "absurd" in - (tclTHEN (intro_using diseq) - (tclTHEN (choose_noteq eqonleft) + (intro_using_then diseq (fun diseq -> + tclTHEN (choose_noteq eqonleft) (tclTHEN (rewrite_and_clear (List.rev hyps)) (tclTHEN (red_in_concl) - (tclTHEN (intro_using absurd) - (tclTHEN (Simple.apply (mkVar diseq)) + (intro_using_then absurd (fun absurd -> + tclTHEN (Simple.apply (mkVar diseq)) (tclTHEN (injHyp absurd) (full_trivial [])))))))) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 70cea89ccb..eb7b7e363f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1068,6 +1068,10 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_mustbe_force = function + | [] -> Proofview.tclUNIT() + | str::l -> Tacticals.New.tclTHEN (intro_mustbe_force str) (intros_mustbe_force l) + let rec intros_using_then_helper tac acc = function | [] -> tac (List.rev acc) | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 00739306a7..54c781af5c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -65,10 +65,13 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic +[@@ocaml.deprecated "Prefer [intro_using_then] to avoid renaming issues."] val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic +val intros_mustbe_force : Id.t list -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic +[@@ocaml.deprecated "Prefer [intros_using_then] to avoid renaming issues."] val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/bug_12676.v b/test-suite/bugs/closed/bug_12676.v new file mode 100644 index 0000000000..5118ddb472 --- /dev/null +++ b/test-suite/bugs/closed/bug_12676.v @@ -0,0 +1,13 @@ + + +Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}. +Proof. + pose (diseq := false). + decide equality. +Defined. + +Set Mangle Names. +Definition nat_eq_dec_mangle (i j:nat) : {i=j}+{i<>j}. +Proof. + decide equality. (*Error: Anomaly "variable diseq unbound." ...*) +Defined. diff --git a/test-suite/bugs/closed/bug_12860.v b/test-suite/bugs/closed/bug_12860.v new file mode 100644 index 0000000000..243aeceba2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12860.v @@ -0,0 +1,10 @@ +Require Import Coq.nsatz.NsatzTactic. +Require Import Coq.ZArith.ZArith Coq.QArith.QArith. + +Goal forall x y : Z, (x + y = y + x)%Z. + intros; nsatz. +Qed. + +Goal forall x y : Q, Qeq (x + y) (y + x). + intros; nsatz. +Qed. diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v index 70180f47c7..b684775bb4 100644 --- a/theories/nsatz/Nsatz.v +++ b/theories/nsatz/Nsatz.v @@ -75,43 +75,3 @@ red. exact Rmult_comm. Defined. Instance Rdi : (Integral_domain (Rcr:=Rcri)). constructor. exact Rmult_integral. exact R_one_zero. Defined. - -(* Rational numbers *) -Require Import QArith. - -Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). -Defined. - -Instance Qri : (Ring (Ro:=Qops)). -constructor. -try apply Q_Setoid. -apply Qplus_comp. -apply Qmult_comp. -apply Qminus_comp. -apply Qopp_comp. - exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. - exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. - apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. -reflexivity. exact Qplus_opp_r. -Defined. - -Lemma Q_one_zero: not (Qeq 1%Q 0%Q). -Proof. unfold Qeq. simpl. lia. Qed. - -Instance Qcri: (Cring (Rr:=Qri)). -red. exact Qmult_comm. Defined. - -Instance Qdi : (Integral_domain (Rcr:=Qcri)). -constructor. -exact Qmult_integral. exact Q_one_zero. Defined. - -(* Integers *) -Lemma Z_one_zero: 1%Z <> 0%Z. -Proof. lia. Qed. - -Instance Zcri: (Cring (Rr:=Zr)). -red. exact Z.mul_comm. Defined. - -Instance Zdi : (Integral_domain (Rcr:=Zcri)). -constructor. -exact Zmult_integral. exact Z_one_zero. Defined. diff --git a/theories/nsatz/NsatzTactic.v b/theories/nsatz/NsatzTactic.v index db7dab2c46..0d24de39d1 100644 --- a/theories/nsatz/NsatzTactic.v +++ b/theories/nsatz/NsatzTactic.v @@ -447,3 +447,43 @@ Tactic Notation "nsatz" "with" repeat equalities_to_goal; nsatz_generic radicalmax info lparam lvar end. + +(* Rational numbers *) +Require Import QArith. + +Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. + +Instance Qri : (Ring (Ro:=Qops)). +constructor. +try apply Q_Setoid. +apply Qplus_comp. +apply Qmult_comp. +apply Qminus_comp. +apply Qopp_comp. + exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. + exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. + apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. +reflexivity. exact Qplus_opp_r. +Defined. + +Lemma Q_one_zero: not (Qeq 1%Q 0%Q). +Proof. unfold Qeq. simpl. lia. Qed. + +Instance Qcri: (Cring (Rr:=Qri)). +red. exact Qmult_comm. Defined. + +Instance Qdi : (Integral_domain (Rcr:=Qcri)). +constructor. +exact Qmult_integral. exact Q_one_zero. Defined. + +(* Integers *) +Lemma Z_one_zero: 1%Z <> 0%Z. +Proof. lia. Qed. + +Instance Zcri: (Cring (Rr:=Zr)). +red. exact Z.mul_comm. Defined. + +Instance Zdi : (Integral_domain (Rcr:=Zcri)). +constructor. +exact Zmult_integral. exact Z_one_zero. Defined. |