Documentation

Lean.Elab.Tactic.Omega.OmegaM

The OmegaM state monad. #

We keep track of the linear atoms (up to defeq) that have been encountered so far, and also generate new facts as new atoms are recorded.

The main functions are:

Context for the OmegaM monad, containing the user configurable options.

Instances For

    The internal state for the OmegaM monad, recording previously encountered atoms.

    Instances For

      Cache of expressions that have been visited, and their reflection as a linear combination.

      Equations
      Instances For
        @[reducible, inline]

        The OmegaM monad maintains two pieces of state:

        • the linear atoms discovered while processing hypotheses
        • a cache mapping subexpressions of one side of a linear inequality to LinearCombos (and a proof that the LinearCombo evaluates at the atoms to the original expression).
        Equations
        Instances For

          Run a computation in the OmegaM monad, starting with no recorded atoms.

          Equations
          Instances For

            Retrieve the user-specified configuration options.

            Equations
            Instances For

              Retrieve the list of atoms.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Return the Expr representing the list of atoms.

                Equations
                Instances For

                  Return the Expr representing the list of atoms as a Coeffs.

                  Equations
                  Instances For

                    Run an OmegaM computation, restoring the state afterwards depending on the result.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Run an OmegaM computation, restoring the state afterwards.

                      Equations
                      Instances For

                        Wrapper around Expr.nat? that also allows Nat.cast.

                        Equations
                        Instances For

                          Wrapper around Expr.int? that also allows Nat.cast.

                          Equations
                          Instances For

                            If groundNat? e = some n, then e is definitionally equal to OfNat.ofNat n.

                            If groundInt? e = some i, then e is definitionally equal to the standard expression for i.

                            Construct the term with type hint (Eq.refl a : a = b)

                            Equations
                            Instances For

                              Analyzes a newly recorded atom, returning a collection of interesting facts about it that should be added to the context.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Look up an expression in the atoms, recording it if it has not previously appeared.

                                Return its index, and, if it is new, a collection of interesting facts about the atom.

                                • for each new atom a of the form ((x : Nat) : Int), the fact that 0 ≤ a
                                • for each new atom a of the form x / k, for k a positive numeral, the facts that k * a ≤ x < k * a + k
                                • for each new atom of the form ((a - b : Nat) : Int), the fact: b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For