Polynomial-time finite case analysis

An efficiently computed finite tag selects a branch retaining the original input. Both the tag encoding and output encoding are arbitrary. The finite type and all branch machines are fixed independently of runtime input; this does not enumerate a family whose size grows with the input.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.finite_cases, Turing.MultiTapeTM.ComputableTidilyInPolyTime.finite_cases: finite dispatch with captured input.

References

Adapts Computability/Probabilistic/Finite.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finite_cases {α β Tag : Type} [Finite Tag] {input : α ↪ List Bool} {output : β ↪ List Bool} {tagEncoding : Tag ↪ List Bool} {tag : α → Tag} {branch : Tag → α → β} (htag : ComputableInPolyTime tag input tagEncoding) (hbranch : ∀ (choice : Tag), ComputableInPolyTime (branch choice) input output) : ComputableInPolyTime (fun (a : α) => branch (tag a) a) input output

A fixed finite tag selects a certified branch, charging the tag and captured input. Neither the tag nor the result type requires a default inhabitant.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.finite_cases {α β Tag : Type} [Finite Tag] {input : α ↪ List Bool} {output : β ↪ List Bool} {tagEncoding : Tag ↪ List Bool} {tag : α → Tag} {branch : Tag → α → β} (htag : ComputableTidilyInPolyTime tag input tagEncoding) (hbranch : ∀ (choice : Tag), ComputableTidilyInPolyTime (branch choice) input output) : ComputableTidilyInPolyTime (fun (a : α) => branch (tag a) a) input output

A fixed finite tag selects a certified branch, charging the tag and captured input. Neither the tag nor the result type requires a default inhabitant.