Tify + lra solves programs mixing Z and R

dev/ci/scripts/ci-stdlib.sh

@@ -10,6 +10,6 @@ git_download stdlib
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/stdlib"
-  dev/with-rocq-wrap.sh dune build --root . --only-packages=rocq-stdlib @install
+  dev/with-rocq-wrap.sh dune build --root . --profile release --only-packages=rocq-stdlib @install
   dev/with-rocq-wrap.sh dune install --root . rocq-stdlib --prefix="$CI_INSTALL_DIR"
 )

dev/ci/user-overlays/20288-fajb-tify-lra.sh

@@ -0,0 +1 @@
+overlay stdlib https://github.com/fajb/stdlib rify 20288

doc/corelib/hidden-files

@@ -39,6 +39,7 @@ theories/micromega/Lra.v
 theories/micromega/MExtraction.v
 theories/micromega/OrderedRing.v
 theories/micromega/Psatz.v
+theories/micromega/MMicromega.v
 theories/micromega/QMicromega.v
 theories/micromega/RMicromega.v
 theories/micromega/Refl.v

doc/sphinx/addendum/micromega.rst

@@ -153,17 +153,15 @@ For each conjunct :math:`C_i`, the tactic calls an oracle which searches for
 :gdef:`cone expression` that is normalized by the :tacn:`ring` tactic
 (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`.
 
-`lra`: a decision procedure for linear real and rational arithmetic
+`lra`: a decision procedure for mixed integer linear arithmetic
 -------------------------------------------------------------------
 
 .. tacn:: lra
 
-   This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone*
-   defined as
-
-   .. math::
-
-      \mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}
+   The tactics solves mixed integer arithmetic goals i.e. goals where variables range over either the reals or the integers.
+   In addition to standard linear arithmetic constraints over :g:`R`, the tactic supports the predicate :g:`isZ: R -> Prop`
+   such that :g:`IsZ x` restricts the range of  :g:`x` to be an integer.
+   See  :tacn:`rify` to pre-process the goal.
 
    The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field`
    tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
@@ -357,12 +355,57 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    See the :ref:`example below <lra_example>` and comments in
    `plugin/micromega/coq_micromega.mli`.
 
-`zify`: pre-processing of arithmetic goals
-------------------------------------------
+`tify`: pre-processing of arithmetic goals (generalise `zify`)
+--------------------------------------------------------------
+
+.. tacn:: tify @qualid
+
+   The tactic :tacn:`tify` :g:`T` injects the goal towards the type
+   :g:`T`. It can be extended with new types and operators by
+   declaring and registering new typeclass instances using the
+   following commands.  The typeclass declarations can be found in the
+   module ``TifyClasses``.
+
+.. cmd:: Add Tify @add_tify @qualid
+
+   .. insertprodn add_tify add_tify
+
+   .. prodn::
+      add_tify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
+      | {| PropOp | PropBinOp | PropUOp | Saturate }
+
+   Registers an instance of the specified typeclass.
+   The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that
+   the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`)
+   is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`.
+
+   This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`.
+   In sections only :attr:`local` is supported, outside sections the default is :attr:`global`.
+
+.. cmd:: Show Tify @show_tify
+
+   .. insertprodn show_tify show_tify
+
+   .. prodn::
+      show_tify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
+
+   Prints instances for the specified typeclass.  For instance, :cmd:`Show Tify` ``InjTyp``
+   prints the list of types that supported by :tacn:`tify` e.g.,
+   :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
+
+.. tacn:: tify_elim_let
+          tify_iter_let @ltac_expr
+          tify_iter_specs
+          tify_op @qualid
+          tify_saturate
+
+   For internal use only (it may change without notice).
+
 
 .. tacn:: zify
 
-   This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`.
+   This tactic is internally called by :tacn:`lia` and calls tacn:`tify Z` to inject towards :g:`Z`
+   additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`.
    Additional support is provided by the following modules:
 
    + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`.
@@ -386,43 +429,28 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
      - :g:`Z.euclidean_division_equations_cleanup`, removing impossible hypotheses introduced by the above passes, such as those presupposing :g:`x <> x`
      - :g:`Z.euclidean_division_equations_find_duplicate_quotients`, which heuristically adds equations of the form :g:`q1 = q2 \/ q1 <> q2` when it seems that two quotients might be equal, allowing :g:`nia` to prove more goals, including those relating :g:`Z.quot` and :g:`Z.modulo` to :g:`Z.quot` and :g:`Z.rem`.
 
-   The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
-   The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
 
-.. cmd:: Add Zify @add_zify @qualid
+.. tacn:: zify_elim_let
+          zify_iter_let @ltac_expr
+          zify_iter_specs
+          zify_op
+          zify_saturate
 
-   .. insertprodn add_zify add_zify
+   For internal use only and deprecated by their tacn:`tify` variants  (it may change without notice).
 
-   .. prodn::
-      add_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
-      | {| PropOp | PropBinOp | PropUOp | Saturate }
+.. cmd:: Add Zify @add_tify @qualid
 
-   Registers an instance of the specified typeclass.
-   The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that
-   the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`)
-   is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`.
+   These commands are deprecated, use :g:`Add Tify` instead.
 
-   This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`.
-   In sections only :attr:`local` is supported, outside sections the default is :attr:`global`.
-
-.. cmd:: Show Zify @show_zify
+.. cmd:: Show Zify @show_tify
 
-   .. insertprodn show_zify show_zify
+   These commands are deprecated, use :g:`Show Tify` instead.
 
-   .. prodn::
-      show_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec | Spec }
-
-   Prints instances for the specified typeclass.  For instance, :cmd:`Show Zify` ``InjTyp``
-   prints the list of types that supported by :tacn:`zify` i.e.,
-   :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
-.. tacn:: zify_elim_let
-          zify_iter_let @ltac_expr
-          zify_iter_specs
-          zify_op
-          zify_saturate
+.. tacn:: rify
 
-   For internal use only (it may change without notice).
+   This tactic (found in module ``Rify``) and defined as tacn:`tify` :g:`R` can used to pre-process goals for tacn:`lra`.
+   In particular, it introduces the predicate :g:`isZ` when injecting variables from :g:`Z` to :g:`R`.
 
 .. _lra_example:
 

doc/tools/docgram/common.edit_mlg

@@ -1228,13 +1228,13 @@ printable: [
 | INSERTALL "Print"
 ]
 
-add_zify: [
+add_tify: [
 | [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]  TAG Micromega
 | [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]TAG Micromega
 ]
 
-show_zify: [
-| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]  TAG Micromega
+show_tify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec"  ]  TAG Micromega
 ]
 
 command: [
@@ -1390,8 +1390,19 @@ command: [
 | DELETE "Add" "Zify" "BinOpSpec" reference      (* micromega plugin *)
 | DELETE "Add" "Zify" "UnOpSpec" reference      (* micromega plugin *)
 | DELETE "Add" "Zify" "Saturate" reference      (* micromega plugin *)
-| "Add" "Zify" add_zify reference  TAG Micromega
-
+| "Add" "Zify" add_tify reference  TAG Micromega
+| DELETE "Add" "Tify" "InjTyp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "BinOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "UnOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "CstOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "BinRel" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "PropOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "PropBinOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "PropUOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "BinOpSpec" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "UnOpSpec" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "Saturate" reference      (* micromega plugin *)
+| "Add" "Tify" add_tify reference  TAG Micromega
 | DELETE "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | DELETE "Show" "Zify" "BinOp"      (* micromega plugin *)
 | DELETE "Show" "Zify" "UnOp"      (* micromega plugin *)
@@ -1400,7 +1411,16 @@ command: [
 | DELETE "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | DELETE "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 (* keep this one | "Show" "Zify" "Spec"      (* micromega plugin *)*)
-| "Show" "Zify" show_zify  TAG Micromega
+| "Show" "Zify" show_tify  TAG Micromega
+| DELETE "Show" "Tify" "InjTyp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "BinOp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "UnOp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "CstOp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "BinRel"      (* micromega plugin *)
+| DELETE "Show" "Tify" "UnOpSpec"      (* micromega plugin *)
+| DELETE "Show" "Tify" "BinOpSpec"      (* micromega plugin *)
+(* keep this one | "Show" "Tify" "Spec"      (* micromega plugin *)*)
+| "Show" "Tify" show_tify  TAG Micromega
 | REPLACE "Goal" lconstr
 | WITH "Goal" type
 ]
@@ -1862,6 +1882,8 @@ ltac_defined_tactics: [
 | "tauto"
 | "time_constr" ltac_expr5
 | "zify"
+| "rify"
+| "tify" qualid
 ]
 
 (* todo: need careful review; assume that "[" ... "]" are literals *)

doc/tools/docgram/fullGrammar

@@ -683,13 +683,31 @@ command: [
 | "Add" "Zify" "BinOpSpec" reference      (* micromega plugin *)
 | "Add" "Zify" "UnOpSpec" reference      (* micromega plugin *)
 | "Add" "Zify" "Saturate" reference      (* micromega plugin *)
+| "Add" "Tify" "InjTyp" reference      (* micromega plugin *)
+| "Add" "Tify" "BinOp" reference      (* micromega plugin *)
+| "Add" "Tify" "UnOp" reference      (* micromega plugin *)
+| "Add" "Tify" "CstOp" reference      (* micromega plugin *)
+| "Add" "Tify" "BinRel" reference      (* micromega plugin *)
+| "Add" "Tify" "PropOp" reference      (* micromega plugin *)
+| "Add" "Tify" "PropBinOp" reference      (* micromega plugin *)
+| "Add" "Tify" "PropUOp" reference      (* micromega plugin *)
+| "Add" "Tify" "BinOpSpec" reference      (* micromega plugin *)
+| "Add" "Tify" "UnOpSpec" reference      (* micromega plugin *)
+| "Add" "Tify" "Saturate" reference      (* micromega plugin *)
 | "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | "Show" "Zify" "BinOp"      (* micromega plugin *)
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
+| "Show" "Tify" "InjTyp"      (* micromega plugin *)
+| "Show" "Tify" "BinOp"      (* micromega plugin *)
+| "Show" "Tify" "UnOp"      (* micromega plugin *)
+| "Show" "Tify" "CstOp"      (* micromega plugin *)
+| "Show" "Tify" "BinRel"      (* micromega plugin *)
+| "Show" "Tify" "UnOpSpec"      (* micromega plugin *)
+| "Show" "Tify" "BinOpSpec"      (* micromega plugin *)
 | "Add" "Ring" identref ":" constr OPT ring_mods      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" identref ":" constr OPT field_mods      (* ring plugin *)
@@ -1962,10 +1980,15 @@ simple_tactic: [
 | "wpsatz_Q" nat_or_var ident constr      (* micromega plugin *)
 | "xpsatz_R" nat_or_var tactic      (* micromega plugin *)
 | "zify_iter_specs"      (* micromega plugin *)
+| "tify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
 | "zify_iter_let" tactic      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
+| "tify_op" reference      (* micromega plugin *)
+| "tify_saturate"      (* micromega plugin *)
+| "tify_iter_let" tactic      (* micromega plugin *)
+| "tify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "protect_fv" string "in" ident      (* ring plugin *)
 | "protect_fv" string      (* ring plugin *)

doc/tools/docgram/orderedGrammar

@@ -183,13 +183,13 @@ where: [
 | "after" ident
 ]
 
-add_zify: [
+add_tify: [
 | [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]      (* Micromega plugin *)
 | [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]      (* Micromega plugin *)
 ]
 
-show_zify: [
-| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]      (* Micromega plugin *)
+show_tify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]      (* Micromega plugin *)
 ]
 
 REACHABLE: [
@@ -737,8 +737,10 @@ command: [
 | "Locate" "Term" reference
 | "Locate" "Module" qualid
 | "Info" natural ltac_expr
-| "Add" "Zify" add_zify qualid      (* Micromega plugin *)
-| "Show" "Zify" show_zify      (* Micromega plugin *)
+| "Add" "Zify" add_tify qualid      (* Micromega plugin *)
+| "Show" "Zify" show_tify      (* Micromega plugin *)
+| "Add" "Tify" add_tify qualid      (* Micromega plugin *)
+| "Show" "Tify" show_tify      (* Micromega plugin *)
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -1608,10 +1610,15 @@ simple_tactic: [
 | "wpsatz_Q" nat_or_var ident one_term      (* micromega plugin *)
 | "xpsatz_R" nat_or_var ltac_expr      (* micromega plugin *)
 | "zify_iter_specs"      (* micromega plugin *)
+| "tify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
 | "zify_iter_let" ltac_expr      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
+| "tify_op" qualid      (* micromega plugin *)
+| "tify_saturate"      (* micromega plugin *)
+| "tify_iter_let" ltac_expr      (* micromega plugin *)
+| "tify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" one_term      (* nsatz plugin *)
 | "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
@@ -1640,6 +1647,8 @@ simple_tactic: [
 | "tauto"
 | "time_constr" ltac_expr
 | "zify"
+| "rify"
+| "tify" qualid
 | "assert_fails" ltac_expr3
 | "assert_succeeds" ltac_expr3
 | "clear" "dependent" ident