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
          @[simp]
          @[simp]
          theorem Lean.Omega.IntList.get_cons_zero {x : Int} {xs : List Int} :
          get (x :: xs) 0 = x
          @[simp]
          theorem Lean.Omega.IntList.get_cons_succ {x : Int} {xs : List Int} {i : Nat} :
          get (x :: xs) (i + 1) = get xs i
          theorem Lean.Omega.IntList.get_map {f : IntInt} {i : Nat} {xs : IntList} (h : f 0 = 0) :
          get (List.map f xs) i = f (xs.get i)
          theorem Lean.Omega.IntList.get_of_length_le {i : Nat} {xs : IntList} (h : List.length xs i) :
          xs.get i = 0
          def Lean.Omega.IntList.set (xs : IntList) (i : Nat) (y : Int) :

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

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

              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 ys : 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 ys : IntList) (i : Nat) :
                      (xs + ys).get i = xs.get i + ys.get i
                      @[simp]
                      theorem Lean.Omega.IntList.add_nil (xs : IntList) :
                      xs + [] = xs
                      @[simp]
                      theorem Lean.Omega.IntList.nil_add (xs : IntList) :
                      [] + xs = xs
                      @[simp]
                      theorem Lean.Omega.IntList.cons_add_cons (x : Int) (xs : IntList) (y : Int) (ys : IntList) :
                      x :: xs + y :: ys = (x + y) :: (xs + ys)

                      Implementation of * on IntList.

                      Equations
                        Instances For
                          theorem Lean.Omega.IntList.mul_def (xs ys : IntList) :
                          xs * ys = List.zipWith (fun (x1 x2 : Int) => x1 * x2) xs ys
                          @[simp]
                          theorem Lean.Omega.IntList.mul_get (xs ys : IntList) (i : Nat) :
                          (xs * ys).get i = xs.get i * ys.get i
                          @[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 : IntList) :
                              -xs = List.map (fun (x : Int) => -x) xs
                              @[simp]
                              theorem Lean.Omega.IntList.neg_get (xs : IntList) (i : Nat) :
                              (-xs).get i = -xs.get i
                              @[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 ys : 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 : IntList) (i : Int) :
                                      i * xs = List.map (fun (x : Int) => i * x) xs
                                      @[simp]
                                      theorem Lean.Omega.IntList.smul_get (xs : IntList) (a : Int) (i : Nat) :
                                      (a * xs).get i = a * xs.get i
                                      @[simp]
                                      @[simp]
                                      theorem Lean.Omega.IntList.smul_cons {x : Int} {xs : List Int} {i : Int} :
                                      i * (x :: xs) = i * x :: i * xs
                                      def Lean.Omega.IntList.combo (a : Int) (xs : IntList) (b : Int) (ys : IntList) :

                                      A linear combination of two IntLists.

                                      Equations
                                        Instances For
                                          theorem Lean.Omega.IntList.combo_eq_smul_add_smul (a : Int) (xs : IntList) (b : Int) (ys : IntList) :
                                          combo a xs b ys = a * xs + b * ys
                                          theorem Lean.Omega.IntList.mul_distrib_left (xs ys zs : IntList) :
                                          (xs + ys) * zs = xs * zs + ys * zs
                                          theorem Lean.Omega.IntList.mul_neg_left (xs ys : IntList) :
                                          -xs * ys = -(xs * ys)
                                          theorem Lean.Omega.IntList.sub_eq_add_neg (xs ys : IntList) :
                                          xs - ys = xs + -ys
                                          @[simp]
                                          theorem Lean.Omega.IntList.mul_smul_left {i : Int} {xs ys : IntList} :
                                          i * xs * ys = i * (xs * ys)

                                          The sum of the entries of an IntList.

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

                                              The dot product of two IntLists.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Lean.Omega.IntList.dot_cons₂ {x : Int} {xs : List Int} {y : Int} {ys : List Int} :
                                                  dot (x :: xs) (y :: ys) = x * y + dot xs ys
                                                  @[simp]
                                                  theorem Lean.Omega.IntList.dot_set_left (xs ys : 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 ys zs : IntList) :
                                                  (xs + ys).dot zs = xs.dot zs + ys.dot zs
                                                  @[simp]
                                                  theorem Lean.Omega.IntList.dot_neg_left (xs ys : IntList) :
                                                  (-xs).dot ys = -xs.dot ys
                                                  @[simp]
                                                  theorem Lean.Omega.IntList.dot_smul_left (xs ys : IntList) (i : Int) :
                                                  (i * xs).dot ys = i * xs.dot ys
                                                  theorem Lean.Omega.IntList.dot_of_left_zero {xs ys : IntList} (w : ∀ (x : Int), x xsx = 0) :
                                                  xs.dot ys = 0

                                                  Division of an IntList by a integer.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      @[simp]
                                                      theorem Lean.Omega.IntList.sdiv_cons {x : Int} {xs : List Int} {g : Int} :
                                                      sdiv (x :: xs) g = x / g :: sdiv xs g

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

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Lean.Omega.IntList.gcd_cons {x : Int} {xs : List Int} :
                                                          gcd (x :: xs) = x.natAbs.gcd (gcd xs)
                                                          theorem Lean.Omega.IntList.gcd_cons_div_left {x : Int} {xs : List Int} :
                                                          (gcd (x :: xs)) x
                                                          theorem Lean.Omega.IntList.gcd_cons_div_right' {x : Int} {xs : List Int} :
                                                          (gcd (x :: xs)) (gcd xs)
                                                          theorem Lean.Omega.IntList.gcd_dvd (xs : IntList) {a : Int} (m : a xs) :
                                                          xs.gcd a
                                                          theorem Lean.Omega.IntList.dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a xsc a) :
                                                          c xs.gcd
                                                          theorem Lean.Omega.IntList.gcd_eq_iff {xs : 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 : IntList} :
                                                          xs.gcd = 0 ∀ (x : Int), x xsx = 0
                                                          @[simp]
                                                          theorem Lean.Omega.IntList.dot_mod_gcd_left (xs ys : IntList) :
                                                          xs.dot ys % xs.gcd = 0
                                                          theorem Lean.Omega.IntList.dot_eq_zero_of_left_eq_zero {xs ys : IntList} (h : ∀ (x : Int), x xsx = 0) :
                                                          xs.dot ys = 0
                                                          @[simp]
                                                          theorem Lean.Omega.IntList.dot_sdiv_left (xs ys : 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