Polynomial-time membership tests

Reduction maps and verifiers test membership as they are written on paper, for example keeping the pairs (u, v) with (u, v) ∉ G.2. fun_prop already certifies decide of conjunctions, disjunctions, equalities and disequalities (Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_and and its neighbours). This file adds negation and membership of a computed value in a computed list, so such tests need no rewriting into Boolean operations before fun_prop or polytime runs. Membership is decided by scanning the list for an equal element (Turing.MultiTapeTM.ComputableTidilyInPolyTime.anyWithInput).

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_not: negating a decided proposition.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_mem: membership in a computed list.
• Turing.MultiTapeTM.ComputableInPolyTime.contains: Boolean list membership via List.contains.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_not {γ : Type} {encIn : γ ↪ List Bool} {p : γ → Prop} [(x : γ) → Decidable (p x)] (h : ComputableTidilyInPolyTime (fun (x : γ) => decide (p x)) encIn encBool) : ComputableTidilyInPolyTime (fun (x : γ) => decide ¬p x) encIn encBool

Negation of an efficiently decidable proposition uses the standard Boolean encoding.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.decide_mem {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {list : γ → List α} {value : γ → α} [(x : γ) → Decidable (value x ∈ list x)] (hlist : ComputableTidilyInPolyTime list encIn (encList encA)) (hvalue : ComputableTidilyInPolyTime value encIn encA) : ComputableTidilyInPolyTime (fun (x : γ) => decide (value x ∈ list x)) encIn encBool

Membership of a computed value in a computed list is decided by scanning the list for an equal element.

Plain polynomial-time automation

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_mem {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {list : γ → List α} {value : γ → α} [_inst6 : (x : γ) → Decidable (value x ∈ list x)] (hlist : ComputableInPolyTime list encIn (encList encA)) (hvalue : ComputableInPolyTime value encIn encA) : ComputableInPolyTime (fun (x : γ) => decide (value x ∈ list x)) encIn encBool

Membership of a computed value in a computed list is decided by scanning the list for an equal element.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_not {γ : Type} {encIn : γ ↪ List Bool} {p : γ → Prop} [_inst3 : (x : γ) → Decidable (p x)] (h : ComputableInPolyTime (fun (x : γ) => decide (p x)) encIn encBool) : ComputableInPolyTime (fun (x : γ) => decide ¬p x) encIn encBool

Negation of an efficiently decidable proposition uses the standard Boolean encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.contains {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} [BEq α] [LawfulBEq α] {list : γ → List α} {value : γ → α} (hlist : ComputableInPolyTime list encIn (encList encA)) (hvalue : ComputableInPolyTime value encIn encA) : ComputableInPolyTime (fun (x : γ) => (list x).contains (value x)) encIn encBool

Membership of a computed value in a computed list, tested with List.contains, is polynomial-time computable.