Synthesizing polynomial-time certificates

Adapted from the cslib crypto branch: named certificates are tried before their implementations are unfolded. fun_prop handles composition; Aesop chooses loop rules and uses local growth contracts. Plain and internal tidy goals use separate rules, with fixed machines and polynomial bounds across all encoded inputs. Plain search applies plain statements directly; it does not lower a goal or restate its hypotheses tidily. Unknown algorithms still require certificates.

Main definitions

• polytime: prove a polynomial-time certificate using the PolyTime Aesop rule set.

References

Adapted from Cslib/Tactic/PolyTime.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8; deterministic search consumes the canonical plain calculus.

theorem Cslib.Tactic.PolyTime.Internal.plainBitsCons {α : Type} {encIn : α ↪ List Bool} {f : α → Bool} {g : α → List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn Turing.MultiTapeTM.encBool) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a :: g a) encIn Turing.MultiTapeTM.encBits

Prepend a computed bit with both intermediate raw encodings fixed for the tactic.

theorem Cslib.Tactic.PolyTime.Internal.plainListAppend {α β : Type} {encIn : α ↪ List Bool} {enc : β ↪ List Bool} {f g : α → List β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn (Turing.MultiTapeTM.encList enc)) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn (Turing.MultiTapeTM.encList enc)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a ++ g a) encIn (Turing.MultiTapeTM.encList enc)

Append computed framed lists with their element encoding fixed for the tactic.

theorem Cslib.Tactic.PolyTime.Internal.plainListCons {α β : Type} {encIn : α ↪ List Bool} {enc : β ↪ List Bool} {f : α → β} {g : α → List β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn enc) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn (Turing.MultiTapeTM.encList enc)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a :: g a) encIn (Turing.MultiTapeTM.encList enc)

Prepend a computed element to a framed list with its element encoding fixed.

def Cslib.Tactic.PolyTime.Internal.applyLocalCertificates : Aesop.RuleTac

Retain Aesop's local application alternatives and priority, excluding only rules which would start raw search from a plain goal. Adapted from Aesop.BuiltinRules.applyHyps (Jannis Limperg).

def Cslib.Tactic.PolyTime.Internal.withPlainRuleMemo (action : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Reuse only global classification answers across one invocation. Rule tables, certificate lookup, matching and local evidence are not projected or cached by this wrapper.

def Cslib.Tactic.PolyTime.Internal.withPlainRuleCache (action : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Apply the deterministic boundary using the current tables and scoped classification memo. Explicit raw construction entries and all named-certificate metadata retain their old policy.

def Cslib.Tactic.PolyTime.Internal.funPropWithPlainBoundary (maxSteps : ℕ) : Lean.Elab.Tactic.TacticM Unit

Shared compositional backend with a fresh alias-aware raw-premise boundary. The standard assumption discharger and ordinary transition depth are retained; callers keep their step limit. Consumers can reuse the same boundary for nested plain deterministic goals.

theorem Cslib.Tactic.PolyTime.bool_not_rule {α : Type} {input : α ↪ List Bool} {guard : α → Bool} (hguard : Turing.MultiTapeTM.ComputableTidilyInPolyTime guard input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => !guard a) input Turing.MultiTapeTM.encBool

Expose a negated guard to loop rules when compositional proof search needs their help.

theorem Cslib.Tactic.PolyTime.foldl_bits_rule {γ β : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List Bool} {init : γ → β} {step : β → Bool → β} (hlist : Turing.MultiTapeTM.ComputableTidilyInPolyTime list encIn Turing.MultiTapeTM.encBits) (hinit : Turing.MultiTapeTM.ComputableTidilyInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : β × Bool) => step pair.1 pair.2) (Turing.MultiTapeTM.encPair encB Turing.MultiTapeTM.encBool) encB) {growth : ℕ} (hgrowth : ∀ (state : β), (encB (step state false)).length ≤ (encB state).length + growth ∧ (encB (step state true)).length ≤ (encB state).length + growth) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Fix a raw bit list's encoding and expose the two growth cases before proof search.

theorem Cslib.Tactic.PolyTime.foldl_list_rule {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : Turing.MultiTapeTM.ComputableTidilyInPolyTime list encIn (Turing.MultiTapeTM.encList encA)) (hinit : Turing.MultiTapeTM.ComputableTidilyInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : β × α) => step pair.1 pair.2) (Turing.MultiTapeTM.encPair encB encA) encB) {growth : ℕ} (hgrowth : ∀ (state : β) (value : α), (encB (step state value)).length ≤ (encB state).length + growth) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Fix a framed list's encoding before proof search infers the element encoding.

theorem Cslib.Tactic.PolyTime.Internal.plain_foldl_bits_rule {γ β : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List Bool} {init : γ → β} {step : β → Bool → β} (hlist : Turing.MultiTapeTM.ComputableInPolyTime list encIn Turing.MultiTapeTM.encBits) (hinit : Turing.MultiTapeTM.ComputableInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : β × Bool) => step pair.1 pair.2) (Turing.MultiTapeTM.encPair encB Turing.MultiTapeTM.encBool) encB) {growth : ℕ} (hgrowth : ∀ (state : β), (encB (step state false)).length ≤ (encB state).length + growth ∧ (encB (step state true)).length ≤ (encB state).length + growth) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Fix a raw bit list's encoding and expose the two growth cases before proof search.

theorem Cslib.Tactic.PolyTime.Internal.plain_foldl_list_rule {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : Turing.MultiTapeTM.ComputableInPolyTime list encIn (Turing.MultiTapeTM.encList encA)) (hinit : Turing.MultiTapeTM.ComputableInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : β × α) => step pair.1 pair.2) (Turing.MultiTapeTM.encPair encB encA) encB) {growth : ℕ} (hgrowth : ∀ (state : β) (value : α), (encB (step state value)).length ≤ (encB state).length + growth) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Fix a framed list's encoding before proof search infers the element encoding.

theorem Cslib.Tactic.PolyTime.Internal.plainIterate {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : Turing.MultiTapeTM.ComputableInPolyTime count encIn Turing.MultiTapeTM.encUnary) (hinit : Turing.MultiTapeTM.ComputableInPolyTime init encIn encState) (hstep : Turing.MultiTapeTM.ComputableInPolyTime step encState encState) {growth : ℕ} (hgrowth : ∀ (state : β), (encState (step state)).length ≤ (encState state).length + growth) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState

The plain iteration rule retains the same constant additive growth contract.

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

Prove a polynomial-time certificate from known routines and controlled loop rules.