Synthesizing polynomial-time proofs

polytime proves f ∈ FP, UnaryFn f, and FPPred p by composing existing machine-based closure theorems. It handles pairing, reversal, concatenation, slicing, bit access, unary arithmetic, comparisons, conditionals, and encoded bounded ranges. Local certificates support calls to supplied algorithms. Use polytime [program] to unfold a named program before proof search. Register reusable closure rules and algorithm certificates with @[polytime]. Number-valued certificates should use UnaryFn; local certificates written as membership of a unary encoding in FP are normalized automatically.

Iteration requires a certified step, an efficient unary count, and a constant bound on the number of bits added per step. More general loops can use iterate_mem_FP explicitly, with polytime discharging its efficiency premises and the caller proving the state-size invariant.

This adapts Samuel Schlesinger's Aesop rule-set and local-certificate approach from the CSLib crypto branch to Complexitylib's own FP predicates: https://github.com/SamuelSchlesinger/cslib/blob/b9f4e0dd39cd88231322b4225b2bf7ba6bc7e8a3/Cslib/Tactic/PolyTime.lean

The rules construct ordinary Lean proofs. Unknown algorithms need certificates; neither arbitrary Lean computation nor unrestricted iteration gets unit cost. The underlying Aesop rule set is ComplexityPolyTime.

theorem Complexity.Tactic.PolyTime.id_rule : (fun (x : List Bool) => x) ∈ FP

The identity in the lambda form used by closure rules.

theorem Complexity.Tactic.PolyTime.unary_rule {f : List Bool → ℕ} : (fun (x : List Bool) => List.replicate (f x) true) ∈ FP ↔ UnaryFn f

Normalize unary certificates before matching local hypotheses.

theorem Complexity.Tactic.PolyTime.reverse_rule {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => (f x).reverse) ∈ FP

Reversal after a certified computation.

theorem Complexity.Tactic.PolyTime.tail_rule {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => (f x).tail) ∈ FP

Dropping the first bit after a certified computation.

theorem Complexity.Tactic.PolyTime.fst_rule {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => pairFst (f x)) ∈ FP

First projection after a certified computation.

theorem Complexity.Tactic.PolyTime.snd_rule {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => pairSnd (f x)) ∈ FP

Second projection after a certified computation.

theorem Complexity.Tactic.PolyTime.cons_rule (bit : Bool) {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => bit :: f x) ∈ FP

Prepending a fixed bit after a certified computation.

theorem Complexity.Tactic.PolyTime.lenEqFlag_rule {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : (fun (x : List Bool) => Cobham.lenEqFlag (f x) (g x)) ∈ FP

The flag comparing the lengths of two certified words.

theorem Complexity.Tactic.PolyTime.comp_rule {g : List Bool → List Bool} (hg : g ∈ FP) {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => g (f x)) ∈ FP

Fix the called algorithm before searching for its argument's certificate.

theorem Complexity.Tactic.PolyTime.unary_comp_rule {g : List Bool → ℕ} (hg : UnaryFn g) {f : List Bool → List Bool} (hf : f ∈ FP) : UnaryFn fun (x : List Bool) => g (f x)

Specialize a certified number-valued function before choosing its argument.

theorem Complexity.Tactic.PolyTime.pred_comp_rule {p : List Bool → Prop} (hp : FPPred p) {f : List Bool → List Bool} (hf : f ∈ FP) : FPPred fun (x : List Bool) => p (f x)

Specialize a certified predicate before choosing its argument.

theorem Complexity.Tactic.PolyTime.iterate_rule {f init : List Bool → List Bool} {count : List Bool → ℕ} (hf : f ∈ FP) (hi : init ∈ FP) (hc : UnaryFn count) {growth : ℕ} (hgrowth : ∀ (w : List Bool), (f w).length ≤ w.length + growth) : (fun (z : List Bool) => f^[count z] (init z)) ∈ FP

A unary loop count and constant step growth suffice for polynomial iteration.

def Complexity.Tactic.PolyTime.tacticPolytime : Lean.ParserDescr

Prove polynomial-time membership from registered closure rules and local certificates.

Equations

• Complexity.Tactic.PolyTime.tacticPolytime = Lean.ParserDescr.node `Complexity.Tactic.PolyTime.tacticPolytime 1024 (Lean.ParserDescr.nonReservedSymbol "polytime" false)

def Complexity.Tactic.PolyTime.«tacticPolytime[_,,]» : Lean.ParserDescr

Prove polynomial-time membership from registered closure rules and local certificates.

Equations

• One or more equations did not get rendered due to their size.