Documentation

Std.Tactic.Omega.LinearCombo

Linear combinations #

We use this data structure while processing hypotheses.

Internal representation of a linear combination of atoms, and a constant term.

Instances For
    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.
    theorem Std.Tactic.Omega.LinearCombo.ext {a : Std.Tactic.Omega.LinearCombo} {b : Std.Tactic.Omega.LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) :
    a = b

    Evaluate a linear combination ⟨r, [c_1, …, c_k]⟩ at values [v_1, …, v_k] to obtain r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0)))).

    Equations
    Instances For

      The i-th coordinate function.

      Equations
      Instances For
        theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_8 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {a6 : Int} {a7 : Int} {a8 : Int} {t : List Int} :
        theorem Std.Tactic.Omega.LinearCombo.coordinate_eval_9 {a0 : Int} {a1 : Int} {a2 : Int} {a3 : Int} {a4 : Int} {a5 : Int} {a6 : Int} {a7 : Int} {a8 : Int} {a9 : Int} {t : List Int} :

        Implementation of addition on LinearCombo.

        Equations
        Instances For
          @[simp]
          theorem Std.Tactic.Omega.LinearCombo.add_const {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} :
          (l₁ + l₂).const = l₁.const + l₂.const
          @[simp]
          theorem Std.Tactic.Omega.LinearCombo.add_coeffs {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} :
          (l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs

          Implementation of subtraction on LinearCombo.

          Equations
          Instances For
            @[simp]
            theorem Std.Tactic.Omega.LinearCombo.sub_const {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} :
            (l₁ - l₂).const = l₁.const - l₂.const
            @[simp]
            theorem Std.Tactic.Omega.LinearCombo.sub_coeffs {l₁ : Std.Tactic.Omega.LinearCombo} {l₂ : Std.Tactic.Omega.LinearCombo} :
            (l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs

            Implementation of negation on LinearCombo.

            Equations
            Instances For

              Implementation of scalar multiplication of a LinearCombo by an Int.

              Equations
              Instances For
                @[simp]
                theorem Std.Tactic.Omega.LinearCombo.smul_const {lc : Std.Tactic.Omega.LinearCombo} {i : Int} :
                (i * lc).const = i * lc.const
                @[simp]
                theorem Std.Tactic.Omega.LinearCombo.smul_coeffs {lc : Std.Tactic.Omega.LinearCombo} {i : Int} :
                (i * lc).coeffs = i * lc.coeffs

                Multiplication of two linear combinations. This is useful only if at least one of the linear combinations is constant, and otherwise should be considered as a junk value.

                Equations
                Instances For