Erasing duplicates in polynomial time

List.eraseDupsBy r l keeps each entry of l that is related by r to no entry kept before it. It is a left fold that appends at most one entry at a time (List.eraseDupsBy_eq_foldl), so a polynomial-time comparison, which may capture the original input, makes it polynomial-time (Turing.MultiTapeTM.ComputableInPolyTime.eraseDupsByWithInput).

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.eraseDupsByWithInput: erasing duplicates of a computed framed list with a computed comparison.
• Turing.MultiTapeTM.ComputableInPolyTime.decide_nodup, Turing.MultiTapeTM.ComputableInPolyTime.decide_nodup_bits: deciding List.Nodup on a computed framed list (and its fun_prop specialization to bit strings).

theorem Turing.MultiTapeTM.ComputableInPolyTime.eraseDupsByWithInput {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {list : γ → List α} {r : γ → α → α → Bool} (hlist : ComputableInPolyTime list encIn (encList encA)) (hr : ComputableInPolyTime (fun (p : (γ × α) × α) => r p.1.1 p.1.2 p.2) (encPair (encPair encIn encA) encA) encBool) : ComputableInPolyTime (fun (x : γ) => List.eraseDupsBy (r x) (list x)) encIn (encList encA)

Erase the entries of a computed framed list related by r x to an earlier kept entry. Each step of the fold appends at most one entry of the list, so the accumulator stays polynomially bounded.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_nodup {γ α : Type} [DecidableEq α] {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {list : γ → List α} (hlist : ComputableInPolyTime list encIn (encList encA)) : ComputableInPolyTime (fun (x : γ) => decide (list x).Nodup) encIn encBool

Decide whether a computed framed list has no duplicate entries by comparing it with the result of erasing duplicates by equality (eraseDupsByWithInput).

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_nodup_bits {γ : Type} {encIn : γ ↪ List Bool} {list : γ → List (List Bool)} (hlist : ComputableInPolyTime list encIn (encList encBits)) : ComputableInPolyTime (fun (x : γ) => decide (list x).Nodup) encIn encBool

Decide whether a computed framed list of bit strings has no duplicate entries. Fixing the element encoding to encBits avoids an ambiguous List Bool encoding metavariable during fun_prop search.