Documentation

Lean.Elab.Tactic.Omega.Frontend

Frontend to the omega tactic. #

See Lean.Elab.Tactic.Omega for an overview of the tactic.

Allow elaboration of OmegaConfig arguments to tactics.

Equations
    Instances For

      Match on the two defeq expressions for successor: n+1, n.succ.

      Equations
        Instances For

          A partially processed omega context.

          We have:

          • a Problem representing the integer linear constraints extracted so far, and their proofs
          • the unprocessed facts : List Expr taken from the local context,
          • the unprocessed disjunctions : List Expr, which will only be split one at a time if we can't otherwise find a contradiction.

          We begin with facts := ← getLocalHyps and problem := .trivial, and progressively process the facts.

          As we process the facts, we may generate additional facts (e.g. about coercions and integer divisions). To avoid duplicates, we maintain a HashSet of previously processed facts.

          • problem : Problem

            An integer linear arithmetic problem.

          • facts : List Expr

            Pending facts which have not been processed yet.

          • disjunctions : List Expr

            Pending disjunctions, which we will case split one at a time if we can't get a contradiction.

          • processedFacts : Std.HashSet Expr

            Facts which have already been processed; we keep these to avoid duplicates.

          Instances For

            Construct the rfl proof that lc.eval atoms = e.

            Equations
              Instances For

                If e : Expr is the n-th atom, construct the proof that e = (coordinate n).eval atoms.

                Equations
                  Instances For

                    Construct the linear combination (and its associated proof and new facts) for an atom.

                    Equations
                      Instances For

                        Wrapper for asLinearComboImpl, using a cache for previously visited expressions.

                        Gives a small (10%) speedup in testing. I tried using a pointer based cache, but there was never enough subexpression sharing to make it effective.

                        Translates an expression into a LinearCombo. Also returns:

                        • a proof that this linear combo evaluated at the atoms is equal to the original expression
                        • a list of new facts which should be recorded:
                          • 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 + 1) * a
                          • 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

                        We also transform the expression as we descend into it:

                        • pushing coercions: ↑(x + y), ↑(x * y), ↑(x / k), ↑(x % k), ↑k
                        • unfolding emod: x % kx - x / k

                        Apply a rewrite rule to an expression, and interpret the result as a LinearCombo. (We're not rewriting any subexpressions here, just the top level, for efficiency.)

                        The trivial MetaProblem, with no facts to process and a trivial Problem.

                        Equations
                          Instances For

                            Add an integer equality to the Problem.

                            We solve equalities as they are discovered, as this often results in an earlier contradiction.

                            Equations
                              Instances For

                                Add an integer inequality to the Problem.

                                We solve equalities as they are discovered, as this often results in an earlier contradiction.

                                Equations
                                  Instances For

                                    Given a fact h with type ¬ P, return a more useful fact obtained by pushing the negation.

                                    Equations
                                      Instances For

                                        Parse an Expr and extract facts, also returning the number of new facts found.

                                        Process all the facts in a MetaProblem, returning the new problem, and the number of new facts.

                                        This is partial because new facts may be generated along the way.

                                        Helpful error message when omega cannot find a solution

                                        Equations
                                          Instances For

                                            Split a disjunction in a MetaProblem, and if we find a new usable fact call omegaImpl in both branches.

                                            Implementation of the omega algorithm, and handling disjunctions.

                                            Given a collection of facts, try prove False using the omega algorithm, and close the goal using that.

                                            Equations
                                              Instances For

                                                The omega tactic, for resolving integer and natural linear arithmetic problems.

                                                Equations
                                                  Instances For

                                                    The omega tactic, for resolving integer and natural linear arithmetic problems. This TacticM Unit frontend with default configuration can be used as an Aesop rule, for example via the tactic call aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault).

                                                    Equations
                                                      Instances For
                                                        @[deprecated Lean.Elab.Tactic.Omega.bitvec_to_nat (since := "2025-02-10")]