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
      @[reducible, inline]

      An intermediate layer in the OmegaM monad.

      Equations
        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
                            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
                                        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
                                                            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
                                                                Instances For