Basic polynomial-time rules

Polynomial-time counterparts of Christian Reitwiessner's degree-bounded operations, and Boolean rules for fun_prop.

Main results

• Turing.MultiTapeTM.PolyBounded.exists_polynomial: express a resource bound by a polynomial.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.exists_degree: polynomial-time functions admit explicit time and output degrees.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.polyBounded: a computed unary value bounds resources polynomially in the original input encoding.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_enc_eq: reuse identical encoded outputs.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.encoded, .unframe, .dropFrame: compose encoded values and total frame parsing without requiring an inverse for an encoding.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_finite: functions on finite domains.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.fstWithEncoding, .sndWithEncoding: projections that compose with a known encoding conversion.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_eq, .beq: equality for fixed encodings.

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_and', .decide_and, .cond, .ite_decide: compound guards and conditionals with fixed intermediate Boolean encodings.

• Turing.MultiTapeTM.ComputableInPolyTime.decide_or, .bool_or', .bne, .decide_ne: disjunction and inequality for plain certificates.

theorem Turing.MultiTapeTM.PolyBounded.exists_polynomial {α : Type u_1} {size u : α → ℕ} (h : PolyBounded size u) : ∃ (p : Polynomial ℕ), ∀ (a : α), u a ≤ Polynomial.eval (size a) p

A polynomially bounded resource admits a polynomial upper bound at every input size.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.polyBounded {α : Type} {encA : α ↪ List Bool} {f : α → ℕ} (hf : ComputableTidilyInPolyTime f encA encUnary) : PolyBounded (fun (x : α) => (encA x).length) f

