Documentation

Init.Omega.Coeffs

Coeffs as a wrapper for IntList #

Currently omega uses a dense representation for coefficients. However, we can swap this out for a sparse representation.

This file sets up Coeffs as a type synonym for IntList, and abbreviations for the functions in the IntList namespace which we need to use in the omega algorithm.

There is an equivalent file setting up Coeffs as a type synonym for AssocList Nat Int, currently in a private branch. Not all the theorems about the algebraic operations on that representation have been proved yet. When they are ready, we can replace the implementation in omega simply by importing Init.Omega.IntDict instead of Init.Omega.IntList.

For small problems, the sparse representation is actually slightly slower, so it is not urgent to make this replacement.

@[inline, reducible]

Type synonym for IntList := List Int.

Equations
Instances For
    @[inline, reducible]

    Identity, turning Coeffs into List Int.

    Equations
    Instances For
      @[inline, reducible]

      Identity, turning List Int into Coeffs.

      Equations
      Instances For
        @[inline, reducible]

        Are the coefficients all zero?

        Equations
        Instances For
          @[inline, reducible]

          Shim for IntList.set.

          Equations
          Instances For
            @[inline, reducible]

            Shim for IntList.get.

            Equations
            Instances For
              @[inline, reducible]

              Shim for IntList.gcd.

              Equations
              Instances For
                @[inline, reducible]

                Shim for IntList.smul.

                Equations
                Instances For
                  @[inline, reducible]

                  Shim for IntList.sdiv.

                  Equations
                  Instances For
                    @[inline, reducible]

                    Shim for IntList.dot.

                    Equations
                    Instances For
                      @[inline, reducible]

                      Shim for IntList.add.

                      Equations
                      Instances For
                        @[inline, reducible]

                        Shim for IntList.sub.

                        Equations
                        Instances For
                          @[inline, reducible]

                          Shim for IntList.neg.

                          Equations
                          Instances For
                            @[inline, reducible]

                            Shim for IntList.combo.

                            Equations
                            Instances For
                              @[inline, reducible]

                              Shim for List.length.

                              Equations
                              Instances For
                                @[inline, reducible]

                                Shim for IntList.leading.

                                Equations
                                Instances For
                                  @[inline, reducible]

                                  Shim for List.map.

                                  Equations
                                  Instances For
                                    @[inline, reducible]

                                    Shim for .enum.find?.

                                    Equations
                                    Instances For
                                      @[inline, reducible]

                                      Shim for IntList.bmod.

                                      Equations
                                      Instances For