Polynomial-time finite table operations

Programs construct finite tables as ordinary functions and use ordinary application and update. The certificates store the complete table using encPi and the existing list machinery. The index type is fixed independently of the input; values need not be finite or inhabited. The plain construction, access and update rules are proved in the internal primitives module and re-exported here; the polytime tactic applies the computed-index rules. This module adds the tidy forms of construction and fixed-index access that tidy proofs still use.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.ofFn, .pi: construct fixed finite families.
• Turing.MultiTapeTM.ComputableInPolyTime.pi_apply, .pi_update: fixed-index access.
• Turing.MultiTapeTM.ComputableInPolyTime.pi_apply', .pi_update': computed-index access.

References

Adapts Computability/Probabilistic/Pi.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to plain polynomial time.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.ofFn {α Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} {count : ℕ} {values : α → Fin count → Value} (hvalues : ∀ (i : Fin count), ComputableTidilyInPolyTime (fun (a : α) => values a i) input enc) : ComputableTidilyInPolyTime (fun (a : α) => List.ofFn (values a)) input (encList enc)

Construct a list of a fixed number of efficiently computed entries.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.pi {α Index Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} [Fintype Index] {values : α → Index → Value} (hvalues : ∀ (i : Index), ComputableTidilyInPolyTime (fun (a : α) => values a i) input enc) : ComputableTidilyInPolyTime values input (encPi enc)

Construct a table by computing each entry, retaining the original input in each computation.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.pi_apply {Index Value : Type} [Fintype Index] (enc : Value ↪ List Bool) (i : Index) : ComputableTidilyInPolyTime (fun (values : Index → Value) => values i) (encPi enc) enc

Read a fixed entry, charging for the stored prefix without requiring a default value.