An efficiently computed unary value is polynomially bounded in the original encoded input. This supplies input-dependent resource bounds without exposing their polynomial coefficients.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.trans {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {δ : Type} {encD : δ ↪ List Bool} {f : α → β} {g : β → δ} (hf : ComputableTidilyInPolyTime f encA encB) (hg : ComputableTidilyInPolyTime g encB encD) : ComputableTidilyInPolyTime (fun (x : α) => g (f x)) encA encD

Compose in execution order. This also lets fun_prop infer the intermediate encoding from the inner function when it cannot be inferred from the outer function.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.fst' {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {δ : Type} {encD : δ ↪ List Bool} {f : α → β × δ} (hf : ComputableTidilyInPolyTime f encA (encPair encB encD)) : ComputableTidilyInPolyTime (fun (x : α) => (f x).1) encA encB

Project the first component of a polynomial-time pair-valued function.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.snd' {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {δ : Type} {encD : δ ↪ List Bool} {f : α → β × δ} (hf : ComputableTidilyInPolyTime f encA (encPair encB encD)) : ComputableTidilyInPolyTime (fun (x : α) => (f x).2) encA encD

Project the second component of a polynomial-time pair-valued function.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.fstWithEncoding {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {γ : Type} {encC : γ ↪ List Bool} {output : α ↪ List Bool} {f : γ → α × β} (hf : ComputableTidilyInPolyTime f encC (encPair encA encB)) (h : ComputableTidilyInPolyTime (fun (a : α) => a) encA output) : ComputableTidilyInPolyTime (fun (p : γ) => (f p).1) encC output

Project a first component and convert its encoding. Certifying the pair-valued function first determines the source encoding before automation searches for the conversion certificate.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sndWithEncoding {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {γ : Type} {encC : γ ↪ List Bool} {output : β ↪ List Bool} {f : γ → α × β} (hf : ComputableTidilyInPolyTime f encC (encPair encA encB)) (h : ComputableTidilyInPolyTime (fun (a : β) => a) encB output) : ComputableTidilyInPolyTime (fun (p : γ) => (f p).2) encC output

Project a second component and convert its encoding. The pair certificate fixes the source encoding; the conversion certificate supplies the efficient change of representation.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.exists_degree {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {f : α → β} (hf : ComputableTidilyInPolyTime f encA encB) : ∃ (d : ℕ) (e : ℕ), ComputableTidilyInDegree f encA encB d e

Every polynomial-time function admits explicit time and output degrees.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_enc_eq {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {δ : Type} {encD : δ ↪ List Bool} {f : α → β} {g : α → δ} (hf : ComputableTidilyInPolyTime f encA encB) (h : ∀ (a : α), encD (g a) = encB (f a)) : ComputableTidilyInPolyTime g encA encD

Reuse a computation when the new function emits the same encoded output word.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.encode {α : Type} (enc : α ↪ List Bool) : ComputableTidilyInPolyTime (⇑enc) enc encBits

Expose an already encoded value as a raw word. No inverse for the encoding is required.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.encoded {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {f : α → β} (hf : ComputableTidilyInPolyTime f encA encB) : ComputableTidilyInPolyTime (fun (a : α) => encB (f a)) encA encBits

Compute a value and expose its representation, inferring that representation from the supplied certificate before composing.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unframe : ComputableTidilyInPolyTime MultiTapeTM.unframe encBits encBits

Read the first frame from any raw word, including malformed encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.dropFrame : ComputableTidilyInPolyTime MultiTapeTM.dropFrame encBits encBits

Drop the first frame from any raw word, including malformed encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_finite {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [Finite α] (f : α → β) : ComputableTidilyInPolyTime f encA encB

Every function on a finite domain is polynomial-time for any fixed encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_not : ComputableTidilyInPolyTime not encBool encBool

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_and : ComputableTidilyInPolyTime (fun (p : Bool × Bool) => p.1 && p.2) (encPair encBool encBool) encBool

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_and' {α : Type} {encA : α ↪ List Bool} {left right : α → Bool} (hleft : ComputableTidilyInPolyTime left encA encBool) (hright : ComputableTidilyInPolyTime right encA encBool) : ComputableTidilyInPolyTime (fun (a : α) => left a && right a) encA encBool

Conjoin computed guards, fixing both intermediate Boolean encodings.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_or : ComputableTidilyInPolyTime (fun (p : Bool × Bool) => p.1 || p.2) (encPair encBool encBool) encBool

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_xor : ComputableTidilyInPolyTime (fun (p : Bool × Bool) => p.1 ^^ p.2) (encPair encBool encBool) encBool

Exclusive-or is a finite Boolean computation.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_and {α : Type} {encA : α ↪ List Bool} {left right : α → Prop} [(a : α) → Decidable (left a)] [(a : α) → Decidable (right a)] (hleft : ComputableTidilyInPolyTime (fun (a : α) => decide (left a)) encA encBool) (hright : ComputableTidilyInPolyTime (fun (a : α) => decide (right a)) encA encBool) : ComputableTidilyInPolyTime (fun (a : α) => decide (left a ∧ right a)) encA encBool

Conjunction of efficiently decidable propositions uses the standard Boolean encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_or {α : Type} {encA : α ↪ List Bool} {left right : α → Prop} [(a : α) → Decidable (left a)] [(a : α) → Decidable (right a)] (hleft : ComputableTidilyInPolyTime (fun (a : α) => decide (left a)) encA encBool) (hright : ComputableTidilyInPolyTime (fun (a : α) => decide (right a)) encA encBool) : ComputableTidilyInPolyTime (fun (a : α) => decide (left a ∨ right a)) encA encBool

Disjunction of efficiently decidable propositions uses the standard Boolean encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.cond {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {condition : α → Bool} {yes no : α → β} (hcondition : ComputableTidilyInPolyTime condition encA encBool) (hyes : ComputableTidilyInPolyTime yes encA encB) (hno : ComputableTidilyInPolyTime no encA encB) : ComputableTidilyInPolyTime (fun (a : α) => if condition a = true then yes a else no a) encA encB

A Boolean conditional fixes the guard encoding before automation synthesizes its proof.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.ite_decide {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {condition : α → Prop} [(a : α) → Decidable (condition a)] {yes no : α → β} (hcondition : ComputableTidilyInPolyTime (fun (a : α) => decide (condition a)) encA encBool) (hyes : ComputableTidilyInPolyTime yes encA encB) (hno : ComputableTidilyInPolyTime no encA encB) : ComputableTidilyInPolyTime (fun (a : α) => if condition a then yes a else no a) encA encB

A proposition-valued conditional computes its decision in the standard Boolean encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.bool_beq : ComputableTidilyInPolyTime (fun (p : Bool × Bool) => p.1 == p.2) (encPair encBool encBool) encBool

Comparing two Boolean values is a finite-domain computation.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_eq {α : Type} [DecidableEq α] (enc : α ↪ List Bool) : ComputableTidilyInPolyTime (fun (p : α × α) => decide (p.1 = p.2)) (encPair enc enc) encBool

Equality is polynomial-time for any encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_eq' {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [DecidableEq β] {left right : α → β} (hleft : ComputableTidilyInPolyTime left encA encB) (hright : ComputableTidilyInPolyTime right encA encB) : ComputableTidilyInPolyTime (fun (x : α) => decide (left x = right x)) encA encBool

Compare computed values for equality, inferring their common encoding from the arguments.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.beq {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [BEq β] [LawfulBEq β] {left right : α → β} (hleft : ComputableTidilyInPolyTime left encA encB) (hright : ComputableTidilyInPolyTime right encA encB) : ComputableTidilyInPolyTime (fun (x : α) => left x == right x) encA encBool

Lawful Boolean equality compares computed values through their common encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_ne {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [DecidableEq β] {left right : α → β} (hleft : ComputableTidilyInPolyTime left encA encB) (hright : ComputableTidilyInPolyTime right encA encB) : ComputableTidilyInPolyTime (fun (x : α) => decide (left x ≠ right x)) encA encBool

Compare two computed values using their common encoding.

Plain polynomial-time automation

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_or {α : Type} {encA : α ↪ List Bool} {left right : α → Prop} [(a : α) → Decidable (left a)] [(a : α) → Decidable (right a)] (hleft : ComputableInPolyTime (fun (a : α) => decide (left a)) encA encBool) (hright : ComputableInPolyTime (fun (a : α) => decide (right a)) encA encBool) : ComputableInPolyTime (fun (a : α) => decide (left a ∨ right a)) encA encBool

Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_or for plain certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bool_or' {α : Type} {encA : α ↪ List Bool} {left right : α → Bool} (hleft : ComputableInPolyTime left encA encBool) (hright : ComputableInPolyTime right encA encBool) : ComputableInPolyTime (fun (a : α) => left a || right a) encA encBool

Disjoin computed guards, fixing both intermediate Boolean encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bne {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [BEq β] [LawfulBEq β] {left right : α → β} (hleft : ComputableInPolyTime left encA encB) (hright : ComputableInPolyTime right encA encB) : ComputableInPolyTime (fun (x : α) => left x != right x) encA encBool

Lawful Boolean inequality compares computed values through their common encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_ne {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} [DecidableEq β] {left right : α → β} (hleft : ComputableInPolyTime left encA encB) (hright : ComputableInPolyTime right encA encB) : ComputableInPolyTime (fun (x : α) => decide (left x ≠ right x)) encA encBool

Compare two computed values using their common encoding.