From f3094d333a35fb8d6a0a0edeed9aa45cf0b265bd Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 02:31:44 +0000 Subject: [PATCH] refactor(encodings): computable FinEnum-based encoding for concrete finite types Add computable `Turing.MultiTapeTM.encFinEnum` and `length_encFinEnum_lt` alongside `encFinite` in `Encodings/Finite.lean`, migrate concrete finite tag and symbol encodings across TreeEval, USTCON, SpaceUniversal, IP/TQBF, Tableau/Space, Configuration, PCP, and tests to `encFinEnum`, and drop `noncomputable` from concrete encoding definitions. Closes #630 --- .../Circuit/Boolean/Tableau/Space.lean | 15 +++++--- .../Complexity/Classes/IP/Simulation.lean | 4 +-- .../Complexity/Classes/IP/TQBF/Verifier.lean | 22 +++++++----- .../Complexity/Classes/Inclusions.lean | 8 ++--- .../Complexity/Classes/MIP/NEXP.lean | 4 +-- .../Complexity/Classes/Oracle/Monotone.lean | 6 ++-- .../Complexity/Classes/Oracle/PP.lean | 6 ++-- .../Complexity/Classes/Oracle/Simulation.lean | 4 +-- .../Complexity/LogSpace/Reachability.lean | 2 +- .../Complexity/PolyTime/Configuration.lean | 10 +++--- .../PolyTime/RotationMap/Family.lean | 4 +-- .../Turing/MultiTape/Complexity/Space.lean | 2 +- .../MultiTape/Complexity/Space/Savitch.lean | 4 +-- .../Turing/MultiTape/Counting/Checker.lean | 2 +- .../Turing/MultiTape/Encodings/Finite.lean | 23 ++++++++++++ .../MultiTape/Universal/SpaceBudget.lean | 6 +++- .../PCP/Approximation/LabelCover.lean | 4 +-- .../PCP/Encoded/Amplification/Arithmetic.lean | 8 ++--- .../Computability/PCP/Encoded/Power.lean | 8 ++--- .../Computability/PCP/Encoded/ThreeSAT.lean | 12 +++---- .../Computability/PCP/Power/Complexity.lean | 2 +- .../Probabilistic/Oracle/Normalization.lean | 4 +-- .../Probabilistic/Oracle/Parameter.lean | 6 ++-- .../Probabilistic/Oracle/Substitution.lean | 16 +++++---- .../Realization/OpenOracleSimulation.lean | 13 +++---- .../TreeEval/Reader/Cert/Machine.lean | 2 +- .../TreeEval/Reader/Cert/Offset.lean | 8 ++--- .../TreeEval/Reader/Cert/Regs.lean | 2 +- .../TreeEval/Reader/Cert/Step.lean | 21 +++++------ .../Computability/TreeEval/Reader/Encode.lean | 18 +++++----- .../Computability/TreeEval/Reader/Size.lean | 8 ++--- .../Computability/USTCON/Reader/Cert.lean | 12 +++---- .../Computability/USTCON/Reader/Encode.lean | 36 ++++++++++++------- .../USTCON/Reader/Invariant.lean | 12 +++---- ComplexityTests/ConfigurationPolyTime.lean | 2 +- ComplexityTests/ExpanderContraction.lean | 16 ++++----- ComplexityTests/FiniteControl.lean | 10 +++++- ComplexityTests/FiniteTables.lean | 2 ++ .../OracleComposition/Substitution.lean | 4 +-- ComplexityTests/PCPApproximation.lean | 2 +- ComplexityTests/PCPEncodedAmplification.lean | 26 +++++++------- .../PCPEncodedAssignmentTester.lean | 8 ++--- ComplexityTests/PCPEncodedComposition.lean | 2 +- ComplexityTests/PCPEncodedEnumeration.lean | 6 ++-- ComplexityTests/PCPEncodedPreprocess.lean | 4 +-- ComplexityTests/PCPExpander.lean | 12 +++---- ComplexityTests/PCPPreprocessPrograms.lean | 10 +++--- .../PCPSelectedAssignmentTester.lean | 4 +-- ComplexityTests/PolyTimeTactic.lean | 4 +-- ComplexityTests/RotationWalk.lean | 5 +-- 50 files changed, 247 insertions(+), 184 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean index 980a52982e..2dc1449979 100644 --- a/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Space.lean @@ -204,9 +204,16 @@ theorem blockSize_inSpace : budget_natAdd (colStart_inSpace (k := k) (State := State) hT hin) (budget_natMul (numCols_inSpace hT hin) (budget_const _ hin)) +instance : FinEnum ColSel := + FinEnum.ofList [.same, .prev, .next, .last] fun x => by cases x <;> decide + +instance : FinEnum Guard := + FinEnum.ofList [.always, .pos, .ltLast, .inRange, .outRange, .isZero, .isEnd, .leEnd] + fun x => by cases x <;> decide + omit [DecidableEq State] in private theorem regionStart_inSpace {i : α → Fin 4} - (hi : ComputableTidilyInSpace i encIn (encFinite (Fin 4)) Bs) : + (hi : ComputableTidilyInSpace i encIn (encFinEnum (Fin 4)) Bs) : ComputableTidilyInSpace (fun x => regionStart k State (T x) (i x)) encIn encNat Bs := by have h₀ := budget_finite (encC := encBool) (fun j : Fin 4 => decide (j = 0)) hi have h₁ := budget_finite (encC := encBool) (fun j : Fin 4 => decide (j = 1)) hi @@ -248,7 +255,7 @@ private theorem resolve_inSpace {r : α → Ref k State} have hinp := budget_ite hinpc (budget_natSub hc (budget_const 1 hin)) hn -- the guard have hg := budget_finite (encC := encBool) Guard.ofTests - (budget_prod (budget_finite (encC := encFinite Guard) Ref.guardOf hr) + (budget_prod (budget_finite (encC := encFinEnum Guard) Ref.guardOf hr) (budget_prod hc0 (budget_prod hcT (budget_prod hcn (budget_prod hcz (budget_prod hce hcn2)))))) -- the position @@ -256,8 +263,8 @@ private theorem resolve_inSpace {r : α → Ref k State} have hprev := budget_finite (encC := encBool) Ref.prevOf hr have ht' := budget_ite hprev (budget_natSub ht (budget_const 1 hin)) ht have hreg := regionStart_inSpace (k := k) (State := State) hT hin - (budget_finite (encC := encFinite (Fin 4)) Loc.region hloc) - have hcs := budget_finite (encC := encFinite ColSel) Ref.csOf hr + (budget_finite (encC := encFinEnum (Fin 4)) Loc.region hloc) + have hcs := budget_finite (encC := encFinEnum ColSel) Ref.csOf hr have hcs₀ := budget_finite (encC := encBool) (fun cs : ColSel => decide (cs = .same)) hcs have hcs₁ := budget_finite (encC := encBool) (fun cs : ColSel => decide (cs = .prev)) hcs have hcs₂ := budget_finite (encC := encBool) (fun cs : ColSel => decide (cs = .next)) hcs diff --git a/Complexity/Computability/Complexity/Classes/IP/Simulation.lean b/Complexity/Computability/Complexity/Classes/IP/Simulation.lean index c30206ed89..ef864cc484 100644 --- a/Complexity/Computability/Complexity/Classes/IP/Simulation.lean +++ b/Complexity/Computability/Complexity/Classes/IP/Simulation.lean @@ -227,8 +227,8 @@ private theorem computableTidilyInPolyTime_instruction : (fun p : MultiTapeMachine.FiniteConfig k Bool Control Unit × Bool => (p.1.tapes.state, p.1.tapes.inputSymbol, p.1.tapes.workTapeSymbols, p.1.answerSymbols, p.2)) (encPair encFiniteConfig encBool) - (encPair (encFinite (Option Control)) (encPair (encFinite (Option Bool)) - (encPair (encFinite (Fin k → Option Bool)) (encPair (encFinite (Unit → Option Bool)) + (encPair (encFinite (Option Control)) (encPair (encFinEnum (Option Bool)) + (encPair (encFinEnum (Fin k → Option Bool)) (encPair (encFinite (Unit → Option Bool)) encBool)))) := by fun_prop exact ((of_finite fun obs : Option Control × Option Bool × (Fin k → Option Bool) × diff --git a/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean b/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean index 4b5126bc32..78b379550a 100644 --- a/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean +++ b/Complexity/Computability/Complexity/Classes/IP/TQBF/Verifier.lean @@ -82,9 +82,13 @@ namespace Machine /-! ### States -/ +instance : FinEnum ArithQBF.Kind := + FinEnum.ofList [.var, .top, .bot, .not, .and, .or, .ex, .all, .lin] + fun k => by cases k <;> decide + /-- Tokens of arithmetic formulas, the kind framed before the variable in binary. -/ -noncomputable abbrev encArithToken : ArithQBF.Kind × ℕ ↪ List Bool := - encPair (encFinite ArithQBF.Kind) encNat +abbrev encArithToken : ArithQBF.Kind × ℕ ↪ List Bool := + encPair (encFinEnum ArithQBF.Kind) encNat /-- Points as lists of pairs of a variable, in binary, and a value, in unary. -/ abbrev encPt : List (ℕ × ℕ) ↪ List Bool := encList (encPair encNat encUnary) @@ -101,7 +105,7 @@ private abbrev encParams : Params ↪ List Bool := abbrev LoopInput := Params × List (ArithQBF.Kind × ℕ) /-- The encoding of the input of the loop. -/ -private noncomputable abbrev encLoopInput : LoopInput ↪ List Bool := +private abbrev encLoopInput : LoopInput ↪ List Bool := encPair encParams (encList encArithToken) /-- A pending claim: a point and a value. -/ @@ -115,14 +119,14 @@ check so far passed. -/ abbrev VState := List (ArithQBF.Kind × ℕ) × List Claim × Bool /-- The encoding of the states. -/ -noncomputable abbrev encVState : VState ↪ List Bool := +abbrev encVState : VState ↪ List Bool := encPair (encList encArithToken) (encPair (encList encClaim) encBool) /-- The data of a step: the input of the loop and the current state. -/ abbrev StepData := LoopInput × VState /-- The encoding of the data of a step. -/ -private noncomputable abbrev encStepData : StepData ↪ List Bool := encPair encLoopInput encVState +private abbrev encStepData : StepData ↪ List Bool := encPair encLoopInput encVState namespace StepData @@ -151,7 +155,7 @@ end StepData /-! ### The step -/ /-- The message of a step: the remaining tokens and the point of the claim on top of the stack. -/ -noncomputable def message (a : StepData) : List Bool := +def message (a : StepData) : List Bool := encPair (encList encArithToken) encPt (a.2.1, a.top.1) /-- The state after a failed check: the token and the claim are dropped. -/ @@ -338,7 +342,7 @@ private theorem isOraclePPTOn_step : IsOraclePPTOn encStepData encVState (fun a : StepData => step a.1 a.2) := by unfold step exact IsOraclePPTOn.cond (by fun_prop) - (IsOraclePPTOn.finite_cases (tagEncoding := encFinite ArithQBF.Kind) + (IsOraclePPTOn.finite_cases (tagEncoding := encFinEnum ArithQBF.Kind) (tag := fun a : StepData => a.head.1) (branch := stepAt) (by fun_prop) stepAt_pt) (ComputableTidilyInPolyTime.isOraclePPTOn (f := fun a : StepData => a.2) (by fun_prop)) @@ -541,10 +545,10 @@ open ComputableTidilyInPolyTime TQBF ComputableTidilyInPolyTime QBF.Kind.isQuantifier encKind encBool := of_finite _ @[local fun_prop] private lemma arith_pt : - ComputableTidilyInPolyTime QBF.Kind.arith encKind (encFinite ArithQBF.Kind) := of_finite _ + ComputableTidilyInPolyTime QBF.Kind.arith encKind (encFinEnum ArithQBF.Kind) := of_finite _ @[local fun_prop] private lemma lin_pt {α : Type} {enc : α ↪ List Bool} : - ComputableTidilyInPolyTime (fun _ : α => ArithQBF.Kind.lin) enc (encFinite ArithQBF.Kind) := + ComputableTidilyInPolyTime (fun _ : α => ArithQBF.Kind.lin) enc (encFinEnum ArithQBF.Kind) := const _ private lemma linVars_pt : ComputableTidilyInPolyTime linVars encQBF (encList encNat) := by diff --git a/Complexity/Computability/Complexity/Classes/Inclusions.lean b/Complexity/Computability/Complexity/Classes/Inclusions.lean index 5302eacba6..b8b240efb3 100644 --- a/Complexity/Computability/Complexity/Classes/Inclusions.lean +++ b/Complexity/Computability/Complexity/Classes/Inclusions.lean @@ -178,14 +178,14 @@ theorem PSPACE_subset_EXP : PSPACE enc ⊆ EXP enc := by ((ComputableTidilyInPolyTime.const 2).prod hwidth)).prod (ComputableTidilyInPolyTime.const 2)) have hedge : ComputableTidilyInPolyTime (fun q : Unit × List Bool × List Bool => (fun _ => ntm.codeEdge) q.1 q.2.1 q.2.2) - (encPair (encFinite Unit) (encPair encBits encBits)) encBool := + (encPair (encFinEnum Unit) (encPair encBits encBits)) encBool := ntm.computableTidilyInPolyTime_codeEdge ((ComputableTidilyInPolyTime.fst _ _).comp (.snd _ _)) ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _)) have hin : ComputableTidilyInPolyTime (fun a => ((), 2 * ntm.codeWidth c d (enc a) + 2, 2 * ntm.codeWidth c d (enc a) + 2, MultiTapeNTM.viewCode (ntm.codeWidth c d (enc a)) (ntm.initView (enc a)), MultiTapeNTM.acceptCode (ntm.codeWidth c d (enc a)))) enc - (Cslib.Reachability.encArgs (encFinite Unit)) := + (Cslib.Reachability.encArgs (encFinEnum Unit)) := (ComputableTidilyInPolyTime.const ()).prod (hcodes.prod (hcodes.prod ((MultiTapeNTM.computableTidilyInPolyTime_viewCode_initView hwidth (.encode enc)).prod (MultiTapeNTM.computableTidilyInPolyTime_acceptCode hwidth)))) @@ -193,7 +193,7 @@ theorem PSPACE_subset_EXP : PSPACE enc ⊆ EXP enc := by obtain ⟨ti, si, hti, -, hi⟩ := hin have hedgeO : ComputableTidilyInO _ _ encBool te se := ⟨1, he.mono (fun _ => by omega) fun _ => by omega, fun _ => by simp⟩ - have hinO : ComputableTidilyInO _ enc (Cslib.Reachability.encArgs (encFinite Unit)) ti + have hinO : ComputableTidilyInO _ enc (Cslib.Reachability.encArgs (encFinEnum Unit)) ti fun a => ti a + si a := ⟨1, hi.mono (fun _ => by omega) fun _ => by dsimp only; omega, fun a => by have := hi.length_le a @@ -206,7 +206,7 @@ theorem PSPACE_subset_EXP : PSPACE enc ⊆ EXP enc := by obtain ⟨cW, dW, hW⟩ := hwidth.polyBounded_length.exists_le obtain ⟨cT, dT, hT⟩ := hti.exists_le obtain ⟨cE, dE, hE⟩ := hte.exists_le - set L := (encFinite Unit ()).length + set L := (encFinEnum Unit ()).length have hedgeMax (w : ℕ) : Cslib.Reachability.edgeMax te () w ≤ cE * (2 * L + 3 * w + 3) ^ dE := listMax_le fun u hu => listMax_le fun v hv => by refine (hE _).trans (Nat.mul_le_mul_left cE (Nat.pow_le_pow_left ?_ dE)) diff --git a/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean b/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean index 0f7699f3f8..f4688c5c8d 100644 --- a/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean +++ b/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean @@ -296,8 +296,8 @@ theorem computableTidilyInPolyTime_instruction : (fun q : MultiTapeMachine.FiniteConfig k Bool Control (Fin p) × Bool => (q.1.tapes.state, q.1.tapes.inputSymbol, q.1.tapes.workTapeSymbols, q.1.answerSymbols, q.2)) (encPair encFiniteConfig encBool) - (encPair (encFinite (Option Control)) (encPair (encFinite (Option Bool)) - (encPair (encFinite (Fin k → Option Bool)) (encPair (encFinite (Fin p → Option Bool)) + (encPair (encFinite (Option Control)) (encPair (encFinEnum (Option Bool)) + (encPair (encFinEnum (Fin k → Option Bool)) (encPair (encFinite (Fin p → Option Bool)) encBool)))) := by fun_prop exact ((of_finite fun obs : Option Control × Option Bool × (Fin k → Option Bool) × diff --git a/Complexity/Computability/Complexity/Classes/Oracle/Monotone.lean b/Complexity/Computability/Complexity/Classes/Oracle/Monotone.lean index 4aff9e3367..f864eb118f 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/Monotone.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/Monotone.lean @@ -60,8 +60,8 @@ theorem ComputableInPolyTimeWithOracle.of_polyTimeReducible {A B : Set (List Boo refine ⟨fun a => OracleComp.interpret G (program a), ?_, fun a => ?_⟩ · -- substitute the handler answering requests to `A` through `B` have hhandler : IsOraclePPTOn - (encPair input (encPair (encPair (encFinite Unit) encBits) (encFinite Unit))) - (encPair encBits (encFinite Unit)) + (encPair input (encPair (encPair (encFinEnum Unit) encBits) (encFinEnum Unit))) + (encPair encBits (encFinEnum Unit)) (fun pair : α × (Unit × List Bool) × Unit => (fun r => (r, ())) <$> (List.take 1 <$> ProbOracleComp.query (spec := fun _ : Unit × List Bool => List Bool) ((), g pair.2.1.2))) := @@ -78,7 +78,7 @@ theorem ComputableInPolyTimeWithOracle.of_polyTimeReducible {A B : Set (List Boo obtain ⟨r, hr, rfl⟩ := ProbOracleComp.mem_support_map hresult obtain ⟨r', -, rfl⟩ := ProbOracleComp.mem_support_map hr exact ⟨trivial, List.length_take_le _ _, Nat.le_add_right _ _⟩) - refine (hsub.map (ComputableTidilyInPolyTime.fst output (encFinite Unit))).congr + refine (hsub.map (ComputableTidilyInPolyTime.fst output (encFinEnum Unit))).congr fun a State oracle s => ?_ congr 2 rw [OracleComp.interpret_interpret, OracleComp.interpret_interpret] diff --git a/Complexity/Computability/Complexity/Classes/Oracle/PP.lean b/Complexity/Computability/Complexity/Classes/Oracle/PP.lean index 6d05d265e2..1cce766360 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/PP.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/PP.lean @@ -385,8 +385,8 @@ theorem PWithSharpPOracle_subset_PWithPPOracle : PWithSharpPOracle enc ⊆ PWith exact (isOraclePPTOn_search (u := unframe) (N := fun w => r.eval w.length + 1) (by fun_prop) (by fun_prop)).map_with hlast have hhandler : IsOraclePPTOn - (encPair enc (encPair (encPair (encFinite Unit) encBits) (encFinite Unit))) - (encPair encBits (encFinite Unit)) + (encPair enc (encPair (encPair (encFinEnum Unit) encBits) (encFinEnum Unit))) + (encPair encBits (encFinEnum Unit)) (fun pair : α × (Unit × List Bool) × Unit => (fun reply => (reply, ())) <$> OracleComp.interpret ProbOracleComp.query (bitQuery r pair.2.1)) := (hG.preprocess (prepare := fun pair : α × (Unit × List Bool) × Unit => pair.2.1.2) @@ -402,7 +402,7 @@ theorem PWithSharpPOracle_subset_PWithPPOracle : PWithSharpPOracle enc ⊆ PWith rw [bitQuery, OracleComp.interpret_map] at hreply obtain ⟨lo, -, rfl⟩ := ProbOracleComp.mem_support_map hreply exact ⟨trivial, by simp, Nat.le_add_right _ _⟩) - refine (hsub.map (ComputableTidilyInPolyTime.fst encBool (encFinite Unit))).congr + refine (hsub.map (ComputableTidilyInPolyTime.fst encBool (encFinEnum Unit))).congr fun a State oracle s => ?_ congr 2 rw [OracleComp.interpret_interpret, OracleComp.interpret_interpret] diff --git a/Complexity/Computability/Complexity/Classes/Oracle/Simulation.lean b/Complexity/Computability/Complexity/Classes/Oracle/Simulation.lean index 9d86af4136..279911afdc 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/Simulation.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/Simulation.lean @@ -193,8 +193,8 @@ variable [Finite Control] [Fintype Operation] omit [DecidableEq Operation] in private theorem observe_pt : ComputableTidilyInPolyTime (observe (k := k) (Control := Control) (Operation := Operation)) encFiniteConfig - (encPair (encFinite (Option Control)) (encPair (encFinite (Option Bool)) - (encPair (encFinite (Fin k → Option Bool)) (encFinite (Operation → Option Bool))))) := by + (encPair (encFinite (Option Control)) (encPair (encFinEnum (Option Bool)) + (encPair (encFinEnum (Fin k → Option Bool)) (encFinite (Operation → Option Bool))))) := by unfold observe fun_prop diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean index 99d222e99c..37399f90a5 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean @@ -200,7 +200,7 @@ theorem computableTidilyInPolyTime_viewSucc : rfl rw [heq] refine ComputableTidilyInPolyTime.finite_cases - (tagEncoding := encPair (encFinite _) (encPair (encFinite _) (encFinite _))) ?_ fun tag => ?_ + (tagEncoding := encPair (encFinite _) (encPair (encFinEnum _) (encFinEnum _))) ?_ fun tag => ?_ · exact ComputableTidilyInPolyTime.finiteCfg_state.prod (ComputableTidilyInPolyTime.finiteCfg_inputSymbol.prod ComputableTidilyInPolyTime.finiteCfg_workTapeSymbols) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean index 575cc70ed0..9bbf4b6150 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean @@ -92,22 +92,22 @@ theorem finiteCfg_output : ComputableTidilyInPolyTime (FiniteCfg.output (k := k) /-- Observe the read-only input, including both blank boundary cells. -/ @[fun_prop] theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime - (FiniteCfg.inputSymbol (k := k) (State := State)) encFiniteCfg (encFinite (Option Bool)) := by + (FiniteCfg.inputSymbol (k := k) (State := State)) encFiniteCfg (encFinEnum (Option Bool)) := by have hlist : ComputableTidilyInPolyTime (fun cfg : FiniteCfg k Bool State => none :: cfg.input.map some) - encFiniteCfg (encList (encFinite (Option Bool))) := by + encFiniteCfg (encList (encFinEnum (Option Bool))) := by have hsome : ComputableTidilyInPolyTime (some (α := Bool)) - encBool (encFinite (Option Bool)) := of_finite _ + encBool (encFinEnum (Option Bool)) := of_finite _ exact (const none).cons' ((map hsome).comp (bitsToList.comp finiteCfg_input)) simpa only [Function.comp_def, List.getD_eq_getElem?_getD, ← FiniteCfg.inputSymbol_eq_getD] using - (listGetD (encA := encFinite (Option Bool)) none).comp (hlist.prod finiteCfg_inputPos) + (listGetD (encA := encFinEnum (Option Bool)) none).comp (hlist.prod finiteCfg_inputPos) /-- Observe all work heads as a single fixed finite value. -/ @[fun_prop] theorem finiteCfg_workTapeSymbols : ComputableTidilyInPolyTime (FiniteCfg.workTapeSymbols (k := k) (State := State)) encFiniteCfg - (encFinite (Fin k → Option Bool)) := by + (encFinEnum (Fin k → Option Bool)) := by have hheads : ComputableTidilyInPolyTime (fun cfg : FiniteCfg k Bool State => fun tape => (cfg.workTapes tape).head) encFiniteCfg (encPi (encOption encBool)) := by fun_prop diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean index 7ab1825985..96756795f6 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean @@ -68,10 +68,10 @@ theorem polytime_contract (hb : 0 < b) (label : D ↪ List Bool) (ComputableTidilyInPolyTime.unary_mul.comp (hsize.prod hdecoded.fst'))) have htarget := (polytime_lookup label).comp (htable.prod (hindex.prod hdecoded.snd')) - have hslot := (ComputableTidilyInPolyTime.unary_finMod hb (encFinite (Fin b))).comp + have hslot := (ComputableTidilyInPolyTime.unary_finMod hb (encFinEnum (Fin b))).comp (ComputableTidilyInPolyTime.unary_div.comp (htarget.fst'.prod hsize)) have hencode : ComputableTidilyInPolyTime (id : (Fin b × (D × D)) → _) - (encPair (encFinite (Fin b)) (encPair label label)) slot := .of_finite _ + (encPair (encFinEnum (Fin b)) (encPair label label)) slot := .of_finite _ have hresult := (ComputableTidilyInPolyTime.unary_mod.comp (htarget.fst'.prod hsize)).prod (hencode.comp (hslot.prod htarget.snd')) have hlength := (ComputableTidilyInPolyTime.length diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean index a879b40a13..71c62d5f65 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean @@ -132,7 +132,7 @@ theorem computableTidilyInPolyTime_viewStepB : (encFiniteCfg (k := k) (State := State)) rw [heq] refine ComputableTidilyInPolyTime.finite_cases - (tagEncoding := encPair (encFinite _) (encPair (encFinite _) (encFinite _))) ?_ fun tag => ?_ + (tagEncoding := encPair (encFinite _) (encPair (encFinEnum _) (encFinEnum _))) ?_ fun tag => ?_ · exact (ComputableTidilyInPolyTime.finiteCfg_state.comp hfst).prod ((ComputableTidilyInPolyTime.finiteCfg_inputSymbol.comp hfst).prod (ComputableTidilyInPolyTime.finiteCfg_workTapeSymbols.comp hfst)) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Savitch.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Savitch.lean index e78aab889e..019375a016 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Savitch.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Savitch.lean @@ -123,14 +123,14 @@ theorem exists_polyBounded_space_savitchDecide {α : Type} (enc : α ↪ List Bo by fun_prop have hedge : ComputableTidilyInPolyTime (fun q : Unit × List Bool × List Bool => (fun _ => ntm.codeEdge) q.1 q.2.1 q.2.2) - (encPair (encFinite Unit) (encPair encBits encBits)) encBool := + (encPair (encFinEnum Unit) (encPair encBits encBits)) encBool := ntm.computableTidilyInPolyTime_codeEdge ((ComputableTidilyInPolyTime.fst _ _).comp (.snd _ _)) ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _)) have hin : ComputableTidilyInPolyTime (fun a => ((), 2 * ntm.codeWidth c d (enc a) + 2, 2 * ntm.codeWidth c d (enc a) + 2, viewCode (ntm.codeWidth c d (enc a)) (ntm.initView (enc a)), acceptCode (ntm.codeWidth c d (enc a)))) enc - (Cslib.Reachability.encArgs (encFinite Unit)) := + (Cslib.Reachability.encArgs (encFinEnum Unit)) := (ComputableTidilyInPolyTime.const ()).prod (hcodes.prod (hcodes.prod ((computableTidilyInPolyTime_viewCode_initView hwidth (.encode enc)).prod (computableTidilyInPolyTime_acceptCode hwidth)))) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Counting/Checker.lean b/Complexity/Computability/Machines/Turing/MultiTape/Counting/Checker.lean index e2d3d477aa..1e1674357c 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Counting/Checker.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Counting/Checker.lean @@ -152,7 +152,7 @@ theorem computableTidilyInPolyTime_indexStep [Finite State] have hview : ComputableTidilyInPolyTime (fun p : Storage k State × ℕ => (state, p.1.tapes.inputSymbol, p.1.tapes.workTapeSymbols)) encIn (encPair (encFinite State) - (encPair (encFinite (Option Bool)) (encFinite (Fin k → Option Bool)))) := by fun_prop + (encPair (encFinEnum (Option Bool)) (encFinEnum (Fin k → Option Bool)))) := by fun_prop have hactions : ComputableTidilyInPolyTime (fun p : Storage k State × ℕ => localActions machine (state, p.1.tapes.inputSymbol, p.1.tapes.workTapeSymbols)) encIn (encList (encFinite (Turing.Action k Bool State))) := diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Finite.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Finite.lean index 5bc5f05132..bce0737ab5 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Finite.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Finite.lean @@ -8,6 +8,8 @@ module -- upstream: candidate public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives +public import Mathlib.Data.FinEnum +public import Mathlib.Data.FinEnum.Option public import Mathlib.Data.Fintype.EquivFin public import Mathlib.SetTheory.Cardinal.Finite @@ -16,13 +18,19 @@ public import Mathlib.SetTheory.Cardinal.Finite A finite type is encoded by unary ranks in one fixed enumeration. The enumeration and its size are independent of the runtime input; this does not give a uniform algorithm for growing types. +Concrete finite types with a `FinEnum` instance use `Turing.MultiTapeTM.encFinEnum`, which is +computable; generic `[Finite α]` parameters use `Turing.MultiTapeTM.encFinite`. ## Main definitions +* `Turing.MultiTapeTM.encFinEnum`: computable unary ranks for a constructively enumerated finite + type. * `Turing.MultiTapeTM.encFinite`: unary ranks for a fixed finite type. ## Main results +* `Turing.MultiTapeTM.length_encFinEnum_lt`: the cardinality bounds every constructively encoded + rank. * `Turing.MultiTapeTM.length_encFinite_lt`: the cardinality bounds every encoded rank. ## References @@ -35,6 +43,21 @@ Adapts `Computability/Probabilistic/Finite.lean` on the cslib `crypto` branch at namespace Turing.MultiTapeTM +/-- Concrete bit enumeration. -/ +instance instFinEnumBool : FinEnum Bool := + FinEnum.ofList [false, true] (by decide) + +/-- Encode a constructively enumerated finite type by unary ranks. -/ +def encFinEnum (α : Type) [FinEnum α] : α ↪ List Bool := + ⟨fun a => encUnary (FinEnum.equiv a).val, fun _ _ h => + FinEnum.equiv.injective (Fin.ext (encUnary.injective h))⟩ + +/-- Every constructively encoded finite tag has length less than the fixed domain's cardinality. -/ +theorem length_encFinEnum_lt {α : Type} [FinEnum α] (a : α) : + (encFinEnum α a).length < Nat.card α := by + let _ : Fintype α := inferInstance + simp [encFinEnum, Nat.card_eq_fintype_card, ← FinEnum.card_eq_fintypeCard] + /-- Encode a fixed finite type by unary ranks in an enumeration chosen once. -/ noncomputable def encFinite (α : Type) [Finite α] : α ↪ List Bool := let _ := Fintype.ofFinite α diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean index c1d4798aec..d5c9cbadf6 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean @@ -676,6 +676,10 @@ lemma final_time' (c N t L P E : ℕ) (hP : P ≤ L) (hE : E ≤ L) : _ ≤ 20 * ((t + 1) * Z) := by omega _ = 20 * ((t + 1) * (N + 1) ^ 2 * Y) := by ring +local instance : FinEnum InState := + FinEnum.ofList [.descMarker, .descBit, .marker, .bit, .digitMarker, .digit, .steps] + fun q => by cases q <;> decide + /-- **The universal machine within a space budget.** The budgeted universal function is tidily computable within space linear in the bound `budgetSpace` on the states of its fold, by the multi-pass fold of the in-place universal machine with the budget test at the end of each pass. @@ -685,7 +689,7 @@ public theorem computableTidilyInTimeAndSpace_budgetedUniversal : ∃ c, (fun i => c * ((i.2.2.1 + 1) * ((eInS i).length + 1) ^ 2 * (budgetSpace i + 1) ^ 3)) (fun i => c * (budgetSpace i + 1)) := by refine Exists.elim (ComputableTidilyInTimeAndSpace.multiPassFold_translate inTr - (encQ := encFinite InState) foldInitS_inO foldNextS_inO + (encQ := encFinEnum InState) foldInitS_inO foldNextS_inO (const (encIn := eSSt) (encMid := encBits) ([] : List Bool)) foldEndS_inO foldContS_inO foldFinishS_inO (passes := fun i => i.2.2.1 - 1) (g := budgetedUniversal) (encOut := eOut) ?_ ?_ (tMax := fun i => 9 * (budgetSpace i + 1) ^ 3) diff --git a/Complexity/Computability/PCP/Approximation/LabelCover.lean b/Complexity/Computability/PCP/Approximation/LabelCover.lean index e76c452ce0..fa595a3478 100644 --- a/Complexity/Computability/PCP/Approximation/LabelCover.lean +++ b/Complexity/Computability/PCP/Approximation/LabelCover.lean @@ -152,7 +152,7 @@ edge lists, with constraint tables listing ranks of labels. The constraint graph bipartite. This is a conjecture, stated and not assumed. -/ def UniqueGamesConjecture : Prop := ∀ ε δ : ℝ, 0 < ε → 0 < δ → δ < 1 - ε → ∃ L : ℕ, - PromiseProblem.NPHard (Graph.encoding (encPi (encFinite (Fin L)))) + PromiseProblem.NPHard (Graph.encoding (encPi (encFinEnum (Fin L)))) (GapUniqueGames (Fin L) (1 - ε) δ) /-- Under the Unique Games Conjecture, for every `ε, δ > 0` with `δ < 1 - ε` there is a number `L` @@ -160,7 +160,7 @@ of labels such that every weaker gap problem on `Fin L`, with completeness at mo soundness at least `δ`, is NP-hard. -/ theorem UniqueGamesConjecture.npHard_of_le (h : UniqueGamesConjecture) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (hεδ : δ < 1 - ε) : ∃ L : ℕ, ∀ c s : ℝ, c ≤ 1 - ε → δ ≤ s → s < c → - PromiseProblem.NPHard (Graph.encoding (encPi (encFinite (Fin L)))) + PromiseProblem.NPHard (Graph.encoding (encPi (encFinEnum (Fin L)))) (GapUniqueGames (Fin L) c s) := by obtain ⟨L, hL⟩ := h ε δ hε hδ hεδ exact ⟨L, fun c s hc hs hsc => hL.mono (GapUniqueGames_mono hc hs hsc).1 diff --git a/Complexity/Computability/PCP/Encoded/Amplification/Arithmetic.lean b/Complexity/Computability/PCP/Encoded/Amplification/Arithmetic.lean index 367470b075..da417d5fea 100644 --- a/Complexity/Computability/PCP/Encoded/Amplification/Arithmetic.lean +++ b/Complexity/Computability/PCP/Encoded/Amplification/Arithmetic.lean @@ -50,14 +50,12 @@ local notation "Alphabet" => (Bool × (Fin 6 → Bool)) local notation "Constraint" => (Alphabet → Alphabet → Bool) local notation "Label" => RotationMap.AffinePlaneFamilyLabel (ZMod 257) 257 -/-- Concrete bit enumeration, registered locally for the complete arithmetic amplifier. -/ -local instance instFinEnumBool : FinEnum Bool := FinEnum.ofList [false, true] (by decide) - /-- Concrete enumeration of the arithmetic expander's fixed field. -/ local instance instFinEnumZMod257 : FinEnum (ZMod 257) := FinEnum.ofEquiv (Fin 257) (ZMod.finEquiv 257).toEquiv.symm -attribute [local instance] Cslib.PCP.HadamardTester.Rand.finEnum SelectedComposeSlot.finEnum +attribute [local instance] HadamardTester.instFinEnumBool + Cslib.PCP.HadamardTester.Rand.finEnum SelectedComposeSlot.finEnum /-- Complete normalized rounds with fixed arithmetic expanders and fixed numerical parameters. -/ @[irreducible] @@ -74,7 +72,7 @@ theorem isPolyTime_arithmeticAmplify {Input : Type} {input : Input ↪ List Bool (hwellFormed : ∀ x, (graph x).WellFormed) : ComputableTidilyInPolyTime (fun x => arithmeticAmplify (graph x)) input (encoding (encPi (encPi encBool))) := by - have hcost := RotationMap.polytime_arithmeticExpanderRotate (encFinite Label) + have hcost := RotationMap.polytime_arithmeticExpanderRotate (encFinEnum Label) unfold arithmeticAmplify exact isPolyTime_amplifyIter_clog hgraph hwellFormed RotationMap.arithmeticExpander RotationMap.arithmeticExpanderRotate RotationMap.arithmeticExpanderRotate_eq hcost diff --git a/Complexity/Computability/PCP/Encoded/Power.lean b/Complexity/Computability/PCP/Encoded/Power.lean index 1405147fe9..aa4eae6b9b 100644 --- a/Complexity/Computability/PCP/Encoded/Power.lean +++ b/Complexity/Computability/PCP/Encoded/Power.lean @@ -208,7 +208,7 @@ private theorem polytime_powerPreprocessEdge (eval : C → α → α → Bool) ( (fun p : Graph C × ((ℕ × Bool) × PowerLabel D T q) => p.1.powerPreprocessEdge eval fallback rotate T q p.2) (encPair (encoding enc) (encPair (encPair encUnary encBool) - (encPair (encPi (encFinite (PreprocessLabel D))) (encPi (encFinite (Fin q)))))) + (encPair (encPi (encFinite (PreprocessLabel D))) (encPi (encFinEnum (Fin q)))))) (Edge.encoding (encPi (encPi encBool))) := by have hr : ComputableTidilyInPolyTime (fun p : Graph C × ((ℕ × Bool) × PreprocessLabel D) => @@ -224,9 +224,9 @@ private theorem polytime_powerPreprocessEdge (eval : C → α → α → Bool) ( (encPair (encPair encUnary encBool) (encFinite (PreprocessLabel D))) (encPair alphabet alphabet))) encBool := by fun_prop - have hwalk := rotationMap_killedPowRotWithInput hr T q (encFinite (Fin q)) + have hwalk := rotationMap_killedPowRotWithInput hr T q (encFinEnum (Fin q)) have hrel := RegularConstraintGraph.isPolyTime_powerRelationWithInput - hr he T q (encFinite (Fin q)) + hr he T q (encFinEnum (Fin q)) unfold powerPreprocessEdge apply Edge.isPolyTime_mk · fun_prop @@ -253,7 +253,7 @@ private theorem polytime_powerPreprocess (eval : C → α → α → Bool) (fall have hdarts : ComputableTidilyInPolyTime (fun g : Graph C => g.halfEdges.product walks) (encoding enc) (encList (encPair (encPair encUnary encBool) - (encPair (encPi (encFinite (PreprocessLabel D))) (encPi (encFinite (Fin q)))))) := by + (encPair (encPi (encFinite (PreprocessLabel D))) (encPi (encFinEnum (Fin q)))))) := by unfold List.product fun_prop unfold powerPreprocess diff --git a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean index dd72eb2ef7..74a6f97411 100644 --- a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean +++ b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean @@ -84,7 +84,7 @@ theorem isPolyTime_clauseHolds : ComputableTidilyInPolyTime (fun p : Clause ℕ × (Fin 3 → Bool) => clauseHolds p.1 p.2) (encPair (encList (encPair encUnary encBool)) (encPi encBool)) encBool := by unfold clauseHolds - apply anyWithInput (encA := encFinite (Fin 3)) (by fun_prop) + apply anyWithInput (encA := encFinEnum (Fin 3)) (by fun_prop) apply finite_cases (branch := fun (i : Fin 3) (p : (Clause ℕ × (Fin 3 → Bool)) × Fin 3) => p.1.1[i.val]?.elim false (fun l => p.1.2 i == l.2)) (snd _ _) intro i @@ -95,21 +95,21 @@ theorem isPolyTime_clauseHolds : theorem isPolyTime_cnfEdge : ComputableTidilyInPolyTime (fun p : CNF ℕ × (ℕ × Fin 3) => cnfEdge p.1 p.2) (encPair (encList (encList (encPair encUnary encBool))) - (encPair encUnary (encFinite (Fin 3)))) + (encPair encUnary (encFinEnum (Fin 3)))) (Edge.encoding (encPi (encPi encBool))) := by have hindex : ComputableTidilyInPolyTime (Fin.val (n := 3)) - (encFinite (Fin 3)) encUnary := .of_finite _ + (encFinEnum (Fin 3)) encUnary := .of_finite _ have hclause : ComputableTidilyInPolyTime (fun p : CNF ℕ × (ℕ × Fin 3) => p.1.getD p.2.1 []) (encPair (encList (encList (encPair encUnary encBool))) - (encPair encUnary (encFinite (Fin 3)))) (encList (encPair encUnary encBool)) := by + (encPair encUnary (encFinEnum (Fin 3)))) (encList (encPair encUnary encBool)) := by fun_prop have hliteral := ComputableTidilyInPolyTime.getElem? (encA := encPair encUnary encBool) hclause (hindex.comp ((snd _ _).snd')) unfold cnfEdge apply Edge.isPolyTime_mk (by fun_prop) (by fun_prop) refine pi fun a => pi fun b => ?_ - have ha : ComputableTidilyInPolyTime a (encFinite (Fin 3)) encBool := .of_finite _ + have ha : ComputableTidilyInPolyTime a (encFinEnum (Fin 3)) encBool := .of_finite _ fun_prop /-- Constructing all edges and copying their constraints is polynomial-time. -/ @@ -121,7 +121,7 @@ theorem isPolyTime_ofCNF : have hdarts : ComputableTidilyInPolyTime (fun p : ℕ × CNF ℕ => (List.range p.2.length).product (List.finRange 3)) (encPair encUnary (encList (encList (encPair encUnary encBool)))) - (encList (encPair encUnary (encFinite (Fin 3)))) := by + (encList (encPair encUnary (encFinEnum (Fin 3)))) := by unfold List.product fun_prop unfold ofCNF diff --git a/Complexity/Computability/PCP/Power/Complexity.lean b/Complexity/Computability/PCP/Power/Complexity.lean index 328f5a1112..07e724774b 100644 --- a/Complexity/Computability/PCP/Power/Complexity.lean +++ b/Complexity/Computability/PCP/Power/Complexity.lean @@ -102,7 +102,7 @@ theorem isPolyTime_powerRelationWithInput · simpa only [check, ite_eq_right hi] using (const (encIn := enc) true) have htest : ComputableTidilyInPolyTime (fun p : PowerInput P W D α T q × Fin T => check p.1 p.2) - (encPair enc (encFinite (Fin T))) encBool := + (encPair enc (encFinEnum (Fin T))) encBool := (snd _ _).finite_cases fun i => (hcheck i).comp (fst _ _) exact allWithInput (const (List.finRange T)) htest exact ((snd _ _).fst'.snd').finite_cases hbranch diff --git a/Complexity/Computability/Probabilistic/Oracle/Normalization.lean b/Complexity/Computability/Probabilistic/Oracle/Normalization.lean index eaabc2598c..0179932498 100644 --- a/Complexity/Computability/Probabilistic/Oracle/Normalization.lean +++ b/Complexity/Computability/Probabilistic/Oracle/Normalization.lean @@ -98,8 +98,8 @@ theorem IsTidyOraclePPTOn.finiteStep [Fintype Operation] [Finite Control] (tag := fun pair : (ℕ × FiniteConfig k Bool Control Operation) × Bool => (pair.1.2.tapes.inputSymbol, pair.1.2.tapes.workTapeSymbols, pair.1.2.answerSymbols, pair.2)) - (tagEncoding := encPair (encFinite (Option Bool)) - (encPair (encFinite (Fin k → Option Bool)) + (tagEncoding := encPair (encFinEnum (Option Bool)) + (encPair (encFinEnum (Fin k → Option Bool)) (encPair (encFinite (Operation → Option Bool)) encBool))) (branch := fun symbols (pair : (ℕ × FiniteConfig k Bool Control Operation) × Bool) => match machine.tr control symbols.1 symbols.2.1 symbols.2.2.1 symbols.2.2.2 with diff --git a/Complexity/Computability/Probabilistic/Oracle/Parameter.lean b/Complexity/Computability/Probabilistic/Oracle/Parameter.lean index 01e49df04b..0bd662f463 100644 --- a/Complexity/Computability/Probabilistic/Oracle/Parameter.lean +++ b/Complexity/Computability/Probabilistic/Oracle/Parameter.lean @@ -118,15 +118,15 @@ theorem IsOraclePPT.run_interpret_preprocess {Caller State : Type} [Finite Opera result retains the handler's final state and every external oracle's state, and a local invariant charges reply length and all added encoded storage. -/ theorem IsOraclePPT.run_interpret_preprocess_open {External Caller State : Type} - [Finite Operation] [DecidableEq External] [Finite External] {input : Caller ↪ List Bool} - {stateEncoding : State ↪ List Bool} + [DecidableEq External] [Finite External] {input : Caller ↪ List Bool} + {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} {handler : Caller → Operation × List Bool → State → WordOracleComp External (List Bool × State)} {prepare : Caller → ℕ × List Bool} {initial : Caller → State} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPT output program) (hprepare : ComputableTidilyInPolyTime prepare input (encPair encUnary encBits)) (hhandler : IsOraclePPTOn - (encPair input (encPair (encPair (encFinite Operation) encBits) stateEncoding)) + (encPair input (encPair (encPair operationEncoding encBits) stateEncoding)) (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) (hinitial : ComputableTidilyInPolyTime initial input stateEncoding) (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a)) diff --git a/Complexity/Computability/Probabilistic/Oracle/Substitution.lean b/Complexity/Computability/Probabilistic/Oracle/Substitution.lean index 3ce11615f1..efed665572 100644 --- a/Complexity/Computability/Probabilistic/Oracle/Substitution.lean +++ b/Complexity/Computability/Probabilistic/Oracle/Substitution.lean @@ -53,17 +53,18 @@ handler's final state and every external oracle's state. The efficiently compute bounds each reply and the added encoded state; one invariant must hold for every possible handler result under every external oracle. External replies to the handler need no length bound. -/ theorem IsOraclePPTOn.run_interpret_preprocess_open - {Operation External α β Caller State : Type} [DecidableEq Operation] [Finite Operation] + {Operation External α β Caller State : Type} [DecidableEq Operation] [DecidableEq External] [Finite External] {source : α ↪ List Bool} {input : Caller ↪ List Bool} {output : β ↪ List Bool} - {stateEncoding : State ↪ List Bool} {program : α → WordOracleComp Operation β} + {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} + {program : α → WordOracleComp Operation β} {handler : Caller → Operation × List Bool → State → WordOracleComp External (List Bool × State)} {prepare : Caller → α} {initial : Caller → State} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPTOn source output program) (hprepare : ComputableTidilyInPolyTime prepare input source) (hhandler : IsOraclePPTOn - (encPair input (encPair (encPair (encFinite Operation) encBits) stateEncoding)) + (encPair input (encPair (encPair operationEncoding encBits) stateEncoding)) (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) (hinitial : ComputableTidilyInPolyTime initial input stateEncoding) (invariant : Caller → State → Prop) (hinit : ∀ a, invariant a (initial a)) @@ -87,7 +88,8 @@ theorem IsOraclePPTOn.run_interpret_preprocess_open simp only [encUnary_apply, List.length_replicate, length_encPair, encBits_apply] at h exact h.trans (Nat.mul_le_mul_left resourceCoeff (Nat.pow_le_pow_left (by lia) resourceDegree)) - obtain ⟨_, k, Control, hfinite, machine, c, d, hrealize⟩ := hprogram + obtain ⟨hfiniteOp, k, Control, hfinite, machine, c, d, hrealize⟩ := hprogram + let _ := hfiniteOp let _ := hfinite have hword : ComputableTidilyInPolyTime (fun a => source (prepare a)) input encBits := hprepare.of_enc_eq (fun _ => rfl) @@ -131,8 +133,8 @@ theorem IsOraclePPTOn.interpret_bitQueries (OracleComp.interpret (fun q : Unit × List Bool => List.take 1 <$> OracleComp.query ((), request q.2)) (program a))) := by have hhandler : IsOraclePPTOn - (encPair input (encPair (encPair (encFinite Unit) encBits) (encFinite Unit))) - (encPair encBits (encFinite Unit)) + (encPair input (encPair (encPair (encFinEnum Unit) encBits) (encFinEnum Unit))) + (encPair encBits (encFinEnum Unit)) (fun pair : α × (Unit × List Bool) × Unit => (fun r => (r, ())) <$> (List.take 1 <$> ProbOracleComp.query (spec := fun _ : Unit × List Bool => List Bool) ((), request pair.2.1.2))) := @@ -149,7 +151,7 @@ theorem IsOraclePPTOn.interpret_bitQueries obtain ⟨r, hr, rfl⟩ := ProbOracleComp.mem_support_map hresult obtain ⟨r', -, rfl⟩ := ProbOracleComp.mem_support_map hr exact ⟨trivial, List.length_take_le _ _, Nat.le_add_right _ _⟩) - refine (hsub.map (ComputableTidilyInPolyTime.fst output (encFinite Unit))).congr + refine (hsub.map (ComputableTidilyInPolyTime.fst output (encFinEnum Unit))).congr fun a State oracle s => ?_ congr 2 rw [OracleComp.interpret_interpret, OracleComp.interpret_interpret] diff --git a/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean b/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean index 21afb404f7..fadfc2d304 100644 --- a/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean +++ b/Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean @@ -95,11 +95,11 @@ variable [Finite Control] [DecidableEq External] [Finite External] /-- A handler certified as strict oracle PPT makes one complete interpreter step strict oracle PPT. Only the selected transition runs, so a non-query step makes no external call. -/ theorem isOraclePPTOn_step [Fintype Operation] {input : α ↪ List Bool} - {stateEncoding : State ↪ List Bool} + {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} (machine : MultiTapePTM k Bool Control Operation) {handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)} (hhandler : IsOraclePPTOn - (encPair input (encPair (encPair (encFinite Operation) encBits) stateEncoding)) + (encPair input (encPair (encPair operationEncoding encBits) stateEncoding)) (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) : IsOraclePPTOn (encPair input (encPair encFiniteConfig stateEncoding)) (encPair encFiniteConfig stateEncoding) @@ -127,8 +127,8 @@ theorem isOraclePPTOn_step [Fintype Operation] {input : α ↪ List Bool} (tag := fun pair : (α × (FiniteConfig k Bool Control Operation × State)) × Bool => (pair.1.2.1.tapes.inputSymbol, pair.1.2.1.tapes.workTapeSymbols, pair.1.2.1.answerSymbols, pair.2)) - (tagEncoding := encPair (encFinite (Option Bool)) - (encPair (encFinite (Fin k → Option Bool)) + (tagEncoding := encPair (encFinEnum (Option Bool)) + (encPair (encFinEnum (Fin k → Option Bool)) (encPair (encFinite (Operation → Option Bool)) encBool))) (branch := fun symbols (pair : (α × (FiniteConfig k Bool Control Operation × State)) × Bool) => @@ -151,13 +151,14 @@ theorem isOraclePPTOn_step [Fintype Operation] {input : α ↪ List Bool} over every possible handler result under every external oracle, bounds reply length and private-state growth; the loop certificate charges all interpreter storage. -/ theorem isOraclePPTOn_run [Finite Operation] {input : α ↪ List Bool} - {stateEncoding : State ↪ List Bool} (machine : MultiTapePTM k Bool Control Operation) + {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} + (machine : MultiTapePTM k Bool Control Operation) {word : α → List Bool} {count : α → ℕ} {handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)} {initial : α → State} (hword : ComputableTidilyInPolyTime word input encBits) (hcount : ComputableTidilyInPolyTime count input encUnary) (hhandler : IsOraclePPTOn - (encPair input (encPair (encPair (encFinite Operation) encBits) stateEncoding)) + (encPair input (encPair (encPair operationEncoding encBits) stateEncoding)) (encPair encBits stateEncoding) (fun pair => handler pair.1 pair.2.1 pair.2.2)) (hinitial : ComputableTidilyInPolyTime initial input stateEncoding) (invariant : α → State → Prop) (hinit : ∀ a, invariant a (initial a)) diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean b/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean index 85a4293f3a..2a0c207d2a 100644 --- a/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean +++ b/Complexity/Computability/TreeEval/Reader/Cert/Machine.lean @@ -91,7 +91,7 @@ private theorem addrT_inSpace : /-! ### On states -/ /-- **The space budget of a state.** -/ -noncomputable def stateBudget (s : State) : ℕ := stepBudget (s.toTuple, false) +def stateBudget (s : State) : ℕ := stepBudget (s.toTuple, false) private theorem stepBudget_bool (x : Tuple) (b : Bool) : stepBudget (x, b) = stepBudget (x, false) := by diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean b/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean index 15b8f5a3eb..b86a8b20bc 100644 --- a/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean +++ b/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean @@ -189,8 +189,8 @@ private theorem bodyLength_inSpace : /-! ### Frames -/ /-- The encoding of tuples of frames. -/ -noncomputable abbrev encFrameTuple : ℕ × Fin 4 × Bool × Fin 3 ↪ List Bool := - encPair encNat (encFinite (Fin 4 × Bool × Fin 3)) +abbrev encFrameTuple : ℕ × Fin 4 × Bool × Fin 3 ↪ List Bool := + encPair encNat (encFinEnum (Fin 4 × Bool × Fin 3)) theorem encFrame_apply (fr : Frame) : encFrame fr = encFrameTuple (Frame.equiv fr) := rfl @@ -198,14 +198,14 @@ theorem encFrame_apply (fr : Frame) : encFrame fr = encFrameTuple (Frame.equiv f theorem frameFinite_inSpace {β : Type} {encB : β ↪ List Bool} (g : Fin 4 × Bool × Fin 3 → β) : ComputableTidilyInSpace (fun fr : Frame => g (Frame.equiv fr).2) encFrame encB fun fr => (encFrame fr).length := by - have h := budget_finite (encC := encB) g (snd encNat (encFinite (Fin 4 × Bool × Fin 3))) + have h := budget_finite (encC := encB) g (snd encNat (encFinEnum (Fin 4 × Bool × Fin 3))) exact h.of_encIn_eq Frame.equiv fun _ => rfl /-- The round of a frame. -/ theorem round_inSpace : ComputableTidilyInSpace (fun fr : Frame => fr.round) encFrame encNat fun fr => (encFrame fr).length := - (fst encNat (encFinite (Fin 4 × Bool × Fin 3))).of_encIn_eq Frame.equiv fun _ => rfl + (fst encNat (encFinEnum (Fin 4 × Bool × Fin 3))).of_encIn_eq Frame.equiv fun _ => rfl /-! ### The offset of the node at the path of a stack -/ diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Regs.lean b/Complexity/Computability/TreeEval/Reader/Cert/Regs.lean index bf4e66944a..5449374828 100644 --- a/Complexity/Computability/TreeEval/Reader/Cert/Regs.lean +++ b/Complexity/Computability/TreeEval/Reader/Cert/Regs.lean @@ -32,7 +32,7 @@ namespace Reader open Turing MultiTapeTM ComputableTidilyInSpace /-- The encoding of register indices. -/ -noncomputable abbrev encReg : Fin 3 ↪ List Bool := encFinite (Fin 3) +abbrev encReg : Fin 3 ↪ List Bool := encFinEnum (Fin 3) variable {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Step.lean b/Complexity/Computability/TreeEval/Reader/Cert/Step.lean index f7d44bdcdc..867124d290 100644 --- a/Complexity/Computability/TreeEval/Reader/Cert/Step.lean +++ b/Complexity/Computability/TreeEval/Reader/Cert/Step.lean @@ -49,10 +49,10 @@ def regLen (x : Tuple) : ℕ := x.regs.1.length + x.regs.2.1.length + x.regs.2.2.length + x.acc.length /-- The encoding of the inputs of a step. -/ -noncomputable abbrev encStepInT : Tuple × Bool ↪ List Bool := encPair encTuple encBool +abbrev encStepInT : Tuple × Bool ↪ List Bool := encPair encTuple encBool /-- **The space budget of a step**, on the tuple and the bit read. -/ -noncomputable def stepBudget (y : Tuple × Bool) : ℕ := +def stepBudget (y : Tuple × Bool) : ℕ := (encStepInT y).length + y.1.ell + y.1.height + 1 + (regLen y.1 + y.1.ell + 1) * ((encNat y.1.p).length + (encNat (y.1.stack.headD dfr).round).length + @@ -129,7 +129,7 @@ private theorem hCtl : ComputableTidilyInSpace stepBudget := snd' (snd' hTup) theorem hTag : ComputableTidilyInSpace (fun y : Tuple × Bool => y.1.tag) encStepInT - (encFinite (Fin 7)) stepBudget := fst' hCtl + (encFinEnum (Fin 7)) stepBudget := fst' hCtl theorem hN₁ : ComputableTidilyInSpace (fun y : Tuple × Bool => y.1.n₁) encStepInT encNat stepBudget := fst' (snd' hCtl) @@ -179,7 +179,7 @@ variable {β : Type} {encIn : β ↪ List Bool} {Bs : β → ℕ} private theorem mkFrame_inSpace {j : β → ℕ} {g : β → Fin 4 × Bool × Fin 3} (hj : ComputableTidilyInSpace j encIn encNat Bs) - (hg : ComputableTidilyInSpace g encIn (encFinite (Fin 4 × Bool × Fin 3)) Bs) : + (hg : ComputableTidilyInSpace g encIn (encFinEnum (Fin 4 × Bool × Fin 3)) Bs) : ComputableTidilyInSpace (fun x => Frame.equiv.symm (j x, g x)) encIn encFrame Bs := (budget_prod hj hg).of_enc_eq fun x => by rw [encFrame_apply, Equiv.apply_symm_apply] @@ -204,7 +204,7 @@ private theorem mkTuple_inSpace {e h p : β → ℕ} {R : β → Regs} {st : β (budget_prod (budget_prod hst hm) hc) private theorem mkCtl_inSpace {t : β → Fin 7} {a b : β → ℕ} {acc : β → List ℕ} - (ht : ComputableTidilyInSpace t encIn (encFinite (Fin 7)) Bs) + (ht : ComputableTidilyInSpace t encIn (encFinEnum (Fin 7)) Bs) (ha : ComputableTidilyInSpace a encIn encNat Bs) (hb : ComputableTidilyInSpace b encIn encNat Bs) (hacc : ComputableTidilyInSpace acc encIn (encList encNat) Bs) : @@ -218,7 +218,7 @@ end Build section Branches /-- The encoding of the results of a step. -/ -noncomputable abbrev encStepOut : Tuple × List Bool ↪ List Bool := encPair encTuple encBits +abbrev encStepOut : Tuple × List Bool ↪ List Bool := encPair encTuple encBits private theorem out_inSpace {T : Tuple × Bool → Tuple} (hT : ComputableTidilyInSpace T encStepInT encTuple stepBudget) : @@ -231,7 +231,8 @@ private theorem withCtl_inSpace {c : Tuple × Bool → Fin 7 × ℕ × ℕ × Li budget_prod (fst' hTup) (budget_prod hStackMode hc) private theorem hConstTag (t : Fin 7) : - ComputableTidilyInSpace (fun _ : Tuple × Bool => t) encStepInT (encFinite (Fin 7)) stepBudget := + ComputableTidilyInSpace (fun _ : Tuple × Bool => t) encStepInT + (encFinEnum (Fin 7)) stepBudget := budget_const t len_le_stepBudget private theorem hConstNat (n : ℕ) : @@ -377,7 +378,7 @@ private theorem hRegPlus (k : Fin 3) : private theorem hFrPhase (ph : Fin 4) : ComputableTidilyInSpace (fun y : Tuple × Bool => { y.1.stack.headD dfr with phase := ph }) encStepInT encFrame stepBudget := - (mkFrame_inSpace hRound (hTopFinite (encB := encFinite (Fin 4 × Bool × Fin 3)) + (mkFrame_inSpace hRound (hTopFinite (encB := encFinEnum (Fin 4 × Bool × Fin 3)) fun g => (ph, g.2.1, g.2.2))).of_enc_eq fun _ => rfl /-- The pass over the table of the gate of the top frame. -/ @@ -453,13 +454,13 @@ private theorem scaleT_inSpace {R : Tuple × Bool → Regs} {r : Tuple × Bool private theorem hFrame0 : ComputableTidilyInSpace (fun y : Tuple × Bool => (⟨0, 0, y.1.mode.neg, y.1.mode.target⟩ : Frame)) encStepInT encFrame stepBudget := - (mkFrame_inSpace (hConstNat 0) (hModeFinite (encB := encFinite (Fin 4 × Bool × Fin 3)) + (mkFrame_inSpace (hConstNat 0) (hModeFinite (encB := encFinEnum (Fin 4 × Bool × Fin 3)) fun m => (0, m.neg, m.target))).of_enc_eq fun _ => rfl private theorem hFrameNext : ComputableTidilyInSpace (fun y : Tuple × Bool => (⟨(y.1.stack.headD dfr).round + 1, 0, (y.1.stack.headD dfr).neg, (y.1.stack.headD dfr).target⟩ : Frame)) encStepInT encFrame stepBudget := - (mkFrame_inSpace (hSucc hRound) (hTopFinite (encB := encFinite (Fin 4 × Bool × Fin 3)) + (mkFrame_inSpace (hSucc hRound) (hTopFinite (encB := encFinEnum (Fin 4 × Bool × Fin 3)) fun g => (0, g.2.1, g.2.2))).of_enc_eq fun _ => rfl private theorem hRun : ComputableTidilyInSpace diff --git a/Complexity/Computability/TreeEval/Reader/Encode.lean b/Complexity/Computability/TreeEval/Reader/Encode.lean index 77e804ab68..6c7e50e8b6 100644 --- a/Complexity/Computability/TreeEval/Reader/Encode.lean +++ b/Complexity/Computability/TreeEval/Reader/Encode.lean @@ -41,8 +41,8 @@ def Frame.equiv : Frame ≃ ℕ × Fin 4 × Bool × Fin 3 where right_inv _ := rfl /-- The encoding of frames. -/ -noncomputable def encFrame : Frame ↪ List Bool := - encOfEquiv Frame.equiv (encPair encNat (encFinite (Fin 4 × Bool × Fin 3))) +def encFrame : Frame ↪ List Bool := + encOfEquiv Frame.equiv (encPair encNat (encFinEnum (Fin 4 × Bool × Fin 3))) /-- A mode as an option. -/ def Mode.equiv : Mode ≃ Option (Bool × Fin 3) where @@ -55,10 +55,10 @@ def Mode.equiv : Mode ≃ Option (Bool × Fin 3) where left_inv m := by cases m <;> rfl right_inv o := by rcases o with _ | ⟨_, _⟩ <;> rfl -instance : Finite Mode := Finite.of_equiv _ Mode.equiv.symm +instance : FinEnum Mode := FinEnum.ofEquiv _ Mode.equiv /-- The encoding of modes. -/ -noncomputable def encMode : Mode ↪ List Bool := encFinite Mode +def encMode : Mode ↪ List Bool := encFinEnum Mode /-- The control state as a tuple: a tag, two naturals and a list. -/ def Ctl.toTuple : Ctl → Fin 7 × ℕ × ℕ × List ℕ @@ -75,11 +75,11 @@ theorem Ctl.toTuple_injective : Function.Injective Ctl.toTuple := by cases c <;> cases c' <;> simp_all [Ctl.toTuple] /-- The encoding of tuples of control states. -/ -noncomputable abbrev encCtlTuple : Fin 7 × ℕ × ℕ × List ℕ ↪ List Bool := - encPair (encFinite (Fin 7)) (encPair encNat (encPair encNat (encList encNat))) +abbrev encCtlTuple : Fin 7 × ℕ × ℕ × List ℕ ↪ List Bool := + encPair (encFinEnum (Fin 7)) (encPair encNat (encPair encNat (encList encNat))) /-- The encoding of control states. -/ -noncomputable def encCtl : Ctl ↪ List Bool := +def encCtl : Ctl ↪ List Bool := ⟨fun c => encCtlTuple c.toTuple, encCtlTuple.injective.comp Ctl.toTuple_injective⟩ /-- The encoding of registers. -/ @@ -100,12 +100,12 @@ theorem State.toTuple_injective : Function.Injective State.toTuple := by rw [Ctl.toTuple_injective hc] /-- The encoding of tuples of states. -/ -noncomputable abbrev encTuple : Tuple ↪ List Bool := +abbrev encTuple : Tuple ↪ List Bool := encPair (encPair (encPair encNat (encPair encNat encNat)) encRegs) (encPair (encPair (encList encFrame) encMode) encCtlTuple) /-- **The encoding of states.** -/ -noncomputable def encState : State ↪ List Bool := +def encState : State ↪ List Bool := ⟨fun s => encTuple s.toTuple, encTuple.injective.comp State.toTuple_injective⟩ @[simp] theorem encState_apply (s : State) : encState s = encTuple s.toTuple := rfl diff --git a/Complexity/Computability/TreeEval/Reader/Size.lean b/Complexity/Computability/TreeEval/Reader/Size.lean index c0c2f6e10c..f0e654e87c 100644 --- a/Complexity/Computability/TreeEval/Reader/Size.lean +++ b/Complexity/Computability/TreeEval/Reader/Size.lean @@ -60,7 +60,7 @@ private theorem length_lt_primeFor {ℓ v : ℕ} (hv : v ≤ primeFor ℓ) : (en private theorem length_encFrame_le {fr : Frame} {P : ℕ} (h : (encNat fr.round).length ≤ P) : (encFrame fr).length ≤ 2 * P + 25 := by rw [encFrame_apply, length_encPair] - have := length_encFinite_lt (Frame.equiv fr).2 + have := length_encFinEnum_lt (Frame.equiv fr).2 simp only [Nat.card_eq_fintype_card, Fintype.card_prod, Fintype.card_fin, Fintype.card_bool] at this simp only [Frame.equiv, Equiv.coe_fn_mk] at this ⊢ @@ -73,14 +73,14 @@ private theorem length_encList_frames_le {st : List Frame} {P : ℕ} (by ring) private theorem length_encMode_lt (m : Mode) : (encMode m).length < 7 := by - have := length_encFinite_lt m + have := length_encFinEnum_lt m have hc : Nat.card Mode = 7 := by rw [Nat.card_congr Mode.equiv]; simp rw [hc] at this exact this -private theorem length_encTag_lt (t : Fin 7) : (encFinite (Fin 7) t).length < 7 := by - simpa using length_encFinite_lt t +private theorem length_encTag_lt (t : Fin 7) : (encFinEnum (Fin 7) t).length < 7 := by + simpa using length_encFinEnum_lt t /-- The bounds on the components of a state that satisfies the invariant. -/ structure Bounds (ℓ H : ℕ) (s : State) : Prop where diff --git a/Complexity/Computability/USTCON/Reader/Cert.lean b/Complexity/Computability/USTCON/Reader/Cert.lean index 464223e81d..0b45f15686 100644 --- a/Complexity/Computability/USTCON/Reader/Cert.lean +++ b/Complexity/Computability/USTCON/Reader/Cert.lean @@ -43,11 +43,11 @@ namespace Cslib.USTCON.Reader open Turing MultiTapeTM ComputableTidilyInSpace Cslib.RotationMap Cslib.Reachability.Reingold /-- The encoding of the inputs of a step: the tuple and the bit read. -/ -noncomputable abbrev encStepIn : Tuple × Bool ↪ List Bool := +abbrev encStepIn : Tuple × Bool ↪ List Bool := encPair encTuple encBool /-- **The space budget of a step**: the length of the encoded tuple and bit. -/ -noncomputable def stepBudget (y : Tuple × Bool) : ℕ := +def stepBudget (y : Tuple × Bool) : ℕ := (encStepIn y).length private theorem len_le_stepBudget : (fun y => (encStepIn y).length) ≼ stepBudget := @@ -256,10 +256,10 @@ within work space linear in their number. -/ private theorem labelOfNat_inSpace : ComputableTidilyInSpace labelOfNat encNat encLab fun w => (encNat w).length := by have hfold := of_inO (ComputableTidilyInO.foldl_bits_finite - (encFinite (ZMod numLabels × ZMod numLabels)) modStep (0, 1)) + (encFinEnum (ZMod numLabels × ZMod numLabels)) modStep (0, 1)) have h := hfold.of_encIn_eq (α' := ℕ) (encIn' := encNat) Nat.bits fun w ↦ by rw [encNat_apply, encBits_apply] - have h' := budget_comp_linear (of_finite (encIn := encFinite (ZMod numLabels × ZMod numLabels)) + have h' := budget_comp_linear (of_finite (encIn := encFinEnum (ZMod numLabels × ZMod numLabels)) (encB := encLab) fun p : ZMod numLabels × ZMod numLabels ↦ labelOfZMod p.1) h exact (h'.weaken (.const 0 _)).of_enc_eq fun w ↦ by rw [labelOfNat_eq] @@ -441,7 +441,7 @@ private theorem stepT_inSpace : ComputableTidilyInSpace stepT encStepIn (encPair done)))))))) refine h.of_enc_eq fun y ↦ ?_ obtain ⟨⟨⟨ctl, cnt⟩, ⟨⟨n, s, t⟩, d, l⟩, ⟨c, w, j⟩, v, low, fr⟩, b⟩ := y - congr 1 + apply congrArg (encPair encTuple encBits) cases ctl case eval => by_cases hfr : fr = [] @@ -465,7 +465,7 @@ private theorem stepT_inSpace : ComputableTidilyInSpace stepT encStepIn (encPair /-! ### On states -/ /-- **The space budget of a state**: the length of its encoded tuple with a bit. -/ -noncomputable def stateBudget (q : State) : ℕ := +def stateBudget (q : State) : ℕ := stepBudget (q.toTuple, false) private theorem stepBudget_bool (x : Tuple) (b : Bool) : stepBudget (x, b) = stepBudget diff --git a/Complexity/Computability/USTCON/Reader/Encode.lean b/Complexity/Computability/USTCON/Reader/Encode.lean index 574f17d459..cda409074b 100644 --- a/Complexity/Computability/USTCON/Reader/Encode.lean +++ b/Complexity/Computability/USTCON/Reader/Encode.lean @@ -19,9 +19,9 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair The states of `Cslib.USTCON.Reader.machine` are encoded through tuples of the control, numbers in binary, and lists of labels and frames, every label and frame by its rank among the finitely many -(`Turing.MultiTapeTM.encFinite`). The machines simulating the read machine keep the encoded state on -their work tapes, so its length bounds their work space, up to a constant factor and the position -of the input head. +(`Turing.MultiTapeTM.encFinEnum`). The machines simulating the read machine keep the encoded state +on their work tapes, so its length bounds their work space, up to a constant factor and the +position of the input head. ## Main definitions @@ -43,6 +43,18 @@ instance : Fintype Ctl where elems := {.hdrN, .hdrS, .hdrT, .size, .start, .fill, .next, .eval, .check, .done} complete x := by cases x <;> simp +instance : FinEnum Ctl := + FinEnum.ofList [.hdrN, .hdrS, .hdrT, .size, .start, .fill, .next, .eval, .check, .done] + fun x => by cases x <;> decide + +instance : FinEnum ReingoldPc := + FinEnum.ofList [.zig₀, .call₀, .zag₀, .zig₁, .call₁, .zag₁, .finish] + fun x => by cases x <;> decide + +/-- Concrete enumeration of a positive modular ring. -/ +instance instFinEnumZMod (n : ℕ) [NeZero n] : FinEnum (ZMod n) := + FinEnum.ofEquiv (Fin n) (ZMod.finEquiv n).toEquiv.symm + /-- The states as tuples: the control and the header counter, the parameters of the instance and of Reingold's graph, and the counters of the walks with the state of the evaluation. -/ abbrev Tuple : Type := @@ -68,32 +80,32 @@ theorem State.toTuple_ofTuple (x : Tuple) : (State.ofTuple x).toTuple = x := rfl /-- Labels, by their ranks. -/ -noncomputable def encLab : Label ↪ List Bool := - encFinite Label +def encLab : Label ↪ List Bool := + encFinEnum Label /-- Frames, by their ranks. -/ -noncomputable def encFrame : ReingoldPc × Label ↪ List Bool := - encFinite (ReingoldPc × Label) +def encFrame : ReingoldPc × Label ↪ List Bool := + encFinEnum (ReingoldPc × Label) /-- Three numbers. -/ abbrev encNat3 : ℕ × ℕ × ℕ ↪ List Bool := encPair encNat (encPair encNat encNat) /-- The state of the evaluation: the slot, the labels and the frames. -/ -noncomputable abbrev encEval : (ℕ × ℕ) × List Label × List (ReingoldPc × Label) ↪ List Bool := +abbrev encEval : (ℕ × ℕ) × List Label × List (ReingoldPc × Label) ↪ List Bool := encPair (encPair encNat encNat) (encPair (encList encLab) (encList encFrame)) /-- The control, by its rank. -/ -noncomputable def encCtl : Ctl ↪ List Bool := - encFinite Ctl +def encCtl : Ctl ↪ List Bool := + encFinEnum Ctl /-- The encoding of tuples. -/ -noncomputable abbrev encTuple : Tuple ↪ List Bool := +abbrev encTuple : Tuple ↪ List Bool := encPair (encPair encCtl encNat) (encPair (encPair encNat3 (encPair encNat encNat)) (encPair encNat3 encEval)) /-- The encoding of the states, through their tuples. -/ -noncomputable def encState : State ↪ List Bool := +def encState : State ↪ List Bool := ⟨fun q ↦ encTuple q.toTuple, fun q q' h ↦ by rw [← State.ofTuple_toTuple q, ← State.ofTuple_toTuple q', encTuple.injective h]⟩ diff --git a/Complexity/Computability/USTCON/Reader/Invariant.lean b/Complexity/Computability/USTCON/Reader/Invariant.lean index 43ac1d0daf..78805f5b1e 100644 --- a/Complexity/Computability/USTCON/Reader/Invariant.lean +++ b/Complexity/Computability/USTCON/Reader/Invariant.lean @@ -307,13 +307,13 @@ theorem inv_run (k : ℕ) : Inv I (machine.run I.encode k).state := by /-! ### The size of the states -/ /-- The encoded labels of a list, each by its rank. -/ -private theorem length_encList_finite_le {α : Type} [Finite α] (l : List α) : - (encList (encFinite α) l).length ≤ l.length * (2 * Nat.card α + 1) := by +private theorem length_encList_finEnum_le {α : Type} [FinEnum α] (l : List α) : + (encList (encFinEnum α) l).length ≤ l.length * (2 * Nat.card α + 1) := by rw [length_encList] induction l with | nil => simp | cons a l ih => - have := length_encFinite_lt a + have := length_encFinEnum_lt a simp only [List.map_cons, List.sum_cons, List.length_cons] nlinarith @@ -371,12 +371,12 @@ private theorem length_encState_le_of_bounds {q : State} (hb : Bounds I q) : rw [length_encNat_eq_size, ← hT]; exact size_le_of_le_pow hb.c have h₁₁ : (encNat q.w).length ≤ 65 * (4168 * a + 136240) + 1 := by rw [length_encNat_eq_size, ← hT]; exact size_le_of_le_pow hb.w - have h₁₂ : (encCtl q.ctl).length ≤ 10 := card_ctl ▸ (length_encFinite_lt _).le + have h₁₂ : (encCtl q.ctl).length ≤ 10 := card_ctl ▸ (length_encFinEnum_lt _).le have h₁₃ : (encList encLab q.ev.lower).length ≤ (16 * a + 525) * (2 * Nat.card Label + 1) := - (length_encList_finite_le _).trans (Nat.mul_le_mul_right _ (by have := hb.lower; omega)) + (length_encList_finEnum_le _).trans (Nat.mul_le_mul_right _ (by have := hb.lower; omega)) have h₁₄ : (encList encFrame q.ev.frames).length ≤ (16 * a + 525) * (2 * Nat.card (ReingoldPc × Label) + 1) := - (length_encList_finite_le _).trans (Nat.mul_le_mul_right _ (by have := hb.frames; omega)) + (length_encList_finEnum_le _).trans (Nat.mul_le_mul_right _ (by have := hb.frames; omega)) rw [natCard_label] at h₁₃ rw [card_frame] at h₁₄ refine (length_encState_le q).trans ?_ diff --git a/ComplexityTests/ConfigurationPolyTime.lean b/ComplexityTests/ConfigurationPolyTime.lean index cc1eadf0ba..c20e59334b 100644 --- a/ComplexityTests/ConfigurationPolyTime.lean +++ b/ComplexityTests/ConfigurationPolyTime.lean @@ -37,7 +37,7 @@ example : ComputableTidilyInPolyTime example {α : Type} (input : α ↪ List Bool) (cfg : α → Config) (hcfg : ComputableTidilyInPolyTime cfg input encFiniteConfig) : ComputableTidilyInPolyTime (fun a => (cfg a).tapes.inputSymbol) input - (encFinite (Option Bool)) := by fun_prop + (encFinEnum (Option Bool)) := by fun_prop -- A different input encoding uses its existing conversion certificate; no program rewrite. example : ComputableTidilyInPolyTime (FiniteConfig.init (k := 2) (Oracle := Fin 2) (0 : Fin 2)) diff --git a/ComplexityTests/ExpanderContraction.lean b/ComplexityTests/ExpanderContraction.lean index a181b12d34..19dfd71307 100644 --- a/ComplexityTests/ExpanderContraction.lean +++ b/ComplexityTests/ExpanderContraction.lean @@ -54,16 +54,16 @@ example : Function.IsPartialInv (RotationMap.finSlotEncode (by decide : 0 ≤ 0 -- Actual finite witnesses for the complete contraction certificate. example : ComputableTidilyInPolyTime threeVertices.rot - (encPair (encFinite (Fin 3)) (encPair (encFinite (Fin 2)) (encFinite (Fin 5)))) - (encPair (encFinite (Fin 3)) (encPair (encFinite (Fin 2)) (encFinite (Fin 5)))) := by + (encPair (encFinEnum (Fin 3)) (encPair (encFinEnum (Fin 2)) (encFinEnum (Fin 5)))) + (encPair (encFinEnum (Fin 3)) (encPair (encFinEnum (Fin 2)) (encFinEnum (Fin 5)))) := by have he : ComputableTidilyInPolyTime (RotationMap.finSlotEncode (by decide : 5 ≤ 2 * 3)) - (encFinite (Fin 5)) (encPair (encFinite (Fin 3)) (encFinite (Fin 2))) := .of_finite _ + (encFinEnum (Fin 5)) (encPair (encFinEnum (Fin 3)) (encFinEnum (Fin 2))) := .of_finite _ have hd : ComputableTidilyInPolyTime (RotationMap.finSlotDecode (m := 5)) - (encPair (encFinite (Fin 3)) (encFinite (Fin 2))) - (encOption (encFinite (Fin 5))) := .of_finite _ + (encPair (encFinEnum (Fin 3)) (encFinEnum (Fin 2))) + (encOption (encFinEnum (Fin 5))) := .of_finite _ have hg : ComputableTidilyInPolyTime completeFive.rot - (encPair (encFinite (Fin 5)) (encFinite (Fin 5))) - (encPair (encFinite (Fin 5)) (encFinite (Fin 5))) := .of_finite _ + (encPair (encFinEnum (Fin 5)) (encFinEnum (Fin 5))) + (encPair (encFinEnum (Fin 5)) (encFinEnum (Fin 5))) := .of_finite _ fun_prop [threeVertices, RotationMap.contractFin] example {V W I D : Type} (G : RotationMap V D) (encode : V → W × I) @@ -111,7 +111,7 @@ example : ComputableTidilyInPolyTime example : ComputableTidilyInPolyTime (fun p : Option (Fin 0) × List Bool => p.1.elim p.2 (fun v => Fin.elim0 v)) - (encPair (encOption (encFinite (Fin 0))) encBits) encBits := by + (encPair (encOption (encFinEnum (Fin 0))) encBits) encBits := by apply ComputableTidilyInPolyTime.optionElimWithInput · fun_prop · fun_prop diff --git a/ComplexityTests/FiniteControl.lean b/ComplexityTests/FiniteControl.lean index 3f0b93877c..ae5f14d741 100644 --- a/ComplexityTests/FiniteControl.lean +++ b/ComplexityTests/FiniteControl.lean @@ -52,7 +52,15 @@ example {α Index Value : Type} [Fintype Index] {input : α ↪ List Bool} -- A different encoding of the same index type uses the same lookup rule. example : ComputableTidilyInPolyTime (fun pair : (Bool → List Bool) × Bool => pair.1 pair.2) - (encPair (encPi encBits) (encFinite Bool)) encBits := by polytime + (encPair (encPi encBits) (encFinEnum Bool)) encBits := by polytime + +/-- info: [true, true] -/ +#guard_msgs in +#eval encFinEnum (Fin 3) 2 + +/-- info: [true] -/ +#guard_msgs in +#eval encFinEnum (Option Bool) (some true) -- Computed update and lookup preserve unbounded words in all unselected entries. example : ComputableTidilyInPolyTime diff --git a/ComplexityTests/FiniteTables.lean b/ComplexityTests/FiniteTables.lean index 95de587ec7..178a4c0bb9 100644 --- a/ComplexityTests/FiniteTables.lean +++ b/ComplexityTests/FiniteTables.lean @@ -71,6 +71,8 @@ example {Index Value : Type} [Fintype Index] [DecidableEq Index] (encPair (encPi enc) enc) (encPi enc) := by fun_prop -- Unary ranks are bounded for each fixed finite type; no efficient growing enumeration is claimed. +example (tag : Fin 7) : (encFinEnum (Fin 7) tag).length < 7 := by + simpa using length_encFinEnum_lt tag example (tag : Fin 7) : (encFinite (Fin 7) tag).length < 7 := by simpa using length_encFinite_lt tag diff --git a/ComplexityTests/OracleComposition/Substitution.lean b/ComplexityTests/OracleComposition/Substitution.lean index ab99e24f3b..cf39a59e9d 100644 --- a/ComplexityTests/OracleComposition/Substitution.lean +++ b/ComplexityTests/OracleComposition/Substitution.lean @@ -44,7 +44,7 @@ private theorem run_cached (n : ℕ) (request : Unit × List Bool) -- The cache is certified from the memoization contract and the bounded-prefix query. private theorem cached_isOraclePPTOn : IsOraclePPTOn (encPair encUnary - (encPair (encPair (encFinite Unit) encBits) (encList (encPair encBits encBits)))) + (encPair (encPair (encFinEnum Unit) encBits) (encList (encPair encBits encBits)))) (encPair encBits (encList (encPair encBits encBits))) (fun pair => cached pair.1 pair.2.1 pair.2.2) := by unfold cached @@ -143,7 +143,7 @@ private theorem run_double (n : ℕ) (request : Unit × List Bool) (state : List -- Each doubling call is strict oracle PPT in its caller, request and state. example : IsOraclePPTOn - (encPair encUnary (encPair (encPair (encFinite Unit) encBits) encBits)) + (encPair encUnary (encPair (encPair (encFinEnum Unit) encBits) encBits)) (encPair encBits encBits) (fun pair => double pair.1 pair.2.1 pair.2.2) := by unfold double fun_prop diff --git a/ComplexityTests/PCPApproximation.lean b/ComplexityTests/PCPApproximation.lean index 08b2d35a42..99d9eaf1ef 100644 --- a/ComplexityTests/PCPApproximation.lean +++ b/ComplexityTests/PCPApproximation.lean @@ -174,7 +174,7 @@ example {c s : ℝ} (hc : c ≤ 1) : /-- The conjecture is a proposition; nothing assumes it. -/ example : UniqueGamesConjecture → ∃ L : ℕ, PromiseProblem.NPHard - (Graph.encoding (encPi (encFinite (Fin L)))) (GapUniqueGames (Fin L) (1 / 2) (1 / 4)) := + (Graph.encoding (encPi (encFinEnum (Fin L)))) (GapUniqueGames (Fin L) (1 / 2) (1 / 4)) := fun h => (h (1 / 2) (1 / 4) (by norm_num) (by norm_num) (by norm_num)).imp fun _ hL => by norm_num at hL ⊢ exact hL diff --git a/ComplexityTests/PCPEncodedAmplification.lean b/ComplexityTests/PCPEncodedAmplification.lean index cd19da013d..a7e7659c60 100644 --- a/ComplexityTests/PCPEncodedAmplification.lean +++ b/ComplexityTests/PCPEncodedAmplification.lean @@ -30,8 +30,8 @@ private theorem rotateReflection_eq (n : ℕ) (v : Fin n) (d : Unit) : private theorem isPolyTime_rotateReflection : ComputableTidilyInPolyTime rotateReflection - (encPair encUnary (encPair encUnary (encFinite Unit))) - (encPair encUnary (encFinite Unit)) := by + (encPair encUnary (encPair encUnary (encFinEnum Unit))) + (encPair encUnary (encFinEnum Unit)) := by unfold rotateReflection fun_prop @@ -155,8 +155,8 @@ example {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph Bo (hgraph : ComputableTidilyInPolyTime graph input (Graph.encoding encBool)) (rotate : ℕ × (ℕ × Unit) → ℕ × Unit) (hr : ComputableTidilyInPolyTime rotate - (encPair encUnary (encPair encUnary (encFinite Unit))) - (encPair encUnary (encFinite Unit))) : + (encPair encUnary (encPair encUnary (encFinEnum Unit))) + (encPair encUnary (encFinEnum Unit))) : ComputableTidilyInPolyTime (fun x => let g := graph x g.powerPreprocess evalConstraint false rotate 1 2 walks) @@ -184,8 +184,8 @@ example {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph Bo (hgraph : ComputableTidilyInPolyTime graph input (Graph.encoding encBool)) (rotate : ℕ × (ℕ × Fin 16) → ℕ × Fin 16) (hr : ComputableTidilyInPolyTime rotate - (encPair encUnary (encPair encUnary (encFinite (Fin 16)))) - (encPair encUnary (encFinite (Fin 16)))) : + (encPair encUnary (encPair encUnary (encFinEnum (Fin 16)))) + (encPair encUnary (encFinEnum (Fin 16)))) : ComputableTidilyInPolyTime (fun x => let powered := (graph x).powerPreprocess unitEval false rotate 4 2 [(fun _ => .inr (), fun _ => 0)] @@ -193,7 +193,7 @@ example {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph Bo input (Graph.encoding (encPi (encPi encBool))) := by have he : ComputableTidilyInPolyTime (fun p : Bool × (Unit × Unit) => unitEval p.1 p.2.1 p.2.2) - (encPair encBool (encPair (encFinite Unit) (encFinite Unit))) encBool := by + (encPair encBool (encPair (encFinEnum Unit) (encFinEnum Unit))) encBool := by unfold unitEval fun_prop fun_prop @@ -204,8 +204,8 @@ example {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph Bo (hgraph : ComputableTidilyInPolyTime graph input (Graph.encoding encBool)) (rotate : ℕ × (ℕ × Fin 16) → ℕ × Fin 16) (hr : ComputableTidilyInPolyTime rotate - (encPair encUnary (encPair encUnary (encFinite (Fin 16)))) - (encPair encUnary (encFinite (Fin 16)))) + (encPair encUnary (encPair encUnary (encFinEnum (Fin 16)))) + (encPair encUnary (encFinEnum (Fin 16)))) (output : (Graph.PowerAlphabet (Fin 16) Unit 4 → Graph.PowerAlphabet (Fin 16) Unit 4 → Bool) ↪ List Bool) : ComputableTidilyInPolyTime @@ -214,7 +214,7 @@ example {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph Bo input (Graph.encoding output) := by have he : ComputableTidilyInPolyTime (fun p : Bool × (Unit × Unit) => unitEval p.1 p.2.1 p.2.2) - (encPair encBool (encPair (encFinite Unit) (encFinite Unit))) encBool := by + (encPair encBool (encPair (encFinEnum Unit) (encFinEnum Unit))) encBool := by unfold unitEval fun_prop fail_if_success (clear hgraph; polytime) @@ -248,7 +248,7 @@ example : ComputableTidilyInPolyTime selectedPartialRound (Graph.encoding encBoo have hr := isPolyTime_rotateReflection have he : ComputableTidilyInPolyTime (fun p : Bool × (Unit × Unit) => unitEval p.1 p.2.1 p.2.2) - (encPair encBool (encPair (encFinite Unit) (encFinite Unit))) encBool := by + (encPair encBool (encPair (encFinEnum Unit) (encFinEnum Unit))) encBool := by unfold unitEval fun_prop unfold selectedPartialRound Graph.amplify @@ -301,7 +301,7 @@ example : ComputableTidilyInPolyTime completeRound (Graph.encoding encBool) have hr := RotationMap.polytime_arithmeticExpanderRotate (encFinite ArithmeticLabel) have he : ComputableTidilyInPolyTime (fun p : Bool × (Unit × Unit) => unitEval p.1 p.2.1 p.2.2) - (encPair encBool (encPair (encFinite Unit) (encFinite Unit))) encBool := by + (encPair encBool (encPair (encFinEnum Unit) (encFinEnum Unit))) encBool := by unfold unitEval fun_prop unfold completeRound @@ -317,7 +317,7 @@ example {Input : Type} (input : Input ↪ List Bool) (graph : Input → Graph Bo have hr := RotationMap.polytime_arithmeticExpanderRotate (encFinite ArithmeticLabel) have he : ComputableTidilyInPolyTime (fun p : Bool × (Unit × Unit) => unitEval p.1 p.2.1 p.2.2) - (encPair encBool (encPair (encFinite Unit) (encFinite Unit))) encBool := by + (encPair encBool (encPair (encFinEnum Unit) (encFinEnum Unit))) encBool := by unfold unitEval fun_prop polytime diff --git a/ComplexityTests/PCPEncodedAssignmentTester.lean b/ComplexityTests/PCPEncodedAssignmentTester.lean index 6a66481547..d0387c3237 100644 --- a/ComplexityTests/PCPEncodedAssignmentTester.lean +++ b/ComplexityTests/PCPEncodedAssignmentTester.lean @@ -82,8 +82,8 @@ example {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bo example : ComputableTidilyInPolyTime (fun p : (Bool → Bool → Bool) × Rand Bool × Query => Encoded.HadamardTester.query p.1 p.2.1 p.2.2) - (encPair (encPi (encPi encBool)) (encPair (encFinite (Rand Bool)) (encFinite Query))) - (encFinite (Pos Bool)) := by fun_prop + (encPair (encPi (encPi encBool)) (encPair (encFinite (Rand Bool)) (encFinEnum Query))) + (encFinEnum (Pos Bool)) := by fun_prop example : ComputableTidilyInPolyTime (fun p : (Bool → Bool → Bool) × Rand Bool × (Query → Bool) => @@ -95,7 +95,7 @@ example : ComputableTidilyInPolyTime example : ComputableTidilyInPolyTime (fun p : List Bool × Rand Bool × Query => Encoded.HadamardTester.query (fun a b => p.1.getD (a.toNat + 2 * b.toNat) false) p.2.1 p.2.2) - (encPair encBits (encPair (encFinite (Rand Bool)) (encFinite Query))) - (encFinite (Pos Bool)) := by polytime + (encPair encBits (encPair (encFinite (Rand Bool)) (encFinEnum Query))) + (encFinEnum (Pos Bool)) := by polytime end ComplexityTests.PCPEncodedTester diff --git a/ComplexityTests/PCPEncodedComposition.lean b/ComplexityTests/PCPEncodedComposition.lean index 5b0f3edeb0..447755ed66 100644 --- a/ComplexityTests/PCPEncodedComposition.lean +++ b/ComplexityTests/PCPEncodedComposition.lean @@ -93,7 +93,7 @@ example : ComputableTidilyInPolyTime (Graph.compose (numberSlots boolAlphabet).2 boolCoins queries) (Graph.encoding (encPi (encPi encBool))) (Graph.encoding (encPair (encPi (encPi encBool)) - (encPair (encFinite (Rand Bool)) (encFinite Query)))) := by fun_prop + (encPair (encFinite (Rand Bool)) (encFinEnum Query)))) := by fun_prop -- The composed descriptors normalize to fixed tables over the 17-query answer alphabet. example : ComputableTidilyInPolyTime diff --git a/ComplexityTests/PCPEncodedEnumeration.lean b/ComplexityTests/PCPEncodedEnumeration.lean index 403ca510e6..b5d8db92ff 100644 --- a/ComplexityTests/PCPEncodedEnumeration.lean +++ b/ComplexityTests/PCPEncodedEnumeration.lean @@ -46,14 +46,14 @@ private theorem rotateLoops_eq (n : ℕ) (v : Fin n) (d : Unit) : private theorem polytime_rotateLoops : ComputableTidilyInPolyTime rotateLoops - (encPair encUnary (encPair encUnary (encFinite Unit))) - (encPair encUnary (encFinite Unit)) := by + (encPair encUnary (encPair encUnary (encFinEnum Unit))) + (encPair encUnary (encFinEnum Unit)) := by unfold rotateLoops fun_prop private theorem polytime_unitEval : ComputableTidilyInPolyTime (fun p : Bool × (Unit × Unit) => unitEval p.1 p.2.1 p.2.2) - (encPair encBool (encPair (encFinite Unit) (encFinite Unit))) encBool := by + (encPair encBool (encPair (encFinEnum Unit) (encFinEnum Unit))) encBool := by unfold unitEval fun_prop diff --git a/ComplexityTests/PCPEncodedPreprocess.lean b/ComplexityTests/PCPEncodedPreprocess.lean index 9634fe24fd..635cd33351 100644 --- a/ComplexityTests/PCPEncodedPreprocess.lean +++ b/ComplexityTests/PCPEncodedPreprocess.lean @@ -32,8 +32,8 @@ private theorem rotateReflection_eq (n : ℕ) (v : Fin n) (d : Unit) : private theorem isPolyTime_rotateReflection : ComputableTidilyInPolyTime rotateReflection - (encPair encUnary (encPair encUnary (encFinite Unit))) - (encPair encUnary (encFinite Unit)) := by + (encPair encUnary (encPair encUnary (encFinEnum Unit))) + (encPair encUnary (encFinEnum Unit)) := by unfold rotateReflection polytime diff --git a/ComplexityTests/PCPExpander.lean b/ComplexityTests/PCPExpander.lean index ad12d556fa..be15c132fe 100644 --- a/ComplexityTests/PCPExpander.lean +++ b/ComplexityTests/PCPExpander.lean @@ -18,7 +18,7 @@ namespace ComplexityTests.PCPExpander example : ComputableTidilyInPolyTime (fun index : ℕ => (⟨index % 1, Nat.mod_lt _ (by decide)⟩ : Fin 1)) - encUnary (encFinite (Fin 1)) := + encUnary (encFinEnum (Fin 1)) := ComputableTidilyInPolyTime.unary_finMod (by decide) _ -- The fixed finite output may use binary indices instead of the finite-rank encoding. @@ -38,14 +38,14 @@ private def coordinates : Fin 16 ≃ (Fin 2 → Fin 2 × Fin 2) := (finTwoArrowEquiv (Fin 2 × Fin 2)).symm) example : ComputableTidilyInPolyTime (TowerTable.build base coordinates (by decide)) - encUnary (TowerTable.encoding (encFinite (Fin 2))) := + encUnary (TowerTable.encoding (encFinEnum (Fin 2))) := TowerTable.polytime_build base coordinates (by decide) _ -- Equivalent call spellings and captured inputs use the same uniform certificate. example : ComputableTidilyInPolyTime (fun p : Bool × ℕ => TowerTable.build base coordinates (by decide) (p.2 + 1)) - (encPair encBool encUnary) (TowerTable.encoding (encFinite (Fin 2))) := by - have h := TowerTable.polytime_build base coordinates (by decide) (encFinite (Fin 2)) + (encPair encBool encUnary) (TowerTable.encoding (encFinEnum (Fin 2))) := by + have h := TowerTable.polytime_build base coordinates (by decide) (encFinEnum (Fin 2)) polytime example : (TowerTable.build base coordinates (by decide) 0).length = 16 := by decide @@ -75,8 +75,8 @@ example (size : ℕ) (vertex : Fin (16 ^ (Nat.clog 16 size - 1 + 1))) (label : F example : ComputableTidilyInPolyTime (TowerTable.rotateFamily base coordinates (by decide)) (encPair encUnary (encPair encUnary - (encFinite ((Fin 16 × (Fin 2 × Fin 2)) ⊕ (Fin 16 × (Fin 2 × Fin 2)))))) - (encPair encUnary (encFinite ((Fin 16 × (Fin 2 × Fin 2)) ⊕ + (encFinEnum ((Fin 16 × (Fin 2 × Fin 2)) ⊕ (Fin 16 × (Fin 2 × Fin 2)))))) + (encPair encUnary (encFinEnum ((Fin 16 × (Fin 2 × Fin 2)) ⊕ (Fin 16 × (Fin 2 × Fin 2))))) := TowerTable.polytime_rotateFamily base coordinates (by decide) _ diff --git a/ComplexityTests/PCPPreprocessPrograms.lean b/ComplexityTests/PCPPreprocessPrograms.lean index 8b49fd9928..389419ca03 100644 --- a/ComplexityTests/PCPPreprocessPrograms.lean +++ b/ComplexityTests/PCPPreprocessPrograms.lean @@ -85,8 +85,8 @@ example : ComputableTidilyInPolyTime (fun p : Graph Bool × ((ℕ × Bool) × Graph.PreprocessLabel Bool) => p.1.preprocessRotation false rotateReflection p.2) (encPair (Graph.encoding encBool) - (encPair (encPair encUnary encBool) (encFinite (Graph.PreprocessLabel Bool)))) - (encPair (encPair encUnary encBool) (encFinite (Graph.PreprocessLabel Bool))) := by + (encPair (encPair encUnary encBool) (encFinEnum (Graph.PreprocessLabel Bool)))) + (encPair (encPair encUnary encBool) (encFinEnum (Graph.PreprocessLabel Bool))) := by have h := isPolyTime_rotateReflection fun_prop @@ -94,7 +94,7 @@ example : ComputableTidilyInPolyTime (fun g : Graph Bool => g.preprocessRotation false rotateReflection ((g.edges.length, false), cloud false)) (Graph.encoding encBool) - (encPair (encPair encUnary encBool) (encFinite (Graph.PreprocessLabel Bool))) := by + (encPair (encPair encUnary encBool) (encFinEnum (Graph.PreprocessLabel Bool))) := by have h := isPolyTime_rotateReflection fun_prop @@ -103,8 +103,8 @@ example (T : ℕ) : ComputableTidilyInPolyTime (fun p : Graph Bool × ((ℕ × Bool) × Graph.PreprocessLabel Bool) => p.1.preprocessRotation false rotateReflection p.2) T) (encPair (Graph.encoding encBool) - (encPair (encPair encUnary encBool) (encPi (encFinite (Graph.PreprocessLabel Bool))))) - (encPair (encPair encUnary encBool) (encPi (encFinite (Graph.PreprocessLabel Bool)))) := by + (encPair (encPair encUnary encBool) (encPi (encFinEnum (Graph.PreprocessLabel Bool))))) + (encPair (encPair encUnary encBool) (encPi (encFinEnum (Graph.PreprocessLabel Bool)))) := by have h := isPolyTime_rotateReflection fun_prop diff --git a/ComplexityTests/PCPSelectedAssignmentTester.lean b/ComplexityTests/PCPSelectedAssignmentTester.lean index f31781429b..5ef7808299 100644 --- a/ComplexityTests/PCPSelectedAssignmentTester.lean +++ b/ComplexityTests/PCPSelectedAssignmentTester.lean @@ -70,8 +70,8 @@ example : ComputableTidilyInPolyTime (fun p : (Bool → Bool → Bool) × (Fin 5 × Rand Bool) × Fin 6 => Encoded.SelectedHadamardTester.query p.1 p.2.1 p.2.2) (encPair (encPi (encPi encBool)) - (encPair (encFinite (Fin 5 × Rand Bool)) (encFinite (Fin 6)))) - (encFinite (Pos Bool)) := by fun_prop + (encPair (encFinite (Fin 5 × Rand Bool)) (encFinEnum (Fin 6)))) + (encFinEnum (Pos Bool)) := by fun_prop example : ComputableTidilyInPolyTime (fun p : (Bool → Bool → Bool) × (Fin 5 × Rand Bool) × (Fin 6 → Bool) => diff --git a/ComplexityTests/PolyTimeTactic.lean b/ComplexityTests/PolyTimeTactic.lean index 306b7897e2..440245a920 100644 --- a/ComplexityTests/PolyTimeTactic.lean +++ b/ComplexityTests/PolyTimeTactic.lean @@ -30,7 +30,7 @@ example (f : Bool → ℕ) : ComputableTidilyInPolyTime f encBool encUnary := by -- Fixed finite products also support lookup without a specialized callback certificate. example (f : Fin 7 × Bool → ℕ) : - ComputableTidilyInPolyTime f (encPair (encFinite (Fin 7)) encBool) encUnary := by + ComputableTidilyInPolyTime f (encPair (encFinEnum (Fin 7)) encBool) encUnary := by polytime -- A finite output alone does not certify an arbitrary function on an infinite input type. @@ -346,7 +346,7 @@ example {α : Type} (encA : α ↪ List Bool) (encL : List α ↪ List Bool) -- Empty element types still have the empty list as a computational input. example : ComputableTidilyInPolyTime (List.head? (α := Fin 0)) - (encList (encFinite (Fin 0))) (encOption (encFinite (Fin 0))) := by fun_prop + (encList (encFinEnum (Fin 0))) (encOption (encFinEnum (Fin 0))) := by fun_prop -- Nested range/map, Boolean folds and majority share the computation calculus. example (call : List Bool → ℕ → ℕ → Bool) diff --git a/ComplexityTests/RotationWalk.lean b/ComplexityTests/RotationWalk.lean index b5f70f9a8c..fb2ce2cdf5 100644 --- a/ComplexityTests/RotationWalk.lean +++ b/ComplexityTests/RotationWalk.lean @@ -109,8 +109,9 @@ example : ComputableTidilyInPolyTime example : ComputableTidilyInPolyTime (RotationMap.killedPowRotWithInput rotate 3 2) (encPair encUnary (encPair (encPair encUnary encBool) - (encPair (encPi encBool) (encPi (encFinite (Fin 2)))))) - (encPair (encPair encUnary encBool) (encPair (encPi encBool) (encPi (encFinite (Fin 2))))) := by + (encPair (encPi encBool) (encPi (encFinEnum (Fin 2)))))) + (encPair (encPair encUnary encBool) + (encPair (encPi encBool) (encPi (encFinEnum (Fin 2))))) := by have := polytime_rotation fun_prop