refactor(encodings): computable FinEnum-based encoding for concrete finite types

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,16 +255,16 @@ 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
   have hloc := budget_finite (encC := encFinite (Loc k State)) Ref.locOf hr
   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

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) ×

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

Complexity/Computability/Complexity/Classes/Inclusions.lean

@@ -178,22 +178,22 @@ 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))))
   obtain ⟨te, se, hte, -, he⟩ := hedge
   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))

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) ×

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]

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]

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
 

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)

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

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

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))

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))))

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))) :=