Equality of unary naturals in polynomial time

Turing.MultiTapeTM.ComputableInPolyTime.decide_eq' compares two computed values through a common encoding inferred from its operands. For natural numbers that encoding is ambiguous (encUnary or encNat), so proof search cannot certify guards such as if word.length = n then … else …, where both sides are unary. This module fixes the unary encoding, so that fun_prop and polytime certify such guards with plain rules, together with Turing.MultiTapeTM.ComputableInPolyTime.ite_decide.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.unary_eq': compare computed unary naturals.
• Turing.MultiTapeTM.ComputableInPolyTime.unary_beq': Boolean equality of computed unary naturals.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_eq' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => decide (left a = right a)) input encBool

Compare computed unary naturals for equality, with both operand encodings fixed.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_beq' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encUnary) (hright : ComputableInPolyTime right input encUnary) : ComputableInPolyTime (fun (a : α) => left a == right a) input encBool

Compare computed unary naturals with Boolean equality, with both operand encodings fixed.