Documentation

Init.Omega.IntList

@[reducible, inline]

A type synonym for List Int, used by omega for dense representation of coefficients.

We define algebraic operations, interpreting List Int as a finitely supported function NatInt.

Equations
Instances For

    Get the i-th element (interpreted as 0 if the list is not long enough).

    Equations
    Instances For
      theorem Lean.Omega.IntList.get_map {f : IntInt} {i : Nat} {xs : Lean.Omega.IntList} (h : f 0 = 0) :
      Lean.Omega.IntList.get (List.map f xs) i = f (xs.get i)

      Like List.set, but right-pad with zeroes as necessary first.

      Equations
      Instances For
        @[simp]
        theorem Lean.Omega.IntList.set_cons_zero {x : Int} {xs : List Int} {y : Int} :
        Lean.Omega.IntList.set (x :: xs) 0 y = y :: xs
        @[simp]
        theorem Lean.Omega.IntList.set_cons_succ {x : Int} {xs : List Int} {i : Nat} {y : Int} :

        Returns the leading coefficient, i.e. the first non-zero entry.

        Equations
        Instances For

          Implementation of + on IntList.

          Equations
          Instances For
            theorem Lean.Omega.IntList.add_def (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) :
            xs + ys = List.zipWithAll (fun (x y : Option Int) => x.getD 0 + y.getD 0) xs ys
            @[simp]
            theorem Lean.Omega.IntList.add_get (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) :
            (xs + ys).get i = xs.get i + ys.get i
            @[simp]
            @[simp]
            @[simp]
            theorem Lean.Omega.IntList.cons_add_cons (x : Int) (xs : Lean.Omega.IntList) (y : Int) (ys : Lean.Omega.IntList) :
            x :: xs + y :: ys = (x + y) :: (xs + ys)

            Implementation of * on IntList.

            Equations
            Instances For
              theorem Lean.Omega.IntList.mul_def (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) :
              xs * ys = List.zipWith (fun (x1 x2 : Int) => x1 * x2) xs ys
              @[simp]
              theorem Lean.Omega.IntList.mul_get (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) :
              (xs * ys).get i = xs.get i * ys.get i
              @[simp]
              theorem Lean.Omega.IntList.mul_nil_left {ys : List Int} :
              [] * ys = []
              @[simp]
              theorem Lean.Omega.IntList.mul_nil_right {xs : List Int} :
              xs * [] = []
              @[simp]
              theorem Lean.Omega.IntList.mul_cons₂ {x : Int} {xs : List Int} {y : Int} {ys : List Int} :
              (x :: xs) * (y :: ys) = x * y :: xs * ys

              Implementation of negation on IntList.

              Equations
              Instances For
                theorem Lean.Omega.IntList.neg_def (xs : Lean.Omega.IntList) :
                -xs = List.map (fun (x : Int) => -x) xs
                @[simp]
                theorem Lean.Omega.IntList.neg_get (xs : Lean.Omega.IntList) (i : Nat) :
                (-xs).get i = -xs.get i
                @[simp]
                @[simp]
                theorem Lean.Omega.IntList.neg_cons {x : Int} {xs : List Int} :
                -(x :: xs) = -x :: -xs

                Implementation of subtraction on IntList.

                Equations
                Instances For
                  theorem Lean.Omega.IntList.sub_def (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) :
                  xs - ys = List.zipWithAll (fun (x y : Option Int) => x.getD 0 - y.getD 0) xs ys

                  Implementation of scalar multiplication by an integer on IntList.

                  Equations
                  Instances For
                    theorem Lean.Omega.IntList.smul_def (xs : Lean.Omega.IntList) (i : Int) :
                    i * xs = List.map (fun (x : Int) => i * x) xs
                    @[simp]
                    theorem Lean.Omega.IntList.smul_get (xs : Lean.Omega.IntList) (a : Int) (i : Nat) :
                    (a * xs).get i = a * xs.get i
                    @[simp]
                    theorem Lean.Omega.IntList.smul_nil {i : Int} :
                    i * [] = []
                    @[simp]
                    theorem Lean.Omega.IntList.smul_cons {x : Int} {xs : List Int} {i : Int} :
                    i * (x :: xs) = i * x :: i * xs

                    A linear combination of two IntLists.

                    Equations
                    Instances For
                      @[simp]
                      theorem Lean.Omega.IntList.mul_smul_left {i : Int} {xs : Lean.Omega.IntList} {ys : Lean.Omega.IntList} :
                      i * xs * ys = i * (xs * ys)

                      The sum of the entries of an IntList.

                      Equations
                      Instances For
                        theorem Lean.Omega.IntList.sum_add (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) :
                        (xs + ys).sum = xs.sum + ys.sum
                        @[simp]
                        theorem Lean.Omega.IntList.sum_neg (xs : Lean.Omega.IntList) :
                        (-xs).sum = -xs.sum
                        @[simp]
                        theorem Lean.Omega.IntList.sum_smul (i : Int) (xs : Lean.Omega.IntList) :
                        (i * xs).sum = i * xs.sum

                        The dot product of two IntLists.

                        Equations
                        • xs.dot ys = (xs * ys).sum
                        Instances For
                          @[simp]
                          @[simp]
                          theorem Lean.Omega.IntList.dot_cons₂ {x : Int} {xs : List Int} {y : Int} {ys : List Int} :
                          @[simp]
                          theorem Lean.Omega.IntList.dot_set_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Nat) (z : Int) :
                          (xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i
                          theorem Lean.Omega.IntList.dot_distrib_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (zs : Lean.Omega.IntList) :
                          (xs + ys).dot zs = xs.dot zs + ys.dot zs
                          @[simp]
                          theorem Lean.Omega.IntList.dot_neg_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) :
                          (-xs).dot ys = -xs.dot ys
                          @[simp]
                          theorem Lean.Omega.IntList.dot_smul_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) (i : Int) :
                          (i * xs).dot ys = i * xs.dot ys
                          theorem Lean.Omega.IntList.dot_of_left_zero {xs : Lean.Omega.IntList} {ys : Lean.Omega.IntList} (w : ∀ (x : Int), x xsx = 0) :
                          xs.dot ys = 0

                          Division of an IntList by a integer.

                          Equations
                          Instances For

                            The gcd of the absolute values of the entries of an IntList.

                            Equations
                            Instances For
                              @[simp]
                              theorem Lean.Omega.IntList.gcd_dvd (xs : Lean.Omega.IntList) {a : Int} (m : a xs) :
                              xs.gcd a
                              theorem Lean.Omega.IntList.dvd_gcd (xs : Lean.Omega.IntList) (c : Nat) (w : ∀ {a : Int}, a xsc a) :
                              c xs.gcd
                              theorem Lean.Omega.IntList.gcd_eq_iff {xs : Lean.Omega.IntList} {g : Nat} :
                              xs.gcd = g (∀ {a : Int}, a xsg a) ∀ (c : Nat), (∀ {a : Int}, a xsc a)c g
                              @[simp]
                              theorem Lean.Omega.IntList.gcd_eq_zero {xs : Lean.Omega.IntList} :
                              xs.gcd = 0 ∀ (x : Int), x xsx = 0
                              @[simp]
                              theorem Lean.Omega.IntList.dot_mod_gcd_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) :
                              xs.dot ys % xs.gcd = 0
                              theorem Lean.Omega.IntList.dot_eq_zero_of_left_eq_zero {xs : Lean.Omega.IntList} {ys : Lean.Omega.IntList} (h : ∀ (x : Int), x xsx = 0) :
                              xs.dot ys = 0
                              theorem Lean.Omega.IntList.dot_sdiv_left (xs : Lean.Omega.IntList) (ys : Lean.Omega.IntList) {d : Int} (h : d xs.gcd) :
                              (xs.sdiv d).dot ys = xs.dot ys / d
                              @[reducible, inline]

                              Apply "balanced mod" to each entry in an IntList.

                              Equations
                              Instances For
                                @[reducible, inline]

                                The difference between the balanced mod of a dot product, and the dot product with balanced mod applied to each entry of the left factor.

                                Equations
                                Instances For