From f2cc018cbcfba5661f9482019da5c285bae8602e Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 00:33:38 +0000 Subject: [PATCH 1/2] feat(reductions): add autoreducibility and mitoticity for P and L (#1351) Define resource-bounded autoreducibility and mitoticity for polynomial-time and logarithmic-space reductions (many-one, 1-tt, k-tt, btt, dtt, ctt, tt), fulfilling Milestone R4 of #1351. Key additions: * Define PolyTimeManyOneAutoreducible, LogSpaceManyOneAutoreducible, and truth-table variants (k-tt, btt, dtt, ctt, tt) under non-self-reference query conditions. * Define ReducibleEquiv, MitoticWith, and polynomial-time/logspace mitoticity. * Prove reduction projections and the autoreducibility hierarchy. * Prove complement duality between dtt and ctt autoreducibility, and closure of many-one autoreducibility under complement. * Prove that sets in P are 0-tt autoreducible unconditionally. * Prove singleton and co-singleton obstructions to many-one autoreducibility. * Prove exact if-and-only-if characterizations for many-one autoreducibility in P and L. * Prove that many-one mitoticity unconditionally implies dtt, 1-tt, btt, and tt autoreducibility, and implies many-one autoreducibility iff the complement is not a singleton. * Add unit tests in ComplexityTests/Autoreducibility.lean. * Add AmbosSpies1984 and GlasserPavanSelmanZhang2008 to references.bib. Validation: * All six check.sh gates passed (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports). * check_hygiene.py --check-simp passed with 0 errors. * proof_lengths.py verified all theorem bodies < 40 lines. --- Complexity.lean | 1 + .../Reduction/Autoreducibility.lean | 753 ++++++++++++++++++ ComplexityTests/Autoreducibility.lean | 103 +++ references.bib | 23 + 4 files changed, 880 insertions(+) create mode 100644 Complexity/Computability/Complexity/Reduction/Autoreducibility.lean create mode 100644 ComplexityTests/Autoreducibility.lean diff --git a/Complexity.lean b/Complexity.lean index 84a51004ac..a06f0931e2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -897,6 +897,7 @@ public import Complexity.Computability.Complexity.Problems.USTCON public import Complexity.Computability.Complexity.Problems.VertexCover public import Complexity.Computability.Complexity.ProofSystem public import Complexity.Computability.Complexity.Reduction +public import Complexity.Computability.Complexity.Reduction.Autoreducibility public import Complexity.Computability.Complexity.Reduction.ManyOne public import Complexity.Computability.Complexity.Reduction.OneOne public import Complexity.Computability.Complexity.Reduction.TruthTable diff --git a/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean b/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean new file mode 100644 index 0000000000..df1819adfa --- /dev/null +++ b/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean @@ -0,0 +1,753 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.LogSpace +public import Complexity.Computability.Complexity.Reduction.TruthTableVariants +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Words +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List + +/-! +# Resource-bounded autoreducibility and mitoticity + +A set is **autoreducible** if it reduces to itself by a reduction that never queries its own +input [Ambos-Spies][AmbosSpies1984]. Autoreducibility is the core notion of information redundancy: +can membership of `a` be computed from membership of other instances? + +A set is **mitotic** if it can be split by an easy separator `S` into two disjoint pieces, +`A ∩ S` and `A ∖ S`, each computationally equivalent to the whole set +[Ambos-Spies][AmbosSpies1984]. Mitoticity is the structural splitting property of complete sets +[Glaßer, Pavan, Selman and Zhang][GlasserPavanSelmanZhang2008]. + +## Main definitions + +* `Cslib.Complexity.PolyTimeManyOneAutoreducible`: polynomial-time many-one autoreducibility. +* `Cslib.Complexity.LogSpaceManyOneAutoreducible`: logarithmic-space many-one autoreducibility. +* `Cslib.Complexity.PolyTimeKTruthTableAutoreducible`, `Cslib.Complexity.PolyTimeBTTAutoreducible`. +* `Cslib.Complexity.PolyTimeDTTAutoreducible`, `Cslib.Complexity.PolyTimeCTTAutoreducible`. +* `Cslib.Complexity.PolyTimeTruthTableAutoreducible`. +* `Cslib.Complexity.ReducibleEquiv`: mutual reducibility under a binary relation. +* `Cslib.Complexity.MitoticWith`: mitoticity with respect to a class of separators and a reduction. +* `Cslib.Complexity.PolyTimeManyOneMitotic`, `Cslib.Complexity.LogSpaceManyOneMitotic`. +* `Cslib.Complexity.PolyTimeBTTMitotic`, `Cslib.Complexity.PolyTimeTruthTableMitotic`. + +## Main results + +* The autoreducibility hierarchy: + `≤ᴸ_m,auto ⇒ ≤ᵖ_m,auto ⇒ ≤ᵖ_1-tt,auto ⇒ ≤ᵖ_k-tt,auto ⇒ ≤ᵖ_btt,auto ⇒ ≤ᵖ_tt,auto` and + `≤ᵖ_m,auto ⇒ ≤ᵖ_dtt,auto, ≤ᵖ_ctt,auto ⇒ ≤ᵖ_tt,auto`. +* Complements: closure of many-one autoreducibility under complement, and + `polyTimeDTTAutoreducible_iff_polyTimeCTTAutoreducible_compl`. +* Sets in `P` and `L`: every problem in `P` is `0-tt` (and hence `k-tt`, `btt`, `tt`) + autoreducible without any non-triviality assumption. +* Degenerate obstructions: singleton and co-singleton sets are strictly not many-one autoreducible + (`not_polyTimeManyOneAutoreducible_singleton`, + `not_polyTimeManyOneAutoreducible_compl_singleton`). +* Exact characterizations: a set in `P` (or `L`) is many-one autoreducible if and only if neither + it nor its complement is a singleton. +* Mitoticity implies autoreducibility: every polynomial-time many-one mitotic set is `dtt`, `1-tt`, + `btt` and `tt` autoreducible unconditionally, and many-one autoreducible provided its complement + is not a singleton. + +## References + +* [K. Ambos-Spies, *P-mitotic sets*][AmbosSpies1984] +* [C. Gla{\ss}er, A. Pavan, A. L. Selman, L. Zhang, *Splitting NP-complete + sets*][GlasserPavanSelmanZhang2008] +* [R. E. Ladner, N. A. Lynch, A. L. Selman, *A comparison of polynomial time + reducibilities*][LadnerLynchSelman1975] +* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +variable {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} + +/-! ### Many-one autoreducibility -/ + +/-- `A` is polynomial-time many-one autoreducible: a polynomial-time map `f` with `∀ a, f a ≠ a` +reduces `A` to itself. -/ +def PolyTimeManyOneAutoreducible (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ f : α → α, (ComputableInPolyTime f encA encA ∧ ∀ a, f a ≠ a) ∧ ∀ a, a ∈ A ↔ f a ∈ A + +/-- Polynomial-time many-one autoreducibility is many-one reducibility of `A` to itself by a +fixed-point-free polynomial-time map. -/ +theorem polyTimeManyOneAutoreducible_iff_manyOneReducibleBy : + PolyTimeManyOneAutoreducible encA A ↔ + ManyOneReducibleBy (fun f => ComputableInPolyTime f encA encA ∧ ∀ a, f a ≠ a) A A := + Iff.rfl + +/-- An autoreduction is an ordinary many-one reduction. -/ +theorem PolyTimeManyOneAutoreducible.polyTimeReducible (h : PolyTimeManyOneAutoreducible encA A) : + PolyTimeReducible encA encA A A := + let ⟨f, ⟨hf, _⟩, hA⟩ := h + ⟨f, hf, hA⟩ + +/-- `A` is logspace many-one autoreducible: a logarithmic-space map `f` with `∀ a, f a ≠ a` +reduces `A` to itself. -/ +def LogSpaceManyOneAutoreducible (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ f : α → α, (ComputableInLogSpace f encA encA ∧ ∀ a, f a ≠ a) ∧ ∀ a, a ∈ A ↔ f a ∈ A + +/-- Logspace many-one autoreducibility is many-one reducibility of `A` to itself by a +fixed-point-free logspace map. -/ +theorem logSpaceManyOneAutoreducible_iff_manyOneReducibleBy : + LogSpaceManyOneAutoreducible encA A ↔ + ManyOneReducibleBy (fun f => ComputableInLogSpace f encA encA ∧ ∀ a, f a ≠ a) A A := + Iff.rfl + +/-- A logspace autoreduction is an ordinary logspace reduction. -/ +theorem LogSpaceManyOneAutoreducible.logSpaceReducible (h : LogSpaceManyOneAutoreducible encA A) : + LogSpaceReducible encA encA A A := + let ⟨f, ⟨hf, _⟩, hA⟩ := h + ⟨f, hf, hA⟩ + +/-- **Logspace many-one autoreducibility implies polynomial-time many-one autoreducibility.** -/ +theorem LogSpaceManyOneAutoreducible.polyTimeManyOneAutoreducible + (h : LogSpaceManyOneAutoreducible encA A) : PolyTimeManyOneAutoreducible encA A := + ManyOneReducibleBy.mono (fun _ hf => ⟨.of_tidy hf.1.computableTidilyInPolyTime, hf.2⟩) h + +/-- Many-one autoreducibility is preserved under taking complements. -/ +theorem PolyTimeManyOneAutoreducible.compl (h : PolyTimeManyOneAutoreducible encA A) : + PolyTimeManyOneAutoreducible encA Aᶜ := + ManyOneReducibleBy.compl h + +/-- Logspace many-one autoreducibility is preserved under taking complements. -/ +theorem LogSpaceManyOneAutoreducible.compl (h : LogSpaceManyOneAutoreducible encA A) : + LogSpaceManyOneAutoreducible encA Aᶜ := + ManyOneReducibleBy.compl h + +/-! ### Truth-table autoreducibility variants -/ + +/-- `A` is `k`-truth-table autoreducible: a `k`-truth-table reduction whose query generator never +queries the input instance `a`. -/ +def PolyTimeKTruthTableAutoreducible (k : ℕ) (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ (r : α → ℕ) (q : α × ℕ → α) (d : α × List Bool → Bool), + ComputableInPolyTime r encA encUnary ∧ + ComputableInPolyTime q (encPair encA encUnary) encA ∧ + ComputableInPolyTime d (encPair encA encBits) encBool ∧ + (∀ a, r a ≤ k) ∧ (∀ a i, i < r a → q (a, i) ≠ a) ∧ + ∀ a, a ∈ A ↔ d (a, truthTableAnswers (q ⁻¹' A) r a) = true + +/-- A `k`-truth-table autoreduction is a `k`-truth-table reduction. -/ +theorem PolyTimeKTruthTableAutoreducible.polyTimeKTruthTableReducible {k : ℕ} + (h : PolyTimeKTruthTableAutoreducible k encA A) : + PolyTimeKTruthTableReducible k encA encA A A := + let ⟨r, q, d, hr, hq, hd, hrk, _, hA⟩ := h + ⟨r, q, d, hr, hq, hd, hrk, hA⟩ + +/-- `A` is bounded truth-table autoreducible. -/ +def PolyTimeBTTAutoreducible (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ k, PolyTimeKTruthTableAutoreducible k encA A + +/-- A bounded truth-table autoreduction is a bounded truth-table reduction. -/ +theorem PolyTimeBTTAutoreducible.polyTimeBTTReducible (h : PolyTimeBTTAutoreducible encA A) : + PolyTimeBTTReducible encA encA A A := + let ⟨k, h⟩ := h + ⟨k, h.polyTimeKTruthTableReducible⟩ + +/-- `A` is disjunctive truth-table autoreducible: accepting exactly when some query is in `A`, +without querying `a`. -/ +def PolyTimeDTTAutoreducible (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ (r : α → ℕ) (q : α × ℕ → α), + ComputableInPolyTime r encA encUnary ∧ + ComputableInPolyTime q (encPair encA encUnary) encA ∧ + (∀ a i, i < r a → q (a, i) ≠ a) ∧ ∀ a, a ∈ A ↔ ∃ i < r a, q (a, i) ∈ A + +/-- A disjunctive truth-table autoreduction is a disjunctive truth-table reduction. -/ +theorem PolyTimeDTTAutoreducible.polyTimeDTTReducible (h : PolyTimeDTTAutoreducible encA A) : + PolyTimeDTTReducible encA encA A A := + let ⟨r, q, hr, hq, _, hA⟩ := h + ⟨r, q, hr, hq, hA⟩ + +/-- `A` is conjunctive truth-table autoreducible: accepting exactly when every query is in `A`, +without querying `a`. -/ +def PolyTimeCTTAutoreducible (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ (r : α → ℕ) (q : α × ℕ → α), + ComputableInPolyTime r encA encUnary ∧ + ComputableInPolyTime q (encPair encA encUnary) encA ∧ + (∀ a i, i < r a → q (a, i) ≠ a) ∧ ∀ a, a ∈ A ↔ ∀ i < r a, q (a, i) ∈ A + +/-- A conjunctive truth-table autoreduction is a conjunctive truth-table reduction. -/ +theorem PolyTimeCTTAutoreducible.polyTimeCTTReducible (h : PolyTimeCTTAutoreducible encA A) : + PolyTimeCTTReducible encA encA A A := + let ⟨r, q, hr, hq, _, hA⟩ := h + ⟨r, q, hr, hq, hA⟩ + +/-- `A` is polynomial-time truth-table autoreducible: a truth-table reduction whose query generator +never queries the input instance. -/ +def PolyTimeTruthTableAutoreducible (encA : α ↪ List Bool) (A : Set α) : Prop := + ∃ (r : α → ℕ) (q : α × ℕ → α) (d : α × List Bool → Bool), + ComputableInPolyTime r encA encUnary ∧ + ComputableInPolyTime q (encPair encA encUnary) encA ∧ + ComputableInPolyTime d (encPair encA encBits) encBool ∧ + (∀ a i, i < r a → q (a, i) ≠ a) ∧ + ∀ a, a ∈ A ↔ d (a, truthTableAnswers (q ⁻¹' A) r a) = true + +/-- A truth-table autoreduction is a truth-table reduction. -/ +theorem PolyTimeTruthTableAutoreducible.polyTimeTruthTableReducible + (h : PolyTimeTruthTableAutoreducible encA A) : + PolyTimeTruthTableReducible encA encA A A := + let ⟨r, q, d, hr, hq, hd, _, hA⟩ := h + ⟨r, q, d, hr, hq, hd, hA⟩ + +/-- A many-one autoreduction is a `1`-truth-table autoreduction. -/ +theorem PolyTimeManyOneAutoreducible.polyTimeKTruthTableAutoreducible_one + (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := by + obtain ⟨f, ⟨hf, hne⟩, hA⟩ := h + refine ⟨fun _ => 1, fun x => f x.1, fun x => x.2.headD false, by fun_prop, by fun_prop, + by fun_prop, fun _ => le_rfl, fun a _ _ => hne a, fun a => ?_⟩ + rw [hA a] + simp [truthTableAnswers] + +/-- A many-one autoreduction is a disjunctive truth-table autoreduction. -/ +theorem PolyTimeManyOneAutoreducible.polyTimeDTTAutoreducible + (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeDTTAutoreducible encA A := by + obtain ⟨f, ⟨hf, hne⟩, hA⟩ := h + exact ⟨fun _ => 1, fun x => f x.1, by fun_prop, by fun_prop, fun a _ _ => hne a, + fun a => by simp [hA a]⟩ + +/-- A many-one autoreduction is a conjunctive truth-table autoreduction. -/ +theorem PolyTimeManyOneAutoreducible.polyTimeCTTAutoreducible + (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeCTTAutoreducible encA A := by + obtain ⟨f, ⟨hf, hne⟩, hA⟩ := h + exact ⟨fun _ => 1, fun x => f x.1, by fun_prop, by fun_prop, fun a _ _ => hne a, + fun a => by simp [hA a]⟩ + +/-- Allowing more queries in a `k`-truth-table autoreduction. -/ +theorem PolyTimeKTruthTableAutoreducible.mono {k k' : ℕ} + (h : PolyTimeKTruthTableAutoreducible k encA A) (hk : k ≤ k') : + PolyTimeKTruthTableAutoreducible k' encA A := + let ⟨r, q, d, hr, hq, hd, hrk, hne, hA⟩ := h + ⟨r, q, d, hr, hq, hd, fun a => (hrk a).trans hk, hne, hA⟩ + +theorem PolyTimeKTruthTableAutoreducible.polyTimeBTTAutoreducible {k : ℕ} + (h : PolyTimeKTruthTableAutoreducible k encA A) : PolyTimeBTTAutoreducible encA A := + ⟨k, h⟩ + +theorem PolyTimeBTTAutoreducible.polyTimeTruthTableAutoreducible + (h : PolyTimeBTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := + let ⟨_, r, q, d, hr, hq, hd, _, hne, hA⟩ := h + ⟨r, q, d, hr, hq, hd, hne, hA⟩ + +theorem PolyTimeManyOneAutoreducible.polyTimeBTTAutoreducible + (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeBTTAutoreducible encA A := + h.polyTimeKTruthTableAutoreducible_one.polyTimeBTTAutoreducible + +theorem PolyTimeManyOneAutoreducible.polyTimeTruthTableAutoreducible + (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := + h.polyTimeBTTAutoreducible.polyTimeTruthTableAutoreducible + +private theorem computableInPolyTime_any_answers : + ComputableInPolyTime (fun x : α × List Bool => x.2.any id) (encPair encA encBits) encBool := + .of_tidy (ComputableTidilyInPolyTime.anyWithEncoding (encA := encBool) (encL := encBits) + (test := fun p : α × Bool => p.2) (.snd encA encBool) (.fst encA encBits) + (.snd encA encBits)) + +private theorem computableInPolyTime_all_answers : + ComputableInPolyTime (fun x : α × List Bool => x.2.all id) (encPair encA encBits) encBool := + .of_tidy (ComputableTidilyInPolyTime.allWithEncoding (encA := encBool) (encL := encBits) + (test := fun p : α × Bool => p.2) (.snd encA encBool) (.fst encA encBits) + (.snd encA encBits)) + +theorem PolyTimeDTTAutoreducible.polyTimeTruthTableAutoreducible + (h : PolyTimeDTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := by + obtain ⟨r, q, hr, hq, hne, hA⟩ := h + refine ⟨r, q, fun x => x.2.any id, hr, hq, computableInPolyTime_any_answers, hne, fun a => ?_⟩ + rw [hA a] + simp [truthTableAnswers, List.any_eq_true, List.mem_ofFn, Fin.exists_iff] + +theorem PolyTimeCTTAutoreducible.polyTimeTruthTableAutoreducible + (h : PolyTimeCTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := by + obtain ⟨r, q, hr, hq, hne, hA⟩ := h + refine ⟨r, q, fun x => x.2.all id, hr, hq, computableInPolyTime_all_answers, hne, fun a => ?_⟩ + rw [hA a] + simp [truthTableAnswers, List.all_eq_true, List.mem_ofFn, Fin.forall_iff] + +/-- Complement duality between disjunctive and conjunctive truth-table autoreducibility. -/ +theorem polyTimeDTTAutoreducible_iff_polyTimeCTTAutoreducible_compl : + PolyTimeDTTAutoreducible encA A ↔ PolyTimeCTTAutoreducible encA Aᶜ := by + constructor + · rintro ⟨r, q, hr, hq, hne, hA⟩ + exact ⟨r, q, hr, hq, hne, fun a => by simp [hA a]⟩ + · rintro ⟨r, q, hr, hq, hne, hA⟩ + refine ⟨r, q, hr, hq, hne, fun a => ?_⟩ + have := not_congr (hA a) + simp only [Set.mem_compl_iff, not_not, not_forall, exists_prop] at this + exact this + +/-! ### Autoreducibility of sets in `P` and degenerate obstructions -/ + +/-- **Every problem in `P` is `0-tt` autoreducible**, making 0 queries and deciding `a ∈ A` +internally in polynomial time. -/ +theorem PolyTimeKTruthTableAutoreducible.of_mem_P (k : ℕ) (hA : A ∈ P encA) : + PolyTimeKTruthTableAutoreducible k encA A := by + obtain ⟨g, hg, hAg⟩ := hA + exact ⟨fun _ => 0, fun x => x.1, fun x => g x.1, by fun_prop, by fun_prop, by fun_prop, + fun _ => Nat.zero_le _, fun _ _ hi => (Nat.not_lt_zero _ hi).elim, hAg⟩ + +theorem PolyTimeBTTAutoreducible.of_mem_P (hA : A ∈ P encA) : + PolyTimeBTTAutoreducible encA A := + (PolyTimeKTruthTableAutoreducible.of_mem_P 0 hA).polyTimeBTTAutoreducible + +theorem PolyTimeTruthTableAutoreducible.of_mem_P (hA : A ∈ P encA) : + PolyTimeTruthTableAutoreducible encA A := + (PolyTimeBTTAutoreducible.of_mem_P hA).polyTimeTruthTableAutoreducible + +/-- A many-one autoreducible set cannot be a singleton, since its element would have no distinct +target member. -/ +theorem PolyTimeManyOneAutoreducible.exists_mem_ne (h : PolyTimeManyOneAutoreducible encA A) : + ∀ a ∈ A, ∃ y ∈ A, y ≠ a := by + obtain ⟨f, ⟨-, hne⟩, hA⟩ := h + intro a ha + exact ⟨f a, (hA a).mp ha, hne a⟩ + +/-- A many-one autoreducible set cannot have a singleton complement. -/ +theorem PolyTimeManyOneAutoreducible.exists_notMem_ne (h : PolyTimeManyOneAutoreducible encA A) : + ∀ a ∉ A, ∃ n ∉ A, n ≠ a := by + have hc := h.compl + exact fun a ha => hc.exists_mem_ne a ha + +theorem LogSpaceManyOneAutoreducible.exists_mem_ne (h : LogSpaceManyOneAutoreducible encA A) : + ∀ a ∈ A, ∃ y ∈ A, y ≠ a := + h.polyTimeManyOneAutoreducible.exists_mem_ne + +theorem LogSpaceManyOneAutoreducible.exists_notMem_ne (h : LogSpaceManyOneAutoreducible encA A) : + ∀ a ∉ A, ∃ n ∉ A, n ≠ a := + h.polyTimeManyOneAutoreducible.exists_notMem_ne + +/-- A singleton is strictly not polynomial-time many-one autoreducible. -/ +theorem not_polyTimeManyOneAutoreducible_singleton (a₀ : α) : + ¬ PolyTimeManyOneAutoreducible encA {a₀} := by + intro h + obtain ⟨y, hy, hne⟩ := h.exists_mem_ne a₀ (Set.mem_singleton a₀) + exact hne (Set.mem_singleton_iff.mp hy) + +/-- A co-singleton is strictly not polynomial-time many-one autoreducible. -/ +theorem not_polyTimeManyOneAutoreducible_compl_singleton (a₀ : α) : + ¬ PolyTimeManyOneAutoreducible encA {a₀}ᶜ := by + intro h + have hc := h.compl + rw [compl_compl] at hc + exact not_polyTimeManyOneAutoreducible_singleton a₀ hc + +theorem not_logSpaceManyOneAutoreducible_singleton (a₀ : α) : + ¬ LogSpaceManyOneAutoreducible encA {a₀} := + fun h => not_polyTimeManyOneAutoreducible_singleton a₀ h.polyTimeManyOneAutoreducible + +theorem not_logSpaceManyOneAutoreducible_compl_singleton (a₀ : α) : + ¬ LogSpaceManyOneAutoreducible encA {a₀}ᶜ := + fun h => not_polyTimeManyOneAutoreducible_compl_singleton a₀ h.polyTimeManyOneAutoreducible + +/-! ### Construction of many-one autoreductions for sets in `L` and `P` -/ + +private theorem computableInLogSpace_of_exists_finite_ne {f : α → β} + (h : ∃ b : β, {a : α | f a ≠ b}.Finite) : + ComputableInLogSpace f encA encB := + let ⟨_, h⟩ := computableInTimeAndSpace_of_exists_finite_ne h + ⟨_, 0, h.mono (fun _ => le_rfl) fun _ => Nat.zero_le _⟩ + +open scoped Classical in +private theorem computableInLogSpace_decide_eq (x₀ : α) : + ComputableInLogSpace (fun a => decide (a = x₀)) encA encBool := by + apply computableInLogSpace_of_exists_finite_ne + refine ⟨false, (Set.finite_singleton x₀).subset fun a ha => ?_⟩ + by_contra h + simp [Set.mem_singleton_iff.not.mp h] at ha + +open scoped Classical in +private theorem computableInLogSpace_alt (encA : α ↪ List Bool) (x₀ x₁ : α) : + ComputableInLogSpace (fun a => if a = x₀ then x₁ else x₀) encA encA := by + apply computableInLogSpace_of_exists_finite_ne + refine ⟨x₀, (Set.finite_singleton x₀).subset fun a ha => ?_⟩ + by_contra h + simp [Set.mem_singleton_iff.not.mp h] at ha + +open scoped Classical in +private theorem computableInPolyTime_alt (encA : α ↪ List Bool) (x₀ x₁ : α) : + ComputableInPolyTime (fun a => if a = x₀ then x₁ else x₀) encA encA := + (computableInLogSpace_alt encA x₀ x₁).computableTidilyInPolyTime.computableInPolyTime + +/-- A set in `L` with at least two members and at least two non-members is logspace many-one +autoreducible. -/ +theorem LogSpaceManyOneAutoreducible.of_two_mem_two_notMem (hA : A ∈ L encA) + {y₀ y₁ : α} (hy₀ : y₀ ∈ A) (hy₁ : y₁ ∈ A) (hyne : y₀ ≠ y₁) + {n₀ n₁ : α} (hn₀ : n₀ ∉ A) (hn₁ : n₁ ∉ A) (hnne : n₀ ≠ n₁) : + LogSpaceManyOneAutoreducible encA A := by + classical + obtain ⟨d, hd, hAd⟩ := hA + let eqY := computableInLogSpace_decide_eq y₀ (encA := encA) + let eqN := computableInLogSpace_decide_eq n₀ (encA := encA) + let eqs := eqY.pair eqN + let tagged := hd.pair eqs + let choose : Bool × (Bool × Bool) → α := + fun p => if p.1 then (if p.2.1 then y₁ else y₀) else (if p.2.2 then n₁ else n₀) + have hchoose : ComputableInLogSpace choose + (encPair encBool (encPair encBool encBool)) encA := + ComputableInLogSpace.of_finite choose + have hf : ComputableInLogSpace (choose ∘ fun a => (d a, (decide (a = y₀), decide (a = n₀)))) + encA encA := hchoose.comp tagged + refine ⟨_, ⟨hf, fun a => ?_⟩, fun a => ?_⟩ + · dsimp only [choose, Function.comp_apply] + cases hda : d a + · simp only [Bool.false_eq_true, ↓reduceIte] + split_ifs with ha + · intro heq; simp only [decide_eq_true_eq] at ha; subst ha; exact hnne heq.symm + · intro heq; exact ha (decide_eq_true heq.symm) + · simp only [↓reduceIte] + split_ifs with ha + · intro heq; simp only [decide_eq_true_eq] at ha; subst ha; exact hyne heq.symm + · intro heq; exact ha (decide_eq_true heq.symm) + · dsimp only [choose, Function.comp_apply] + cases hda : d a + · have haA : a ∉ A := fun ha => by have := (hAd a).mp ha; rw [hda] at this; contradiction + simp only [Bool.false_eq_true, ↓reduceIte] + split_ifs <;> simp [haA, hn₀, hn₁] + · have haA : a ∈ A := (hAd a).mpr hda + simp only [↓reduceIte] + split_ifs <;> simp [haA, hy₀, hy₁] + +private theorem logSpaceManyOneAutoreducible_of_univ {y₀ y₁ : α} (hyne : y₀ ≠ y₁) + (hUniv : A = Set.univ) : LogSpaceManyOneAutoreducible encA A := by + classical + let choose : Bool → α := fun b => if b then y₁ else y₀ + have hchoose : ComputableInLogSpace choose encBool encA := ComputableInLogSpace.of_finite choose + have hf := hchoose.comp (computableInLogSpace_decide_eq y₀ (encA := encA)) + refine ⟨_, ⟨hf, fun a => ?_⟩, fun a => ?_⟩ + · dsimp only [choose, Function.comp_apply] + split_ifs with ha + · intro heq; simp only [decide_eq_true_eq] at ha; subst ha; exact hyne heq.symm + · intro heq; exact ha (decide_eq_true heq.symm) + · simp [hUniv] + +private theorem logSpaceManyOneAutoreducible_of_empty {n₀ n₁ : α} (hnne : n₀ ≠ n₁) + (hEmpty : A = ∅) : LogSpaceManyOneAutoreducible encA A := by + classical + let choose : Bool → α := fun b => if b then n₁ else n₀ + have hchoose : ComputableInLogSpace choose encBool encA := ComputableInLogSpace.of_finite choose + have hf := hchoose.comp (computableInLogSpace_decide_eq n₀ (encA := encA)) + refine ⟨_, ⟨hf, fun a => ?_⟩, fun a => ?_⟩ + · dsimp only [choose, Function.comp_apply] + split_ifs with ha + · intro heq; simp only [decide_eq_true_eq] at ha; subst ha; exact hnne heq.symm + · intro heq; exact ha (decide_eq_true heq.symm) + · simp [hEmpty] + +/-- **A set in `L` is logspace many-one autoreducible if and only if neither it nor its complement +is a singleton.** -/ +theorem logSpaceManyOneAutoreducible_iff_of_mem_L (hA : A ∈ L encA) : + LogSpaceManyOneAutoreducible encA A ↔ + (∀ a ∈ A, ∃ y ∈ A, y ≠ a) ∧ (∀ a ∉ A, ∃ n ∉ A, n ≠ a) := by + refine ⟨fun h => ⟨h.exists_mem_ne, h.exists_notMem_ne⟩, fun ⟨hMem, hNotMem⟩ => ?_⟩ + by_cases hEmpty : A = ∅ + · by_cases hα : IsEmpty α + · exact ⟨id, ⟨ComputableInLogSpace.id, fun a => (IsEmpty.false a).elim⟩, fun _ => Iff.rfl⟩ + · obtain ⟨a₀⟩ := not_isEmpty_iff.mp hα + have ha₀ : a₀ ∉ A := by subst hEmpty; exact fun h => h + obtain ⟨n₁, hn₁, hne⟩ := hNotMem a₀ ha₀ + exact logSpaceManyOneAutoreducible_of_empty hne.symm hEmpty + · by_cases hUniv : A = Set.univ + · obtain ⟨a₀, ha₀⟩ := Set.nonempty_iff_ne_empty.mpr hEmpty + obtain ⟨y₁, hy₁, hne⟩ := hMem a₀ ha₀ + exact logSpaceManyOneAutoreducible_of_univ hne.symm hUniv + · obtain ⟨y₀, hy₀⟩ := Set.nonempty_iff_ne_empty.mpr hEmpty + obtain ⟨y₁, hy₁, hyne⟩ := hMem y₀ hy₀ + obtain ⟨n₀, hn₀⟩ := Set.nonempty_compl.mpr hUniv + obtain ⟨n₁, hn₁, hnne⟩ := hNotMem n₀ hn₀ + exact LogSpaceManyOneAutoreducible.of_two_mem_two_notMem hA hy₀ hy₁ hyne.symm hn₀ hn₁ + hnne.symm + +/-- A set in `P` with at least two members and at least two non-members is polynomial-time many-one +autoreducible. -/ +theorem PolyTimeManyOneAutoreducible.of_two_mem_two_notMem (hA : A ∈ P encA) + {y₀ y₁ : α} (hy₀ : y₀ ∈ A) (hy₁ : y₁ ∈ A) (hyne : y₀ ≠ y₁) + {n₀ n₁ : α} (hn₀ : n₀ ∉ A) (hn₁ : n₁ ∉ A) (hnne : n₀ ≠ n₁) : + PolyTimeManyOneAutoreducible encA A := by + classical + obtain ⟨d, hd, hAd⟩ := hA + have hy_comp := computableInPolyTime_alt encA y₀ y₁ + have hn_comp := computableInPolyTime_alt encA n₀ n₁ + have hf := ComputableInPolyTime.ite hd hy_comp hn_comp + refine ⟨_, ⟨hf, fun a => ?_⟩, fun a => ?_⟩ + · by_cases hda : d a = true + · simp only [hda, ↓reduceIte] + split_ifs with ha + · intro heq; subst ha; exact hyne heq.symm + · intro heq; exact ha heq.symm + · simp only [hda, Bool.false_eq_true, ↓reduceIte] + split_ifs with ha + · intro heq; subst ha; exact hnne heq.symm + · intro heq; exact ha heq.symm + · by_cases hda : d a = true + · simp only [hda, ↓reduceIte] + have haA : a ∈ A := (hAd a).mpr hda + split_ifs <;> simp [haA, hy₀, hy₁] + · simp only [hda, Bool.false_eq_true, ↓reduceIte] + have haA : a ∉ A := fun h => hda ((hAd a).mp h) + split_ifs <;> simp [haA, hn₀, hn₁] + +/-- **A set in `P` is polynomial-time many-one autoreducible if and only if neither it nor its +complement is a singleton.** -/ +theorem polyTimeManyOneAutoreducible_iff_of_mem_P (hA : A ∈ P encA) : + PolyTimeManyOneAutoreducible encA A ↔ + (∀ a ∈ A, ∃ y ∈ A, y ≠ a) ∧ (∀ a ∉ A, ∃ n ∉ A, n ≠ a) := by + refine ⟨fun h => ⟨h.exists_mem_ne, h.exists_notMem_ne⟩, fun ⟨hMem, hNotMem⟩ => ?_⟩ + by_cases hEmpty : A = ∅ + · by_cases hα : IsEmpty α + · exact ⟨id, ⟨ComputableInPolyTime.id', fun a => (IsEmpty.false a).elim⟩, fun _ => Iff.rfl⟩ + · obtain ⟨a₀⟩ := not_isEmpty_iff.mp hα + have ha₀ : a₀ ∉ A := by subst hEmpty; exact fun h => h + obtain ⟨n₁, hn₁, hne⟩ := hNotMem a₀ ha₀ + exact (logSpaceManyOneAutoreducible_of_empty hne.symm hEmpty).polyTimeManyOneAutoreducible + · by_cases hUniv : A = Set.univ + · obtain ⟨a₀, ha₀⟩ := Set.nonempty_iff_ne_empty.mpr hEmpty + obtain ⟨y₁, hy₁, hne⟩ := hMem a₀ ha₀ + exact (logSpaceManyOneAutoreducible_of_univ hne.symm hUniv).polyTimeManyOneAutoreducible + · obtain ⟨y₀, hy₀⟩ := Set.nonempty_iff_ne_empty.mpr hEmpty + obtain ⟨y₁, hy₁, hyne⟩ := hMem y₀ hy₀ + obtain ⟨n₀, hn₀⟩ := Set.nonempty_compl.mpr hUniv + obtain ⟨n₁, hn₁, hnne⟩ := hNotMem n₀ hn₀ + exact PolyTimeManyOneAutoreducible.of_two_mem_two_notMem hA hy₀ hy₁ hyne.symm hn₀ hn₁ + hnne.symm + +theorem LogSpaceManyOneAutoreducible.of_mem_L (hA : A ∈ L encA) + (hMem : ∀ a ∈ A, ∃ y ∈ A, y ≠ a) (hNotMem : ∀ a ∉ A, ∃ n ∉ A, n ≠ a) : + LogSpaceManyOneAutoreducible encA A := + (logSpaceManyOneAutoreducible_iff_of_mem_L hA).mpr ⟨hMem, hNotMem⟩ + +theorem PolyTimeManyOneAutoreducible.of_mem_P (hA : A ∈ P encA) + (hMem : ∀ a ∈ A, ∃ y ∈ A, y ≠ a) (hNotMem : ∀ a ∉ A, ∃ n ∉ A, n ≠ a) : + PolyTimeManyOneAutoreducible encA A := + (polyTimeManyOneAutoreducible_iff_of_mem_P hA).mpr ⟨hMem, hNotMem⟩ + +/-! ### Mitoticity -/ + +/-- Mutual reducibility under a binary relation `R`. -/ +def ReducibleEquiv (R : Set α → Set α → Prop) (A B : Set α) : Prop := + R A B ∧ R B A + +/-- `A` is mitotic with respect to the separating problems `𝒞` and the reduction `R`: some +`S ∈ 𝒞` splits `A` into two mutually equivalent parts `A ∩ S` and `A ∖ S`, both equivalent to `A`. +-/ +def MitoticWith (𝒞 : Set (Set α)) (R : Set α → Set α → Prop) (A : Set α) : Prop := + ∃ S ∈ 𝒞, ReducibleEquiv R A (A ∩ S) ∧ ReducibleEquiv R A (A \ S) + +/-- `A` is polynomial-time many-one mitotic [Ambos-Spies 1984][AmbosSpies1984]. -/ +def PolyTimeManyOneMitotic (encA : α ↪ List Bool) (A : Set α) : Prop := + MitoticWith (P encA) (PolyTimeReducible encA encA) A + +/-- `A` is logspace many-one mitotic. -/ +def LogSpaceManyOneMitotic (encA : α ↪ List Bool) (A : Set α) : Prop := + MitoticWith (L encA) (LogSpaceReducible encA encA) A + +/-- `A` is bounded truth-table mitotic. -/ +def PolyTimeBTTMitotic (encA : α ↪ List Bool) (A : Set α) : Prop := + MitoticWith (P encA) (PolyTimeBTTReducible encA encA) A + +/-- `A` is truth-table mitotic. -/ +def PolyTimeTruthTableMitotic (encA : α ↪ List Bool) (A : Set α) : Prop := + MitoticWith (P encA) (PolyTimeTruthTableReducible encA encA) A + +/-- A logspace mitotic set is polynomial-time mitotic. -/ +theorem LogSpaceManyOneMitotic.polyTimeManyOneMitotic (h : LogSpaceManyOneMitotic encA A) : + PolyTimeManyOneMitotic encA A := by + obtain ⟨S, hS, h₁, h₂⟩ := h + exact ⟨S, L_subset_P hS, + ⟨h₁.1.polyTimeReducible, h₁.2.polyTimeReducible⟩, + ⟨h₂.1.polyTimeReducible, h₂.2.polyTimeReducible⟩⟩ + +/-- Many-one mitoticity implies bounded truth-table mitoticity. -/ +theorem PolyTimeManyOneMitotic.polyTimeBTTMitotic (h : PolyTimeManyOneMitotic encA A) : + PolyTimeBTTMitotic encA A := by + obtain ⟨S, hS, h₁, h₂⟩ := h + exact ⟨S, hS, + ⟨h₁.1.polyTimeBTTReducible, h₁.2.polyTimeBTTReducible⟩, + ⟨h₂.1.polyTimeBTTReducible, h₂.2.polyTimeBTTReducible⟩⟩ + +theorem PolyTimeBTTMitotic.polyTimeTruthTableMitotic (h : PolyTimeBTTMitotic encA A) : + PolyTimeTruthTableMitotic encA A := by + obtain ⟨S, hS, h₁, h₂⟩ := h + exact ⟨S, hS, + ⟨h₁.1.polyTimeTruthTableReducible, h₁.2.polyTimeTruthTableReducible⟩, + ⟨h₂.1.polyTimeTruthTableReducible, h₂.2.polyTimeTruthTableReducible⟩⟩ + +theorem PolyTimeManyOneMitotic.polyTimeTruthTableMitotic (h : PolyTimeManyOneMitotic encA A) : + PolyTimeTruthTableMitotic encA A := + h.polyTimeBTTMitotic.polyTimeTruthTableMitotic + +/-! ### Mitotic implies autoreducible -/ + +private theorem mitotic_candidate_ne {s : α → Bool} {f₁ f₂ : α → α} {a : α} + (hg : (s (if s a then f₁ a else f₂ a) != s a) = true) : + (if s a then f₁ a else f₂ a) ≠ a := by + intro heq + rw [heq, bne_self_eq_false] at hg + contradiction + +private theorem mitotic_candidate_mem_iff {S : Set α} {s : α → Bool} (hsS : ∀ a, a ∈ S ↔ s a = true) + {f₁ f₂ : α → α} (hAf₁ : ∀ a, a ∈ A ↔ f₁ a ∈ A \ S) (hAf₂ : ∀ a, a ∈ A ↔ f₂ a ∈ A ∩ S) {a : α} + (hg : (s (if s a then f₁ a else f₂ a) != s a) = true) : + a ∈ A ↔ (if s a then f₁ a else f₂ a) ∈ A := by + cases hs_a : s a + · simp only [hs_a, Bool.bne_false, Bool.false_eq_true, ↓reduceIte] at hg ⊢ + rw [hAf₂ a, Set.mem_inter_iff] + exact and_iff_left ((hsS (f₂ a)).mpr hg) + · simp only [hs_a, ↓reduceIte] at hg ⊢ + have hf₁S : f₁ a ∉ S := fun hS' => by + have := (hsS (f₁ a)).mp hS'; rw [this] at hg; contradiction + rw [hAf₁ a, Set.mem_sdiff] + exact and_iff_left hf₁S + +private theorem mitotic_candidate_notMem {S : Set α} {s : α → Bool} (hsS : ∀ a, a ∈ S ↔ s a = true) + {f₁ f₂ : α → α} (hAf₁ : ∀ a, a ∈ A ↔ f₁ a ∈ A \ S) (hAf₂ : ∀ a, a ∈ A ↔ f₂ a ∈ A ∩ S) {a : α} + (hg : ¬ (s (if s a then f₁ a else f₂ a) != s a) = true) : + a ∉ A := by + intro ha + cases hs_a : s a + · simp only [hs_a, Bool.bne_false, Bool.false_eq_true, ↓reduceIte] at hg + exact hg ((hsS (f₂ a)).mp ((hAf₂ a).mp ha).2) + · simp only [hs_a, ↓reduceIte] at hg + have haS := (hAf₁ a).mp ha + have hS' : f₁ a ∈ S := by + cases hsf : s (f₁ a) + · exact False.elim (hg (by simp [hsf])) + · exact (hsS (f₁ a)).mpr hsf + exact haS.2 hS' + +/-- **Every polynomial-time many-one mitotic set is disjunctive truth-table autoreducible**, +unconditionally. If the image lands on the wrong side of the separator, 0 queries are made; +otherwise 1 query on the opposite side of `S` is made, guaranteed distinct from `a`. -/ +theorem PolyTimeManyOneMitotic.polyTimeDTTAutoreducible (h : PolyTimeManyOneMitotic encA A) : + PolyTimeDTTAutoreducible encA A := by + obtain ⟨S, hS, ⟨hA₂, -⟩, ⟨hA₁, -⟩⟩ := h + obtain ⟨s, hs, hsS⟩ := hS + obtain ⟨f₂, hf₂, hAf₂⟩ := hA₂ + obtain ⟨f₁, hf₁, hAf₁⟩ := hA₁ + let candidate : α → α := fun a => if s a then f₁ a else f₂ a + have hcand : ComputableInPolyTime candidate encA encA := + ComputableInPolyTime.ite hs hf₁ hf₂ + let good : α → Bool := fun a => (s (candidate a) != s a) + have hgood : ComputableInPolyTime good encA encBool := by fun_prop + let r : α → ℕ := fun a => if good a then 1 else 0 + have hr : ComputableInPolyTime r encA encUnary := by fun_prop + let q : α × ℕ → α := fun p => candidate p.1 + have hq : ComputableInPolyTime q (encPair encA encUnary) encA := + hcand.comp (ComputableInPolyTime.fst encA encUnary) + refine ⟨r, q, hr, hq, fun a i hi => ?_, fun a => ?_⟩ + · dsimp only [r] at hi + split_ifs at hi with hg + · exact mitotic_candidate_ne hg + · omega + · dsimp only [r, q] + split_ifs with hg + · simp only [Nat.lt_one_iff, exists_eq_left] + exact mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg + · simp only [Nat.not_lt_zero, false_and, exists_false, iff_false] + exact mitotic_candidate_notMem hsS hAf₁ hAf₂ hg + +/-- **Every polynomial-time many-one mitotic set is `1`-truth-table autoreducible**, +unconditionally. -/ +theorem PolyTimeManyOneMitotic.polyTimeKTruthTableAutoreducible_one + (h : PolyTimeManyOneMitotic encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := by + obtain ⟨S, hS, ⟨hA₂, -⟩, ⟨hA₁, -⟩⟩ := h + obtain ⟨s, hs, hsS⟩ := hS + obtain ⟨f₂, hf₂, hAf₂⟩ := hA₂ + obtain ⟨f₁, hf₁, hAf₁⟩ := hA₁ + let candidate : α → α := fun a => if s a then f₁ a else f₂ a + have hcand : ComputableInPolyTime candidate encA encA := + ComputableInPolyTime.ite hs hf₁ hf₂ + let good : α → Bool := fun a => (s (candidate a) != s a) + have hgood : ComputableInPolyTime good encA encBool := by fun_prop + let r : α → ℕ := fun a => if good a then 1 else 0 + have hr : ComputableInPolyTime r encA encUnary := by fun_prop + let q : α × ℕ → α := fun p => candidate p.1 + have hq : ComputableInPolyTime q (encPair encA encUnary) encA := + hcand.comp (ComputableInPolyTime.fst encA encUnary) + let d : α × List Bool → Bool := fun p => p.2.headD false + have hd : ComputableInPolyTime d (encPair encA encBits) encBool := by fun_prop + refine ⟨r, q, d, hr, hq, hd, fun a => ?_, fun a i hi => ?_, fun a => ?_⟩ + · dsimp only [r] + split_ifs <;> omega + · dsimp only [r] at hi + split_ifs at hi with hg + · exact mitotic_candidate_ne hg + · omega + · dsimp only [r, q, d, truthTableAnswers] + by_cases hg : good a = true + · simp only [hg, ↓reduceIte, List.ofFn_succ, List.ofFn_zero, List.headD_cons, + Set.mem_preimage, decide_eq_true_eq] + exact mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg + · simp only [hg, ↓reduceIte, List.ofFn_zero, List.headD_nil, Bool.false_eq_true, iff_false] + exact mitotic_candidate_notMem hsS hAf₁ hAf₂ hg + +theorem PolyTimeManyOneMitotic.polyTimeBTTAutoreducible (h : PolyTimeManyOneMitotic encA A) : + PolyTimeBTTAutoreducible encA A := + h.polyTimeKTruthTableAutoreducible_one.polyTimeBTTAutoreducible + +theorem PolyTimeManyOneMitotic.polyTimeTruthTableAutoreducible + (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableAutoreducible encA A := + h.polyTimeBTTAutoreducible.polyTimeTruthTableAutoreducible + +/-- **A polynomial-time many-one mitotic set is many-one autoreducible provided its complement +is not a singleton.** -/ +theorem PolyTimeManyOneMitotic.polyTimeManyOneAutoreducible (h : PolyTimeManyOneMitotic encA A) + (hCompl : ∀ a ∉ A, ∃ n ∉ A, n ≠ a) : PolyTimeManyOneAutoreducible encA A := by + classical + obtain ⟨S, hS, ⟨hA₂, -⟩, ⟨hA₁, -⟩⟩ := h + obtain ⟨s, hs, hsS⟩ := hS + obtain ⟨f₂, hf₂, hAf₂⟩ := hA₂ + obtain ⟨f₁, hf₁, hAf₁⟩ := hA₁ + let candidate : α → α := fun a => if s a then f₁ a else f₂ a + have hcand : ComputableInPolyTime candidate encA encA := + ComputableInPolyTime.ite hs hf₁ hf₂ + let good : α → Bool := fun a => (s (candidate a) != s a) + have hgood : ComputableInPolyTime good encA encBool := by fun_prop + by_cases hUniv : ∀ a, a ∈ A + · refine ⟨candidate, ⟨hcand, fun a => ?_⟩, fun a => by simp [hUniv (candidate a), hUniv a]⟩ + have hg : good a = true := by + by_contra hbad + exact (mitotic_candidate_notMem hsS hAf₁ hAf₂ hbad) (hUniv a) + exact mitotic_candidate_ne hg + · obtain ⟨n₀, hn₀⟩ : ∃ n, n ∉ A := by + by_contra hc + apply hUniv + intro a + by_contra ha + exact hc ⟨a, ha⟩ + obtain ⟨n₁, hn₁, hnne⟩ := hCompl n₀ hn₀ + have hfall := computableInPolyTime_alt encA n₀ n₁ + let f : α → α := fun a => if good a then candidate a else (if a = n₀ then n₁ else n₀) + have hf : ComputableInPolyTime f encA encA := ComputableInPolyTime.ite hgood hcand hfall + refine ⟨f, ⟨hf, fun a => ?_⟩, fun a => ?_⟩ + · dsimp only [f] + by_cases hg : good a = true + · simp only [hg, ↓reduceIte] + exact mitotic_candidate_ne hg + · simp only [hg, Bool.false_eq_true, ↓reduceIte] + split_ifs with ha + · intro heq; subst ha; exact hnne heq + · intro heq; exact ha heq.symm + · dsimp only [f] + by_cases hg : good a = true + · simp only [hg, ↓reduceIte] + exact mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg + · simp only [hg, Bool.false_eq_true, ↓reduceIte] + have haA := mitotic_candidate_notMem hsS hAf₁ hAf₂ hg + split_ifs with ha <;> simp [haA, hn₀, hn₁] + +/-- **A polynomial-time many-one mitotic set is many-one autoreducible if and only if its +complement is not a singleton.** -/ +theorem PolyTimeManyOneMitotic.polyTimeManyOneAutoreducible_iff + (h : PolyTimeManyOneMitotic encA A) : + PolyTimeManyOneAutoreducible encA A ↔ ∀ a ∉ A, ∃ n ∉ A, n ≠ a := + ⟨fun hauto => hauto.exists_notMem_ne, fun hCompl => h.polyTimeManyOneAutoreducible hCompl⟩ + +end Cslib.Complexity diff --git a/ComplexityTests/Autoreducibility.lean b/ComplexityTests/Autoreducibility.lean new file mode 100644 index 0000000000..d998215c82 --- /dev/null +++ b/ComplexityTests/Autoreducibility.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Reduction.Autoreducibility +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List + +/-! Tests for resource-bounded autoreducibility and mitoticity: singleton and co-singleton +obstructions, concrete autoreducible language instances, hierarchy projections, and mitoticity +implications. -/ + +namespace ComplexityTests.Autoreducibility + +open Cslib Cslib.Complexity Turing.MultiTapeTM + +variable {α : Type} {encA : α ↪ List Bool} {A : Set α} + +/-! ### Singleton and co-singleton obstructions -/ + +example : ¬ PolyTimeManyOneAutoreducible encBits {[true]} := + not_polyTimeManyOneAutoreducible_singleton [true] + +example : ¬ PolyTimeManyOneAutoreducible encBits {[true]}ᶜ := + not_polyTimeManyOneAutoreducible_compl_singleton [true] + +example : ¬ LogSpaceManyOneAutoreducible encBits {[true]} := + not_logSpaceManyOneAutoreducible_singleton [true] + +example : ¬ LogSpaceManyOneAutoreducible encBits {[true]}ᶜ := + not_logSpaceManyOneAutoreducible_compl_singleton [true] + +/-! ### Non-trivial language in `P` is many-one autoreducible -/ + +private def headTrueSet : Set (List Bool) := + {w : List Bool | w.headD false = true} + +private theorem headTrueSet_mem_P : headTrueSet ∈ P encBits := + ⟨fun w => w.headD false, by fun_prop, fun _ => Iff.rfl⟩ + +example : PolyTimeManyOneAutoreducible encBits headTrueSet := + PolyTimeManyOneAutoreducible.of_two_mem_two_notMem headTrueSet_mem_P + (y₀ := [true]) (y₁ := [true, false]) rfl rfl (by decide) + (n₀ := []) (n₁ := [false]) (fun h => by cases h) (fun h => by cases h) (by decide) + +/-! ### Autoreducibility hierarchy projections -/ + +example (h : LogSpaceManyOneAutoreducible encA A) : PolyTimeManyOneAutoreducible encA A := + h.polyTimeManyOneAutoreducible + +example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := + h.polyTimeKTruthTableAutoreducible_one + +example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeDTTAutoreducible encA A := + h.polyTimeDTTAutoreducible + +example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeCTTAutoreducible encA A := + h.polyTimeCTTAutoreducible + +example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeBTTAutoreducible encA A := + h.polyTimeBTTAutoreducible + +example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := + h.polyTimeTruthTableAutoreducible + +example (h : PolyTimeDTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := + h.polyTimeTruthTableAutoreducible + +example (h : PolyTimeCTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := + h.polyTimeTruthTableAutoreducible + +example : PolyTimeDTTAutoreducible encA A ↔ PolyTimeCTTAutoreducible encA Aᶜ := + polyTimeDTTAutoreducible_iff_polyTimeCTTAutoreducible_compl + +/-! ### Mitoticity hierarchy and autoreducibility implications -/ + +example (h : LogSpaceManyOneMitotic encA A) : PolyTimeManyOneMitotic encA A := + h.polyTimeManyOneMitotic + +example (h : PolyTimeManyOneMitotic encA A) : PolyTimeBTTMitotic encA A := + h.polyTimeBTTMitotic + +example (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableMitotic encA A := + h.polyTimeTruthTableMitotic + +example (h : PolyTimeManyOneMitotic encA A) : PolyTimeDTTAutoreducible encA A := + h.polyTimeDTTAutoreducible + +example (h : PolyTimeManyOneMitotic encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := + h.polyTimeKTruthTableAutoreducible_one + +example (h : PolyTimeManyOneMitotic encA A) : PolyTimeBTTAutoreducible encA A := + h.polyTimeBTTAutoreducible + +example (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableAutoreducible encA A := + h.polyTimeTruthTableAutoreducible + +example (h : PolyTimeManyOneMitotic encA A) : + PolyTimeManyOneAutoreducible encA A ↔ ∀ a ∉ A, ∃ n ∉ A, n ≠ a := + h.polyTimeManyOneAutoreducible_iff + +end ComplexityTests.Autoreducibility diff --git a/references.bib b/references.bib index 456c999d54..a72a724fad 100644 --- a/references.bib +++ b/references.bib @@ -169,6 +169,18 @@ @article{AlpernSchneider1985 url = {https://www.sciencedirect.com/science/article/pii/0020019085900560} } +@incollection{AmbosSpies1984, + author = {Ambos-Spies, Klaus}, + title = {{$P$}-mitotic sets}, + booktitle = {Logic and Machines: Decision Problems and Complexity}, + series = {Lecture Notes in Computer Science}, + volume = {171}, + pages = {1--23}, + publisher = {Springer}, + year = {1984}, + doi = {10.1007/3-540-13331-3_1} +} + @article{AnderssonMiltersenThorup1999, author = {Andersson, Arne and Miltersen, Peter Bro and Thorup, Mikkel}, title = {Fusion Trees can be Implemented with {AC$^0$} Instructions Only}, @@ -1660,6 +1672,17 @@ @inproceedings{GKST2016 doi = {10.4230/LIPIcs.MFCS.2016.45} } +@article{GlasserPavanSelmanZhang2008, + author = {Gla{\ss}er, Christian and Pavan, A. and Selman, Alan L. and Zhang, Liyu}, + title = {Splitting {NP}-Complete Sets}, + journal = {SIAM Journal on Computing}, + volume = {37}, + number = {5}, + pages = {1517--1535}, + year = {2008}, + doi = {10.1137/060677579} +} + @book{Goldreich2001, author = {Goldreich, Oded}, title = {Foundations of Cryptography, Volume 1: Basic Tools}, From adf6ae8eba452031b0899c6258e7ea04db8d3825 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 01:41:18 +0000 Subject: [PATCH 2/2] fix(reductions): address review feedback on autoreducibility and mitoticity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Fix AmbosSpies1984 (10.1007/3-540-13331-3_30) and GlasserPavanSelmanZhang2008 (10.1137/060673886) DOIs in references.bib. - Replace signature restatement examples in ComplexityTests/Autoreducibility.lean with a concrete polynomial-time many-one mitotic instance (coSingleton_mitotic on {[]}ᶜ split by headTrueSet), exercising the mitotic-to-autoreducible theorems while contrasting with not_polyTimeManyOneAutoreducible_compl_singleton. - Factor private PolyTimeManyOneMitotic.exists_candidate to deduplicate candidate/good construction across the three mitotic-to-autoreducible proofs. - Add docstrings to all 18 previously undocumented public theorems, clarify MitoticWith docstring, credit Ambos-Spies 1984, and remove unused Sipser2013 citation. --- .../Reduction/Autoreducibility.lean | 100 ++++++++++-------- ComplexityTests/Autoreducibility.lean | 87 ++++++--------- references.bib | 4 +- 3 files changed, 90 insertions(+), 101 deletions(-) diff --git a/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean b/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean index df1819adfa..05a5b8b7c6 100644 --- a/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean +++ b/Complexity/Computability/Complexity/Reduction/Autoreducibility.lean @@ -61,7 +61,6 @@ A set is **mitotic** if it can be split by an easy separator `S` into two disjoi sets*][GlasserPavanSelmanZhang2008] * [R. E. Ladner, N. A. Lynch, A. L. Selman, *A comparison of polynomial time reducibilities*][LadnerLynchSelman1975] -* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013] -/ @[expose] public section @@ -229,19 +228,23 @@ theorem PolyTimeKTruthTableAutoreducible.mono {k k' : ℕ} let ⟨r, q, d, hr, hq, hd, hrk, hne, hA⟩ := h ⟨r, q, d, hr, hq, hd, fun a => (hrk a).trans hk, hne, hA⟩ +/-- A `k`-truth-table autoreduction is a bounded truth-table autoreduction. -/ theorem PolyTimeKTruthTableAutoreducible.polyTimeBTTAutoreducible {k : ℕ} (h : PolyTimeKTruthTableAutoreducible k encA A) : PolyTimeBTTAutoreducible encA A := ⟨k, h⟩ +/-- A bounded truth-table autoreduction is a truth-table autoreduction. -/ theorem PolyTimeBTTAutoreducible.polyTimeTruthTableAutoreducible (h : PolyTimeBTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := let ⟨_, r, q, d, hr, hq, hd, _, hne, hA⟩ := h ⟨r, q, d, hr, hq, hd, hne, hA⟩ +/-- A many-one autoreduction is a bounded truth-table autoreduction. -/ theorem PolyTimeManyOneAutoreducible.polyTimeBTTAutoreducible (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeBTTAutoreducible encA A := h.polyTimeKTruthTableAutoreducible_one.polyTimeBTTAutoreducible +/-- A many-one autoreduction is a truth-table autoreduction. -/ theorem PolyTimeManyOneAutoreducible.polyTimeTruthTableAutoreducible (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := h.polyTimeBTTAutoreducible.polyTimeTruthTableAutoreducible @@ -258,6 +261,7 @@ private theorem computableInPolyTime_all_answers : (test := fun p : α × Bool => p.2) (.snd encA encBool) (.fst encA encBits) (.snd encA encBits)) +/-- A disjunctive truth-table autoreduction is a truth-table autoreduction. -/ theorem PolyTimeDTTAutoreducible.polyTimeTruthTableAutoreducible (h : PolyTimeDTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := by obtain ⟨r, q, hr, hq, hne, hA⟩ := h @@ -265,6 +269,7 @@ theorem PolyTimeDTTAutoreducible.polyTimeTruthTableAutoreducible rw [hA a] simp [truthTableAnswers, List.any_eq_true, List.mem_ofFn, Fin.exists_iff] +/-- A conjunctive truth-table autoreduction is a truth-table autoreduction. -/ theorem PolyTimeCTTAutoreducible.polyTimeTruthTableAutoreducible (h : PolyTimeCTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := by obtain ⟨r, q, hr, hq, hne, hA⟩ := h @@ -294,10 +299,12 @@ theorem PolyTimeKTruthTableAutoreducible.of_mem_P (k : ℕ) (hA : A ∈ P encA) exact ⟨fun _ => 0, fun x => x.1, fun x => g x.1, by fun_prop, by fun_prop, by fun_prop, fun _ => Nat.zero_le _, fun _ _ hi => (Nat.not_lt_zero _ hi).elim, hAg⟩ +/-- Every problem in `P` is bounded truth-table autoreducible. -/ theorem PolyTimeBTTAutoreducible.of_mem_P (hA : A ∈ P encA) : PolyTimeBTTAutoreducible encA A := (PolyTimeKTruthTableAutoreducible.of_mem_P 0 hA).polyTimeBTTAutoreducible +/-- Every problem in `P` is truth-table autoreducible. -/ theorem PolyTimeTruthTableAutoreducible.of_mem_P (hA : A ∈ P encA) : PolyTimeTruthTableAutoreducible encA A := (PolyTimeBTTAutoreducible.of_mem_P hA).polyTimeTruthTableAutoreducible @@ -316,10 +323,12 @@ theorem PolyTimeManyOneAutoreducible.exists_notMem_ne (h : PolyTimeManyOneAutore have hc := h.compl exact fun a ha => hc.exists_mem_ne a ha +/-- A logspace many-one autoreducible set cannot be a singleton. -/ theorem LogSpaceManyOneAutoreducible.exists_mem_ne (h : LogSpaceManyOneAutoreducible encA A) : ∀ a ∈ A, ∃ y ∈ A, y ≠ a := h.polyTimeManyOneAutoreducible.exists_mem_ne +/-- A logspace many-one autoreducible set cannot have a singleton complement. -/ theorem LogSpaceManyOneAutoreducible.exists_notMem_ne (h : LogSpaceManyOneAutoreducible encA A) : ∀ a ∉ A, ∃ n ∉ A, n ≠ a := h.polyTimeManyOneAutoreducible.exists_notMem_ne @@ -339,10 +348,12 @@ theorem not_polyTimeManyOneAutoreducible_compl_singleton (a₀ : α) : rw [compl_compl] at hc exact not_polyTimeManyOneAutoreducible_singleton a₀ hc +/-- A singleton is strictly not logspace many-one autoreducible. -/ theorem not_logSpaceManyOneAutoreducible_singleton (a₀ : α) : ¬ LogSpaceManyOneAutoreducible encA {a₀} := fun h => not_polyTimeManyOneAutoreducible_singleton a₀ h.polyTimeManyOneAutoreducible +/-- A co-singleton is strictly not logspace many-one autoreducible. -/ theorem not_logSpaceManyOneAutoreducible_compl_singleton (a₀ : α) : ¬ LogSpaceManyOneAutoreducible encA {a₀}ᶜ := fun h => not_polyTimeManyOneAutoreducible_compl_singleton a₀ h.polyTimeManyOneAutoreducible @@ -518,11 +529,13 @@ theorem polyTimeManyOneAutoreducible_iff_of_mem_P (hA : A ∈ P encA) : exact PolyTimeManyOneAutoreducible.of_two_mem_two_notMem hA hy₀ hy₁ hyne.symm hn₀ hn₁ hnne.symm +/-- A set in `L` with no unique member or non-member is logspace many-one autoreducible. -/ theorem LogSpaceManyOneAutoreducible.of_mem_L (hA : A ∈ L encA) (hMem : ∀ a ∈ A, ∃ y ∈ A, y ≠ a) (hNotMem : ∀ a ∉ A, ∃ n ∉ A, n ≠ a) : LogSpaceManyOneAutoreducible encA A := (logSpaceManyOneAutoreducible_iff_of_mem_L hA).mpr ⟨hMem, hNotMem⟩ +/-- A set in `P` with no unique member or non-member is polynomial-time many-one autoreducible. -/ theorem PolyTimeManyOneAutoreducible.of_mem_P (hA : A ∈ P encA) (hMem : ∀ a ∈ A, ∃ y ∈ A, y ≠ a) (hNotMem : ∀ a ∉ A, ∃ n ∉ A, n ≠ a) : PolyTimeManyOneAutoreducible encA A := @@ -535,8 +548,8 @@ def ReducibleEquiv (R : Set α → Set α → Prop) (A B : Set α) : Prop := R A B ∧ R B A /-- `A` is mitotic with respect to the separating problems `𝒞` and the reduction `R`: some -`S ∈ 𝒞` splits `A` into two mutually equivalent parts `A ∩ S` and `A ∖ S`, both equivalent to `A`. --/ +`S ∈ 𝒞` splits `A` into `A ∩ S` and `A ∖ S`, each `R`-equivalent to `A` (hence to each other +when `R` is transitive) [Ambos-Spies 1984][AmbosSpies1984]. -/ def MitoticWith (𝒞 : Set (Set α)) (R : Set α → Set α → Prop) (A : Set α) : Prop := ∃ S ∈ 𝒞, ReducibleEquiv R A (A ∩ S) ∧ ReducibleEquiv R A (A \ S) @@ -572,6 +585,7 @@ theorem PolyTimeManyOneMitotic.polyTimeBTTMitotic (h : PolyTimeManyOneMitotic en ⟨h₁.1.polyTimeBTTReducible, h₁.2.polyTimeBTTReducible⟩, ⟨h₂.1.polyTimeBTTReducible, h₂.2.polyTimeBTTReducible⟩⟩ +/-- Bounded truth-table mitoticity implies truth-table mitoticity. -/ theorem PolyTimeBTTMitotic.polyTimeTruthTableMitotic (h : PolyTimeBTTMitotic encA A) : PolyTimeTruthTableMitotic encA A := by obtain ⟨S, hS, h₁, h₂⟩ := h @@ -579,6 +593,7 @@ theorem PolyTimeBTTMitotic.polyTimeTruthTableMitotic (h : PolyTimeBTTMitotic enc ⟨h₁.1.polyTimeTruthTableReducible, h₁.2.polyTimeTruthTableReducible⟩, ⟨h₂.1.polyTimeTruthTableReducible, h₂.2.polyTimeTruthTableReducible⟩⟩ +/-- Many-one mitoticity implies truth-table mitoticity. -/ theorem PolyTimeManyOneMitotic.polyTimeTruthTableMitotic (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableMitotic encA A := h.polyTimeBTTMitotic.polyTimeTruthTableMitotic @@ -622,20 +637,31 @@ private theorem mitotic_candidate_notMem {S : Set α} {s : α → Bool} (hsS : · exact (hsS (f₁ a)).mpr hsf exact haS.2 hS' -/-- **Every polynomial-time many-one mitotic set is disjunctive truth-table autoreducible**, -unconditionally. If the image lands on the wrong side of the separator, 0 queries are made; -otherwise 1 query on the opposite side of `S` is made, guaranteed distinct from `a`. -/ -theorem PolyTimeManyOneMitotic.polyTimeDTTAutoreducible (h : PolyTimeManyOneMitotic encA A) : - PolyTimeDTTAutoreducible encA A := by - obtain ⟨S, hS, ⟨hA₂, -⟩, ⟨hA₁, -⟩⟩ := h - obtain ⟨s, hs, hsS⟩ := hS - obtain ⟨f₂, hf₂, hAf₂⟩ := hA₂ - obtain ⟨f₁, hf₁, hAf₁⟩ := hA₁ +private theorem PolyTimeManyOneMitotic.exists_candidate (h : PolyTimeManyOneMitotic encA A) : + ∃ (candidate : α → α) (good : α → Bool), + ComputableInPolyTime candidate encA encA ∧ + ComputableInPolyTime good encA encBool ∧ + (∀ a, good a = true → candidate a ≠ a) ∧ + (∀ a, good a = true → (a ∈ A ↔ candidate a ∈ A)) ∧ + (∀ a, ¬ good a = true → a ∉ A) := by + obtain ⟨S, ⟨s, hs, hsS⟩, ⟨⟨f₂, hf₂, hAf₂⟩, -⟩, ⟨⟨f₁, hf₁, hAf₁⟩, -⟩⟩ := h let candidate : α → α := fun a => if s a then f₁ a else f₂ a have hcand : ComputableInPolyTime candidate encA encA := ComputableInPolyTime.ite hs hf₁ hf₂ let good : α → Bool := fun a => (s (candidate a) != s a) have hgood : ComputableInPolyTime good encA encBool := by fun_prop + exact ⟨candidate, good, hcand, hgood, + fun a hg => mitotic_candidate_ne hg, + fun a hg => mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg, + fun a hg => mitotic_candidate_notMem hsS hAf₁ hAf₂ hg⟩ + +/-- **Every polynomial-time many-one mitotic set is disjunctive truth-table autoreducible**, +unconditionally [Ambos-Spies 1984][AmbosSpies1984]. If the image lands on the wrong side of the +separator, 0 queries are made; otherwise 1 query on the opposite side of `S` is made, guaranteed +distinct from `a`. -/ +theorem PolyTimeManyOneMitotic.polyTimeDTTAutoreducible (h : PolyTimeManyOneMitotic encA A) : + PolyTimeDTTAutoreducible encA A := by + obtain ⟨candidate, good, hcand, hgood, hne, hmem, hnotMem⟩ := h.exists_candidate let r : α → ℕ := fun a => if good a then 1 else 0 have hr : ComputableInPolyTime r encA encUnary := by fun_prop let q : α × ℕ → α := fun p => candidate p.1 @@ -644,28 +670,20 @@ theorem PolyTimeManyOneMitotic.polyTimeDTTAutoreducible (h : PolyTimeManyOneMito refine ⟨r, q, hr, hq, fun a i hi => ?_, fun a => ?_⟩ · dsimp only [r] at hi split_ifs at hi with hg - · exact mitotic_candidate_ne hg + · exact hne a hg · omega · dsimp only [r, q] split_ifs with hg · simp only [Nat.lt_one_iff, exists_eq_left] - exact mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg + exact hmem a hg · simp only [Nat.not_lt_zero, false_and, exists_false, iff_false] - exact mitotic_candidate_notMem hsS hAf₁ hAf₂ hg + exact hnotMem a hg /-- **Every polynomial-time many-one mitotic set is `1`-truth-table autoreducible**, -unconditionally. -/ +unconditionally [Ambos-Spies 1984][AmbosSpies1984]. -/ theorem PolyTimeManyOneMitotic.polyTimeKTruthTableAutoreducible_one (h : PolyTimeManyOneMitotic encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := by - obtain ⟨S, hS, ⟨hA₂, -⟩, ⟨hA₁, -⟩⟩ := h - obtain ⟨s, hs, hsS⟩ := hS - obtain ⟨f₂, hf₂, hAf₂⟩ := hA₂ - obtain ⟨f₁, hf₁, hAf₁⟩ := hA₁ - let candidate : α → α := fun a => if s a then f₁ a else f₂ a - have hcand : ComputableInPolyTime candidate encA encA := - ComputableInPolyTime.ite hs hf₁ hf₂ - let good : α → Bool := fun a => (s (candidate a) != s a) - have hgood : ComputableInPolyTime good encA encBool := by fun_prop + obtain ⟨candidate, good, hcand, hgood, hne, hmem, hnotMem⟩ := h.exists_candidate let r : α → ℕ := fun a => if good a then 1 else 0 have hr : ComputableInPolyTime r encA encUnary := by fun_prop let q : α × ℕ → α := fun p => candidate p.1 @@ -678,44 +696,38 @@ theorem PolyTimeManyOneMitotic.polyTimeKTruthTableAutoreducible_one split_ifs <;> omega · dsimp only [r] at hi split_ifs at hi with hg - · exact mitotic_candidate_ne hg + · exact hne a hg · omega · dsimp only [r, q, d, truthTableAnswers] by_cases hg : good a = true · simp only [hg, ↓reduceIte, List.ofFn_succ, List.ofFn_zero, List.headD_cons, Set.mem_preimage, decide_eq_true_eq] - exact mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg + exact hmem a hg · simp only [hg, ↓reduceIte, List.ofFn_zero, List.headD_nil, Bool.false_eq_true, iff_false] - exact mitotic_candidate_notMem hsS hAf₁ hAf₂ hg + exact hnotMem a hg +/-- Every polynomial-time many-one mitotic set is bounded truth-table autoreducible. -/ theorem PolyTimeManyOneMitotic.polyTimeBTTAutoreducible (h : PolyTimeManyOneMitotic encA A) : PolyTimeBTTAutoreducible encA A := h.polyTimeKTruthTableAutoreducible_one.polyTimeBTTAutoreducible +/-- Every polynomial-time many-one mitotic set is truth-table autoreducible. -/ theorem PolyTimeManyOneMitotic.polyTimeTruthTableAutoreducible (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableAutoreducible encA A := h.polyTimeBTTAutoreducible.polyTimeTruthTableAutoreducible /-- **A polynomial-time many-one mitotic set is many-one autoreducible provided its complement -is not a singleton.** -/ +is not a singleton** [Ambos-Spies 1984][AmbosSpies1984]. -/ theorem PolyTimeManyOneMitotic.polyTimeManyOneAutoreducible (h : PolyTimeManyOneMitotic encA A) (hCompl : ∀ a ∉ A, ∃ n ∉ A, n ≠ a) : PolyTimeManyOneAutoreducible encA A := by classical - obtain ⟨S, hS, ⟨hA₂, -⟩, ⟨hA₁, -⟩⟩ := h - obtain ⟨s, hs, hsS⟩ := hS - obtain ⟨f₂, hf₂, hAf₂⟩ := hA₂ - obtain ⟨f₁, hf₁, hAf₁⟩ := hA₁ - let candidate : α → α := fun a => if s a then f₁ a else f₂ a - have hcand : ComputableInPolyTime candidate encA encA := - ComputableInPolyTime.ite hs hf₁ hf₂ - let good : α → Bool := fun a => (s (candidate a) != s a) - have hgood : ComputableInPolyTime good encA encBool := by fun_prop + obtain ⟨candidate, good, hcand, hgood, hne, hmem, hnotMem⟩ := h.exists_candidate by_cases hUniv : ∀ a, a ∈ A · refine ⟨candidate, ⟨hcand, fun a => ?_⟩, fun a => by simp [hUniv (candidate a), hUniv a]⟩ have hg : good a = true := by by_contra hbad - exact (mitotic_candidate_notMem hsS hAf₁ hAf₂ hbad) (hUniv a) - exact mitotic_candidate_ne hg + exact (hnotMem a hbad) (hUniv a) + exact hne a hg · obtain ⟨n₀, hn₀⟩ : ∃ n, n ∉ A := by by_contra hc apply hUniv @@ -730,7 +742,7 @@ theorem PolyTimeManyOneMitotic.polyTimeManyOneAutoreducible (h : PolyTimeManyOne · dsimp only [f] by_cases hg : good a = true · simp only [hg, ↓reduceIte] - exact mitotic_candidate_ne hg + exact hne a hg · simp only [hg, Bool.false_eq_true, ↓reduceIte] split_ifs with ha · intro heq; subst ha; exact hnne heq @@ -738,13 +750,13 @@ theorem PolyTimeManyOneMitotic.polyTimeManyOneAutoreducible (h : PolyTimeManyOne · dsimp only [f] by_cases hg : good a = true · simp only [hg, ↓reduceIte] - exact mitotic_candidate_mem_iff hsS hAf₁ hAf₂ hg + exact hmem a hg · simp only [hg, Bool.false_eq_true, ↓reduceIte] - have haA := mitotic_candidate_notMem hsS hAf₁ hAf₂ hg + have haA := hnotMem a hg split_ifs with ha <;> simp [haA, hn₀, hn₁] /-- **A polynomial-time many-one mitotic set is many-one autoreducible if and only if its -complement is not a singleton.** -/ +complement is not a singleton** [Ambos-Spies 1984][AmbosSpies1984]. -/ theorem PolyTimeManyOneMitotic.polyTimeManyOneAutoreducible_iff (h : PolyTimeManyOneMitotic encA A) : PolyTimeManyOneAutoreducible encA A ↔ ∀ a ∉ A, ∃ n ∉ A, n ≠ a := diff --git a/ComplexityTests/Autoreducibility.lean b/ComplexityTests/Autoreducibility.lean index d998215c82..dc9df70476 100644 --- a/ComplexityTests/Autoreducibility.lean +++ b/ComplexityTests/Autoreducibility.lean @@ -44,60 +44,37 @@ example : PolyTimeManyOneAutoreducible encBits headTrueSet := (y₀ := [true]) (y₁ := [true, false]) rfl rfl (by decide) (n₀ := []) (n₁ := [false]) (fun h => by cases h) (fun h => by cases h) (by decide) -/-! ### Autoreducibility hierarchy projections -/ - -example (h : LogSpaceManyOneAutoreducible encA A) : PolyTimeManyOneAutoreducible encA A := - h.polyTimeManyOneAutoreducible - -example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := - h.polyTimeKTruthTableAutoreducible_one - -example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeDTTAutoreducible encA A := - h.polyTimeDTTAutoreducible - -example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeCTTAutoreducible encA A := - h.polyTimeCTTAutoreducible - -example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeBTTAutoreducible encA A := - h.polyTimeBTTAutoreducible - -example (h : PolyTimeManyOneAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := - h.polyTimeTruthTableAutoreducible - -example (h : PolyTimeDTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := - h.polyTimeTruthTableAutoreducible - -example (h : PolyTimeCTTAutoreducible encA A) : PolyTimeTruthTableAutoreducible encA A := - h.polyTimeTruthTableAutoreducible - -example : PolyTimeDTTAutoreducible encA A ↔ PolyTimeCTTAutoreducible encA Aᶜ := - polyTimeDTTAutoreducible_iff_polyTimeCTTAutoreducible_compl - -/-! ### Mitoticity hierarchy and autoreducibility implications -/ - -example (h : LogSpaceManyOneMitotic encA A) : PolyTimeManyOneMitotic encA A := - h.polyTimeManyOneMitotic - -example (h : PolyTimeManyOneMitotic encA A) : PolyTimeBTTMitotic encA A := - h.polyTimeBTTMitotic - -example (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableMitotic encA A := - h.polyTimeTruthTableMitotic - -example (h : PolyTimeManyOneMitotic encA A) : PolyTimeDTTAutoreducible encA A := - h.polyTimeDTTAutoreducible - -example (h : PolyTimeManyOneMitotic encA A) : PolyTimeKTruthTableAutoreducible 1 encA A := - h.polyTimeKTruthTableAutoreducible_one - -example (h : PolyTimeManyOneMitotic encA A) : PolyTimeBTTAutoreducible encA A := - h.polyTimeBTTAutoreducible - -example (h : PolyTimeManyOneMitotic encA A) : PolyTimeTruthTableAutoreducible encA A := - h.polyTimeTruthTableAutoreducible - -example (h : PolyTimeManyOneMitotic encA A) : - PolyTimeManyOneAutoreducible encA A ↔ ∀ a ∉ A, ∃ n ∉ A, n ≠ a := - h.polyTimeManyOneAutoreducible_iff +/-! ### Concrete polynomial-time many-one mitotic set -/ + +/-- `{[]}ᶜ` is polynomial-time many-one mitotic, split by `headTrueSet`. Both halves `{w | w ≠ [] ∧ +w.headD false = true}` and `{w | w ≠ [] ∧ w.headD false = false}` are non-empty and non-universal +sets in `P`, so both are mutually polynomial-time reducible to `{[]}ᶜ`. -/ +theorem coSingleton_mitotic : PolyTimeManyOneMitotic encBits ({[]}ᶜ : Set (List Bool)) := + ⟨headTrueSet, headTrueSet_mem_P, + ⟨⟨fun w => if w.isEmpty then [] else [true], by fun_prop, + fun w => by cases w <;> simp [headTrueSet]⟩, + ⟨fun w => if w.headD false then [true] else [], by fun_prop, + fun w => by rcases w with _ | ⟨_ | _, _⟩ <;> simp [headTrueSet]⟩⟩, + ⟨⟨fun w => if w.isEmpty then [] else [false], by fun_prop, + fun w => by cases w <;> simp [headTrueSet]⟩, + ⟨fun w => if !w.isEmpty && !w.headD false then [true] else [], by fun_prop, + fun w => by rcases w with _ | ⟨_ | _, _⟩ <;> simp [headTrueSet]⟩⟩⟩ + +-- `{[]}ᶜ` is disjunctive, 1-truth-table, bounded truth-table, and truth-table autoreducible. +example : PolyTimeDTTAutoreducible encBits ({[]}ᶜ : Set (List Bool)) := + coSingleton_mitotic.polyTimeDTTAutoreducible + +example : PolyTimeKTruthTableAutoreducible 1 encBits ({[]}ᶜ : Set (List Bool)) := + coSingleton_mitotic.polyTimeKTruthTableAutoreducible_one + +example : PolyTimeBTTAutoreducible encBits ({[]}ᶜ : Set (List Bool)) := + coSingleton_mitotic.polyTimeBTTAutoreducible + +example : PolyTimeTruthTableAutoreducible encBits ({[]}ᶜ : Set (List Bool)) := + coSingleton_mitotic.polyTimeTruthTableAutoreducible + +-- However, `{[]}ᶜ` is strictly not many-one autoreducible, because its complement is a singleton. +example : ¬ PolyTimeManyOneAutoreducible encBits ({[]}ᶜ : Set (List Bool)) := + not_polyTimeManyOneAutoreducible_compl_singleton [] end ComplexityTests.Autoreducibility diff --git a/references.bib b/references.bib index a72a724fad..1d00b99d37 100644 --- a/references.bib +++ b/references.bib @@ -178,7 +178,7 @@ @incollection{AmbosSpies1984 pages = {1--23}, publisher = {Springer}, year = {1984}, - doi = {10.1007/3-540-13331-3_1} + doi = {10.1007/3-540-13331-3_30} } @article{AnderssonMiltersenThorup1999, @@ -1680,7 +1680,7 @@ @article{GlasserPavanSelmanZhang2008 number = {5}, pages = {1517--1535}, year = {2008}, - doi = {10.1137/060677579} + doi = {10.1137/060673886} } @book{Goldreich2001,