2.2. Polynomial Time🔗

ComputableInPolyTime f encIn encOut says that some multi-tape Turing machine with a binary alphabet and finitely many states computes f, reading encIn a and writing encOut (f a), within time and space bounded by polynomials in the length of encIn a. This is the notion that definitions and theorems use.

You rarely build machines. Closure rules for the usual operations are registered with fun_prop, so a function written with certified operations gets its certificate automatically:

example : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 * p.2 + 1)
    (encPair encNat encNat) encNat := by⊢ ComputableInPolyTime (fun p => p.1 * p.2 + 1) (encPair encNat encNat) encNat
  fun_propAll goals completed! 🐙

example : ComputableInPolyTime (fun l : List ℕ => l.map (· + 1))
    (encList encNat) (encList encNat) := by⊢ ComputableInPolyTime (fun l => List.map (fun x => x + 1) l) (encList encNat) (encList encNat)
  fun_propAll goals completed! 🐙

Loops whose body depends on the rest of the input, such as a filter that compares each element with another part of the input, need the polytime tactic, which chooses loop rules and composes certificates. Membership tests and their negations are certified too:

example : ComputableInPolyTime (fun p : List ℕ × ℕ => p.1.filter (· ≤ p.2))
    (encPair (encList encNat) encNat) (encList encNat) := by⊢ ComputableInPolyTime (fun p => List.filter (fun x => decide (x ≤ p.2)) p.1) (encPair (encList encNat) encNat)
  (encList encNat)
  polytimeAll goals completed! 🐙

example : ComputableInPolyTime
    (fun p : List ℕ × List ℕ => p.1.filter fun x => x ∉ p.2)
    (encPair (encList encNat) (encList encNat)) (encList encNat) := by⊢ ComputableInPolyTime (fun p => List.filter (fun x => decide (x ∉ p.2)) p.1) (encPair (encList encNat) (encList encNat))
  (encList encNat)
  polytimeAll goals completed! 🐙

Both tactics prove only the cost. That f computes what you intend is a separate proof.