Compositional polynomial resource bounds

growth_poly proves Turing.MultiTapeTM.PolyBounded size cost by the existing constant, input-size, addition, multiplication and fixed-power rules, together with logarithm, square root, maximum, truncated subtraction and division bounds. It also accepts Cslib.PolynomiallyBounded goals through the existing fun_prop rules.

The leaves come from the local context:

• PolyBounded hypotheses, also inside conjunctions and inside definitions that unfold to them, such as a native certificate's IsPolynomial;
• certificates whose output length is polynomially bounded, such as ComputableInPolyTime f encIn encOut; with encOut = encUnary the value f a itself is bounded, and with encOut = encBits the length of the word f a;
• Cslib.PolynomiallyBounded p hypotheses, or fun_prop facts, applied as p (u a);
• a PolyBounded size' v hypothesis at another size applied as v (g a), which leaves the substitution PolyBounded size (fun a => size' (g a)).

A certificate supplies a leaf only through a lemma, and this module does not import those lemmas, so that it stays below the machine layers. For each kind of certificate the proof uses, import the module that proves its lemma (names relative to CslibFrontier.Computability.Machines.Turing, the last one to CslibFrontier.Computability):

• ComputableInPolyTime, output length: MultiTape.Internal.PolyTimePrimitives, which MultiTape.Complexity.PolyTime.Basic imports;
• ComputableInPolyTime with encUnary output, the value: MultiTape.Internal.PolyTimeLoops, which MultiTape.Complexity.PolyTime.Fold imports;
• ComputableInPolySpace: MultiTape.Complexity.PolySpace.Plain;
• ComputableInLogSpace: MultiTape.Complexity.LogSpace;
• DegreeBounded: MultiTape.ResourceBounds.Degree;
• Cslib.GenericRAM.NativeCertificate: GenericRAM.Native.Certificate.

When a certificate in the context gives no leaf because its lemma is not imported, the failure message names the module to import.

Local let values, and definitions whose bodies are arithmetic, are unfolded. The tactic proves polynomial growth only. Word admission, exact time bounds and signed overflow conditions remain separate obligations, and it does not guess an intermediate size measure: a substitution needs the outer bound as a fact. Each step follows the syntax of the bound without backtracking, so a goal outside these rules fails at once and names the term it could not bound.

Main declarations

• Turing.MultiTapeTM.PolyBounded.log, sqrt, max, sub, div: further closure rules.
• Turing.MultiTapeTM.PolyBounded.of_polynomiallyBounded_comp: substitution into a polynomially bounded function of one natural number.
• growth_poly, growth_poly [h₁, h₂]: prove polynomial growth from these rules and the local context, with extra facts h₁ and h₂.
• Cslib.Tactic.GrowthPoly.certificateLemmas: the certificate lemmas the tactic uses, with the modules that prove them.

The closure layer adapts Samuel Schlesinger's existing polynomial-bound API. The input-size logarithm and square-root rules and the first growth_poly tactic are by Erik Demaine.

theorem Turing.MultiTapeTM.PolyBounded.log {α : Type u_1} {size u : α → ℕ} (b : ℕ) (hu : PolyBounded size u) : PolyBounded size fun (a : α) => Nat.log b (u a)

Natural logarithms preserve polynomial growth in any input-size measure.

theorem Turing.MultiTapeTM.PolyBounded.sqrt {α : Type u_1} {size u : α → ℕ} (hu : PolyBounded size u) : PolyBounded size fun (a : α) => (u a).sqrt

Natural square roots preserve polynomial growth in any input-size measure.

theorem Turing.MultiTapeTM.PolyBounded.max {α : Type u_1} {size u v : α → ℕ} (hu : PolyBounded size u) (hv : PolyBounded size v) : PolyBounded size fun (a : α) => Max.max (u a) (v a)

The maximum of two polynomially bounded functions is polynomially bounded.

theorem Turing.MultiTapeTM.PolyBounded.sub {α : Type u_1} {size u : α → ℕ} (hu : PolyBounded size u) (v : α → ℕ) : PolyBounded size fun (a : α) => u a - v a

Truncated subtraction preserves a polynomial bound on its first argument.

theorem Turing.MultiTapeTM.PolyBounded.div {α : Type u_1} {size u : α → ℕ} (hu : PolyBounded size u) (v : α → ℕ) : PolyBounded size fun (a : α) => u a / v a

Natural division preserves a polynomial bound on its dividend.

theorem Turing.MultiTapeTM.PolyBounded.of_polynomiallyBounded_comp {α : Type u_1} {size u : α → ℕ} {p : ℕ → ℕ} (hp : Cslib.PolynomiallyBounded p) (hu : PolyBounded size u) : PolyBounded size fun (a : α) => p (u a)

Substitute a polynomially bounded argument into a polynomially bounded function of one natural number.

def growthPoly : Lean.ParserDescr

growth_poly proves Turing.MultiTapeTM.PolyBounded size cost by the closure rules for constants, the input size, +, *, fixed powers, Nat.log, Nat.sqrt, max, truncated - and /. The leaves come from local PolyBounded facts, also inside conjunctions and definitions that unfold to them; from local certificates, through their output-length bound; and from local Cslib.PolynomiallyBounded functions or PolyBounded facts at another size, applied to a bounded argument. growth_poly [h₁, h₂] adds the facts h₁ and h₂.

A certificate gives a leaf only when the module proving its bound is imported; the module docstring lists them, for example MultiTape.Internal.PolyTimePrimitives for the output length of ComputableInPolyTime. When a certificate in the context gives no leaf for this reason, the failure names the module to import.

Local let values and arithmetic definitions are unfolded. The search follows the syntax of the bound without backtracking: a goal outside these rules fails at once and names the term it could not bound. Cslib.PolynomiallyBounded goals go to fun_prop.

structure Cslib.Tactic.GrowthPoly.CertificateLemma : Type

A lemma from a certificate to a PolyBounded fact or to another certificate.

• name : Lean.Name

  The lemma, applied to the local hypotheses whose head it matches when it is in scope.

• head : Lean.Name

  The head constant of the certificate it takes, its last explicit hypothesis.

• outEnc : Option Lean.Name

  The output encoding, the certificate's last argument, that the lemma requires, if any.

• module : Lean.Name

  The module proving the lemma, named when the lemma is not in scope.

def Cslib.Tactic.GrowthPoly.certificateLemmas : List CertificateLemma

The certificate lemmas, applied when they are in scope. This module does not import them, which would make it depend on the machine layers. A lemma that requires an output encoding comes before the general lemma with the same head, and its module imports that lemma's module. The drift check in the PolynomialGrowth test checks that each lemma is proved in its module.