diff options
| author | coqbot-app[bot] | 2021-04-06 14:55:06 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-06 14:55:06 +0000 |
| commit | 2360e5ba31c350f25d49fc71736282bfad9975ed (patch) | |
| tree | 6c3204f2ef382d452ad8684fd46e5e10a81be5c4 | |
| parent | dc565f2898145536cc6d3cf4346b6a60726bb8a9 (diff) | |
| parent | d3a51ac24244f586dfeff1a93b68cb084370534e (diff) | |
Merge PR #13741: Remove omega tactic (deprecated in 8.12)
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01
54 files changed, 158 insertions, 3689 deletions
diff --git a/META.coq-core.in b/META.coq-core.in index c58513979d..bc56b7b66e 100644 --- a/META.coq-core.in +++ b/META.coq-core.in @@ -320,21 +320,6 @@ package "plugins" ( plugin(native) = "tauto_plugin.cmxs" ) - package "omega" ( - - description = "Coq omega plugin" - version = "8.14" - - requires = "coq-core.plugins.ltac" - directory = "omega" - - archive(byte) = "omega_plugin.cmo" - archive(native) = "omega_plugin.cmx" - - plugin(byte) = "omega_plugin.cmo" - plugin(native) = "omega_plugin.cmxs" - ) - package "micromega" ( description = "Coq micromega plugin" diff --git a/Makefile.common b/Makefile.common index dc40413078..a21e974ed5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -102,7 +102,7 @@ CORESRCDIRS:=\ tactics vernac stm sysinit toplevel PLUGINDIRS:=\ - omega micromega \ + micromega \ ring extraction \ cc funind firstorder derive \ rtauto nsatz syntax btauto \ @@ -138,7 +138,6 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l # plugins object files ########################################################################### -OMEGACMO:=plugins/omega/omega_plugin.cmo MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo RINGCMO:=plugins/ring/ring_plugin.cmo NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo @@ -159,7 +158,7 @@ SSRSEARCHCMO=plugins/ssrsearch/ssrsearch_plugin.cmo LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo ZIFYCMO:=plugins/micromega/zify_plugin.cmo -PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \ +PLUGINSCMO:=$(LTACCMO) $(MICROMEGACMO) \ $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ diff --git a/Makefile.dev b/Makefile.dev index cfb02b6d80..c573fccf95 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -141,7 +141,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ### 4) plugins ################ -OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO)) MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO)) RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO)) NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO)) @@ -153,7 +152,6 @@ CCVO:= DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO)) LTACVO:=$(filter theories/ltac/%, $(THEORIESVO)) -omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) @@ -164,7 +162,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMO) btauto: $(BTAUTOVO) $(BTAUTOCMO) ltac: $(LTACVO) $(LTACCMO) -.PHONY: omega micromega ring nsatz extraction +.PHONY: micromega ring nsatz extraction .PHONY: funind cc rtauto btauto ltac # For emacs: diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 67555da0a2..0093b5fca2 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -139,7 +139,8 @@ project compcert "https://github.com/AbsInt/CompCert" "master" ######################################################################## # VST ######################################################################## -project vst "https://github.com/PrincetonUniversity/VST" "master" +# todo: 2021 03 11: switch back to master once vst merges the compcert3.9 branch +project vst "https://github.com/PrincetonUniversity/VST" "compcert3.9" ######################################################################## # cross-crypto @@ -247,7 +248,7 @@ project reduction_effects "https://github.com/coq-community/reduction-effects" " # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122" +project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20210310" ######################################################################## # aac_tactics diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index cb6c3e6452..01723e5b5c 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -5,4 +5,10 @@ ci_dir="$(dirname "$0")" git_download flocq -( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) +( cd "${CI_BUILD_DIR}/flocq" + ( if [ ! -x ./configure ]; then + autoconf + ./configure COQEXTRAFLAGS="-compat 8.13"; + fi ) + ./remake "-j${NJOBS}" + ./remake install ) diff --git a/doc/changelog/04-tactics/13741-remove_omega.rst b/doc/changelog/04-tactics/13741-remove_omega.rst new file mode 100644 index 0000000000..0b25c01958 --- /dev/null +++ b/doc/changelog/04-tactics/13741-remove_omega.rst @@ -0,0 +1,7 @@ +- **Removed:** + Removed the `omega` tactic (deprecated in 8.12) and 4 `* Omega *` flags. + Use `lia` instead. + (`#13741 <https://github.com/coq/coq/pull/13741>`_, + by Jim Fehrle, who addressed the final details, building on much work by + Frédéric Besson, who greatly improved :tacn:`lia`, Maxime Dénès, + Vincent Laporte and with the help of many package maintainers, among others). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d471c695c..d718454364 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -159,7 +159,6 @@ and checked to be :math:`-1`. This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. - High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst deleted file mode 100644 index 86bb0502c6..0000000000 --- a/doc/sphinx/addendum/omega.rst +++ /dev/null @@ -1,210 +0,0 @@ -.. _omega_chapter: - -Omega: a (deprecated) solver for arithmetic -===================================================================== - -:Author: Pierre Crégut - -.. warning:: - - The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` - tactic. The goal is to consolidate the arithmetic solving - capabilities of Coq into a single engine; moreover, :tacn:`lia` is - in general more powerful than :tacn:`omega` (it is a complete - Presburger arithmetic solver while :tacn:`omega` was known to be - incomplete). - - It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing - projects. We also ask that you report (in our `bug tracker - <https://github.com/coq/coq/issues>`_) any issue you encounter, especially - if the issue was not present in :tacn:`omega`. If no new issues are - reported, :tacn:`omega` will be removed soon. - - Note that replacing :tacn:`omega` with :tacn:`lia` can break - non-robust proof scripts which rely on incompleteness bugs of - :tacn:`omega` (e.g. using the pattern :g:`; try omega`). - -Description of ``omega`` ------------------------- - -.. tacn:: omega - - .. deprecated:: 8.12 - - Use :tacn:`lia` instead. - - :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, - i.e. for proving formulas made of equations and inequalities over the - type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. - Formulas on ``nat`` are automatically injected into ``Z``. The procedure - may use any hypothesis of the current proof session to solve the goal. - - Multiplication is handled by :tacn:`omega` but only goals where at - least one of the two multiplicands of products is a constant are - solvable. This is the restriction meant by "Presburger arithmetic". - - If the tactic cannot solve the goal, it fails with an error message. - In any case, the computation eventually stops. - -Arithmetical goals recognized by ``omega`` ------------------------------------------- - -:tacn:`omega` applies only to quantifier-free formulas built from the connectives:: - - /\ \/ ~ -> - -on atomic formulas. Atomic formulas are built from the predicates:: - - = < <= > >= - -on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes:: - - + - * S O pred - -and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and:: - - + - * Z.succ Z.pred - -All expressions of type ``nat`` or ``Z`` not built on these -operators are considered abstractly as if they -were arbitrary variables of type ``nat`` or ``Z``. - -Messages from ``omega`` ------------------------ - -When :tacn:`omega` does not solve the goal, one of the following errors -is generated: - -.. exn:: omega can't solve this system. - - This may happen if your goal is not quantifier-free (if it is - universally quantified, try :tacn:`intros` first; if it contains - existentials quantifiers too, :tacn:`omega` is not strong enough to solve your - goal). This may happen also if your goal contains arithmetical - operators not recognized by :tacn:`omega`. Finally, your goal may be simply - not true! - -.. exn:: omega: Not a quantifier-free goal. - - If your goal is universally quantified, you should first apply - :tacn:`intro` as many times as needed. - -.. exn:: omega: Unrecognized predicate or connective: @ident. - :undocumented: - -.. exn:: omega: Unrecognized atomic proposition: ... - :undocumented: - -.. exn:: omega: Can't solve a goal with proposition variables. - :undocumented: - -.. exn:: omega: Unrecognized proposition. - :undocumented: - -.. exn:: omega: Can't solve a goal with non-linear products. - :undocumented: - -.. exn:: omega: Can't solve a goal with equality on type ... - :undocumented: - - -Using ``omega`` ---------------- - -The ``omega`` tactic does not belong to the core system. It should be -loaded by - -.. coqtop:: in - - Require Import Omega. - -.. example:: - - .. coqtop:: all warn - - Require Import Omega. - - Open Scope Z_scope. - - Goal forall m n:Z, 1 + 2 * m <> 2 * n. - intros; omega. - Abort. - - Goal forall z:Z, z > 0 -> 2 * z + 1 > z. - intro; omega. - Abort. - - -Options -------- - -.. flag:: Stable Omega - - .. deprecated:: 8.5 - - This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It - resets internal name counters to make executions of :tacn:`omega` independent. - -.. flag:: Omega UseLocalDefs - - This flag (on by default) allows :tacn:`omega` to use the :term:`bodies <body>` of local - variables. - -.. flag:: Omega System - - This flag (off by default) activate the printing of debug information - -.. flag:: Omega Action - - This flag (off by default) activate the printing of debug information - -Technical data --------------- - -Overview of the tactic -~~~~~~~~~~~~~~~~~~~~~~ - - * The goal is negated twice and the first negation is introduced as a hypothesis. - * Hypotheses are decomposed in simple equations or inequalities. Multiple - goals may result from this phase. - * Equations and inequalities over ``nat`` are translated over - ``Z``, multiple goals may result from the translation of subtraction. - * Equations and inequalities are normalized. - * Goals are solved by the OMEGA decision procedure. - * The script of the solution is replayed. - -Overview of the OMEGA decision procedure -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The OMEGA decision procedure involved in the :tacn:`omega` tactic uses -a small subset of the decision procedure presented in :cite:`TheOmegaPaper` -Here is an overview, refer to the original paper for more information. - - * Equations and inequalities are normalized by division by the GCD of their - coefficients. - * Equations are eliminated, using the Banerjee test to get a coefficient - equal to one. - * Note that each inequality cuts the Euclidean space in half. - * Inequalities are solved by projecting on the hyperspace - defined by cancelling one of the variables. They are partitioned - according to the sign of the coefficient of the eliminated - variable. Pairs of inequalities from different classes define a - new edge in the projection. - * Redundant inequalities are eliminated or merged in new - equations that can be eliminated by the Banerjee test. - * The last two steps are iterated until a contradiction is reached - (success) or there is no more variable to eliminate (failure). - -It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure are not implemented, so the -decision procedure is only partial. - -Bugs ----- - - * The simplification procedure is very dumb and this results in - many redundant cases to explore. - - * Much too slow. - - * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index bf8174f246..f8d6b35226 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -778,10 +778,8 @@ The main changes include: of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. -Additionally, the :tacn:`omega` tactic is deprecated in this version of Coq, -and we recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +Additionally, the `omega` tactic is deprecated in this version of Coq, +and we recommend users to switch to :tacn:`lia` in new proof scripts. See the `Changes in 8.12+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked @@ -1046,7 +1044,7 @@ Tactics <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). - **Changed:** The :g:`auto with zarith` tactic and variations (including - :tacn:`intuition`) may now call :tacn:`lia` instead of :tacn:`omega` + :tacn:`intuition`) may now call :tacn:`lia` instead of `omega` (when the `Omega` module is loaded); more goals may be automatically solved, fewer section variables will be captured spuriously (`#11018 <https://github.com/coq/coq/pull/11018>`_, @@ -1142,7 +1140,7 @@ Tactics (`#11883 <https://github.com/coq/coq/pull/11883>`_, by Attila Gáspár). - **Deprecated:** - The :tacn:`omega` tactic is deprecated; + The `omega` tactic is deprecated; use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead (`#11976 <https://github.com/coq/coq/pull/11976>`_, by Vincent Laporte). @@ -2129,11 +2127,9 @@ The main changes brought by Coq version 8.11 are: - :ref:`Revision<811Reals>` of the :g:`Coq.Reals` library, its axiomatisation and instances of the constructive and classical real numbers. -Additionally, while the :tacn:`omega` tactic is not yet deprecated in +Additionally, while the `omega` tactic is not yet deprecated in this version of Coq, it should soon be the case and we already -recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +recommend users to switch to :tacn:`lia` in new proof scripts. The ``dev/doc/critical-bugs`` file documents the known critical bugs of Coq and affected releases. See the `Changes in 8.11+beta1`_ diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b1759bf71b..88fca93547 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1666,7 +1666,7 @@ Proving a subgoal as a separate lemma: abstract is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. - This is useful with tactics such as :tacn:`omega` or + This is useful with tactics such as :tacn:`discriminate` that generate huge proof terms with many intermediate goals. It can significantly reduce peak memory use. In most cases it doesn't have a significant impact on run time. One case in which it can reduce run time @@ -2317,11 +2317,10 @@ performance issue. .. coqtop:: reset in - Set Warnings "-omega-is-deprecated". - Require Import Coq.omega.Omega. + Require Import Lia. Ltac mytauto := tauto. - Ltac tac := intros; repeat split; omega || mytauto. + Ltac tac := intros; repeat split; lia || mytauto. Notation max x y := (x + (y - x)) (only parsing). @@ -2340,7 +2339,7 @@ performance issue. Set Ltac Profiling. tac. Show Ltac Profile. - Show Ltac Profile "omega". + Show Ltac Profile "lia". .. coqtop:: in diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index c3712b109d..e458c3a9f5 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -14,7 +14,6 @@ complex goals in new domains. :maxdepth: 1 logic - ../../addendum/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index e4f0967794..bca66cc61b 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -58,10 +58,7 @@ theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/NsatzTactic.v theories/nsatz/Nsatz.v -theories/omega/Omega.v theories/omega/OmegaLemmas.v -theories/omega/OmegaPlugin.v -theories/omega/OmegaTactic.v theories/omega/PreOmega.v theories/quote/Quote.v theories/romega/ROmega.v diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 4ba60ddd9f..873b2f8dff 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -21,7 +21,6 @@ (glob_files %{project_root}/plugins/ltac/*.mlg) (glob_files %{project_root}/plugins/micromega/*.mlg) (glob_files %{project_root}/plugins/nsatz/*.mlg) - (glob_files %{project_root}/plugins/omega/*.mlg) (glob_files %{project_root}/plugins/ring/*.mlg) (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/ssr/*.mlg) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index a6a7f7d742..72b54d329f 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -177,7 +177,6 @@ let concl_next_tac = "symmetry" ] @ [ "assumption"; - "omega"; "ring"; "auto"; "eauto"; diff --git a/ide/coqide/preferences.ml b/ide/coqide/preferences.ml index 5a77f4ebcf..8361cc3940 100644 --- a/ide/coqide/preferences.ml +++ b/ide/coqide/preferences.ml @@ -304,7 +304,7 @@ let encoding = new preference ~name:["encoding"] ~init ~repr let automatic_tactics = - let init = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ] in + let init = ["trivial"; "tauto"; "auto"; "auto with *"; "intuition" ] in new preference ~name:["automatic_tactics"] ~init ~repr:Repr.(string_list) let cmd_print = diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml deleted file mode 100644 index 9d92ffde74..0000000000 --- a/plugins/omega/coq_omega.ml +++ /dev/null @@ -1,1939 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - -open CErrors -open Util -open Names -open Constr -open Context -open Nameops -open EConstr -open Tacticals.New -open Tacmach.New -open Tactics -open Libnames -open Nametab -open Contradiction -open Tactypes -open Context.Named.Declaration - -module NamedDecl = Context.Named.Declaration - -module ZOmega = struct - type bigint = Z.t - let equal = Z.equal - let less_than = Z.lt - let add = Z.add - let sub = Z.sub - let mult = Z.mul - let euclid = Z.div_rem - let neg = Z.neg - let zero = Z.zero - let one = Z.one - let to_string = Z.to_string -end - -module OmegaSolver = Omega.MakeOmegaSolver (ZOmega) -open OmegaSolver - -(* Added by JCF, 09/03/98 *) - -let elim_id id = simplest_elim (mkVar id) - -let resolve_id id = apply (mkVar id) - -let display_system_flag = ref false -let display_action_flag = ref false -let old_style_flag = ref false -let letin_flag = ref true - -(* Should we reset all variable labels between two runs of omega ? *) - -let reset_flag = ref true - -(* Coq < 8.5 was not performing such resets, hence omega was slightly - non-deterministic: successive runs of omega on the same problem may - lead to distinct proof-terms. - At the very least, these terms differed on the inner - variable names, but they could even be non-convertible : - the OmegaSolver relies on Hashtbl.iter, it can hence find a different - solution when variable indices differ. *) - -let read f () = !f -let write f x = f:=x - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"System"]; - optread = read display_system_flag; - optwrite = write display_system_flag } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"Action"]; - optread = read display_action_flag; - optwrite = write display_action_flag } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"OldStyle"]; - optread = read old_style_flag; - optwrite = write old_style_flag } - -let () = - declare_bool_option - { optdepr = true; - optkey = ["Stable";"Omega"]; - optread = read reset_flag; - optwrite = write reset_flag } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"UseLocalDefs"]; - optread = read letin_flag; - optwrite = write letin_flag } - -let intref, reset_all_references = - let refs = ref [] in - (fun n -> let r = ref n in refs := (r,n) :: !refs; r), - (fun () -> List.iter (fun (r,n) -> r:=n) !refs) - -let new_identifier = - let cpt = intref 0 in - (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) - -let new_identifier_var = - let cpt = intref 0 in - (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) - -let new_id = - let cpt = intref 0 in fun () -> incr cpt; !cpt - -let new_var_num = - let cpt = intref 1000 in (fun () -> incr cpt; !cpt) - -let new_var = - let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) - -let display_var i = Printf.sprintf "X%d" i - -let intern_id,unintern_id,reset_intern_tables = - let cpt = ref 0 in - let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in - (fun (name : Id.t) -> - try Hashtbl.find table name with Not_found -> - let idx = !cpt in - Hashtbl.add table name idx; - Hashtbl.add co_table idx name; - incr cpt; idx), - (fun idx -> - try Hashtbl.find co_table idx with Not_found -> - let v = new_var () in - Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), - (fun () -> cpt := 0; Hashtbl.clear table) - -let mk_then tacs = tclTHENLIST tacs - -let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) - -let generalize_tac t = generalize t -let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] -let pf_nf gl c = pf_apply Tacred.simpl gl c - -let rev_assoc k = - let rec loop = function - | [] -> raise Not_found - | (v,k')::_ when Int.equal k k' -> v - | _ :: l -> loop l - in - loop - -let tag_hypothesis, hyp_of_tag, clear_tags = - let l = ref ([]:(Id.t * int) list) in - (fun h id -> l := (h,id):: !l), - (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), - (fun () -> l := []) - -let hide_constr,find_constr,clear_constr_tables,dump_tables = - let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in - (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun sigma h -> - try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"), - (fun () -> l := []), - (fun () -> !l) - -let reset_all () = - if !reset_flag then begin - reset_all_references (); - reset_intern_tables (); - clear_tags (); - clear_constr_tables () - end - -(* Lazy evaluation is used for Coq constants, because this code - is evaluated before the compiled modules are loaded. - To use the constant Zplus, one must type "Lazy.force coq_Zplus" - This is the right way to access to Coq constants in tactics ML code *) - -let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global - |> EConstr.of_constr) - - -(* Zarith *) -let coq_xH = gen_constant "num.pos.xH" -let coq_xO = gen_constant "num.pos.xO" -let coq_xI = gen_constant "num.pos.xI" -let coq_Z0 = gen_constant "num.Z.Z0" -let coq_Zpos = gen_constant "num.Z.Zpos" -let coq_Zneg = gen_constant "num.Z.Zneg" -let coq_Z = gen_constant "num.Z.type" -let coq_comparison = gen_constant "core.comparison.type" -let coq_Gt = gen_constant "core.comparison.Gt" -let coq_Zplus = gen_constant "num.Z.add" -let coq_Zmult = gen_constant "num.Z.mul" -let coq_Zopp = gen_constant "num.Z.opp" -let coq_Zminus = gen_constant "num.Z.sub" -let coq_Zsucc = gen_constant "num.Z.succ" -let coq_Zpred = gen_constant "num.Z.pred" -let coq_Z_of_nat = gen_constant "num.Z.of_nat" -let coq_inj_plus = gen_constant "num.Nat2Z.inj_add" -let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul" -let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub" -let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2" -let coq_inj_S = gen_constant "num.Nat2Z.inj_succ" -let coq_inj_eq = gen_constant "plugins.omega.inj_eq" -let coq_inj_neq = gen_constant "plugins.omega.inj_neq" -let coq_inj_le = gen_constant "plugins.omega.inj_le" -let coq_inj_lt = gen_constant "plugins.omega.inj_lt" -let coq_inj_ge = gen_constant "plugins.omega.inj_ge" -let coq_inj_gt = gen_constant "plugins.omega.inj_gt" -let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse" -let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc" -let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse" -let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute" -let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm" -let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm" -let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx" -let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1" -let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2" -let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3" -let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4" -let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5" -let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6" -let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7" -let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8" -let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9" -let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10" -let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11" -let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12" -let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13" -let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14" -let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15" -let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16" -let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17" -let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18" -let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19" -let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20" -let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0" -let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1" -let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2" -let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3" -let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4" -let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5" -let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6" -let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l" -let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr" -let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r" -let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1" -let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left" -let coq_Zne_left = gen_constant "plugins.omega.Zne_left" -let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left" -let coq_Zge_left = gen_constant "plugins.omega.Zge_left" -let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left" -let coq_Zle_left = gen_constant "plugins.omega.Zle_left" -let coq_new_var = gen_constant "plugins.omega.new_var" -let coq_intro_Z = gen_constant "plugins.omega.intro_Z" - -let coq_dec_eq = gen_constant "num.Z.eq_decidable" -let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne" -let coq_dec_Zle = gen_constant "num.Z.le_decidable" -let coq_dec_Zlt = gen_constant "num.Z.lt_decidable" -let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt" -let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge" - -let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq" -let coq_not_Zne = gen_constant "plugins.omega.not_Zne" -let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt" -let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge" -let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt" -let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le" -let coq_neq = gen_constant "plugins.omega.neq" -let coq_Zne = gen_constant "plugins.omega.Zne" -let coq_Zle = gen_constant "num.Z.le" -let coq_Zlt = gen_constant "num.Z.lt" -let coq_Zge = gen_constant "num.Z.ge" -let coq_Zgt = gen_constant "num.Z.gt" - -(* Peano/Datatypes *) -let coq_nat = gen_constant "num.nat.type" -let coq_O = gen_constant "num.nat.O" -let coq_S = gen_constant "num.nat.S" -let coq_le = gen_constant "num.nat.le" -let coq_lt = gen_constant "num.nat.lt" -let coq_ge = gen_constant "num.nat.ge" -let coq_gt = gen_constant "num.nat.gt" -let coq_plus = gen_constant "num.nat.add" -let coq_minus = gen_constant "num.nat.sub" -let coq_mult = gen_constant "num.nat.mul" -let coq_pred = gen_constant "num.nat.pred" - -(* Compare_dec/Peano_dec/Minus *) -let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus" -let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec" -let coq_dec_eq_nat = gen_constant "num.nat.eq_dec" -let coq_dec_le = gen_constant "num.nat.dec_le" -let coq_dec_lt = gen_constant "num.nat.dec_lt" -let coq_dec_ge = gen_constant "num.nat.dec_ge" -let coq_dec_gt = gen_constant "num.nat.dec_gt" -let coq_not_eq = gen_constant "num.nat.not_eq" -let coq_not_le = gen_constant "num.nat.not_le" -let coq_not_lt = gen_constant "num.nat.not_lt" -let coq_not_ge = gen_constant "num.nat.not_ge" -let coq_not_gt = gen_constant "num.nat.not_gt" - -(* Logic/Decidable *) -let coq_eq_ind_r = gen_constant "core.eq.ind_r" - -let coq_dec_or = gen_constant "core.dec.or" -let coq_dec_and = gen_constant "core.dec.and" -let coq_dec_imp = gen_constant "core.dec.imp" -let coq_dec_iff = gen_constant "core.dec.iff" -let coq_dec_not = gen_constant "core.dec.not" -let coq_dec_False = gen_constant "core.dec.False" -let coq_dec_not_not = gen_constant "core.dec.not_not" -let coq_dec_True = gen_constant "core.dec.True" - -let coq_not_or = gen_constant "core.dec.not_or" -let coq_not_and = gen_constant "core.dec.not_and" -let coq_not_imp = gen_constant "core.dec.not_imp" -let coq_not_iff = gen_constant "core.dec.not_iff" -let coq_not_not = gen_constant "core.dec.dec_not_not" -let coq_imp_simp = gen_constant "core.dec.imp_simp" -let coq_iff = gen_constant "core.iff.type" -let coq_not = gen_constant "core.not.type" -let coq_and = gen_constant "core.and.type" -let coq_or = gen_constant "core.or.type" -let coq_eq = gen_constant "core.eq.type" -let coq_ex = gen_constant "core.ex.type" -let coq_False = gen_constant "core.False.type" -let coq_True = gen_constant "core.True.type" - -(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) - -(* For unfold *) -let evaluable_ref_of_constr s c = - let env = Global.env () in - let evd = Evd.from_env env in - let open Tacred in - match EConstr.kind evd (Lazy.force c) with - | Const (kn,u) when is_evaluable env (EvalConstRef kn) -> - EvalConstRef kn - | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) - -let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) -let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) -let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) -let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) -let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) -let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) - -let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) -let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) -let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) -let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) -let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 -let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) -let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) -let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) -let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) -let mk_not t = mkApp (Lazy.force coq_not, [| t |]) -let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) - -let mk_integer n = - let rec loop n = - if n =? one then Lazy.force coq_xH else - mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI), - [| loop (n/two) |]) - in - if n =? zero then Lazy.force coq_Z0 - else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg), - [| loop (abs n) |]) - -type omega_constant = - | Zplus | Zmult | Zminus | Zsucc | Zopp | Zpred - | Plus | Mult | Minus | Pred | S | O - | Zpos | Zneg | Z0 | Z_of_nat - | Eq | Neq - | Zne | Zle | Zlt | Zge | Zgt - | Z | Nat - | And | Or | False | True | Not | Iff - | Le | Lt | Ge | Gt - | Other of string - -type result = - | Kvar of Id.t - | Kapp of omega_constant * constr list - | Kimp of constr * constr - | Kufo - -(* Nota: Kimp correspond to a binder (Prod), but hopefully we won't - have to bother with term lifting: Kimp will correspond to anonymous - product, for which (Rel 1) doesn't occur in the right term. - Moreover, we'll work on fully introduced goals, hence no Rel's in - the term parts that we manipulate, but rather Var's. - Said otherwise: all constr manipulated here are closed *) - -let destructurate_prop sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let c, args = decompose_app sigma t in - match EConstr.kind sigma c, args with - | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args) - | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args) - | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args) - | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args) - | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args) - | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args) - | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args) - | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args) - | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args) - | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) - | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) - | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) - | Const (sp,_), args -> - Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args) - | Construct (csp,_) , args -> - Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args) - | Ind (isp,_), args -> - Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args) - | Var id,[] -> Kvar id - | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) - | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") - | _ -> Kufo - -let nf = Tacred.simpl - -let destructurate_type env sigma t = - let is_conv = Reductionops.is_conv env sigma in - let c, args = decompose_app sigma (nf env sigma t) in - match EConstr.kind sigma c, args with - | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args) - | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args) - | _ -> Kufo - -let destructurate_term sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let c, args = decompose_app sigma t in - match EConstr.kind sigma c, args with - | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args) - | _, [_] when eq_constr c (Lazy.force coq_Zsucc) -> Kapp (Zsucc,args) - | _, [_] when eq_constr c (Lazy.force coq_Zpred) -> Kapp (Zpred,args) - | _, [_] when eq_constr c (Lazy.force coq_Zopp) -> Kapp (Zopp,args) - | _, [_;_] when eq_constr c (Lazy.force coq_plus) -> Kapp (Plus,args) - | _, [_;_] when eq_constr c (Lazy.force coq_mult) -> Kapp (Mult,args) - | _, [_;_] when eq_constr c (Lazy.force coq_minus) -> Kapp (Minus,args) - | _, [_] when eq_constr c (Lazy.force coq_pred) -> Kapp (Pred,args) - | _, [_] when eq_constr c (Lazy.force coq_S) -> Kapp (S,args) - | _, [] when eq_constr c (Lazy.force coq_O) -> Kapp (O,args) - | _, [_] when eq_constr c (Lazy.force coq_Zpos) -> Kapp (Zneg,args) - | _, [_] when eq_constr c (Lazy.force coq_Zneg) -> Kapp (Zpos,args) - | _, [] when eq_constr c (Lazy.force coq_Z0) -> Kapp (Z0,args) - | _, [_] when eq_constr c (Lazy.force coq_Z_of_nat) -> Kapp (Z_of_nat,args) - | Var id,[] -> Kvar id - | _ -> Kufo - -let recognize_number sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let rec loop t = - match decompose_app sigma t with - | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t - | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t - | f, [] when eq_constr f (Lazy.force coq_xH) -> one - | _ -> failwith "not a number" - in - match decompose_app sigma t with - | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t - | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t) - | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero - | _ -> failwith "not a number" - -type constr_path = - | P_APP of int - (* Abstraction and product *) - | P_TYPE - -let context sigma operation path (t : constr) = - let rec loop i p0 t = - match (p0,EConstr.kind sigma t) with - | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) - | ([], _) -> operation i t - | ((P_APP n :: p), App (f,v)) -> - let v' = Array.copy v in - v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v') - | (p, Fix ((_,n as ln),(tys,lna,v))) -> - let l = Array.length v in - let v' = Array.copy v in - v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) - | ((P_TYPE :: p), Prod (n,t,c)) -> - (mkProd (n,loop i p t,c)) - | ((P_TYPE :: p), Lambda (n,t,c)) -> - (mkLambda (n,loop i p t,c)) - | ((P_TYPE :: p), LetIn (n,b,t,c)) -> - (mkLetIn (n,b,loop i p t,c)) - | (p, _) -> - failwith ("abstract_path " ^ string_of_int(List.length p)) - in - loop 1 path t - -let occurrence sigma path (t : constr) = - let rec loop p0 t = match (p0,EConstr.kind sigma t) with - | (p, Cast (c,_,_)) -> loop p c - | ([], _) -> t - | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) - | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n) - | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term - | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term - | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term - | (p, _) -> - failwith ("occurrence " ^ string_of_int(List.length p)) - in - loop path t - -let abstract_path sigma typ path t = - let term_occur = ref (mkRel 0) in - let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in - mkLambda (make_annot (Name (Id.of_string "x")) Sorts.Relevant, typ, abstract), !term_occur - -let focused_simpl path = - let open Tacmach.New in - Proofview.Goal.enter begin fun gl -> - let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl ~check:false newc DEFAULTcast - end - -let focused_simpl path = focused_simpl path - -type oformula = - | Oplus of oformula * oformula - | Otimes of oformula * oformula - | Oatom of Id.t - | Oz of bigint - | Oufo of constr - -let rec oprint = function - | Oplus(t1,t2) -> - print_string "("; oprint t1; print_string "+"; - oprint t2; print_string ")" - | Otimes (t1,t2) -> - print_string "("; oprint t1; print_string "*"; - oprint t2; print_string ")" - | Oatom s -> print_string (Id.to_string s) - | Oz i -> print_string (string_of_bigint i) - | Oufo f -> print_string "?" - -let rec weight = function - | Oatom c -> intern_id c - | Oz _ -> -1 - | Otimes(c,_) -> weight c - | Oplus _ -> failwith "weight" - | Oufo _ -> -1 - -let rec val_of = function - | Oatom c -> mkVar c - | Oz c -> mk_integer c - | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |]) - | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) - | Oufo c -> c - -let compile name kind = - let rec loop accu = function - | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r - | Oz n -> - let id = new_id () in - tag_hypothesis name id; - {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly (Pp.str "compile_equation.") - in - loop [] - -let decompile af = - let rec loop = function - | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r) - | [] -> Oz af.constant - in - loop af.body - -(** Backward compat to emulate the old Refine: normalize the goal conclusion *) -let new_hole env sigma c = - let c = Reductionops.nf_betaiota env sigma c in - Evarutil.new_evar env sigma c - -let clever_rewrite_base_poly typ p result theorem = - let open Tacmach.New in - Proofview.Goal.enter begin fun gl -> - let full = pf_concl gl in - let env = pf_env gl in - let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in - Refine.refine ~typecheck:false begin fun sigma -> - let t = - applist - (mkLambda - (make_annot (Name (Id.of_string "P")) Sorts.Relevant, - mkArrow typ Sorts.Relevant mkProp, - mkLambda - (make_annot (Name (Id.of_string "H")) Sorts.Relevant, - applist (mkRel 1,[result]), - mkApp (Lazy.force coq_eq_ind_r, - [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), - [abstracted]) - in - let argt = mkApp (abstracted, [|result|]) in - let (sigma, hole) = new_hole env sigma argt in - (sigma, applist (t, [hole])) - end - end - -let clever_rewrite_base p result theorem = - clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem - -let clever_rewrite_base_nat p result theorem = - clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem - -let clever_rewrite_gen p result (t,args) = - let theorem = applist(t, args) in - clever_rewrite_base p result theorem - -let clever_rewrite_gen_nat p result (t,args) = - let theorem = applist(t, args) in - clever_rewrite_base_nat p result theorem - -(** Solve using the term the term [t _] *) -let refine_app gl t = - let open Tacmach.New in - Refine.refine ~typecheck:false begin fun sigma -> - let env = pf_env gl in - let ht = match EConstr.kind sigma (pf_get_type_of gl t) with - | Prod (_, t, _) -> t - | _ -> assert false - in - let (sigma, hole) = new_hole env sigma ht in - (sigma, applist (t, [hole])) - end - -let clever_rewrite p vpath t = - let open Tacmach.New in - Proofview.Goal.enter begin fun gl -> - let full = pf_concl gl in - let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in - let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in - let t' = applist(t, (vargs @ [abstracted])) in - refine_app gl t' - end - -(** simpl_coeffs : - The subterm at location [path_init] in the current goal should - look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce - via "simpl" each [ci] and the final constant [k]. - The path [path_k] gives the location of constant [k]. - Earlier, the whole was a mere call to [focused_simpl], - leading to reduction inside the atoms [vi], which is bad, - for instance when the atom is an evaluable definition - (see #4132). *) - -let simpl_coeffs path_init path_k = - Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let rec loop n t = - if Int.equal n 0 then pf_nf gl t - else - (* t should be of the form ((v * c) + ...) *) - match EConstr.kind sigma t with - | App(f,[|t1;t2|]) -> - (match EConstr.kind sigma t1 with - | App (g,[|v;c|]) -> - let c' = pf_nf gl c in - let t2' = loop (pred n) t2 in - mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) - | _ -> assert false) - | _ -> assert false - in - let n = Util.(-) (List.length path_k) (List.length path_init) in - let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) - in - convert_concl ~check:false newc DEFAULTcast - end - -let rec shuffle p (t1,t2) = - match t1,t2 with - | Oplus(l1,r1), Oplus(l2,r2) -> - if weight l1 > weight l2 then - let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in - (clever_rewrite p [[P_APP 1;P_APP 1]; - [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) - :: tac, - Oplus(l1,t')) - else - let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in - (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zplus_permute) - :: tac, - Oplus(l2,t')) - | Oplus(l1,r1), t2 -> - if weight l1 > weight t2 then - let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) - :: tac, - Oplus(l1, t') - else - [clever_rewrite p [[P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zplus_comm)], - Oplus(t2,t1) - | t1,Oplus(l2,r2) -> - if weight l2 > weight t1 then - let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in - clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zplus_permute) - :: tac, - Oplus(l2,t') - else [],Oplus(t1,t2) - | Oz t1,Oz t2 -> - [focused_simpl p], Oz(Z.add t1 t2) - | t1,t2 -> - if weight t1 < weight t2 then - [clever_rewrite p [[P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zplus_comm)], - Oplus(t2,t1) - else [],Oplus(t1,t2) - -let shuffle_mult p_init k1 e1 k2 e2 = - let rec loop p = function - | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> - if Int.equal v1 v2 then - let tac = - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA10) - in - if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then - let tac' = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: - loop p (l1,l2) - else tac :: loop (P_APP 2 :: p) (l1,l2) - else if v1 > v2 then - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2]; - [P_APP 1; P_APP 2]] - (Lazy.force coq_fast_OMEGA11) :: - loop (P_APP 2 :: p) (l1,l2') - else - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) (l1',l2) - | ({c=c1;v=v1}::l1), [] -> - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2]; - [P_APP 1; P_APP 2]] - (Lazy.force coq_fast_OMEGA11) :: - loop (P_APP 2 :: p) (l1,[]) - | [],({c=c2;v=v2}::l2) -> - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) ([],l2) - | [],[] -> [simpl_coeffs p_init p] - in - loop p_init (e1,e2) - -let shuffle_mult_right p_init e1 k2 e2 = - let rec loop p = function - | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> - if Int.equal v1 v2 then - let tac = - clever_rewrite p - [[P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA15) - in - if Z.add c1 (Z.mul k2 c2) =? zero then - let tac' = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) - in - tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: - loop p (l1,l2) - else tac :: loop (P_APP 2 :: p) (l1,l2) - else if v1 > v2 then - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) (l1,l2') - else - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) (l1',l2) - | ({c=c1;v=v1}::l1), [] -> - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) (l1,[]) - | [],({c=c2;v=v2}::l2) -> - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) ([],l2) - | [],[] -> [simpl_coeffs p_init p] - in - loop p_init (e1,e2) - -let rec shuffle_cancel p = function - | [] -> [focused_simpl p] - | ({c=c1}::l1) -> - let tac = - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2; P_APP 1]] - (if c1 >? zero then - (Lazy.force coq_fast_OMEGA13) - else - (Lazy.force coq_fast_OMEGA14)) - in - tac :: shuffle_cancel p l1 - -let rec scalar p n = function - | Oplus(t1,t2) -> - let tac1,t1' = scalar (P_APP 1 :: p) n t1 and - tac2,t2' = scalar (P_APP 2 :: p) n t2 in - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zmult_plus_distr_l) :: - (tac1 @ tac2), Oplus(t1',t2') - | Otimes(t1,Oz x) -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zmult_assoc_reverse); - focused_simpl (P_APP 2 :: p)], - Otimes(t1,Oz (n*x)) - | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") - | (Oatom _ as t) -> [], Otimes(t,Oz n) - | Oz i -> [focused_simpl p],Oz(n*i) - | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) - -let scalar_norm p_init = - let rec loop p = function - | [] -> [simpl_coeffs p_init p] - | (_::l) -> - clever_rewrite p - [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l - in - loop p_init - -let norm_add p_init = - let rec loop p = function - | [] -> [simpl_coeffs p_init p] - | _:: l -> - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) l - in - loop p_init - -let scalar_norm_add p_init = - let rec loop p = function - | [] -> [simpl_coeffs p_init p] - | _ :: l -> - clever_rewrite p - [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]] - (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l - in - loop p_init - -let rec negate p = function - | Oplus(t1,t2) -> - let tac1,t1' = negate (P_APP 1 :: p) t1 and - tac2,t2' = negate (P_APP 2 :: p) t2 in - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zopp_plus_distr) :: - (tac1 @ tac2), - Oplus(t1',t2') - | Otimes(t1,Oz x) -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zopp_mult_distr_r); - focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) - | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") - | (Oatom _ as t) -> - let r = Otimes(t,Oz(negone)) in - [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r - | Oz i -> [focused_simpl p],Oz(neg i) - | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) - -let rec transform sigma p t = - let default isnat t' = - try - let v,th,_ = find_constr sigma t' in - [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with e when CErrors.noncritical e -> - let v = new_identifier_var () - and th = new_identifier () in - hide_constr t' v th isnat; - [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - in - try match destructurate_term sigma t with - | Kapp(Zplus,[t1;t2]) -> - let tac1,t1' = transform sigma (P_APP 1 :: p) t1 - and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in - let tac,t' = shuffle p (t1',t2') in - tac1 @ tac2 @ tac, t' - | Kapp(Zminus,[t1;t2]) -> - let tac,t = - transform sigma p - (mkApp (Lazy.force coq_Zplus, - [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - unfold sp_Zminus :: tac,t - | Kapp(Zsucc,[t1]) -> - let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, - [| t1; mk_integer one |])) in - unfold sp_Zsucc :: tac,t - | Kapp(Zpred,[t1]) -> - let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, - [| t1; mk_integer negone |])) in - unfold sp_Zpred :: tac,t - | Kapp(Zmult,[t1;t2]) -> - let tac1,t1' = transform sigma (P_APP 1 :: p) t1 - and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in - begin match t1',t2' with - | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t' - | (Oz n,_) -> - let sym = - clever_rewrite p [[P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zmult_comm) in - let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t' - | _ -> default false t - end - | Kapp((Zpos|Zneg|Z0),_) -> - (try ([],Oz(recognize_number sigma t)) - with e when CErrors.noncritical e -> default false t) - | Kvar s -> [],Oatom s - | Kapp(Zopp,[t]) -> - let tac,t' = transform sigma (P_APP 1 :: p) t in - let tac',t'' = negate p t' in - tac @ tac', t'' - | Kapp(Z_of_nat,[t']) -> default true t' - | _ -> default false t - with e when noncritical e -> default false t - -let shrink_pair p f1 f2 = - match f1,f2 with - | Oatom v,Oatom _ -> - let r = Otimes(Oatom v,Oz two) in - clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r - | Oatom v, Otimes(_,c2) -> - let r = Otimes(Oatom v,Oplus(c2,Oz one)) in - clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zred_factor2), r - | Otimes (v1,c1),Oatom v -> - let r = Otimes(Oatom v,Oplus(c1,Oz one)) in - clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zred_factor3), r - | Otimes (Oatom v,c1),Otimes (v2,c2) -> - let r = Otimes(Oatom v,Oplus(c1,c2)) in - clever_rewrite p - [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zred_factor4),r - | t1,t2 -> - begin - oprint t1; print_newline (); oprint t2; print_newline (); - flush stdout; CErrors.user_err Pp.(str "shrink.1") - end - -let reduce_factor p = function - | Oatom v -> - let r = Otimes(Oatom v,Oz one) in - [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r - | Otimes(Oatom v,Oz n) as f -> [],f - | Otimes(Oatom v,c) -> - let rec compute = function - | Oz n -> n - | Oplus(t1,t2) -> Z.add (compute t1) (compute t2) - | _ -> CErrors.user_err Pp.(str "condense.1") - in - [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) - | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1") - -let rec condense p = function - | Oplus(f1,(Oplus(f2,r) as t)) -> - if Int.equal (weight f1) (weight f2) then begin - let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in - let assoc_tac = - clever_rewrite p - [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc) in - let tac_list,t' = condense p (Oplus(t,r)) in - (assoc_tac :: shrink_tac :: tac_list), t' - end else begin - let tac,f = reduce_factor (P_APP 1 :: p) f1 in - let tac',t' = condense (P_APP 2 :: p) t in - (tac @ tac'), Oplus(f,t') - end - | Oplus(f1,Oz n) -> - let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n) - | Oplus(f1,f2) -> - if Int.equal (weight f1) (weight f2) then begin - let tac_shrink,t = shrink_pair p f1 f2 in - let tac,t' = condense p t in - tac_shrink :: tac,t' - end else begin - let tac,f = reduce_factor (P_APP 1 :: p) f1 in - let tac',t' = condense (P_APP 2 :: p) f2 in - (tac @ tac'),Oplus(f,t') - end - | Oz _ as t -> [],t - | t -> - let tac,t' = reduce_factor p t in - let final = Oplus(t',Oz zero) in - let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in - tac @ [tac'], final - -let rec clear_zero p = function - | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero -> - let tac = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) in - let tac',t = clear_zero p r in - tac :: tac',t - | Oplus(f,r) -> - 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 - let aux2 = Id.of_string "auxiliary_2" in - let izero = mk_integer zero in - let rec loop t : unit Proofview.tactic = - match t with - | HYP e :: l -> - begin - try - tclTHEN - (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) - (loop l) - with Not_found -> loop l end - | NEGATE_CONTRADICT (e2,e1,b) :: l -> - let eq1 = decompile e1 - and eq2 = decompile e2 in - let id1 = hyp_of_tag e1.id - and id2 = hyp_of_tag e2.id in - let k = if b then negone else one in - let p_initial = [P_APP 1;P_TYPE] in - let tac= shuffle_mult_right p_initial e1.body k e2.body in - tclTHENLIST [ - generalize_tac - [mkApp (Lazy.force coq_OMEGA17, [| - val_of eq1; - val_of eq2; - mk_integer k; - mkVar id1; mkVar id2 |])]; - mk_then tac; - intro_using_then aux (fun aux -> - resolve_id aux); - reflexivity - ] - | CONTRADICTION (e1,e2) :: l -> - let eq1 = decompile e1 - and eq2 = decompile e2 in - let p_initial = [P_APP 2;P_TYPE] in - let tac = shuffle_cancel p_initial e1.body in - let solve_le = - let not_sup_sup = mkApp (Lazy.force coq_eq, - [| - Lazy.force coq_comparison; - Lazy.force coq_Gt; - Lazy.force coq_Gt |]) - in - tclTHENS - (tclTHENLIST [ - unfold sp_Zle; - simpl_in_concl; - intro; - (absurd not_sup_sup) ]) - [ assumption ; reflexivity ] - in - let theorem = - mkApp (Lazy.force coq_OMEGA2, [| - val_of eq1; val_of eq2; - mkVar (hyp_of_tag e1.id); - mkVar (hyp_of_tag e2.id) |]) - in - Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le - | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> - let id = hyp_of_tag e1.id in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in - let kk = mk_integer k - and dd = mk_integer d in - let rhs = mk_plus (mk_times eq2 kk) dd in - let state_eg = mk_eq eq1 rhs in - let tac = scalar_norm_add [P_APP 3] e2.body in - tclTHENS - (cut state_eg) - [ tclTHENS - (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)) - [ 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]); - (intro_mustbe_force id); - (loop l) ])); - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; - reflexivity ] ]; - tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] - ]; - tclTHEN (mk_then tac) reflexivity ] - - | NOT_EXACT_DIVIDE (e1,k) :: l -> - let c = floor_div e1.constant k in - let d = Z.sub e1.constant (Z.mul c k) in - let e2 = {id=e1.id; kind=EQUA;constant = c; - body = map_eq_linear (fun c -> c / k) e1.body } in - let eq2 = val_of(decompile e2) in - let kk = mk_integer k - and dd = mk_integer d in - let tac = scalar_norm_add [P_APP 2] e2.body in - tclTHENS - (cut (mk_gt dd izero)) - [ tclTHENS (cut (mk_gt kk dd)) - [ 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; - reflexivity ] ] - | EXACT_DIVIDE (e1,k) :: l -> - let id = hyp_of_tag e1.id in - let e2 = map_eq_afine (fun c -> c / k) e1 in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in - let kk = mk_integer k in - let state_eq = mk_eq eq1 (mk_times eq2 kk) in - if e1.kind == DISE then - let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS - (cut state_eq) - [ 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)) - [ 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]); - (intro_mustbe_force id); - (loop l) ])); - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ]; - tclTHEN (mk_then tac) reflexivity ] - | (MERGE_EQ(e3,e1,e2)) :: l -> - let id = new_identifier () in - tag_hypothesis id e3; - let id1 = hyp_of_tag e1.id - and id2 = hyp_of_tag e2 in - let eq1 = val_of(decompile e1) - and eq2 = val_of (decompile (negate_eq e1)) in - let tac = - clever_rewrite [P_APP 3] [[P_APP 1]] - (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: - scalar_norm [P_APP 3] e1.body - in - tclTHENS - (cut (mk_eq eq1 (mk_inv eq2))) - [ 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 -> - let id = new_identifier () - and id2 = hyp_of_tag orig.id in - tag_hypothesis id e.id; - let eq1 = val_of(decompile def) - and eq2 = val_of(decompile orig) in - let vid = unintern_id v in - let theorem = - mkApp (Lazy.force coq_ex, [| - Lazy.force coq_Z; - mkLambda - (make_annot (Name vid) Sorts.Relevant, - Lazy.force coq_Z, - mk_eq (mkRel 1) eq1) |]) - in - let mm = mk_integer m in - let p_initial = [P_APP 2;P_TYPE] in - let tac = - clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) - [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: - shuffle_mult_right p_initial - orig.body m ({c= negone;v= v}::def.body) in - tclTHENS - (cut theorem) - [ 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]); - (intro_mustbe_force id); - (loop l) ]))]; - tclTHEN (exists_tac eq1) reflexivity ] - | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> - let id1 = new_identifier () - and id2 = new_identifier () in - tag_hypothesis id1 e1; tag_hypothesis id2 e2; - let id = hyp_of_tag e.id in - let tac1 = norm_add [P_APP 2;P_TYPE] e.body in - let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in - let eq = val_of(decompile e) in - tclTHENS - (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [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; - let id1 = hyp_of_tag e1.id - and id2 = hyp_of_tag e2.id in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in - if k1 =? one && e2.kind == EQUA then - let tac_thm = - match e1.kind with - | EQUA -> Lazy.force coq_OMEGA5 - | INEQ -> Lazy.force coq_OMEGA6 - | DISE -> Lazy.force coq_OMEGA20 - in - let kk = mk_integer k2 in - let p_initial = - if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in - let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - tclTHENLIST [ - (generalize_tac - [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - mk_then tac; - (intro_mustbe_force id); - (loop l) - ] - else - let kk1 = mk_integer k1 - and kk2 = mk_integer k2 in - let p_initial = [P_APP 2;P_TYPE] in - let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - tclTHENS (cut (mk_gt kk1 izero)) - [tclTHENS - (cut (mk_gt kk2 izero)) - [ 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 -> - tclTHEN (resolve_id (hyp_of_tag e)) reflexivity - | CONSTANT_NEG(e,k) :: l -> - tclTHENLIST [ - (generalize_tac [mkVar (hyp_of_tag e)]); - unfold sp_Zle; - simpl_in_concl; - unfold sp_not; - intro_using_then aux (fun aux -> - resolve_id aux <*> reflexivity) - ] - | _ -> Proofview.tclUNIT () - in - loop - -let normalize sigma p_initial t = - let (tac,t') = transform sigma p_initial t in - let (tac',t'') = condense p_initial t' in - let (tac'',t''') = clear_zero p_initial t'' in - tac @ tac' @ tac'' , t''' - -let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = - let p_initial = [P_APP pos ;P_TYPE] in - let (tac,t') = normalize sigma p_initial t in - let shift_left = - tclTHEN - (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) - (tclTRY (clear [id])) - in - if not (List.is_empty tac) then - let id' = new_identifier () in - ((id',(tclTHENLIST [ shift_left; mk_then tac; (intro_mustbe_force id') ])) - :: tactic, - compile id' flag t' :: defs) - else - (tactic,defs) - -let destructure_omega env sigma tac_def (id,c) = - if String.equal (atompart_of_id id) "State" then - tac_def - else - try match destructurate_prop sigma c with - | Kapp(Eq,[typ;t1;t2]) - when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end -> - let t = mk_plus t1 (mk_inv t2) in - normalize_equation sigma - id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def - | Kapp(Zne,[t1;t2]) -> - let t = mk_plus t1 (mk_inv t2) in - normalize_equation sigma - id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def - | Kapp(Zle,[t1;t2]) -> - let t = mk_plus t2 (mk_inv t1) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def - | Kapp(Zlt,[t1;t2]) -> - let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def - | Kapp(Zge,[t1;t2]) -> - let t = mk_plus t1 (mk_inv t2) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def - | Kapp(Zgt,[t1;t2]) -> - let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def - | _ -> tac_def - with e when noncritical e -> tac_def - -let reintroduce id = - (* [id] cannot be cleared if dependent: protect it by a try *) - tclTHEN (tclTRY (clear [id])) (intro_using_then id (fun _ -> tclUNIT())) - -let coq_omega = - Proofview.Goal.enter begin fun gl -> - clear_constr_tables (); - let hyps_types = Tacmach.New.pf_hyps_types gl in - let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in - let tactic_normalisation, system = - List.fold_left destructure_omega ([],[]) hyps_types in - let prelude,sys = - List.fold_left - (fun (tac,sys) (t,(v,th,b)) -> - if b then - let id = new_identifier () in - let i = new_id () in - tag_hypothesis id i; - (tclTHENLIST [ - (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); - (intros_mustbe_force [v; id]); - (elim_id id); - (clear [id]); - (intros_mustbe_force [th;id]); - tac ]), - {kind = INEQ; - body = [{v=intern_id v; c=one}]; - constant = zero; id = i} :: sys - else - (tclTHENLIST [ - (simplest_elim (applist (Lazy.force coq_new_var, [t]))); - (intros_mustbe_force [v;th]); - tac ]), - sys) - (Proofview.tclUNIT (),[]) (dump_tables ()) - in - let system = system @ sys in - if !display_system_flag then display_system display_var system; - if !old_style_flag then begin - try - let _ = simplify (new_id,new_var_num,display_var) false system in - Proofview.tclUNIT () - with UNSOLVABLE -> - let _,path = depend [] [] (history ()) in - if !display_action_flag then display_action display_var path; - (tclTHEN prelude (replay_history tactic_normalisation path)) - end else begin - try - let path = simplify_strong (new_id,new_var_num,display_var) system in - if !display_action_flag then display_action display_var path; - tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION as e -> - let _, info = Exninfo.capture e in - tclZEROMSG ~info (Pp.str"Omega can't solve this system") - end - end - -let coq_omega = coq_omega - -let nat_inject = - Proofview.Goal.enter begin fun gl -> - let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in - let rec explore p t : unit Proofview.tactic = - Proofview.tclEVARMAP >>= fun sigma -> - try match destructurate_term sigma t with - | Kapp(Plus,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_plus),[t1;t2])); - (explore (P_APP 1 :: p) t1); - (explore (P_APP 2 :: p) t2) - ] - | Kapp(Mult,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_mult),[t1;t2])); - (explore (P_APP 1 :: p) t1); - (explore (P_APP 2 :: p) t2) - ] - | Kapp(Minus,[t1;t2]) -> - let id = new_identifier () in - tclTHENS - (tclTHEN - (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) - (intro_mustbe_force id)) - [ - tclTHENLIST [ - (clever_rewrite_gen p - (mk_minus (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); - (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); - (explore (P_APP 1 :: p) t1); - (explore (P_APP 2 :: p) t2) ]; - (tclTHEN - (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) - (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) - ] - | Kapp(S,[t']) -> - let rec is_number t = - try match destructurate_term sigma t with - Kapp(S,[t]) -> is_number t - | Kapp(O,[]) -> true - | _ -> false - with e when noncritical e -> false - in - let rec loop p t : unit Proofview.tactic = - try match destructurate_term sigma t with - Kapp(S,[t]) -> - (tclTHEN - (clever_rewrite_gen p - (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[t])) - (loop (P_APP 1 :: p) t)) - | _ -> explore p t - with e when noncritical e -> explore p t - in - if is_number t' then focused_simpl p else loop p t - | Kapp(Pred,[t]) -> - let t_minus_one = - mkApp (Lazy.force coq_minus, [| t; - mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in - tclTHEN - (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t])) - (explore p t_minus_one) - | Kapp(O,[]) -> focused_simpl p - | _ -> Proofview.tclUNIT () - with e when noncritical e -> Proofview.tclUNIT () - - and loop = function - | [] -> Proofview.tclUNIT () - | (i,t)::lit -> - Proofview.tclEVARMAP >>= fun sigma -> - begin try match destructurate_prop sigma t with - Kapp(Le,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Lt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Ge,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Gt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Neq,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Eq,[typ;t1;t2]) -> - if is_conv typ (Lazy.force coq_nat) then - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 2; P_TYPE] t1); - (explore [P_APP 3; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - else loop lit - | _ -> loop lit - with e when noncritical e -> loop lit end - in - let hyps_types = Tacmach.New.pf_hyps_types gl in - loop (List.rev hyps_types) - end - -let dec_binop = function - | Zne -> coq_dec_Zne - | Zle -> coq_dec_Zle - | Zlt -> coq_dec_Zlt - | Zge -> coq_dec_Zge - | Zgt -> coq_dec_Zgt - | Le -> coq_dec_le - | Lt -> coq_dec_lt - | Ge -> coq_dec_ge - | Gt -> coq_dec_gt - | _ -> raise Not_found - -let not_binop = function - | Zne -> coq_not_Zne - | Zle -> coq_Znot_le_gt - | Zlt -> coq_Znot_lt_ge - | Zge -> coq_Znot_ge_lt - | Zgt -> coq_Znot_gt_le - | Le -> coq_not_le - | Lt -> coq_not_lt - | Ge -> coq_not_ge - | Gt -> coq_not_gt - | _ -> raise Not_found - -(** A decidability check : for some [t], could we build a term - of type [decidable t] (i.e. [t\/~t]) ? Otherwise, we raise - [Undecidable]. Note that a successful check implies that - [t] has type Prop. -*) - -exception Undecidable - -let rec decidability env sigma t = - match destructurate_prop sigma t with - | Kapp(Or,[t1;t2]) -> - mkApp (Lazy.force coq_dec_or, [| t1; t2; - decidability env sigma t1; decidability env sigma t2 |]) - | Kapp(And,[t1;t2]) -> - mkApp (Lazy.force coq_dec_and, [| t1; t2; - decidability env sigma t1; decidability env sigma t2 |]) - | Kapp(Iff,[t1;t2]) -> - mkApp (Lazy.force coq_dec_iff, [| t1; t2; - decidability env sigma t1; decidability env sigma t2 |]) - | Kimp(t1,t2) -> - (* This is the only situation where it's not obvious that [t] - is in Prop. The recursive call on [t2] will ensure that. *) - mkApp (Lazy.force coq_dec_imp, - [| t1; t2; decidability env sigma t1; decidability env sigma t2 |]) - | Kapp(Not,[t1]) -> - mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |]) - | Kapp(Eq,[typ;t1;t2]) -> - begin match destructurate_type env sigma typ with - | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) - | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) - | _ -> raise Undecidable - end - | Kapp(op,[t1;t2]) -> - (try mkApp (Lazy.force (dec_binop op), [| t1; t2 |]) - with Not_found -> raise Undecidable) - | Kapp(False,[]) -> Lazy.force coq_dec_False - | Kapp(True,[]) -> Lazy.force coq_dec_True - | _ -> raise Undecidable - -let fresh_id avoid id gl = - fresh_id_in_env avoid id (Proofview.Goal.env gl) - -let onClearedName id tac = - (* We cannot ensure that hyps can be cleared (because of dependencies), *) - (* so renaming may be necessary *) - tclTHEN - (tclTRY (clear [id])) - (Proofview.Goal.enter begin fun gl -> - let id = fresh_id Id.Set.empty id gl in - tclTHEN (introduction id) (tac id) - end) - -let onClearedName2 id tac = - tclTHEN - (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.singleton id1) (add_suffix id "_right") gl in - tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] - end) - -let destructure_hyps = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let decidability = decidability env sigma in - let rec loop = function - | [] -> (tclTHEN nat_inject coq_omega) - | LocalDef (i,body,typ) :: lit when !letin_flag -> - Proofview.tclEVARMAP >>= fun sigma -> - begin - try - match destructurate_type env sigma typ with - | Kapp(Nat,_) | Kapp(Z,_) -> - let hid = fresh_id Id.Set.empty (add_suffix i.binder_name "_eqn") gl in - let hty = mk_gen_eq typ (mkVar i.binder_name) body in - tclTHEN - (assert_by (Name hid) hty reflexivity) - (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit)) - | _ -> loop lit - with e when noncritical e -> loop lit - end - | decl :: lit -> (* variable without body (or !letin_flag isn't set) *) - let i = NamedDecl.get_id decl in - Proofview.tclEVARMAP >>= fun sigma -> - begin try match destructurate_prop sigma (NamedDecl.get_type decl) with - | Kapp(False,[]) -> elim_id i - | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit - | Kapp(Or,[t1;t2]) -> - (tclTHENS - (elim_id i) - [ onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t1)::lit))); - onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t2)::lit))) ]) - | Kapp(And,[t1;t2]) -> - tclTHEN - (elim_id i) - (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (make_annot i1 Sorts.Relevant,t1) :: - LocalAssum (make_annot i2 Sorts.Relevant,t2) :: lit))) - | Kapp(Iff,[t1;t2]) -> - tclTHEN - (elim_id i) - (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (make_annot i1 Sorts.Relevant,mkArrow t1 Sorts.Relevant t2) :: - LocalAssum (make_annot i2 Sorts.Relevant,mkArrow t2 Sorts.Relevant t1) :: lit))) - | Kimp(t1,t2) -> - (* t1 and t2 might be in Type rather than Prop. - For t1, the decidability check will ensure being Prop. *) - if Termops.is_Prop sigma (Retyping.get_type_of env sigma t2) - then - let d1 = decidability t1 in - tclTHENLIST [ - (generalize_tac [mkApp (Lazy.force coq_imp_simp, - [| t1; t2; d1; mkVar i|])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) t2) :: lit)))) - ] - else - loop lit - | Kapp(Not,[t]) -> - begin match destructurate_prop sigma t with - Kapp(Or,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and (mk_not t1) (mk_not t2)) :: lit)))) - ] - | Kapp(And,[t1;t2]) -> - let d1 = decidability t1 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_and, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) (mk_not t2)) :: lit)))) - ] - | Kapp(Iff,[t1;t2]) -> - let d1 = decidability t1 in - let d2 = decidability t2 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_iff, - [| t1; t2; d1; d2; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_and t1 (mk_not t2)) - (mk_and (mk_not t1) t2)) :: lit)))) - ] - | Kimp(t1,t2) -> - (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. - For t1, being decidable implies being Prop. *) - let d1 = decidability t1 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_imp, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and t1 (mk_not t2)) :: lit)))) - ] - | Kapp(Not,[t]) -> - let d = decidability t in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t) :: lit)))) - ] - | Kapp(op,[t1;t2]) -> - (try - let thm = not_binop op in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); - (onClearedName i (fun _ -> loop lit)) - ] - with Not_found -> loop lit) - | Kapp(Eq,[typ;t1;t2]) -> - if !old_style_flag then begin - match destructurate_type env sigma typ with - | Kapp(Nat,_) -> - tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | Kapp(Z,_) -> - tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | _ -> loop lit - end else begin - match destructurate_type env sigma typ with - | Kapp(Nat,_) -> - (tclTHEN - (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) - (loop lit)) - | Kapp(Z,_) -> - (tclTHEN - (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) - (loop lit)) - | _ -> loop lit - end - | _ -> loop lit - end - | _ -> loop lit - with - | Undecidable -> loop lit - | e when noncritical e -> loop lit - end - in - let hyps = Proofview.Goal.hyps gl in - loop hyps - end - -let destructure_goal = - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let decidability = decidability env sigma in - let rec loop t = - Proofview.tclEVARMAP >>= fun sigma -> - let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in - Proofview.V82.wrap_exceptions prop >>= fun prop -> - match prop with - | Kapp(Not,[t]) -> - (tclTHEN - (tclTHEN (unfold sp_not) intro) - destructure_hyps) - | Kimp(a,b) -> (tclTHEN intro (loop b)) - | Kapp(False,[]) -> destructure_hyps - | _ -> - let goal_tac = - try - let dec = decidability t in - tclTHEN - (Proofview.Goal.enter begin fun gl -> - refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) - end) - intro - with Undecidable -> Tactics.elim_type (Lazy.force coq_False) - | e when Proofview.V82.catchable_exception e -> - let e, info = Exninfo.capture e in - Proofview.tclZERO ~info e - in - tclTHEN goal_tac destructure_hyps - in - (loop concl) - end - -let destructure_goal = destructure_goal - -let warn_omega_is_deprecated = - let name = "omega-is-deprecated" in - let category = "deprecated" in - CWarnings.create ~name ~category (fun () -> - Pp.str "omega is deprecated since 8.12; use “lia” instead.") - -let omega_solver = - Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *) - warn_omega_is_deprecated (); - Coqlib.check_required_library ["Coq";"omega";"Omega"]; - reset_all (); - destructure_goal diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli deleted file mode 100644 index e723082803..0000000000 --- a/plugins/omega/coq_omega.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -val omega_solver : unit Proofview.tactic diff --git a/plugins/omega/dune b/plugins/omega/dune index a3c9342322..e69de29bb2 100644 --- a/plugins/omega/dune +++ b/plugins/omega/dune @@ -1,7 +0,0 @@ -(library - (name omega_plugin) - (public_name coq-core.plugins.omega) - (synopsis "Coq's omega plugin") - (libraries coq-core.plugins.ltac)) - -(coq.pp (modules g_omega)) diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg deleted file mode 100644 index 888a62b2bc..0000000000 --- a/plugins/omega/g_omega.mlg +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - - -DECLARE PLUGIN "omega_plugin" - -{ - -open Ltac_plugin - -} - -TACTIC EXTEND omega -| [ "omega" ] -> { Coq_omega.omega_solver } -END diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml deleted file mode 100644 index 24cd342e42..0000000000 --- a/plugins/omega/omega.ml +++ /dev/null @@ -1,708 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(* 13/10/2002 : modified to cope with an external numbering of equations *) -(* and hypothesis. Its use for Omega is not more complex and it makes *) -(* things much simpler for the reflexive version where we should limit *) -(* the number of source of numbering. *) -(**************************************************************************) - -module type INT = sig - type bigint - val equal : bigint -> bigint -> bool - val less_than : bigint -> bigint -> bool - val add : bigint -> bigint -> bigint - val sub : bigint -> bigint -> bigint - val mult : bigint -> bigint -> bigint - val euclid : bigint -> bigint -> bigint * bigint - val neg : bigint -> bigint - val zero : bigint - val one : bigint - val to_string : bigint -> string -end - -let debug = ref false - -module MakeOmegaSolver (I:INT) = struct - -type bigint = I.bigint -let (=?) = I.equal -let (<?) = I.less_than -let (<=?) x y = I.less_than x y || x = y -let (>?) x y = I.less_than y x -let (>=?) x y = I.less_than y x || x = y -let (+) = I.add -let (-) = I.sub -let ( * ) = I.mult -let (/) x y = fst (I.euclid x y) -let (mod) x y = snd (I.euclid x y) -let zero = I.zero -let one = I.one -let two = one + one -let negone = I.neg one -let abs x = if I.less_than x zero then I.neg x else x -let string_of_bigint = I.to_string -let neg = I.neg - -(* To ensure that polymorphic (<) is not used mistakenly on big integers *) -(* Warning: do not use (=) either on big int *) -let (<) = ((<) : int -> int -> bool) -let (>) = ((>) : int -> int -> bool) -let (<=) = ((<=) : int -> int -> bool) -let (>=) = ((>=) : int -> int -> bool) - -let pp i = print_int i; print_newline (); flush stdout - -let push v l = l := v :: !l - -let rec pgcd x y = if y =? zero then x else pgcd y (x mod y) - -let pgcd_l = function - | [] -> failwith "pgcd_l" - | x :: l -> List.fold_left pgcd x l - -let floor_div a b = - match a >=? zero , b >? zero with - | true,true -> a / b - | false,false -> a / b - | true, false -> (a-one) / b - one - | false,true -> (a+one) / b - one - -type coeff = {c: bigint ; v: int} - -type linear = coeff list - -type eqn_kind = EQUA | INEQ | DISE - -type afine = { - (* a number uniquely identifying the equation *) - id: int ; - (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *) - kind: eqn_kind; - (* the variables and their coefficient *) - body: coeff list; - (* a constant *) - constant: bigint } - -type state_action = { - st_new_eq : afine; - st_def : afine; (* /!\ this represents [st_def = st_var] *) - st_orig : afine; - st_coef : bigint; - st_var : int } - -type action = - | DIVIDE_AND_APPROX of afine * afine * bigint * bigint - | NOT_EXACT_DIVIDE of afine * bigint - | FORGET_C of int - | EXACT_DIVIDE of afine * bigint - | SUM of int * (bigint * afine) * (bigint * afine) - | STATE of state_action - | HYP of afine - | FORGET of int * int - | FORGET_I of int * int - | CONTRADICTION of afine * afine - | NEGATE_CONTRADICT of afine * afine * bool - | MERGE_EQ of int * afine * int - | CONSTANT_NOT_NUL of int * bigint - | CONSTANT_NUL of int - | CONSTANT_NEG of int * bigint - | SPLIT_INEQ of afine * (int * action list) * (int * action list) - | WEAKEN of int * bigint - -exception UNSOLVABLE - -exception NO_CONTRADICTION - -let display_eq print_var (l,e) = - let _ = - List.fold_left - (fun not_first f -> - print_string - (if f.c <? zero then "- " else if not_first then "+ " else ""); - let c = abs f.c in - if c =? one then - Printf.printf "%s " (print_var f.v) - else - Printf.printf "%s %s " (string_of_bigint c) (print_var f.v); - true) - false l - in - if e >? zero then - Printf.printf "+ %s " (string_of_bigint e) - else if e <? zero then - Printf.printf "- %s " (string_of_bigint (abs e)) - -let rec trace_length l = - let action_length accu = function - | SPLIT_INEQ (_,(_,l1),(_,l2)) -> - accu + one + trace_length l1 + trace_length l2 - | _ -> accu + one in - List.fold_left action_length zero l - -let operator_of_eq = function - | EQUA -> "=" | DISE -> "!=" | INEQ -> ">=" - -let kind_of = function - | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation" - -let display_system print_var l = - List.iter - (fun { kind=b; body=e; constant=c; id=id} -> - Printf.printf "E%d: " id; - display_eq print_var (e,c); - Printf.printf "%s 0\n" (operator_of_eq b)) - l; - print_string "------------------------\n\n" - -let display_inequations print_var l = - List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l; - print_string "------------------------\n\n" - -let sbi = string_of_bigint - -let rec display_action print_var = function - | act :: l -> begin match act with - | DIVIDE_AND_APPROX (e1,e2,k,d) -> - Printf.printf - "Inequation E%d is divided by %s and the constant coefficient is \ - rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) - | NOT_EXACT_DIVIDE (e,k) -> - Printf.printf - "Constant in equation E%d is not divisible by the pgcd \ - %s of its other coefficients.\n" e.id (sbi k) - | EXACT_DIVIDE (e,k) -> - Printf.printf - "Equation E%d is divided by the pgcd \ - %s of its coefficients.\n" e.id (sbi k) - | WEAKEN (e,k) -> - Printf.printf - "To ensure a solution in the dark shadow \ - the equation E%d is weakened by %s.\n" e (sbi k) - | SUM (e,(c1,e1),(c2,e2)) -> - Printf.printf - "We state %s E%d = %s %s E%d + %s %s E%d.\n" - (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2) - (kind_of e2.kind) e2.id - | STATE { st_new_eq = e } -> - Printf.printf "We define a new equation E%d: " e.id; - display_eq print_var (e.body,e.constant); - print_string (operator_of_eq e.kind); print_string " 0" - | HYP e -> - Printf.printf "We define E%d: " e.id; - display_eq print_var (e.body,e.constant); - print_string (operator_of_eq e.kind); print_string " 0\n" - | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e - | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 - | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 - | MERGE_EQ (e,e1,e2) -> - Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e - | CONTRADICTION (e1,e2) -> - Printf.printf - "Equations E%d and E%d imply a contradiction on their \ - constant factors.\n" e1.id e2.id - | NEGATE_CONTRADICT(e1,e2,b) -> - Printf.printf - "Equations E%d and E%d state that their body is at the same time \ - equal and different\n" e1.id e2.id - | CONSTANT_NOT_NUL (e,k) -> - Printf.printf "Equation E%d states %s = 0.\n" e (sbi k) - | CONSTANT_NEG(e,k) -> - Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k) - | CONSTANT_NUL e -> - Printf.printf "Inequation E%d states 0 != 0.\n" e - | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> - Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2; - display_action print_var l1; - print_newline (); - display_action print_var l2; - print_newline () - end; display_action print_var l - | [] -> - flush stdout - -let default_print_var v = Printf.sprintf "X%d" v (* For debugging *) - -(*""*) -let add_event, history, clear_history = - let accu = ref [] in - (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu), - (fun () -> !accu), - (fun () -> accu := []) - -let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v) - -let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) - -let map_eq_linear f = - let rec loop = function - | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l - | [] -> [] - in - loop - -let map_eq_afine f e = - { id = e.id; kind = e.kind; body = map_eq_linear f e.body; - constant = f e.constant } - -let negate_eq = map_eq_afine (fun x -> neg x) - -let rec sum p0 p1 = match (p0,p1) with - | ([], l) -> l | (l, []) -> l - | (((x1::l1) as l1'), ((x2::l2) as l2')) -> - if x1.v = x2.v then - let c = x1.c + x2.c in - if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2 - else if x1.v > x2.v then - x1 :: sum l1 l2' - else - x2 :: sum l1' l2 - -let sum_afine new_eq_id eq1 eq2 = - { kind = eq1.kind; id = new_eq_id (); - body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant } - -exception FACTOR1 - -let rec chop_factor_1 = function - | x :: l -> - if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l') - | [] -> raise FACTOR1 - -exception CHOPVAR - -let rec chop_var v = function - | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l') - | [] -> raise CHOPVAR - -let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = - if e = [] then begin - match eq_flag with - | EQUA -> - if x =? zero then [] else begin - add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE - end - | DISE -> - if x <> zero then [] else begin - add_event (CONSTANT_NUL id); raise UNSOLVABLE - end - | INEQ -> - if x >=? zero then [] else begin - add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE - end - end else - let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in - if eq_flag=EQUA && x mod gcd <> zero then begin - add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE - end else if eq_flag=DISE && x mod gcd <> zero then begin - add_event (FORGET_C eq.id); [] - end else if gcd <> one then begin - let c = floor_div x gcd in - let d = x - c * gcd in - let new_eq = {id=id; kind=eq_flag; constant=c; - body=map_eq_linear (fun c -> c / gcd) e} in - add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd) - else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); - [new_eq] - end else [eq] - -let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2 - ({body=e1; constant=c1} as eq1) = - try - let (f,_) = chop_var v e1 in - let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c - else failwith "eliminate_with_in" in - let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in - add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res - with CHOPVAR -> eq1 - -let omega_mod a b = a - b * floor_div (two * a + b) (two * b) -let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = - let e = original.body in - let sigma = new_var_id () in - if e == [] then begin - display_system print_var [original] ; failwith "TL" - end; - let smallest,var = - List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) - (abs (List.hd e).c, (List.hd e).v) (List.tl e) - in - let m = smallest + one in - let new_eq = - { constant = omega_mod original.constant m; - body = {c= neg m;v=sigma} :: - map_eq_linear (fun a -> omega_mod a m) original.body; - id = new_eq_id (); kind = EQUA } in - let definition = - { constant = neg (floor_div (two * original.constant + m) (two * m)); - body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m))) - original.body; - id = new_eq_id (); kind = EQUA } in - add_event (STATE {st_new_eq = new_eq; st_def = definition; - st_orig = original; st_coef = m; st_var = sigma}); - let new_eq = List.hd (normalize new_eq) in - let eliminated_var, def = chop_var var new_eq.body in - let other_equations = - Util.List.map_append - (fun e -> - normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in - let inequations = - Util.List.map_append - (fun e -> - normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in - let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in - let mod_original = map_eq_afine (fun c -> c / m) original' in - add_event (EXACT_DIVIDE (original',m)); - List.hd (normalize mod_original),other_equations,inequations - -let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = - if !debug then display_system print_var (e::other); - try - let v,def = chop_factor_1 e.body in - (Util.List.map_append - (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other, - Util.List.map_append - (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs) - with FACTOR1 -> - eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs) - -let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) = - let rec fst_eq_1 = function - (eq::l) -> - if List.exists (fun x -> abs x.c =? one) eq.body then eq,l - else let (eq',l') = fst_eq_1 l in (eq',eq::l') - | [] -> raise Not_found in - match sys_eq with - [] -> if !debug then display_system print_var sys_ineq; sys_ineq - | (e1::rest) -> - let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in - if eq.body = [] then - if eq.constant =? zero then begin - add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq) - end else begin - add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE - end - else - banerjee new_ids - (eliminate_one_equation new_ids (eq,other,sys_ineq)) - -type kind = INVERTED | NORMAL - -let redundancy_elimination new_eq_id system = - let normal = function - ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED - | e -> e,NORMAL in - let table = Hashtbl.create 7 in - List.iter - (fun e -> - let ({body=ne} as nx) ,kind = normal e in - if ne = [] then - if nx.constant <? zero then begin - add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE - end else add_event (FORGET_C nx.id) - else - try - let (optnormal,optinvert) = Hashtbl.find table ne in - let final = - if kind = NORMAL then begin - match optnormal with - Some v -> - let kept = - if v.constant <? nx.constant - then begin add_event (FORGET (v.id,nx.id));v end - else begin add_event (FORGET (nx.id,v.id));nx end in - (Some(kept),optinvert) - | None -> Some nx,optinvert - end else begin - match optinvert with - Some v -> - let _kept = - if v.constant >? nx.constant - then begin add_event (FORGET_I (v.id,nx.id));v end - else begin add_event (FORGET_I (nx.id,v.id));nx end in - (optnormal,Some(if v.constant >? nx.constant then v else nx)) - | None -> optnormal,Some nx - end in - begin match final with - (Some high, Some low) -> - if high.constant <? low.constant then begin - add_event(CONTRADICTION (high,negate_eq low)); - raise UNSOLVABLE - end - | _ -> () end; - Hashtbl.remove table ne; - Hashtbl.add table ne final - with Not_found -> - Hashtbl.add table ne - (if kind = NORMAL then (Some nx,None) else (None,Some nx))) - system; - let accu_eq = ref [] in - let accu_ineq = ref [] in - Hashtbl.iter - (fun p0 p1 -> match (p0,p1) with - | (e, (Some x, Some y)) when x.constant =? y.constant -> - let id=new_eq_id () in - add_event (MERGE_EQ(id,x,y.id)); - push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq - | (e, (optnorm,optinvert)) -> - begin match optnorm with - Some x -> push x accu_ineq | _ -> () end; - begin match optinvert with - Some x -> push (negate_eq x) accu_ineq | _ -> () end) - table; - !accu_eq,!accu_ineq - -exception SOLVED_SYSTEM - -let select_variable system = - let table = Hashtbl.create 7 in - let push v c= - try let r = Hashtbl.find table v in r := max !r (abs c) - with Not_found -> Hashtbl.add table v (ref (abs c)) in - List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system; - let vmin,cmin = ref (-1), ref zero in - let var_cpt = ref 0 in - Hashtbl.iter - (fun v ({contents = c}) -> - incr var_cpt; - if c <? !cmin || !vmin = (-1) then begin vmin := v; cmin := c end) - table; - if !var_cpt < 1 then raise SOLVED_SYSTEM; - !vmin - -let classify v system = - List.fold_left - (fun (not_occ,below,over) eq -> - try let f,eq' = chop_var v eq.body in - if f.c >=? zero then (not_occ,((f.c,eq) :: below),over) - else (not_occ,below,((neg f.c,eq) :: over)) - with CHOPVAR -> (eq::not_occ,below,over)) - ([],[],[]) system - -let product new_eq_id dark_shadow low high = - List.fold_left - (fun accu (a,eq1) -> - List.fold_left - (fun accu (b,eq2) -> - let eq = - sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1) - (map_eq_afine (fun c -> c * a) eq2) in - add_event(SUM(eq.id,(b,eq1),(a,eq2))); - match normalize eq with - | [eq] -> - let final_eq = - if dark_shadow then - let delta = (a - one) * (b - one) in - add_event(WEAKEN(eq.id,delta)); - {id = eq.id; kind=INEQ; body = eq.body; - constant = eq.constant - delta} - else eq - in final_eq :: accu - | (e::_) -> failwith "Product dardk" - | [] -> accu) - accu high) - [] low - -let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system = - let v = select_variable system in - let (ineq_out, ineq_low,ineq_high) = classify v system in - let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in - if !debug then display_system print_var expanded; expanded - -let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = - if List.exists (fun e -> e.kind = DISE) system then - failwith "disequation in simplify"; - clear_history (); - List.iter (fun e -> add_event (HYP e)) system; - let system = Util.List.map_append normalize system in - let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in - let system = (eqs @ simp_eq,simp_ineq) in - let rec loop1a system = - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq - and loop1b sys_ineq = - let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in - if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) - in - let rec loop2 system = - try - let expanded = fourier_motzkin new_ids dark_shadow system in - loop2 (loop1b expanded) - with SOLVED_SYSTEM -> - if !debug then display_system print_var system; system - in - loop2 (loop1a system) - -let rec depend relie_on accu = function - | act :: l -> - begin match act with - | DIVIDE_AND_APPROX (e,_,_,_) -> - if Int.List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | EXACT_DIVIDE (e,_) -> - if Int.List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | WEAKEN (e,_) -> - if Int.List.mem e relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | SUM (e,(_,e1),(_,e2)) -> - if Int.List.mem e relie_on then - depend (e1.id::e2.id::relie_on) (act::accu) l - else - depend relie_on accu l - | STATE {st_new_eq=e;st_orig=o} -> - if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l - else depend relie_on accu l - | HYP e -> - if Int.List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | FORGET_C _ -> depend relie_on accu l - | FORGET _ -> depend relie_on accu l - | FORGET_I _ -> depend relie_on accu l - | MERGE_EQ (e,e1,e2) -> - if Int.List.mem e relie_on then - depend (e1.id::e2::relie_on) (act::accu) l - else - depend relie_on accu l - | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l - | CONTRADICTION (e1,e2) -> - depend (e1.id::e2.id::relie_on) (act::accu) l - | CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l - | CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l - | CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l - | NEGATE_CONTRADICT (e1,e2,_) -> - depend (e1.id::e2.id::relie_on) (act::accu) l - | SPLIT_INEQ _ -> failwith "depend" - end - | [] -> relie_on, accu - -let negation (eqs,ineqs) = - let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in - let normal = function - | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED - | e -> e,NORMAL in - let table = Hashtbl.create 7 in - List.iter (fun e -> - let {body=ne;constant=c} ,kind = normal e in - Hashtbl.add table (ne,c) (kind,e)) diseq; - List.iter (fun e -> - assert (e.kind = EQUA); - let {body=ne;constant=c},kind = normal e in - try - let (kind',e') = Hashtbl.find table (ne,c) in - add_event (NEGATE_CONTRADICT (e,e',kind=kind')); - raise UNSOLVABLE - with Not_found -> ()) eqs - -exception FULL_SOLUTION of action list * int list - -let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = - clear_history (); - List.iter (fun e -> add_event (HYP e)) system; - (* Initial simplification phase *) - let rec loop1a system = - negation system; - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq - and loop1b sys_ineq = - let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in - if simp_eq = [] then dise @ simp_ineq - else loop1a (simp_eq,dise @ simp_ineq) - in - let rec loop2 system = - try - let expanded = fourier_motzkin new_ids false system in - loop2 (loop1b expanded) - with SOLVED_SYSTEM -> if !debug then display_system print_var system; system - in - let rec explode_diseq = function - | (de::diseq,ineqs,expl_map) -> - let id1 = new_eq_id () - and id2 = new_eq_id () in - let e1 = - {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in - let e2 = - {id = id2; kind=INEQ; body = map_eq_linear neg de.body; - constant = neg de.constant - one} in - let new_sys = - List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) - ineqs @ - List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) - ineqs - in - explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map) - | ([],ineqs,expl_map) -> ineqs,expl_map - in - try - let system = Util.List.map_append normalize system in - let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in - let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in - let system = (eqs @ simp_eq,simp_ineq @ dise) in - let system' = loop1a system in - let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in - let first_segment = history () in - let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in - let all_solutions = - List.map - (fun (decomp,sys) -> - clear_history (); - try let _ = loop2 sys in raise NO_CONTRADICTION - with UNSOLVABLE -> - let relie_on,path = depend [] [] (history ()) in - let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in - let red = List.map (fun (x,_,_) -> x) dc in - (red,relie_on,decomp,path)) - sys_exploded - in - let max_count sys = - let tbl = Hashtbl.create 7 in - let augment x = - try incr (Hashtbl.find tbl x) - with Not_found -> Hashtbl.add tbl x (ref 1) in - let eq = ref (-1) and c = ref 0 in - List.iter (function - | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on)) - | (l,_,_,_) -> List.iter augment l) sys; - Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl; - !eq - in - let rec solve systems = - try - let id = max_count systems in - let rec sign = function - | ((id',_,b)::l) -> if id=id' then b else sign l - | [] -> failwith "solve" in - let s1,s2 = - List.partition (fun (_,_,decomp,_) -> sign decomp) systems in - let remove_int (dep,ro,dc,pa) = - (Util.List.except Int.equal id dep,ro,dc,pa) - in - let s1' = List.map remove_int s1 in - let s2' = List.map remove_int s2 in - let (r1,relie1) = solve s1' - and (r2,relie2) = solve s2' in - let (eq,id1,id2) = Int.List.assoc id explode_map in - [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], - eq.id :: Util.List.union Int.equal relie1 relie2 - with FULL_SOLUTION (x0,x1) -> (x0,x1) - in - let act,relie_on = solve all_solutions in - snd(depend relie_on act first_segment) - with UNSOLVABLE -> snd (depend [] [] (history ())) - -end diff --git a/plugins/omega/omega_plugin.mlpack b/plugins/omega/omega_plugin.mlpack deleted file mode 100644 index df7f1047f2..0000000000 --- a/plugins/omega/omega_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Omega -Coq_omega -G_omega diff --git a/test-suite/bugs/closed/bug_1362.v b/test-suite/bugs/closed/bug_1362.v index 6cafb9f0cd..18b8d743b3 100644 --- a/test-suite/bugs/closed/bug_1362.v +++ b/test-suite/bugs/closed/bug_1362.v @@ -1,26 +1,17 @@ (** Omega is now aware of the bodies of context variables (of type Z or nat). *) -Require Import ZArith Omega. +Require Import ZArith Lia. Open Scope Z. Goal let x := 3 in x = 3. intros. -omega. +lia. Qed. Open Scope nat. Goal let x := 2 in x = 2. intros. -omega. +lia. Qed. - -(** NB: this could be disabled for compatibility reasons *) - -Unset Omega UseLocalDefs. - -Goal let x := 4 in x = 4. -intros. -Fail omega. -Abort. diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v index 0228abbb9b..9f6c8177f6 100644 --- a/test-suite/bugs/closed/bug_1912.v +++ b/test-suite/bugs/closed/bug_1912.v @@ -1,6 +1,6 @@ -Require Import Omega. +Require Import Lia ZArith. Goal forall x, Z.succ (Z.pred x) = x. intros x. -omega. +lia. Qed. diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v index 67ecc3087f..2ebbb66758 100644 --- a/test-suite/bugs/closed/bug_4132.v +++ b/test-suite/bugs/closed/bug_4132.v @@ -1,5 +1,5 @@ -Require Import ZArith Omega. +Require Import ZArith Lia. Open Scope Z_scope. (** bug 4132: omega was using "simpl" either on whole equations, or on @@ -14,18 +14,18 @@ Lemma foo (H : - zxy' <= zxy) (H' : zxy' <= x') : - b <= zxy. Proof. -omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) Qed. Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. -omega. (* Pierre L: according to a comment of bug report #4132, +lia. (* Pierre L: according to a comment of bug report #4132, this might have triggered "index out of bounds" in the past, but I never managed to reproduce that in any version, even before my fix. *) Qed. Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. -omega. (* Pierre L: according to a comment of bug report #4132, +lia. (* Pierre L: according to a comment of bug report #4132, this might have triggered "Failure(occurrence 2)" in the past, but I never managed to reproduce that. *) Qed. diff --git a/test-suite/bugs/closed/bug_4717.v b/test-suite/bugs/closed/bug_4717.v index bd9bac37ef..81bc70d076 100644 --- a/test-suite/bugs/closed/bug_4717.v +++ b/test-suite/bugs/closed/bug_4717.v @@ -1,6 +1,6 @@ (* Omega being smarter on recognizing nat and Z *) -Require Import Omega. +Require Import Lia ZArith. Definition nat' := nat. @@ -10,13 +10,13 @@ Theorem le_not_eq_lt : forall (n m:nat), n < m. Proof. intros. - omega. + lia. Qed. Goal forall (x n : nat'), x = x + n - n. Proof. intros. - omega. + lia. Qed. Open Scope Z_scope. @@ -29,5 +29,5 @@ Theorem Zle_not_eq_lt : forall n m, n < m. Proof. intros. - omega. + lia. Qed. diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v index bad9d64f65..f42e32cf25 100644 --- a/test-suite/bugs/closed/bug_9512.v +++ b/test-suite/bugs/closed/bug_9512.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia. +Require Import Coq.ZArith.BinInt Coq.micromega.Lia. Set Primitive Projections. Record params := { width : Z }. @@ -10,7 +10,6 @@ Set Printing All. Lemma foo : width p = 0%Z -> width p = 0%Z. intros. - assert_succeeds (enough True; [omega|]). assert_succeeds (enough True; [lia|]). (* H : @eq Z (width p) Z0 *) @@ -26,12 +25,6 @@ Lemma foo : width p = 0%Z -> width p = 0%Z. (* @eq Z (width p) Z0 *) assert_succeeds (enough True; [lia|]). - (* Tactic failure: <tactic closure> fails. *) - (* assert_succeeds (enough True; [omega|]). *) - (* Tactic failure: <tactic closure> fails. *) - - (* omega. *) - (* Error: Omega can't solve this system *) lia. (* Tactic failure: Cannot find witness. *) diff --git a/test-suite/bugs/opened/bug_1615.v b/test-suite/bugs/opened/bug_1615.v deleted file mode 100644 index c045335410..0000000000 --- a/test-suite/bugs/opened/bug_1615.v +++ /dev/null @@ -1,11 +0,0 @@ -Require Import Omega. - -Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z. -Proof. - intros. omega. -Qed. - -Lemma foo' : forall n m : nat, n <= n + n * m. -Proof. - intros. Fail omega. -Abort. diff --git a/test-suite/bugs/opened/bug_6602.v b/test-suite/bugs/opened/bug_6602.v deleted file mode 100644 index 3690adf90a..0000000000 --- a/test-suite/bugs/opened/bug_6602.v +++ /dev/null @@ -1,17 +0,0 @@ -Require Import Omega. - -Lemma test_nat: - forall n, (5 + pred n <= 5 + n). -Proof. - intros. - zify. - omega. -Qed. - -Lemma test_N: - forall n, (5 + N.pred n <= 5 + n)%N. -Proof. - intros. - zify. - omega. -Qed. diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index d2e6794c0b..1f4913b49d 100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v @@ -140,35 +140,35 @@ Qed. Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0. Proof. intros. - omega. + lia. Qed. Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0. Proof. intros. - omega. + lia. Qed. Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n). Proof. intros. - omega. + lia. Qed. Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0. Proof. - intros; omega. + intros; lia. Qed. Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0. Proof. - intros; omega. + intros; lia. Qed. Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n. Proof. intros. - omega. + lia. Qed. @@ -1414,13 +1414,13 @@ Qed. Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n. Proof. intros. - omega. + lia. Qed. Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n. Proof. intros. - omega. + lia. Qed. @@ -1501,7 +1501,7 @@ Proof. [ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1)); [ idtac | apply f_equal with Z; auto with zarith ]; rewrite absolu_plus; - [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega + [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; lia | auto with zarith | intro; discriminate ] | rewrite <- H1; reflexivity ]. diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 69ed621877..ae71ddfd1d 100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v @@ -19,6 +19,7 @@ Require Export ZArith. Require Export ZArithRing. +Require Import Lia. Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d. @@ -140,35 +141,35 @@ Qed. Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0. Proof. intros. - omega. + lia. Qed. Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0. Proof. intros. - omega. + lia. Qed. Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n). Proof. intros. - omega. + lia. Qed. Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0. Proof. - intros; omega. + intros; lia. Qed. Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0. Proof. - intros; omega. + intros; lia. Qed. Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n. Proof. intros. - omega. + lia. Qed. @@ -573,7 +574,7 @@ Qed. -Hint Resolve Zmult_pos_pos Zmult_neg_neg Zmult_neg_pos Zmult_pos_neg: zarith. +Local Hint Resolve Zmult_pos_pos Zmult_neg_neg Zmult_neg_pos Zmult_pos_neg: zarith. Lemma Zle_reg_mult_l : @@ -1158,7 +1159,7 @@ Proof. intros [| p| p]; intros; [ Falsum | constructor | constructor ]. Qed. -Hint Resolve square_pos: zarith. +Local Hint Resolve square_pos: zarith. (*###########################################################################*) (** Properties of positive numbers, mapping between Z and nat *) @@ -1414,13 +1415,13 @@ Qed. Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n. Proof. intros. - omega. + lia. Qed. Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n. Proof. intros. - omega. + lia. Qed. @@ -1501,7 +1502,7 @@ Proof. [ replace (Z.abs_nat x) with (Z.abs_nat (x - 1 + 1)); [ idtac | apply f_equal with Z; auto with zarith ]; rewrite absolu_plus; - [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; omega + [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; lia | auto with zarith | intro; discriminate ] | rewrite <- H1; reflexivity ]. @@ -1985,7 +1986,7 @@ Proof. intros [| p| p] Hp; trivial. Qed. -Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8 +Local Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8 Zsgn_9 Zsgn_10 Zsgn_11 Zsgn_12 Zsgn_13 Zsgn_14 Zsgn_15 Zsgn_16 Zsgn_17 Zsgn_18 Zsgn_19 Zsgn_20 Zsgn_21 Zsgn_22 Zsgn_23 Zsgn_24 Zsgn_25 Zsgn_26 Zsgn_27: zarith. @@ -2388,7 +2389,7 @@ Proof. intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos. Qed. -Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9 +Local Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9 Zabs_10 Zabs_11 Zabs_12 Zabs_min Zabs_neg Zabs_mult Zabs_plus Zle_Zabs: zarith. @@ -2949,7 +2950,7 @@ Proof. ring. Qed. -Hint Resolve ZmaxSS Zle_max_r Zle_max_l Zmax_n_n: zarith. +Local Hint Resolve ZmaxSS Zle_max_r Zle_max_l Zmax_n_n: zarith. (*###########################################################################*) (** Properties of Arity *) @@ -3020,7 +3021,7 @@ Proof. Flip. Qed. -Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith. +Local Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith. (*###########################################################################*) (** Properties of Zpower *) @@ -3038,4 +3039,4 @@ Proof. ring. Qed. -Hint Resolve Zpower_1 Zpower_2: zarith. +Local Hint Resolve Zpower_1 Zpower_2: zarith. diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index d52a853aae..24634bd321 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,6 +1,6 @@ (* Cf BZ#546 *) -Require Import Omega. +Require Import Lia. Section S. @@ -19,7 +19,7 @@ induction n. replace (2 * S n0) with (2*n0 + 2) ; auto with arith. apply DummyApp. 2:exact Dummy2. - apply IHn0 ; abstract omega. + apply IHn0 ; abstract lia. Defined. End S. diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 5e0f90d59b..bbdf9762a3 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,5 +1,5 @@ -Require Import Omega. +Require Import Lia ZArith. (* Submitted by Xavier Urbain 18 Jan 2002 *) @@ -7,14 +7,14 @@ Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. - omega. + lia. Qed. (* Proposed by Pierre Crégut *) Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. intro. - omega. + lia. Qed. (* Proposed by Jean-Christophe Filliâtre *) @@ -22,7 +22,7 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. - omega. + lia. Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) @@ -32,7 +32,7 @@ Section A. Variable x y : Z. Hypothesis H : (x > y)%Z. Lemma lem4 : (x > y)%Z. - omega. + lia. Qed. End A. @@ -48,7 +48,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1. Hypothesis M : (H <= 2 * S)%Z. Hypothesis N : (S < H)%Z. Lemma lem5 : (H > 0)%Z. - omega. + lia. Qed. End B. @@ -56,11 +56,11 @@ End B. Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. - omega. + lia. Qed. (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) -Require Import Omega. +Require Import Lia. Section C. Parameter g : forall m : nat, m <> 0 -> Prop. Parameter f : forall (m : nat) (H : m <> 0), g m H. @@ -68,21 +68,21 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - omega. + lia. Qed. End C. (* Problem of dependencies *) -Require Import Omega. +Require Import Lia. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. -intros; omega. +intros; lia. Qed. (* Bug that what caused by the use of intro_using in Omega *) -Require Import Omega. +Require Import Lia. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. -intros; omega. +intros; lia. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) @@ -90,5 +90,5 @@ Qed. (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. -intros; zify; omega. +intros; lia. Qed. diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index 6fd936935c..6ce7264b7a 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -1,4 +1,4 @@ -Require Import ZArith Omega. +Require Import ZArith Lia. Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) @@ -8,7 +8,7 @@ Lemma test_romega_0 : 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. -omega. +lia. Qed. Lemma test_romega_0b : @@ -16,7 +16,7 @@ Lemma test_romega_0b : 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. -omega. +lia. Qed. Lemma test_romega_1 : @@ -29,7 +29,7 @@ Lemma test_romega_1 : z >= 0. Proof. intros. -omega. +lia. Qed. Lemma test_romega_1b : @@ -42,21 +42,21 @@ Lemma test_romega_1b : z >= 0. Proof. intros z z1 z2. -omega. +lia. Qed. Lemma test_romega_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. -omega. +lia. Qed. Lemma test_romega_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. -omega. +lia. Qed. Lemma test_romega_3 : forall a b h hl hr ha hb, @@ -70,7 +70,7 @@ Lemma test_romega_3 : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros. -omega. +lia. Qed. Lemma test_romega_3b : forall a b h hl hr ha hb, @@ -84,7 +84,7 @@ Lemma test_romega_3b : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros a b h hl hr ha hb. -omega. +lia. Qed. @@ -94,7 +94,7 @@ Lemma test_romega_4 : forall hr ha, hr = 0. Proof. intros hr ha. -omega. +lia. Qed. Lemma test_romega_5 : forall hr ha, @@ -103,45 +103,45 @@ Lemma test_romega_5 : forall hr ha, hr = 0. Proof. intros hr ha. -omega. +lia. Qed. Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False. Proof. intros. -omega. +lia. Qed. Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False. Proof. intros z. -omega. +lia. Qed. Lemma test_romega_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -omega. +lia. Qed. Lemma test_romega_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -omega. +lia. Qed. (* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros. -omega. +lia. Qed. Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros x y. -omega. +lia. Qed. diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v index 4e726335c9..b2eef5bcd5 100644 --- a/test-suite/success/Omega2.v +++ b/test-suite/success/Omega2.v @@ -1,4 +1,4 @@ -Require Import ZArith Omega. +Require Import ZArith Lia. (* Submitted by Yegor Bryukhov (BZ#922) *) @@ -23,6 +23,6 @@ forall v1 v2 v3 v4 v5 : Z, ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9)) -> False. intros. -omega. +lia. Qed. diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index 0223255067..32bc99621a 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -1,4 +1,4 @@ -Require Import ZArith Nnat Omega. +Require Import ZArith Nnat Lia. Open Scope Z_scope. (** Test of the zify preprocessor for (R)Omega *) @@ -16,112 +16,111 @@ Open Scope Z_scope. Goal forall a:Z, Z.max a a = a. intros. -zify; omega. +lia. Qed. Goal forall a b:Z, Z.max a b = Z.max b a. intros. -zify; omega. +lia. Qed. Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. -zify; omega. +lia. Qed. Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. -zify; omega. +lia. Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. -zify. -intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *) +intuition; subst; lia. Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. intros. -zify; omega. +lia. Qed. Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. -zify; omega. +lia. Qed. (* zify_nat *) Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. intros. -zify; omega. +lia. Qed. Goal forall m:nat, (m<1)%nat -> (m=0)%nat. intros. -zify; omega. +lia. Qed. Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. intros. -zify; omega. +lia. Qed. (* 2000 instead of 200: works, but quite slow *) Goal forall m: nat, (m*m>=0)%nat. intros. -zify; omega. +lia. Qed. (* zify_positive *) Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. intros. -zify; omega. +lia. Qed. Goal forall m:positive, (m<2)%positive -> (m=1)%positive. intros. -zify; omega. +lia. Qed. Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. intros. -zify; omega. +lia. Qed. Goal forall m: positive, (m*m>=1)%positive. intros. -zify; omega. +lia. Qed. (* zify_N *) Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. intros. -zify; omega. +lia. Qed. Goal forall m:N, (m<1)%N -> (m=0)%N. intros. -zify; omega. +lia. Qed. Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. intros. -zify; omega. +lia. Qed. Goal forall m:N, (m*m>=0)%N. intros. -zify; omega. +lia. Qed. (* mix of datatypes *) Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. -zify; omega. +lia. Qed. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 02adb012d9..ef8617cd9e 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -85,19 +85,19 @@ Time Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) error end. -Require Import Omega Setoid. +Require Import Lia Setoid. Next Obligation. intros ; simpl in *. apply H. - simpl in * ; omega. + simpl in * ; lia. Qed. Next Obligation. simpl in *; intros. revert H0 ; clear_subset_proofs. intros. - case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst. + case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by lia. subst. revert H0 ; clear_subset_proofs ; tauto. - apply H. simpl. omega. + apply H. simpl. lia. Qed. Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v index 6ca32f450f..c0e86b00dd 100644 --- a/test-suite/success/ROmegaPre.v +++ b/test-suite/success/ROmegaPre.v @@ -32,8 +32,7 @@ Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. -zify. -intuition; subst; lia. (* pure multiplication: omega alone can't do it *) +intuition; subst; lia. Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index ff34840d83..b7d5276bc8 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -61,7 +61,7 @@ Qed. (* Check mutually inductive statements *) -Require Import ZArith_base Omega. +Require Import ZArith_base Lia. Open Scope Z_scope. Inductive even: Z -> Prop := @@ -75,13 +75,13 @@ with odd_pos_even_pos : forall n, odd n -> n >= 1. Proof. intros. destruct H. - omega. + lia. apply odd_pos_even_pos in H. - omega. + lia. intros. destruct H. apply even_pos_odd_pos in H. - omega. + lia. Qed. CoInductive a : Prop := acons : b -> a diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index 5638a7d3eb..06847f4f96 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -23,7 +23,7 @@ Qed. Print Equivalent Keys. End foo. -Require Import Arith List Omega. +Require Import Arith List. Definition G {A} (f : A -> A -> A) (x : A) := f x x. diff --git a/test-suite/success/rewrite_iterated.v b/test-suite/success/rewrite_iterated.v index 962dada35a..946011e393 100644 --- a/test-suite/success/rewrite_iterated.v +++ b/test-suite/success/rewrite_iterated.v @@ -1,8 +1,8 @@ -Require Import Arith Omega. +Require Import Arith Lia. Lemma test : forall p:nat, p<>0 -> p-1+1=p. Proof. - intros; omega. + intros; lia. Qed. (** Test of new syntax for rewrite : ! ? and so on... *) diff --git a/test-suite/success/search.v b/test-suite/success/search.v index 92de43e052..627e109d5f 100644 --- a/test-suite/success/search.v +++ b/test-suite/success/search.v @@ -32,4 +32,4 @@ Require Import ZArith. Search Z.mul Z.add "distr". Search "+"%Z "*"%Z "distr" -positive -Prop. -Search (?x * _ + ?x * _)%Z outside OmegaLemmas. +Search (?x * _ + ?x * _)%Z outside Lia. diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v index fe7431dcd3..5cfb9d84c7 100644 --- a/theories/Compat/Coq813.v +++ b/theories/Compat/Coq813.v @@ -11,3 +11,13 @@ (** Compatibility file for making Coq act similar to Coq v8.13 *) Require Export Coq.Compat.Coq814. + +Require Coq.micromega.Lia. +Module Export Coq. + Module Export omega. + Module Export Omega. + #[deprecated(since="8.12", note="The omega tactic was removed in v8.14. You're now relying on the lia tactic.")] + Ltac omega := Lia.lia. + End Omega. + End omega. +End Coq. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 47137414dc..ff1a2b5a53 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1775,8 +1775,6 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos) Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *) -Register Zne as plugins.omega.Zne. - Ltac elim_compare com1 com2 := case (Dcompare (com1 ?= com2)%Z); [ idtac | let x := fresh "H" in diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index ed47539e1e..5490044ac7 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -16,9 +16,11 @@ Require Export ZArith_base. Require Export Zpow_def. -(** Extra modules using [Omega] or [Ring]. *) +(** Extra modules using [Ring]. *) -Require Export Omega. +Require Export OmegaLemmas. +Require Export PreOmega. +Require Export ZArith_hints. Require Export Zcomplements. Require Export Zpower. Require Export Zdiv. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 7f72d42d1f..b7cd849323 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -959,13 +959,6 @@ Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m). Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m). Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m). -Register neq as plugins.omega.neq. -Register inj_eq as plugins.omega.inj_eq. -Register inj_neq as plugins.omega.inj_neq. -Register inj_le as plugins.omega.inj_le. -Register inj_lt as plugins.omega.inj_lt. -Register inj_ge as plugins.omega.inj_ge. -Register inj_gt as plugins.omega.inj_gt. (** For the others, a Notation is fine *) @@ -1033,5 +1026,3 @@ Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0. Proof. intros. rewrite not_le_minus_0; auto with arith. Qed. - -Register inj_minus2 as plugins.omega.inj_minus2. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 4c533ac458..bef9cede12 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -64,11 +64,6 @@ Proof. apply Z.lt_gt_cases. Qed. -Register dec_Zne as plugins.omega.dec_Zne. -Register dec_Zgt as plugins.omega.dec_Zgt. -Register dec_Zge as plugins.omega.dec_Zge. -Register not_Zeq as plugins.omega.not_Zeq. - (** * Relating strict and large orders *) Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). @@ -120,12 +115,6 @@ Proof. destruct (Z.eq_decidable n m); [assumption|now elim H]. Qed. -Register Znot_le_gt as plugins.omega.Znot_le_gt. -Register Znot_lt_ge as plugins.omega.Znot_lt_ge. -Register Znot_ge_lt as plugins.omega.Znot_ge_lt. -Register Znot_gt_le as plugins.omega.Znot_gt_le. -Register not_Zne as plugins.omega.not_Zne. - (** * Equivalence and order properties *) (** Reflexivity *) diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 10ea6cc03e..369a0c46ae 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -93,11 +93,3 @@ Proof. apply Z.le_lt_trans with (m*n+p); trivial. now apply Z.add_lt_mono_l. Qed. - -Register Zegal_left as plugins.omega.Zegal_left. -Register Zne_left as plugins.omega.Zne_left. -Register Zlt_left as plugins.omega.Zlt_left. -Register Zgt_left as plugins.omega.Zgt_left. -Register Zle_left as plugins.omega.Zle_left. -Register Zge_left as plugins.omega.Zge_left. -Register Zmult_le_approx as plugins.omega.Zmult_le_approx. diff --git a/theories/dune b/theories/dune index 1cd3d8c119..ced818c3ba 100644 --- a/theories/dune +++ b/theories/dune @@ -22,7 +22,6 @@ coq-core.plugins.ring coq-core.plugins.nsatz - coq-core.plugins.omega coq-core.plugins.zify coq-core.plugins.micromega diff --git a/theories/omega/Omega.v b/theories/omega/Omega.v deleted file mode 100644 index 5c52284621..0000000000 --- a/theories/omega/Omega.v +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - -(* We import what is necessary for Omega *) -Require Export ZArith_base. -Require Export OmegaLemmas. -Require Export PreOmega. -Require Export ZArith_hints. - -Declare ML Module "omega_plugin". diff --git a/theories/omega/OmegaLemmas.v b/theories/omega/OmegaLemmas.v index 08e9ac345d..8ccd8d76f6 100644 --- a/theories/omega/OmegaLemmas.v +++ b/theories/omega/OmegaLemmas.v @@ -261,47 +261,3 @@ Proof. intros n; exists (Z.of_nat n); split; trivial. rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg. Qed. - -Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse. -Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc. -Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse. -Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute. -Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm. -Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm. - -Register OMEGA1 as plugins.omega.OMEGA1. -Register OMEGA2 as plugins.omega.OMEGA2. -Register OMEGA3 as plugins.omega.OMEGA3. -Register OMEGA4 as plugins.omega.OMEGA4. -Register OMEGA5 as plugins.omega.OMEGA5. -Register OMEGA6 as plugins.omega.OMEGA6. -Register OMEGA7 as plugins.omega.OMEGA7. -Register OMEGA8 as plugins.omega.OMEGA8. -Register OMEGA9 as plugins.omega.OMEGA9. -Register fast_OMEGA10 as plugins.omega.fast_OMEGA10. -Register fast_OMEGA11 as plugins.omega.fast_OMEGA11. -Register fast_OMEGA12 as plugins.omega.fast_OMEGA12. -Register fast_OMEGA13 as plugins.omega.fast_OMEGA13. -Register fast_OMEGA14 as plugins.omega.fast_OMEGA14. -Register fast_OMEGA15 as plugins.omega.fast_OMEGA15. -Register fast_OMEGA16 as plugins.omega.fast_OMEGA16. -Register OMEGA17 as plugins.omega.OMEGA17. -Register OMEGA18 as plugins.omega.OMEGA18. -Register OMEGA19 as plugins.omega.OMEGA19. -Register OMEGA20 as plugins.omega.OMEGA20. - -Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0. -Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1. -Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2. -Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3. -Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4. -Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5. -Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6. - -Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l. -Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr. -Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r. -Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1. - -Register new_var as plugins.omega.new_var. -Register intro_Z as plugins.omega.intro_Z. diff --git a/theories/omega/OmegaPlugin.v b/theories/omega/OmegaPlugin.v deleted file mode 100644 index e0cf24f6aa..0000000000 --- a/theories/omega/OmegaPlugin.v +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* To strictly import the omega tactic *) - -Require ZArith_base. -Require OmegaLemmas. -Require PreOmega. - -Declare ML Module "omega_plugin". diff --git a/theories/omega/OmegaTactic.v b/theories/omega/OmegaTactic.v deleted file mode 100644 index e0cf24f6aa..0000000000 --- a/theories/omega/OmegaTactic.v +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* To strictly import the omega tactic *) - -Require ZArith_base. -Require OmegaLemmas. -Require PreOmega. - -Declare ML Module "omega_plugin". diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 70f25e7243..bf873785d0 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -12,9 +12,10 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. Local Open Scope Z_scope. -(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) +(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: + the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) -(** These tactic use the complete specification of [Z.div] and +(** These tactics use the complete specification of [Z.div] and [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these functions from the goal without losing information. The [Z.euclidean_division_equations_cleanup] tactic removes needless @@ -127,449 +128,6 @@ Module Z. Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup. End Z. -Set Warnings "-deprecated-tactic". - -(** * zify: the Z-ification tactic *) - -(* This tactic searches for nat and N and positive elements in the goal and - translates everything into Z. It is meant as a pre-processor for - (r)omega; for instance a positivity hypothesis is added whenever - - a multiplication is encountered - - an atom is encountered (that is a variable or an unknown construct) - - Recognized relations (can be handled as deeply as allowed by setoid rewrite): - - { eq, le, lt, ge, gt } on { Z, positive, N, nat } - - Recognized operations: - - on Z: Z.min, Z.max, Z.abs, Z.sgn are translated in term of <= < = - - on nat: + * - S O pred min max Pos.to_nat N.to_nat Z.abs_nat - - on positive: Zneg Zpos xI xO xH + * - Pos.succ Pos.pred Pos.min Pos.max Pos.of_succ_nat - - on N: N0 Npos + * - N.pred N.succ N.min N.max N.of_nat Z.abs_N -*) - - - - -(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *) - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop_core t thm a := - (* Let's introduce the specification theorem for t *) - pose proof (thm a); - (* Then we replace (t a) everywhere with a fresh variable *) - let z := fresh "z" in set (z:=t a) in *; clearbody z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop_var_or_term t thm a := - (* If a is a variable, no need for aliasing *) - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_core t thm a) || - (* Otherwise, a is a complex term: we alias it. *) - (remember a as za; zify_unop_core t thm za). - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop t thm a := - (* If a is a scalar, we can simply reduce the unop. *) - (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) - let isz := isZcst a in - match isz with - | true => - let u := eval compute in (t a) in - change (t a) with u in * - | _ => zify_unop_var_or_term t thm a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_unop_nored t thm a := - (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *) - let isz := isZcst a in - match isz with - | true => zify_unop_core t thm a - | _ => zify_unop_var_or_term t thm a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_binop t thm a b:= - (* works as zify_unop, except that we should be careful when - dealing with b, since it can be equal to a *) - let isza := isZcst a in - match isza with - | true => zify_unop (t a) (thm a) b - | _ => - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || - (remember a as za; match goal with - | H : za = b |- _ => zify_unop_nored (t za) (thm za) za - | _ => zify_unop_nored (t za) (thm za) b - end) - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_op_1 := - match goal with - | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b - | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b - | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b - | H : context [ Z.min ?a ?b ] |- _ => zify_binop Z.min Z.min_spec a b - | |- context [ Z.sgn ?a ] => zify_unop Z.sgn Z.sgn_spec a - | H : context [ Z.sgn ?a ] |- _ => zify_unop Z.sgn Z.sgn_spec a - | |- context [ Z.abs ?a ] => zify_unop Z.abs Z.abs_spec a - | H : context [ Z.abs ?a ] |- _ => zify_unop Z.abs Z.abs_spec a - end. - -Ltac zify_op := repeat zify_op_1. - - -(** II) Conversion from nat to Z *) - - -Definition Z_of_nat' := Z.of_nat. - -Ltac hide_Z_of_nat t := - let z := fresh "z" in set (z:=Z.of_nat t) in *; - change Z.of_nat with Z_of_nat' in z; - unfold z in *; clear z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_nat_rel := - match goal with - (* I: equalities *) - | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) - | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H - | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) - (* II: less than *) - | H : context [ lt ?a ?b ] |- _ => rewrite (Nat2Z.inj_lt a b) in H - | |- context [ lt ?a ?b ] => rewrite (Nat2Z.inj_lt a b) - (* III: less or equal *) - | H : context [ le ?a ?b ] |- _ => rewrite (Nat2Z.inj_le a b) in H - | |- context [ le ?a ?b ] => rewrite (Nat2Z.inj_le a b) - (* IV: greater than *) - | H : context [ gt ?a ?b ] |- _ => rewrite (Nat2Z.inj_gt a b) in H - | |- context [ gt ?a ?b ] => rewrite (Nat2Z.inj_gt a b) - (* V: greater or equal *) - | H : context [ ge ?a ?b ] |- _ => rewrite (Nat2Z.inj_ge a b) in H - | |- context [ ge ?a ?b ] => rewrite (Nat2Z.inj_ge a b) - end. - -Ltac zify_nat_op := - match goal with - (* misc type conversions: positive/N/Z to nat *) - | H : context [ Z.of_nat (Pos.to_nat ?a) ] |- _ => rewrite (positive_nat_Z a) in H - | |- context [ Z.of_nat (Pos.to_nat ?a) ] => rewrite (positive_nat_Z a) - | H : context [ Z.of_nat (N.to_nat ?a) ] |- _ => rewrite (N_nat_Z a) in H - | |- context [ Z.of_nat (N.to_nat ?a) ] => rewrite (N_nat_Z a) - | H : context [ Z.of_nat (Z.abs_nat ?a) ] |- _ => rewrite (Zabs2Nat.id_abs a) in H - | |- context [ Z.of_nat (Z.abs_nat ?a) ] => rewrite (Zabs2Nat.id_abs a) - - (* plus -> Z.add *) - | H : context [ Z.of_nat (plus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_add a b) in H - | |- context [ Z.of_nat (plus ?a ?b) ] => rewrite (Nat2Z.inj_add a b) - - (* min -> Z.min *) - | H : context [ Z.of_nat (min ?a ?b) ] |- _ => rewrite (Nat2Z.inj_min a b) in H - | |- context [ Z.of_nat (min ?a ?b) ] => rewrite (Nat2Z.inj_min a b) - - (* max -> Z.max *) - | H : context [ Z.of_nat (max ?a ?b) ] |- _ => rewrite (Nat2Z.inj_max a b) in H - | |- context [ Z.of_nat (max ?a ?b) ] => rewrite (Nat2Z.inj_max a b) - - (* minus -> Z.max (Z.sub ... ...) 0 *) - | H : context [ Z.of_nat (minus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_sub_max a b) in H - | |- context [ Z.of_nat (minus ?a ?b) ] => rewrite (Nat2Z.inj_sub_max a b) - - (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *) - | H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H - | |- context [ Z.of_nat (pred ?a) ] => rewrite (pred_of_minus a) - - (* mult -> Z.mul and a positivity hypothesis *) - | H : context [ Z.of_nat (mult ?a ?b) ] |- _ => - pose proof (Nat2Z.is_nonneg (mult a b)); - rewrite (Nat2Z.inj_mul a b) in * - | |- context [ Z.of_nat (mult ?a ?b) ] => - pose proof (Nat2Z.is_nonneg (mult a b)); - rewrite (Nat2Z.inj_mul a b) in * - - (* O -> Z0 *) - | H : context [ Z.of_nat O ] |- _ => change (Z.of_nat O) with Z0 in H - | |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0 - - (* S -> number or Z.succ *) - | H : context [ Z.of_nat (S ?a) ] |- _ => - let isnat := isnatcst a in - match isnat with - | true => - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t in H - | _ => rewrite (Nat2Z.inj_succ a) in H - | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in this one hypothesis *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H - end - | |- context [ Z.of_nat (S ?a) ] => - let isnat := isnatcst a in - match isnat with - | true => - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t - | _ => rewrite (Nat2Z.inj_succ a) - | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in the goal *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) - end - - (* atoms of type nat : we add a positivity condition (if not already there) *) - | _ : 0 <= Z.of_nat ?a |- _ => hide_Z_of_nat a - | _ : context [ Z.of_nat ?a ] |- _ => - pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a - | |- context [ Z.of_nat ?a ] => - pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *. - -(* III) conversion from positive to Z *) - -Definition Zpos' := Zpos. -Definition Zneg' := Zneg. - -Ltac hide_Zpos t := - let z := fresh "z" in set (z:=Zpos t) in *; - change Zpos with Zpos' in z; - unfold z in *; clear z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_positive_rel := - match goal with - (* I: equalities *) - | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- (@eq positive ?a ?b) => apply Pos2Z.inj - | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H - | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) - (* II: less than *) - | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H - | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b) - (* III: less or equal *) - | H : context [ (?a <= ?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H - | |- context [ (?a <= ?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b) - (* IV: greater than *) - | H : context [ (?a > ?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H - | |- context [ (?a > ?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b) - (* V: greater or equal *) - | H : context [ (?a >= ?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H - | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b) - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_positive_op := - match goal with - (* Z.pow_pos -> Z.pow *) - | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H - | |- context [ Z.pow_pos ?a ?b ] => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) - (* Zneg -> -Zpos (except for numbers) *) - | H : context [ Zneg ?a ] |- _ => - let isp := isPcst a in - match isp with - | true => change (Zneg a) with (Zneg' a) in H - | _ => change (Zneg a) with (- Zpos a) in H - end - | |- context [ Zneg ?a ] => - let isp := isPcst a in - match isp with - | true => change (Zneg a) with (Zneg' a) - | _ => change (Zneg a) with (- Zpos a) - end - - (* misc type conversions: nat to positive *) - | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H - | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) - - (* Z.power_pos *) - | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H - | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) - - (* Pos.add -> Z.add *) - | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H - | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b) - - (* Pos.min -> Z.min *) - | H : context [ Zpos (Pos.min ?a ?b) ] |- _ => rewrite (Pos2Z.inj_min a b) in H - | |- context [ Zpos (Pos.min ?a ?b) ] => rewrite (Pos2Z.inj_min a b) - - (* Pos.max -> Z.max *) - | H : context [ Zpos (Pos.max ?a ?b) ] |- _ => rewrite (Pos2Z.inj_max a b) in H - | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b) - - (* Pos.sub -> Z.max 1 (Z.sub ... ...) *) - | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H - | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b) - - (* Pos.succ -> Z.succ *) - | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H - | |- context [ Zpos (Pos.succ ?a) ] => rewrite (Pos2Z.inj_succ a) - - (* Pos.pred -> Pos.sub ... -1 -> Z.max 1 (Z.sub ... - 1) *) - | H : context [ Zpos (Pos.pred ?a) ] |- _ => rewrite <- (Pos.sub_1_r a) in H - | |- context [ Zpos (Pos.pred ?a) ] => rewrite <- (Pos.sub_1_r a) - - (* Pos.mul -> Z.mul and a positivity hypothesis *) - | H : context [ Zpos (?a * ?b) ] |- _ => - pose proof (Pos2Z.is_pos (Pos.mul a b)); - change (Zpos (a*b)) with (Zpos a * Zpos b) in * - | |- context [ Zpos (?a * ?b) ] => - pose proof (Pos2Z.is_pos (Pos.mul a b)); - change (Zpos (a*b)) with (Zpos a * Zpos b) in * - - (* xO *) - | H : context [ Zpos (xO ?a) ] |- _ => - let isp := isPcst a in - match isp with - | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H - | _ => rewrite (Pos2Z.inj_xO a) in H - end - | |- context [ Zpos (xO ?a) ] => - let isp := isPcst a in - match isp with - | true => change (Zpos (xO a)) with (Zpos' (xO a)) - | _ => rewrite (Pos2Z.inj_xO a) - end - (* xI *) - | H : context [ Zpos (xI ?a) ] |- _ => - let isp := isPcst a in - match isp with - | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H - | _ => rewrite (Pos2Z.inj_xI a) in H - end - | |- context [ Zpos (xI ?a) ] => - let isp := isPcst a in - match isp with - | true => change (Zpos (xI a)) with (Zpos' (xI a)) - | _ => rewrite (Pos2Z.inj_xI a) - end - - (* xI : nothing to do, just prevent adding a useless positivity condition *) - | H : context [ Zpos xH ] |- _ => hide_Zpos xH - | |- context [ Zpos xH ] => hide_Zpos xH - - (* atoms of type positive : we add a positivity condition (if not already there) *) - | _ : 0 < Zpos ?a |- _ => hide_Zpos a - | _ : context [ Zpos ?a ] |- _ => pose proof (Pos2Z.is_pos a); hide_Zpos a - | |- context [ Zpos ?a ] => pose proof (Pos2Z.is_pos a); hide_Zpos a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_positive := - repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *. - - - - - -(* IV) conversion from N to Z *) - -Definition Z_of_N' := Z.of_N. - -Ltac hide_Z_of_N t := - let z := fresh "z" in set (z:=Z.of_N t) in *; - change Z.of_N with Z_of_N' in z; - unfold z in *; clear z. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_N_rel := - match goal with - (* I: equalities *) - | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) - | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H - | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) - (* II: less than *) - | H : context [ (?a < ?b)%N ] |- _ => rewrite (N2Z.inj_lt a b) in H - | |- context [ (?a < ?b)%N ] => rewrite (N2Z.inj_lt a b) - (* III: less or equal *) - | H : context [ (?a <= ?b)%N ] |- _ => rewrite (N2Z.inj_le a b) in H - | |- context [ (?a <= ?b)%N ] => rewrite (N2Z.inj_le a b) - (* IV: greater than *) - | H : context [ (?a > ?b)%N ] |- _ => rewrite (N2Z.inj_gt a b) in H - | |- context [ (?a > ?b)%N ] => rewrite (N2Z.inj_gt a b) - (* V: greater or equal *) - | H : context [ (?a >= ?b)%N ] |- _ => rewrite (N2Z.inj_ge a b) in H - | |- context [ (?a >= ?b)%N ] => rewrite (N2Z.inj_ge a b) - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_N_op := - match goal with - (* misc type conversions: nat to positive *) - | H : context [ Z.of_N (N.of_nat ?a) ] |- _ => rewrite (nat_N_Z a) in H - | |- context [ Z.of_N (N.of_nat ?a) ] => rewrite (nat_N_Z a) - | H : context [ Z.of_N (Z.abs_N ?a) ] |- _ => rewrite (N2Z.inj_abs_N a) in H - | |- context [ Z.of_N (Z.abs_N ?a) ] => rewrite (N2Z.inj_abs_N a) - | H : context [ Z.of_N (Npos ?a) ] |- _ => rewrite (N2Z.inj_pos a) in H - | |- context [ Z.of_N (Npos ?a) ] => rewrite (N2Z.inj_pos a) - | H : context [ Z.of_N N0 ] |- _ => change (Z.of_N N0) with Z0 in H - | |- context [ Z.of_N N0 ] => change (Z.of_N N0) with Z0 - - (* N.add -> Z.add *) - | H : context [ Z.of_N (N.add ?a ?b) ] |- _ => rewrite (N2Z.inj_add a b) in H - | |- context [ Z.of_N (N.add ?a ?b) ] => rewrite (N2Z.inj_add a b) - - (* N.min -> Z.min *) - | H : context [ Z.of_N (N.min ?a ?b) ] |- _ => rewrite (N2Z.inj_min a b) in H - | |- context [ Z.of_N (N.min ?a ?b) ] => rewrite (N2Z.inj_min a b) - - (* N.max -> Z.max *) - | H : context [ Z.of_N (N.max ?a ?b) ] |- _ => rewrite (N2Z.inj_max a b) in H - | |- context [ Z.of_N (N.max ?a ?b) ] => rewrite (N2Z.inj_max a b) - - (* N.sub -> Z.max 0 (Z.sub ... ...) *) - | H : context [ Z.of_N (N.sub ?a ?b) ] |- _ => rewrite (N2Z.inj_sub_max a b) in H - | |- context [ Z.of_N (N.sub ?a ?b) ] => rewrite (N2Z.inj_sub_max a b) - - (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *) - | H : context [ Z.of_N (N.pred ?a) ] |- _ => rewrite (N.pred_sub a) in H - | |- context [ Z.of_N (N.pred ?a) ] => rewrite (N.pred_sub a) - - (* N.succ -> Z.succ *) - | H : context [ Z.of_N (N.succ ?a) ] |- _ => rewrite (N2Z.inj_succ a) in H - | |- context [ Z.of_N (N.succ ?a) ] => rewrite (N2Z.inj_succ a) - - (* N.mul -> Z.mul and a positivity hypothesis *) - | H : context [ Z.of_N (N.mul ?a ?b) ] |- _ => - pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * - | |- context [ Z.of_N (N.mul ?a ?b) ] => - pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * - - (* N.div -> Z.div and a positivity hypothesis *) - | H : context [ Z.of_N (N.div ?a ?b) ] |- _ => - pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * - | |- context [ Z.of_N (N.div ?a ?b) ] => - pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * - - (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *) - | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ => - pose proof (N2Z.is_nonneg (N.modulo a b)); - pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - rewrite (N2Z.inj_rem a b) in * - | |- context [ Z.of_N (N.div ?a ?b) ] => - pose proof (N2Z.is_nonneg (N.modulo a b)); - pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); - rewrite (N2Z.inj_rem a b) in * - - (* atoms of type N : we add a positivity condition (if not already there) *) - | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a - | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a - | |- context [ Z.of_N ?a ] => pose proof (N2Z.is_nonneg a); hide_Z_of_N a - end. - -#[deprecated( note = "Use 'zify' instead")] -Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. - -(** The complete Z-ification tactic *) - Require Import ZifyClasses ZifyInst. Require Zify. diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 9cb3baf92c..e0a1d40395 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -74,7 +74,7 @@ let is_tactic = "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; - "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "set"; "assert"; "do"; "repeat"; "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; |