Documentation

Lean.Elab.Tactic.Omega.Core

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

A delayed proof that a constraint is satisfied at the atoms.

Equations
Instances For

    Our internal representation of an argument "justifying" that a constraint holds on some coefficients. We'll use this to construct the proof term once a contradiction is found.

    Instances For

      Wrapping for Justification.tidy when tidy? is nonempty.

      Equations
      Instances For

        Print a Justification as an indented tree structure.

        Equations
        Instances For
          Equations
          • Lean.Elab.Tactic.Omega.Justification.instToString = { toString := Lean.Elab.Tactic.Omega.Justification.toString }

          Construct the proof term associated to a tidy step.

          Equations
          Instances For

            Construct the proof term associated to a combine step.

            Equations
            Instances For

              Construct the proof term associated to a combo step.

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

                Construct the proof term associated to a bmod step.

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

                  Constructs a proof that s.sat' c v = true

                  Equations
                  Instances For

                    A Justification bundled together with its parameters.

                    Instances For

                      tidy, implemented on Fact.

                      Equations
                      • f.tidy = match f.justification.tidy? with | some fst, fst_1, justification => { coeffs := fst_1, constraint := fst, justification := justification } | none => f
                      Instances For

                        combo, implemented on Fact.

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

                          A omega problem.

                          This is a hybrid structure: it contains both Expr objects giving proofs of the "ground" assumptions (or rather continuations which will produce the proofs when needed) and internal representations of the linear constraints that we manipulate in the algorithm.

                          While the algorithm is running we do not synthesize any new Expr proofs: proof extraction happens only once we've found a contradiction.

                          Instances For
                            theorem Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec (self : Lean.Elab.Tactic.Omega.Problem) :
                            (self.possible || self.proveFalse?.isSome) = true

                            Invariant between possible and proveFalse?.

                            Check if a problem has no constraints.

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

                              Takes a proof that s.sat' x v for some s such that s.isImpossible, and constructs a proof of False.

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

                                Insert a constraint into the problem, without checking if there is already a constraint for these coefficients.

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

                                  Add a constraint into the problem, combining it with any existing constraints for the same coefficients.

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

                                    Walk through the equalities, finding either the first equality with minimal coefficient ±1, or otherwise the equality with minimal (r.minNatAbs, r.maxNatAbs) (ordered lexicographically).

                                    Returns the coefficients of the equality, along with the value of minNatAbs.

                                    Although we don't need to run a termination proof here, it's nevertheless important that we use this ordering so the algorithm terminates in practice!

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

                                      If we have already solved some equalities, apply those to some new Fact.

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

                                        Solve an "easy" equality, i.e. one with a coefficient that is ±1.

                                        After solving, the variable will have been eliminated from all constraints.

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

                                          We deal with a hard equality by introducing a new easy equality.

                                          After solving the easy equality, the minimum lexicographic value of (c.minNatAbs, c.maxNatAbs) will have been reduced.

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

                                            Solve an equality, by deciding whether it is easy (has a ±1 coefficient) or hard, and delegating to the appropriate function.

                                            Equations
                                            • p.solveEquality c m = if m = 1 then pure (p.solveEasyEquality c) else p.dealWithHardEquality c
                                            Instances For

                                              Constructing the proof term for addInequality.

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

                                                Constructing the proof term for addEquality.

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

                                                  Helper function for adding an inequality of the form const + Coeffs.dot coeffs atoms ≥ 0 to a Problem.

                                                  (This is only used while initializing a Problem. During elimination we use addConstraint.)

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

                                                    Helper function for adding an equality of the form const + Coeffs.dot coeffs atoms = 0 to a Problem.

                                                    (This is only used while initializing a Problem. During elimination we use addConstraint.)

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

                                                      Folding addInequality over a list.

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

                                                        Folding addEquality over a list.

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

                                                          Representation of the data required to run Fourier-Motzkin elimination on a variable.

                                                          • var : Nat

                                                            Which variable is being eliminated.

                                                          • The "irrelevant" facts which do not involve the target variable.

                                                          • The facts which give a lower bound on the target variable, and the coefficient of the target variable in each.

                                                          • The facts which give an upper bound on the target variable, and the coefficient of the target variable in each.

                                                          • lowerExact : Bool

                                                            Whether the elimination would be exact, because all of the lower bound coefficients are ±1.

                                                          • upperExact : Bool

                                                            Whether the elimination would be exact, because all of the upper bound coefficients are ±1.

                                                          Instances For

                                                            Is a Fourier-Motzkin elimination empty (i.e. there are no relevant constraints).

                                                            Equations
                                                            • d.isEmpty = (d.lowerBounds.isEmpty && d.upperBounds.isEmpty)
                                                            Instances For

                                                              The number of new constraints that would be introduced by Fourier-Motzkin elimination.

                                                              Equations
                                                              • d.size = d.lowerBounds.length * d.upperBounds.length
                                                              Instances For

                                                                Is the Fourier-Motzkin elimination known to be exact?

                                                                Equations
                                                                • d.exact = (d.lowerExact || d.upperExact)
                                                                Instances For

                                                                  Prepare the Fourier-Motzkin elimination data for each variable.

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

                                                                    Decides which variable to run Fourier-Motzkin elimination on, and returns the associated data.

                                                                    We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations, and break ties by the number of new inequalities introduced.

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

                                                                      Run Fourier-Motzkin elimination on one variable.

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

                                                                        Run the omega algorithm (for now without dark and grey shadows!) on a problem.

                                                                        As for runOmega, but assuming the first round of solving equalities has already happened.