Documentation

Init.Omega.Constraint

A Constraint consists of an optional lower and upper bound (inclusive), constraining a value to a set of the form , {x}, [x, y], [x, ∞), (-∞, y], or (-∞, ∞).

@[reducible, inline]

An optional lower bound on a integer.

Equations
Instances For
    @[reducible, inline]

    An optional upper bound on a integer.

    Equations
    Instances For
      @[reducible, inline]

      A lower bound at x is satisfied at t if x ≤ t.

      Equations
      Instances For
        @[reducible, inline]

        A upper bound at y is satisfied at t if t ≤ y.

        Equations
        Instances For

          A Constraint consists of an optional lower and upper bound (inclusive), constraining a value to a set of the form , {x}, [x, y], [x, ∞), (-∞, y], or (-∞, ∞).

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

            A constraint is satisfied at t is both the lower bound and upper bound are satisfied.

            Equations
            Instances For

              Apply a function to both the lower bound and upper bound.

              Equations
              Instances For

                Translate a constraint.

                Equations
                • c.translate t = c.map fun (x : Int) => x + t
                Instances For
                  theorem Lean.Omega.Constraint.translate_sat {t : Int} {c : Lean.Omega.Constraint} {v : Int} :
                  c.sat v = true(c.translate t).sat (v + t) = true

                  Flip a constraint. This operation is not useful by itself, but is used to implement neg and scale.

                  Equations
                  • c.flip = { lowerBound := c.upperBound, upperBound := c.lowerBound }
                  Instances For

                    Negate a constraint. [x, y] becomes [-y, -x].

                    Equations
                    • c.neg = c.flip.map fun (x : Int) => -x
                    Instances For
                      theorem Lean.Omega.Constraint.neg_sat {c : Lean.Omega.Constraint} {v : Int} :
                      c.sat v = truec.neg.sat (-v) = true

                      The trivial constraint, satisfied everywhere.

                      Equations
                      Instances For

                        The impossible constraint, unsatisfiable.

                        Equations
                        Instances For

                          An exact constraint.

                          Equations
                          Instances For

                            Check if a constraint is unsatisfiable.

                            Equations
                            Instances For

                              Check if a constraint requires an exact value.

                              Equations
                              Instances For

                                Scale a constraint by multiplying by an integer.

                                • If k = 0 this is either impossible, if the original constraint was impossible, or the = 0 exact constraint.
                                • If k is positive this takes [x, y] to [k * x, k * y]
                                • If k is negative this takes [x, y] to [k * y, k * x].
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  The sum of two constraints. [a, b] + [c, d] = [a + c, b + d].

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem Lean.Omega.Constraint.add_sat {c₁ : Lean.Omega.Constraint} {c₂ : Lean.Omega.Constraint} {x₁ : Int} {x₂ : Int} (w₁ : c₁.sat x₁ = true) (w₂ : c₂.sat x₂ = true) :
                                    (c₁.add c₂).sat (x₁ + x₂) = true

                                    A linear combination of two constraints.

                                    Equations
                                    Instances For
                                      theorem Lean.Omega.Constraint.combo_sat {c₁ : Lean.Omega.Constraint} {c₂ : Lean.Omega.Constraint} {x₁ : Int} {x₂ : Int} (a : Int) (w₁ : c₁.sat x₁ = true) (b : Int) (w₂ : c₂.sat x₂ = true) :
                                      (Lean.Omega.Constraint.combo a c₁ b c₂).sat (a * x₁ + b * x₂) = true

                                      The conjunction of two constraints.

                                      Equations
                                      • x.combine y = { lowerBound := max x.lowerBound y.lowerBound, upperBound := min x.upperBound y.upperBound }
                                      Instances For
                                        theorem Lean.Omega.Constraint.combine_sat (c : Lean.Omega.Constraint) (c' : Lean.Omega.Constraint) (t : Int) :
                                        ((c.combine c').sat t = true) = (c.sat t = true c'.sat t = true)

                                        Dividing a constraint by a natural number, and tightened to integer bounds. Thus the lower bound is rounded up, and the upper bound is rounded down.

                                        Equations
                                        Instances For
                                          theorem Lean.Omega.Constraint.div_sat (c : Lean.Omega.Constraint) (t : Int) (k : Nat) (n : k 0) (h : k t) (w : c.sat t = true) :
                                          (c.div k).sat (t / k) = true
                                          @[reducible, inline]

                                          It is convenient below to say that a constraint is satisfied at the dot product of two vectors, so we make an abbreviation sat' for this.

                                          Equations
                                          • c.sat' x y = c.sat (x.dot y)
                                          Instances For
                                            theorem Lean.Omega.Constraint.combine_sat' {s : Lean.Omega.Constraint} {t : Lean.Omega.Constraint} {x : Lean.Omega.Coeffs} {y : Lean.Omega.Coeffs} (ws : s.sat' x y = true) (wt : t.sat' x y = true) :
                                            (s.combine t).sat' x y = true
                                            theorem Lean.Omega.Constraint.div_sat' {c : Lean.Omega.Constraint} {x : Lean.Omega.Coeffs} {y : Lean.Omega.Coeffs} (h : x.gcd 0) (w : c.sat (x.dot y) = true) :
                                            (c.div x.gcd).sat' (x.sdiv x.gcd) y = true
                                            theorem Lean.Omega.Constraint.addInequality_sat {c : Int} {x : Lean.Omega.Coeffs} {y : Lean.Omega.Coeffs} (w : c + x.dot y 0) :
                                            { lowerBound := some (-c), upperBound := none }.sat' x y = true
                                            theorem Lean.Omega.Constraint.addEquality_sat {c : Int} {x : Lean.Omega.Coeffs} {y : Lean.Omega.Coeffs} (w : c + x.dot y = 0) :
                                            { lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true

                                            Normalize a constraint, by dividing through by the GCD.

                                            Return none if there is nothing to do, to avoid adding unnecessary steps to the proof term.

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

                                              Normalize a constraint, by dividing through by the GCD.

                                              Equations
                                              Instances For
                                                @[reducible, inline]

                                                Shorthand for the first component of normalize.

                                                Equations
                                                Instances For
                                                  @[reducible, inline]

                                                  Shorthand for the second component of normalize.

                                                  Equations
                                                  Instances For

                                                    Multiply by -1 if the leading coefficient is negative, otherwise return none.

                                                    Equations
                                                    Instances For

                                                      Multiply by -1 if the leading coefficient is negative, otherwise do nothing.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]

                                                        Shorthand for the first component of positivize.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]

                                                          Shorthand for the second component of positivize.

                                                          Equations
                                                          Instances For

                                                            positivize and normalize, returning none if neither does anything.

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

                                                              Shorthand for the first component of tidy.

                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]

                                                                Shorthand for the second component of tidy.

                                                                Equations
                                                                Instances For
                                                                  theorem Lean.Omega.combo_sat' (s : Lean.Omega.Constraint) (t : Lean.Omega.Constraint) (a : Int) (x : Lean.Omega.Coeffs) (b : Int) (y : Lean.Omega.Coeffs) (v : Lean.Omega.Coeffs) (wx : s.sat' x v = true) (wy : t.sat' y v = true) :
                                                                  @[reducible, inline]

                                                                  The value of the new variable introduced when solving a hard equality.

                                                                  Equations
                                                                  Instances For

                                                                    The coefficients of the new equation generated when solving a hard equality.

                                                                    Equations
                                                                    Instances For
                                                                      theorem Lean.Omega.bmod_sat (m : Nat) (r : Int) (i : Nat) (x : Lean.Omega.Coeffs) (v : Lean.Omega.Coeffs) (h : x.length i) (p : v.get i = Lean.Omega.bmod_div_term m x v) (w : (Lean.Omega.Constraint.exact r).sat' x v = true) :