diff --git a/ToMathlib/Computability/MachineCounting.lean b/ToMathlib/Computability/MachineCounting.lean index 90110b499..dcb0daf14 100644 --- a/ToMathlib/Computability/MachineCounting.lean +++ b/ToMathlib/Computability/MachineCounting.lean @@ -25,14 +25,15 @@ The pieces, each isolated so the diagonalization argument reads as pure counting (`card_tmTable`, bounded by `Turing.SingleTapeTM.B`), and `reify` packages one back into a `SingleTapeTM Bool`. The `Fintype`/`DecidableEq` instances for the underlying `Turing.Dir` and `SingleTapeTM.Stmt Bool` are supplied here. -* **State normalization** (`exists_tmTable_of_card_le`, an isolated `sorry`): any +* **State normalization** (`exists_tmTable_of_card_le`): any `SingleTapeTM Bool` with at most `d` states computes the same string function as `reify` of some `TMTable d`. * **Realizable predicates** (`Computability.RealizableLE`): the predicates realizable by an input/output `EncPolyTime` pair of description size at most `d`. This set is covered by a `Finset` of cardinality at most `B d ^ 2` (`exists_realizableLE_covering`, the - isolated counting `sorry`: the surjection `TMTable d × TMTable d → RealizableLE n d` - built from state normalization), and it is monotone in `d` (`realizableLE_mono`). + counting core: the cover of `RealizableLE n d` by the image of + `TMTable d × TMTable d` under `tablePairPred`, built from state normalization), and it is + monotone in `d` (`realizableLE_mono`). * **Growth bounds**: every polynomial is eventually dominated by `2 ^ (n / 4)` (`Computability.eventually_poly_le`), while the machine count stays below the function count (`Computability.eventually_count_lt`). @@ -103,18 +104,227 @@ def reify {d : ℕ} (t : TMTable d) : SingleTapeTM Bool where q₀ := t.2 tr := t.1 +/-! ## State-relabeling normalization construction + +The machinery discharging `exists_tmTable_of_card_le`: relabel the finite state space of a +machine `tm` through `Fintype.equivFin`, embed `Fin (card tm.State)` into `Fin d` along the +cardinality inequality (`embFin`), and transport the transition function on the image +(`normTr`), sending every spare state (those outside the image, detected by `decFin`) to a +fixed halting transition. Configurations transport along `normCfg`, single steps correspond +(`step_normCfg`), and this lifts through `ReflTransGen` in both directions +(`normCfg_reflTransGen`, `reflTransGen_normCfg_reverse`), giving the `Outputs` equivalence. -/ + +section Normalize + +/-- Embed a finite type into `Fin d` (with `card ≤ d`) via its `Fintype.equivFin` labeling. -/ +noncomputable def embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) : + Fin d := + (Fintype.equivFin α s).castLE hd + +/-- The partial inverse of `embFin`: recover the state whose label is `i`, or `none` for +spare indices `i` with no preimage. -/ +noncomputable def decFin {α : Type*} [Fintype α] {d : ℕ} (i : Fin d) : Option α := + if hi : (i : ℕ) < Fintype.card α then some ((Fintype.equivFin α).symm ⟨i, hi⟩) else none + +/-- `decFin` inverts `embFin` on the image. -/ +lemma decFin_embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) : + (decFin (embFin hd s) : Option α) = some s := by + have hlt : ((embFin hd s : Fin d) : ℕ) < Fintype.card α := by + simp only [embFin, Fin.val_castLE]; exact (Fintype.equivFin α s).isLt + simp only [decFin, dif_pos hlt] + congr 1 + apply (Fintype.equivFin α).symm_apply_eq.mpr + apply Fin.ext + simp [embFin, Fin.val_castLE] + +/-- `embFin` is injective. -/ +lemma embFin_injective {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) : + Function.Injective (embFin hd) := fun _ _ hab => + (Fintype.equivFin α).injective (Fin.castLE_injective hd hab) + +variable {d : ℕ} (tm : SingleTapeTM Bool) (emb : tm.State → Fin d) + (dec : Fin d → Option tm.State) + +/-- Transition table transporting `tm`'s transitions along `emb`; spare states (those with +`dec i = none`) are given a fixed halting transition. -/ +noncomputable def normTr : Fin d → Option Bool → SingleTapeTM.Stmt Bool × Option (Fin d) := + fun i b => + match dec i with + | some s => ((tm.tr s b).1, (tm.tr s b).2.map emb) + | none => (default, none) + +/-- The canonical `d`-state table normalizing `tm` onto `Fin d` along `emb`/`dec`. -/ +noncomputable def normTable : TMTable d := (normTr tm emb dec, emb tm.q₀) + +/-- Transport a configuration of `tm` to the reified normalized machine. -/ +noncomputable def normCfg (c : tm.Cfg) : (reify (normTable tm emb dec)).Cfg := + ⟨c.state.map emb, c.BiTape⟩ + +variable {tm emb dec} + +/-- The reified normalized machine's step transports `tm`'s step along `normCfg`, provided +`dec` inverts `emb` on the image. -/ +lemma step_normCfg (hdec : ∀ s, dec (emb s) = some s) (c : tm.Cfg) : + (reify (normTable tm emb dec)).step (normCfg tm emb dec c) + = (tm.step c).map (normCfg tm emb dec) := by + obtain ⟨st, tp⟩ := c + cases st with + | none => rfl + | some q => + have hdq : dec (emb q) = some q := hdec q + rcases htr : tm.tr q tp.head with ⟨⟨wr, dir⟩, q''⟩ + simp only [step, normCfg, reify, normTable, normTr, Option.map_some, hdq, htr] + +/-- `normCfg` is injective when `emb` is. -/ +lemma normCfg_injective (hemb : Function.Injective emb) : + Function.Injective (normCfg tm emb dec) := by + rintro ⟨s1, t1⟩ ⟨s2, t2⟩ h + simp only [normCfg, Cfg.mk.injEq] at h + obtain ⟨hs, ht⟩ := h + have hss : s1 = s2 := Option.map_injective hemb hs + subst hss; subst ht; rfl + +/-- A run of `tm` maps forward to a run of the normalized machine. -/ +lemma normCfg_reflTransGen (hdec : ∀ s, dec (emb s) = some s) {c c' : tm.Cfg} + (h : Relation.ReflTransGen tm.TransitionRelation c c') : + Relation.ReflTransGen (reify (normTable tm emb dec)).TransitionRelation + (normCfg tm emb dec c) (normCfg tm emb dec c') := by + refine Relation.ReflTransGen.lift (normCfg tm emb dec) ?_ h + intro a b hab + have hs := step_normCfg hdec a + rw [show tm.step a = some b from hab, Option.map_some] at hs + exact hs + +/-- A run of the normalized machine from an image configuration stays in the image and maps +back to a run of `tm`. -/ +lemma reflTransGen_normCfg_reverse (hdec : ∀ s, dec (emb s) = some s) {c : tm.Cfg} + {c' : (reify (normTable tm emb dec)).Cfg} + (h : Relation.ReflTransGen (reify (normTable tm emb dec)).TransitionRelation + (normCfg tm emb dec c) c') : + ∃ c₂, c' = normCfg tm emb dec c₂ ∧ Relation.ReflTransGen tm.TransitionRelation c c₂ := by + induction h with + | refl => exact ⟨c, rfl, Relation.ReflTransGen.refl⟩ + | @tail b e hab hbc ih => + obtain ⟨c₂, rfl, hrun⟩ := ih + have hs := step_normCfg hdec c₂ + rw [show (reify (normTable tm emb dec)).step (normCfg tm emb dec c₂) = some e from hbc] at hs + obtain ⟨c₃, hstep, hc3⟩ := Option.map_eq_some_iff.mp hs.symm + exact ⟨c₃, hc3.symm, hrun.tail hstep⟩ + +end Normalize + +/-! ## Determinism of machine runs + +Supporting facts for `Computability.exists_realizableLE_covering`: a single-tape machine +is deterministic (its `step` is a function), so the output list of a halting run is +unique. This lets the covering predicate attached to a table pair be read off by an +unbounded-search-free choice construction and still agree with any witness predicate. -/ + +section Determinism + +/-- In a relation that is a partial function (deterministic), two irreducible points +reachable from a common source coincide. -/ +theorem _root_.Relation.ReflTransGen.unique_of_deterministic + {α : Type*} {R : α → α → Prop} + (hdet : ∀ {a b c : α}, R a b → R a c → b = c) + {a b c : α} (hb : Relation.ReflTransGen R a b) (hc : Relation.ReflTransGen R a c) + (hbf : ∀ y, ¬ R b y) (hcf : ∀ y, ¬ R c y) : b = c := by + induction hb using Relation.ReflTransGen.head_induction_on with + | refl => + rcases hc.cases_head with h | ⟨y, hy, _⟩ + · exact h + · exact absurd hy (hbf y) + | head h' _ ih => + rename_i a' _ + rcases hc.cases_head with h | ⟨y, hy, hyc⟩ + · exact absurd (h ▸ h') (hcf a') + · rw [hdet h' hy] at ih; exact ih hyc + +/-- Distinct input lists give distinct initial/halting tapes: `BiTape.mk₁` is injective. -/ +theorem _root_.Turing.BiTape.mk₁_injective {Symbol : Type} : + Function.Injective (Turing.BiTape.mk₁ : List Symbol → Turing.BiTape Symbol) := by + intro l₁ l₂ h + cases l₁ with + | nil => + cases l₂ with + | nil => rfl + | cons b t => simp [Turing.BiTape.mk₁, Turing.BiTape.nil] at h + | cons a s => + cases l₂ with + | nil => simp [Turing.BiTape.mk₁, Turing.BiTape.nil] at h + | cons b t => + simp only [Turing.BiTape.mk₁, Turing.BiTape.mk.injEq, Option.some.injEq] at h + obtain ⟨hab, -, hst⟩ := h + have : (s.map some) = (t.map some) := by + have := congrArg Turing.StackTape.toList hst + simpa [Turing.StackTape.mapSome] using this + have hst' : s = t := List.map_injective_iff.mpr (Option.some_injective _) this + rw [hab, hst'] + +variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] + +/-- A halting configuration is irreducible: no transition leaves the halting state. -/ +theorem not_transitionRelation_haltCfg (tm : SingleTapeTM Symbol) (l : List Symbol) + (y : tm.Cfg) : ¬ tm.TransitionRelation (tm.haltCfg l) y := by + intro hy + simp only [TransitionRelation, haltCfg, step] at hy + exact absurd hy (by simp) + +/-- The output list of a halting machine run is unique: the machine is deterministic. -/ +theorem Outputs_unique (tm : SingleTapeTM Symbol) {l l₁ l₂ : List Symbol} + (h1 : tm.Outputs l l₁) (h2 : tm.Outputs l l₂) : l₁ = l₂ := by + have hcfg : tm.haltCfg l₁ = tm.haltCfg l₂ := by + refine Relation.ReflTransGen.unique_of_deterministic (R := tm.TransitionRelation) + (fun {a b c} hab hac => ?_) h1 h2 (not_transitionRelation_haltCfg tm l₁) + (not_transitionRelation_haltCfg tm l₂) + rw [TransitionRelation] at hab hac + rw [hab] at hac + exact Option.some.inj hac + have := congrArg Cfg.BiTape hcfg + simp only [haltCfg] at this + exact Turing.BiTape.mk₁_injective this + +/-- A polynomial-time machine halts with the correct output on every input. -/ +theorem PolyTimeComputable.outputs {f : List Symbol → List Symbol} + (h : PolyTimeComputable f) (a : List Symbol) : h.tm.Outputs a (f a) := by + obtain ⟨m, _, hm⟩ := h.outputsFunInTime a + exact hm.reflTransGen + +end Determinism + /-! ## State normalization -/ -/-- **[Isolated crux, `sorry`]** Every `SingleTapeTM Bool` computing a string function -with at most `d` states computes the same function as `reify` of some `TMTable d` — the -state space is relabeled to `Fin d` along `Fintype.equivFin`, preserving the `Outputs` -relation. Discharging this is the Cslib-internal run-preservation-under-state-relabeling -lemma; it needs an induction over `SingleTapeTM.step` / `RelatesInSteps` transported along -the relabeling. It is the machine-theoretic input to `exists_realizableLE_covering`. -/ +/-- Every `SingleTapeTM Bool` computing a string function with at most `d` states computes +the same function as `reify` of some `TMTable d` — the state space is relabeled to `Fin d` +along `Fintype.equivFin`, preserving the `Outputs` relation. It is the machine-theoretic +input to `exists_realizableLE_covering`. -/ theorem exists_tmTable_of_card_le {f : List Bool → List Bool} (h : PolyTimeComputable f) {d : ℕ} (hd : Fintype.card h.tm.State ≤ d) : ∃ t : TMTable d, ∀ l l', (reify t).Outputs l l' ↔ h.tm.Outputs l l' := by - sorry + set tm := h.tm with htm + refine ⟨normTable tm (embFin hd) (decFin (α := tm.State)), fun l l' => ?_⟩ + have hdec : ∀ s, decFin (α := tm.State) (embFin hd s) = some s := decFin_embFin hd + have hemb : Function.Injective (embFin (α := tm.State) hd) := embFin_injective hd + have hinit : normCfg tm (embFin hd) (decFin (α := tm.State)) (tm.initCfg l) + = (reify (normTable tm (embFin hd) (decFin (α := tm.State)))).initCfg l := rfl + have hhalt : normCfg tm (embFin hd) (decFin (α := tm.State)) (tm.haltCfg l') + = (reify (normTable tm (embFin hd) (decFin (α := tm.State)))).haltCfg l' := rfl + constructor + · intro hout + have hout' : Relation.ReflTransGen + (reify (normTable tm (embFin hd) (decFin (α := tm.State)))).TransitionRelation + (normCfg tm (embFin hd) (decFin (α := tm.State)) (tm.initCfg l)) + ((reify (normTable tm (embFin hd) (decFin (α := tm.State)))).haltCfg l') := by + rw [hinit]; exact hout + obtain ⟨c₂, hc₂, hrun⟩ := reflTransGen_normCfg_reverse hdec hout' + rw [← hhalt] at hc₂ + have hcfg : tm.haltCfg l' = c₂ := normCfg_injective hemb hc₂ + rw [← hcfg] at hrun + exact hrun + · intro hout + have hmap := normCfg_reflTransGen hdec hout + rw [hinit, hhalt] at hmap + exact hmap end Turing.SingleTapeTM @@ -143,16 +353,61 @@ theorem realizableLE_mono {n : ℕ} {d d' : ℕ} (h : d ≤ d') : rintro g ⟨σ, es, init, output, i, o, hi, ho, hg⟩ exact ⟨σ, es, init, output, i, o, hi.trans h, ho.trans h, hg⟩ -/-- **[Isolated counting crux, `sorry`]** The realizable predicates at description size at -most `d` are covered by a `Finset` of cardinality at most `B d ^ 2`. Discharging this uses -state normalization (`exists_tmTable_of_card_le`) to reduce each realizing pair of witness -machines to a pair `TMTable d × TMTable d` of canonical `d`-state tables; the realized -predicate factors through the two tables (decode the output encoding of the composite run), -giving a surjection from `TMTable d × TMTable d` onto `RealizableLE n d`, whence -`card ≤ Fintype.card (TMTable d × TMTable d) = B d ^ 2` (`card_tmTable`). -/ +open Classical in +/-- The total predicate `BitVec n → Bool` attached to a pair of canonical `d`-state tables: +run `reify p.1` on the canonical input encoding of `x`, feed its (deterministic) output to +`reify p.2`, and decode the resulting canonical `Option Bool` encoding. Totality is ensured +by a deterministic choice over the (at most one, by `Outputs_unique`) successful run, with +an arbitrary `false` fallback where no such run exists — no claim that either raw table +pair halts or is polynomial-time. -/ +noncomputable def tablePairPred (n d : ℕ) (p : TMTable d × TMTable d) : BitVec n → Bool := + fun x => + if h : ∃ b : Bool, ∃ l₁ : List Bool, + (reify p.1).Outputs (BitEncFam.bitVecX.enc n x) l₁ ∧ + (reify p.2).Outputs l₁ (BitEncFam.bool.option.enc n (some b)) + then h.choose else false + +/-- The realizable predicates at description size at most `d` are covered by a `Finset` of +cardinality at most `B d ^ 2`. State normalization (`exists_tmTable_of_card_le`) reduces each +realizing pair of witness machines to a pair `TMTable d × TMTable d` of canonical `d`-state +tables; the realized predicate is recovered from the two tables by `tablePairPred` (running +both reified machines and decoding the canonical output encoding, using determinism of the +runs via `Outputs_unique`). Thus `RealizableLE n d` lands in the image of +`TMTable d × TMTable d` under `tablePairPred`, whence +`card ≤ Fintype.card (TMTable d × TMTable d) = B d ^ 2` (`card_tmTable`). The map need not be +injective — it only needs to cover the realizable set. -/ theorem exists_realizableLE_covering (n d : ℕ) : ∃ s : Finset (BitVec n → Bool), RealizableLE n d ⊆ ↑s ∧ s.card ≤ B d ^ 2 := by - sorry + classical + refine ⟨Finset.image (tablePairPred n d) + (Finset.univ : Finset (TMTable d × TMTable d)), ?_, ?_⟩ + · rintro g ⟨σ, es, init, output, i, o, hi, ho, hg⟩ + obtain ⟨t₁, ht₁⟩ := exists_tmTable_of_card_le i.polyTime (d := d) hi + obtain ⟨t₂, ht₂⟩ := exists_tmTable_of_card_le o.polyTime (d := d) ho + refine Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨(t₁, t₂), Finset.mem_univ _, ?_⟩) + funext x + have hrun1 : (reify t₁).Outputs (BitEncFam.bitVecX.enc n x) (es (init x)) := by + rw [ht₁] + have h := i.polyTime.outputs (BitEncFam.bitVecX.enc n x) + rwa [i.map_encode x] at h + have hrun2 : (reify t₂).Outputs (es (init x)) + (BitEncFam.bool.option.enc n (some (g x))) := by + rw [ht₂] + have h := o.polyTime.outputs (es (init x)) + rwa [o.map_encode (init x), hg x] at h + have hex : ∃ b : Bool, ∃ l₁ : List Bool, + (reify t₁).Outputs (BitEncFam.bitVecX.enc n x) l₁ ∧ + (reify t₂).Outputs l₁ (BitEncFam.bool.option.enc n (some b)) := + ⟨g x, es (init x), hrun1, hrun2⟩ + have hpick : tablePairPred n d (t₁, t₂) x = hex.choose := dif_pos hex + rw [hpick] + obtain ⟨l₁', hl1', hl2'⟩ := hex.choose_spec + have hl1eq : l₁' = es (init x) := Outputs_unique _ hl1' hrun1 + rw [hl1eq] at hl2' + have henc := Outputs_unique _ hl2' hrun2 + exact Option.some.inj ((BitEncFam.bool.option).enc_injective n henc) + · refine Finset.card_image_le.trans ?_ + rw [Finset.card_univ, Fintype.card_prod, card_tmTable, sq] /-! ## Cardinality of the predicate space -/ diff --git a/VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean b/VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean index aaaf4b273..30b4669e3 100644 --- a/VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean +++ b/VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean @@ -38,6 +38,194 @@ may depend on them. open OracleSpec Computability +/-! ## Local support: appending a fixed bit on a single-tape machine + +The compiled deterministic run inserts the fixed canonical coin answer into the state +encoding before each `update` step. At the canonical coin boundary the query index has +width `0` and the answer `⟨t, r⟩` encodes as the single bit `[r]`, so "insert the fixed +`true` answer" is exactly appending `[true]` to the state encoding. The Cslib base library +provides `idComputer`, `constComputer`, and `tableComputer`, but no combinator appending a +fixed suffix to an *unbounded* string; we supply one here as local support, in the same +`SingleTapeTM` style. -/ + +namespace Turing.SingleTapeTM + +open Turing Relation + +/-- Append a fixed symbol `c` at the right end of the input: walk right keeping every +symbol (`inl`), write `c` at the trailing blank and turn around (`inr`), then walk back +left keeping every symbol until falling off the left end, where one right step lands the +head on the first symbol of the output `l ++ [c]`. -/ +def snocComputer (c : Bool) : SingleTapeTM Bool where + State := Unit ⊕ Unit + q₀ := .inl () + tr q h := match q with + | .inl () => match h with + | some b => ⟨⟨some b, some .right⟩, some (.inl ())⟩ + | none => ⟨⟨some c, some .left⟩, some (.inr ())⟩ + | .inr () => match h with + | some b => ⟨⟨some b, some .left⟩, some (.inr ())⟩ + | none => ⟨⟨none, some .right⟩, none⟩ + +/-- The left stack after the rightward pass has consumed `l` (starting from stack `L`): +each symbol of `l` is pushed on top in turn, so the top is the last symbol of `l`. -/ +private def snocPush : StackTape Bool → List Bool → StackTape Bool + | L, [] => L + | L, b :: t => snocPush (StackTape.cons (some b) L) t + +@[simp] private lemma snocPush_nil (L : StackTape Bool) : snocPush L [] = L := rfl + +@[simp] private lemma snocPush_cons (L : StackTape Bool) (b : Bool) (t : List Bool) : + snocPush L (b :: t) = snocPush (StackTape.cons (some b) L) t := rfl + +private lemma stackTape_ext {a b : StackTape Bool} (h : a.toList = b.toList) : a = b := by + cases a; cases b; cases h; rfl + +private lemma snocPush_toList (L : StackTape Bool) (l : List Bool) : + (snocPush L l).toList = l.reverse.map some ++ L.toList := by + induction l generalizing L with + | nil => simp + | cons b t ih => + rw [snocPush_cons, ih (StackTape.cons (some b) L), StackTape.cons_some_toList] + simp + +private lemma mapSome_head (l : List Bool) : + (StackTape.mapSome l).head = l.head?.map some := by + cases l <;> rfl + +private lemma mapSome_tail (l : List Bool) : + (StackTape.mapSome l).tail = StackTape.mapSome l.tail := by + cases l <;> rfl + +private lemma mk₁_eq (s : List Bool) : + (BiTape.mk₁ s : BiTape Bool) = + ⟨(StackTape.mapSome s).head, ∅, (StackTape.mapSome s).tail⟩ := by + cases s <;> rfl + +/-- Rightward pass: from head over the first of `l` with left stack `L`, reach the trailing +blank with `l` pushed onto `L`, in `l.length` steps. -/ +private lemma snocComputer_phaseA (c : Bool) (L : StackTape Bool) : ∀ l : List Bool, + RelatesInSteps (snocComputer c).TransitionRelation + ⟨some (.inl ()), ⟨(StackTape.mapSome l).head, L, (StackTape.mapSome l).tail⟩⟩ + ⟨some (.inl ()), ⟨none, snocPush L l, ∅⟩⟩ l.length := by + intro l + induction l generalizing L with + | nil => exact .refl _ + | cons b t ih => + refine .head _ (t' := (⟨some (.inl ()), + ⟨(StackTape.mapSome t).head, StackTape.cons (some b) L, (StackTape.mapSome t).tail⟩⟩ : + (snocComputer c).Cfg)) _ _ ?_ ?_ + · rfl + · simpa using ih (StackTape.cons (some b) L) + +/-- Leftward pass then turn-around: from head over the first of `m` (left stack becomes the +right output), reach the halting configuration reading the reconstructed output, in +`m.length + 1` steps. -/ +private lemma snocComputer_phaseB (c : Bool) : ∀ (m : List Bool) (R : StackTape Bool), + RelatesInSteps (snocComputer c).TransitionRelation + ⟨some (.inr ()), ⟨(StackTape.mapSome m).head, (StackTape.mapSome m).tail, R⟩⟩ + ⟨none, ⟨(snocPush R m).head, ∅, (snocPush R m).tail⟩⟩ (m.length + 1) := by + intro m + induction m with + | nil => intro R; exact .single rfl + | cons b t ih => + intro R + refine .head _ (t' := (⟨some (.inr ()), + ⟨(StackTape.mapSome t).head, (StackTape.mapSome t).tail, StackTape.cons (some b) R⟩⟩ : + (snocComputer c).Cfg)) _ _ ?_ ?_ + · rfl + · simpa using ih (StackTape.cons (some b) R) + +private lemma snocPush_empty (l : List Bool) : + snocPush (∅ : StackTape Bool) l = StackTape.mapSome l.reverse := by + apply stackTape_ext + rw [snocPush_toList] + simp [StackTape.mapSome] + +private lemma snocPush_final (c : Bool) (l : List Bool) : + snocPush (StackTape.cons (some c) ∅) l.reverse = StackTape.mapSome (l ++ [c]) := by + apply stackTape_ext + rw [snocPush_toList, StackTape.cons_some_toList] + simp [StackTape.mapSome] + +/-- The append-a-bit machine outputs `l ++ [c]` within `2 * |l| + 2` steps. -/ +lemma snocComputer_outputsWithinTime (c : Bool) (l : List Bool) : + (snocComputer c).OutputsWithinTime l (l ++ [c]) (2 * l.length + 2) := by + have hA := snocComputer_phaseA c ∅ l + have hB := snocComputer_phaseB c l.reverse (StackTape.cons (some c) ∅) + rw [← snocPush_empty l, snocPush_final c l] at hB + have hchain : + RelatesInSteps (snocComputer c).TransitionRelation + ⟨some (.inl ()), (BiTape.mk₁ l : BiTape Bool)⟩ + ⟨none, (BiTape.mk₁ (l ++ [c]) : BiTape Bool)⟩ + (l.length + (1 + (l.reverse.length + 1))) := by + rw [mk₁_eq l, mk₁_eq (l ++ [c])] + exact hA.trans ((RelatesInSteps.single (by rfl)).trans hB) + refine RelatesWithinSteps.of_le + (RelatesWithinSteps.of_relatesInSteps hchain) ?_ + simp only [List.length_reverse] + omega + +/-- The append-a-bit machine is a `TimeComputable` witness for `fun l => l ++ [c]`. -/ +def snocTimeComputable (c : Bool) : TimeComputable (fun l => l ++ [c]) where + tm := snocComputer c + timeBound n := 2 * n + 2 + outputsFunInTime l := snocComputer_outputsWithinTime c l + +/-- The append-a-bit machine is a `PolyTimeComputable` witness for `fun l => l ++ [c]`. -/ +noncomputable def snocPolyTimeComputable (c : Bool) : + PolyTimeComputable (fun l => l ++ [c]) where + toTimeComputable := snocTimeComputable c + poly := 2 * Polynomial.X + Polynomial.C 2 + bounds n := by simp [snocTimeComputable, two_mul] + +/-- The append-a-bit machine has two states. -/ +theorem size_snocPolyTimeComputable (c : Bool) : + (snocPolyTimeComputable c).size ≤ 2 := by + change Fintype.card (Unit ⊕ Unit) ≤ 2 + simp + +end Turing.SingleTapeTM + +/-! ## Local support: appending a fixed bit, and finite iteration, at the encoding level -/ + +namespace Computability.EncPolyTime + +open Turing.SingleTapeTM + +/-- Append a fixed bit `c` to any encoding: the identity `σ → σ` viewed from encoding `es` +into the encoding `fun s => es s ++ [c]`, computed by the append-a-bit machine. -/ +noncomputable def appendBit {σ : Type} (es : σ → List Bool) (c : Bool) : + EncPolyTime es (fun s => es s ++ [c]) _root_.id where + toFun l := l ++ [c] + polyTime := snocPolyTimeComputable c + map_encode _ := rfl + +theorem size_appendBit {σ : Type} (es : σ → List Bool) (c : Bool) : + (appendBit es c).size ≤ 2 := size_snocPolyTimeComputable c + +/-- Finite iteration of a self-map witness: the `k`-fold composition is polynomial-time +computable, with description size at most `1 + k *` the single-step size. Composition adds +state counts (`size_comp`), so the bound is by induction on `k`. -/ +theorem exists_iterate {σ : Type} (es : σ → List Bool) {g : σ → σ} + (hstep : EncPolyTime es es g) : + ∀ k : ℕ, ∃ h : EncPolyTime es es (g^[k]), h.size ≤ 1 + k * hstep.size := by + intro k + induction k with + | zero => + refine ⟨(EncPolyTime.id es).copy (g^[0]) (fun s => ?_), ?_⟩ + · simp + · simp + | succ k ih => + obtain ⟨h, hh⟩ := ih + refine ⟨(h.comp hstep).copy (g^[k+1]) (fun s => ?_), ?_⟩ + · exact (Function.iterate_succ_apply' g k s).symm + · rw [size_copy, size_comp] + have hmul : (k + 1) * hstep.size = k * hstep.size + hstep.size := by ring + omega + +end Computability.EncPolyTime + namespace OracleComp /-! ## The realizable-predicate bridge @@ -51,22 +239,106 @@ through only the initialization and output witnesses. The general case needs the run's factorization through the witness string functions, isolated as `exists_poly_realizable_of_implements`. -/ -/-- **[B-factor — isolated crux, `sorry`]** For an adversary implementing `pure ∘ f` at the -coin boundary, the input→output behavior `x ↦ (M n).output (run …)` at parameter `n` is -realized by an `EncPolyTime` initialization/output pair whose description sizes are bounded -by a single polynomial `q` in the adversary's `descBound` and `steps`. The compiled run is -an iterate (at most `steps.eval n` times) of the four witness string functions against the -canonical answer encoding, so its input→output map has a machine of `q.eval n`-bounded -description; discharging it needs the run-factorization of the fuelled machine run through -its per-step witnesses. This is the general-`steps` input to the diagonal contradiction; -the `steps = 0` special case is proved directly by -`realizable_of_implements_steps_eq_zero`. -/ +/-- **[B-factor — the compiled deterministic run]** For an adversary implementing `pure ∘ f` +at the coin boundary, the input→output behavior `x ↦ (M n).output (run …)` at parameter `n` +is realized by an `EncPolyTime` initialization/output pair whose description sizes are +bounded by a single polynomial `q` in the adversary's `descBound` and `steps`. + +Proof. Specialize `(himpl n).runK_eq` to `m := Id` and the deterministic constant-`true` +coin handler; the pure simulation collapses to `runD hdl (steps.eval n) (init x) = f n x`, +and `runD_eq_output_stateAfter` (using the adversary's `stable` readout to absorb early +termination) turns this into a readout of the fixed-fuel iterate of the one-step state map +`g = advanceOnce hdl M.toDynSystem`. That one-step map is compiled at the encoding level as +`updateF` precomposed with the fixed canonical coin answer `[true]` (built by the local +`Computability.EncPolyTime.appendBit` / `Turing.SingleTapeTM.snocComputer` support), and its +`steps.eval n`-fold composition is assembled by `Computability.EncPolyTime.exists_iterate`. +Composition adds machine-state counts, so the compiled initialization +`initF ▸ g^[steps.eval n]` has description size at most +`descBound + 1 + steps * (2 + descBound)` evaluated at `n` — one uniform polynomial `q`, +with the (parameter-specific) iteration time absorbed into `RealizableLE`'s time component. +This is the general-`steps` input to the diagonal contradiction; the `steps = 0` special +case is proved directly by `realizable_of_implements_steps_eq_zero`. -/ theorem exists_poly_realizable_of_implements (A : MachineAdversary (BoundaryData.coin BitEncFam.bitVecX BitEncFam.bool)) (f : (n : ℕ) → BitVec n → Bool) (himpl : A.Implements (fun n x => (pure (f n x) : OracleComp coinSpec Bool))) : ∃ q : Polynomial ℕ, ∀ n, f n ∈ RealizableLE n (q.eval n) := by - sorry + classical + -- The deterministic constant-`true` coin handler. + set hdl : OracleHandler coinSpec := OracleHandler.ofFn (fun _ => true) with hhdl + refine ⟨A.descBound + Polynomial.C 1 + A.steps * (Polynomial.C 2 + A.descBound), fun n => ?_⟩ + set M := A.M n with hM + set es := A.state.enc n with hes + set k := A.steps.eval n with hk + -- The one-step state map: expose the coin query, answer `true`, update. + set g : M.State → M.State := OracleStrategy.advanceOnce hdl M.toDynSystem with hg + -- `g` is the flattened update against the canonical `true` answer. + have hg_upd : ∀ s, g s = M.updateFlat (s, ⟨M.expose s, true⟩) := by + intro s + rw [M.updateFlat_expose, hg, hhdl, OracleStrategy.advanceOnce, OracleHandler.ofFn_apply, + PFunctor.PointedMachine.update_toDynSystem] + -- The canonical coin answer encodes to the single bit `[true]`. + have hin : ∀ s : M.State, es s ++ [true] + = (A.state.pairVar (BoundaryData.coin BitEncFam.bitVecX BitEncFam.bool).eIface.encAns).enc n + (s, ⟨M.expose s, true⟩) := by + intro s + rw [StrEncFam.pairVar_enc, hes] + rfl + have hout : ∀ s : M.State, + es (g s) = A.state.enc n (M.updateFlat (s, ⟨M.expose s, true⟩)) := by + intro s; rw [hes]; exact congrArg (A.state.enc n) (hg_upd s) + -- The one-step witness: append the fixed answer, then run the update witness. + set recoded : EncPolyTime (fun s => es s ++ [true]) es g := + (A.updateF.wit n).recode (fun s => (s, ⟨M.expose s, true⟩)) g hin hout with hrec + set hstep : EncPolyTime es es g := + ((EncPolyTime.appendBit es true).comp recoded).copy g (fun _ => rfl) with hstepdef + have hstep_size : hstep.size ≤ 2 + (A.updateF.wit n).size := by + rw [hstepdef, EncPolyTime.size_copy, EncPolyTime.size_comp, hrec, EncPolyTime.size_recode] + have := EncPolyTime.size_appendBit es true + omega + -- Finite iteration of the one-step map, `k = steps.eval n` times. + obtain ⟨hIter, hIter_size⟩ := EncPolyTime.exists_iterate es hstep k + -- Correctness: the compiled run reads out `f n x`. + have hcorrect : ∀ x, M.output ((g^[k] ∘ M.init) x) = some (f n x) := by + intro x + have hstateAfter : g^[k] (M.init x) + = OracleStrategy.stateAfter hdl M.toDynSystem (M.init x) k := by + rw [hg]; rfl + rw [Function.comp_apply, hstateAfter, + ← M.runD_eq_output_stateAfter (A.stable n) hdl k (M.init x)] + have key := (himpl n).runK_eq (m := Id) hdl.toQueryImpl x + rw [OracleMachine.runD, hk, key] + simp only [simulateQ_pure, map_pure] + rfl + -- Description-size bookkeeping. + have hdesc : A.descBound.eval n = A.initF.size.eval n + A.exposeF.size.eval n + + A.updateF.size.eval n + A.outputF.size.eval n := by + simp [MachineAdversary.descBound] + have hinit_le : (A.initF.wit n).size ≤ A.descBound.eval n := + (A.initF.size_le n).trans (by omega) + have hupd_le : (A.updateF.wit n).size ≤ A.descBound.eval n := + (A.updateF.size_le n).trans (by omega) + have hout_le : (A.outputF.wit n).size ≤ A.descBound.eval n := + (A.outputF.size_le n).trans (by omega) + have hqeval : (A.descBound + Polynomial.C 1 + + A.steps * (Polynomial.C 2 + A.descBound)).eval n + = A.descBound.eval n + 1 + k * (2 + A.descBound.eval n) := by + rw [hk]; simp [Polynomial.eval_add, Polynomial.eval_mul] + have hmul : k * hstep.size ≤ k * (2 + A.descBound.eval n) := + Nat.mul_le_mul_left k (hstep_size.trans (by omega)) + have hcomp_size : ((A.initF.wit n).comp hIter).size + ≤ A.descBound.eval n + 1 + k * (2 + A.descBound.eval n) := by + rw [EncPolyTime.size_comp] + have := hIter_size + omega + refine ⟨M.State, es, g^[k] ∘ M.init, M.output, (A.initF.wit n).comp hIter, + A.outputF.wit n, ?_, ?_, hcorrect⟩ + · -- initialization size + rw [hqeval] + exact hcomp_size + · -- output size + rw [hqeval] + exact hout_le.trans (by omega) /-- **Milestone A, realizability step (real).** A round-free adversary implementing `pure ∘ f` realizes `f n` within its description bound: at `steps = 0` the run is the plain