refactor(logics): state the Logics polynomial-time results plainly

Complexity/Computability/Complexity/Classes/Space/TQBF/PolyTime.lean

@@ -316,6 +316,12 @@ theorem computableTidilyInPolyTime_baseFormula {tab : γ → CNF (CookLevin.Var
       (encList (encList (encPair CookLevin.encVar encBool))))
     (hw : ComputableTidilyInPolyTime w encIn encUnary) :
     ComputableTidilyInPolyTime (fun x => baseFormula (tab x) (w x)) encIn encQBF := by
+  have hvars : ComputableTidilyInPolyTime (fun x => (tab x).vars) encIn
+      (encList CookLevin.encVar) :=
+    (CNF.computableInPolyTime_vars CookLevin.encVar).tidy.comp htab
+  have hrelabel : ComputableTidilyInPolyTime (fun x => CNF.relabel tabVar (tab x)) encIn
+      (encList (encList (encPair encNat encBool))) :=
+    (CNF.computableInPolyTime_relabel (.of_tidy computableTidilyInPolyTime_tabVar)).tidy.comp htab
   unfold baseFormula baseVars certLinks
   fun_prop
 

Complexity/Computability/Complexity/Classes/Space/TQBF/Prenex.lean

@@ -246,6 +246,13 @@ theorem computableTidilyInPolyTime_prenexReduce {kV : ℕ} {StateV : Type} [Fint
   have hp : ComputableTidilyInPolyTime (fun a => p.eval (enc a).length) enc encUnary :=
     (unary_eval p).comp (encoding_length enc)
   have hd : ComputableTidilyInPolyTime (fun _ : α => dummyVar) enc encNat := const _
+  have hvars : ComputableTidilyInPolyTime (CNF.vars (V := CookLevin.Var kV StateV))
+      (encList (encList (encPair CookLevin.encVar encBool))) (encList CookLevin.encVar) :=
+    (CNF.computableInPolyTime_vars _).tidy
+  have hrelabel : ComputableTidilyInPolyTime (CNF.relabel (tabVar (k := kV) (State := StateV)))
+      (encList (encList (encPair CookLevin.encVar encBool)))
+      (encList (encList (encPair encNat encBool))) :=
+    (CNF.computableInPolyTime_relabel (.of_tidy computableTidilyInPolyTime_tabVar)).tidy
   unfold prenexReduce gameTableau prenexPairs prenexMatrix gamePairs baseVars certLinkCNF
     encPrenexCNF encCNF
   fun_prop

Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean

@@ -177,6 +177,18 @@ theorem computableTidilyInPolyTime_reduce :
     funext x
     rw [reduce, binaryValue_take_hashBits]
     rfl
+  have hvars : ComputableTidilyInPolyTime (fun x : CNF ℕ × List Bool => x.1.vars)
+      (encPair (encList (encList (encPair encNat encBool))) encBits) (encList encNat) :=
+    (CNF.computableInPolyTime_vars encNat).tidy.comp (by fun_prop)
+  have hinl : ComputableTidilyInPolyTime
+      (fun x : CNF ℕ × List Bool => CNF.relabel (Sum.inl : ℕ → ℕ ⊕ ℕ × ℕ) x.1)
+      (encPair (encList (encList (encPair encNat encBool))) encBits)
+      (encList (encList (encPair (encSum encNat (encPair encUnary encUnary)) encBool))) :=
+    (CNF.computableInPolyTime_relabel (.of_tidy (by fun_prop))).tidy.comp (by fun_prop)
+  have hsplit : ComputableTidilyInPolyTime (CNF.relabel splitVarToNat)
+      (encList (encList (encPair (encSum encNat (encPair encUnary encUnary)) encBool)))
+      (encList (encList (encPair encNat encBool))) :=
+    (CNF.computableInPolyTime_relabel (.of_tidy computableTidilyInPolyTime_splitVarToNat)).tidy
   rw [h]
   unfold reduceWith encCNF
   fun_prop

Complexity/Computability/Complexity/CookLevin/Clauses.lean

@@ -60,6 +60,7 @@ theorem computableTidilyInPolyTime_groups :
   simp only [SProd.sprod, List.product, List.map_flatMap, List.map_map, Function.comp_def]
   fun_prop
 
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Build all exactly-one clauses for one tableau row, including the input-dependent windows. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_oneHotClauses [DecidableEq State]
@@ -87,20 +88,23 @@ theorem computableTidilyInPolyTime_acceptClauses :
       (encList (encList (encPair encVar encBool))) := by
   fun_prop [acceptClauses]
 
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Build the situation clauses at a unary time, with the finite machine data fixed. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_sitClauses :
     ComputableTidilyInPolyTime (sitClauses (k := k) (State := State)) encUnary
       (encList (encList (encPair encVar encBool))) := by
   fun_prop [sitClauses]
 
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Build the uniqueness clauses at a unary time, with the finite machine data fixed. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_uniqueClauses [DecidableEq State] :
     ComputableTidilyInPolyTime (uniqueClauses (k := k) (State := State)) encUnary
       (encList (encList (encPair encVar encBool))) := by
   fun_prop [uniqueClauses]
 
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Build input-symbol clauses from computed input, certificate length, time and position. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_inputClauses {α : Type} {enc : α ↪ List Bool}
@@ -114,6 +118,7 @@ theorem computableTidilyInPolyTime_inputClauses {α : Type} {enc : α ↪ List B
       enc (encList (encList (encPair encVar encBool))) := by
   fun_prop [inputClauses]
 
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Enumerate work-tape and input-symbol clauses, charging the complete input-dependent lists. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_readClauses
@@ -178,6 +183,7 @@ private theorem stepTerms_inPos {j : α → ℕ}
     · fun_prop
 
 omit [DecidableEq State] in
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 private theorem stepImpClauses {t : α → ℕ} {feature : α → Feature k State}
     {terms : α → List (Feature.Term k State)}
     (ht : ComputableTidilyInPolyTime t enc encUnary)

Complexity/Computability/Complexity/CookLevin/Encoding.lean

@@ -123,6 +123,6 @@ theorem computableTidilyInPolyTime_index :
 theorem computableTidilyInPolyTime_relabel :
     ComputableTidilyInPolyTime (Cslib.Logic.PL.CNF.relabel (Var.index (k := k) (State := State)))
       (encList (encList (encPair encVar encBool))) encCNF :=
-  Cslib.Logic.PL.CNF.computableTidilyInPolyTime_relabel computableTidilyInPolyTime_index
+  (Cslib.Logic.PL.CNF.computableInPolyTime_relabel (.of_tidy computableTidilyInPolyTime_index)).tidy
 
 end Cslib.Complexity.CookLevin

Complexity/Computability/Complexity/FineGrained/Sparsification.lean

@@ -345,8 +345,8 @@ open ComputableTidilyInPolyTime
 private theorem computableTidilyInPolyTime_isSparse_head (K α : ℕ) :
     ComputableTidilyInPolyTime (fun s : State => isSparse (threshold K α) K (s.1.headD []))
       encState encBool := by
-  have h := computableTidilyInPolyTime_isSparse encNat
-    (ClauseSet.Sparsification.computableTidilyInPolyTime_threshold_le K α) K
+  have h := (computableInPolyTime_isSparse encNat
+    (ClauseSet.Sparsification.computableInPolyTime_threshold_le K α) K).tidy
   have hH : ComputableTidilyInPolyTime (fun s : State => s.1.headD []) encState encCNF := by
     unfold encState
     fun_prop
@@ -355,15 +355,15 @@ private theorem computableTidilyInPolyTime_isSparse_head (K α : ℕ) :
 private theorem computableTidilyInPolyTime_inner (K α : ℕ) :
     ComputableTidilyInPolyTime (fun s : State => (next (threshold K α) K (s.1.headD []) false ::
       next (threshold K α) K (s.1.headD []) true :: s.1.tail, s.2)) encState encState := by
-  have h := computableTidilyInPolyTime_next encNat
-    (ClauseSet.Sparsification.computableTidilyInPolyTime_threshold_le K α) K
+  have h := (computableInPolyTime_next encNat
+    (ClauseSet.Sparsification.computableInPolyTime_threshold_le K α) K).tidy
   unfold encState encCNF
   fun_prop
 
 private theorem computableTidilyInPolyTime_root (k : ℕ) :
     ComputableTidilyInPolyTime (fun φ : CNF ℕ => (([root k φ], false) : State)) encCNF
       encState := by
-  have h := computableTidilyInPolyTime_normalize encNat
+  have h := (computableInPolyTime_normalize encNat).tidy
   unfold root encState encCNF
   fun_prop
 

Complexity/Computability/Complexity/Problems/CountingSAT.lean

@@ -264,7 +264,8 @@ def padMajority (φ : CNF ℕ) (Q : ℕ) : CNF ℕ :=
 private theorem computableTidilyInPolyTime_shiftOdd :
     ComputableTidilyInPolyTime shiftOdd encCNF encCNF := by
   unfold shiftOdd encCNF
-  fun_prop
+  exact (CNF.computableInPolyTime_relabel (f := fun v : ℕ => v + v + 1)
+    (.of_tidy (by fun_prop))).tidy
 
 @[fun_prop]
 private theorem computableTidilyInPolyTime_dummyClauses :
@@ -297,7 +298,7 @@ theorem computableTidilyInPolyTime_padMajority :
     refine ComputableTidilyInPolyTime.cons' (.const (0, false)) ?_
     exact (ComputableTidilyInPolyTime.map (encA := encNat)
       (encB := encPair encNat encBool) (by fun_prop)).comp
-      ((CNF.computableTidilyInPolyTime_vars encNat).comp hshift)
+      ((CNF.computableInPolyTime_vars encNat).tidy.comp hshift)
 
 private theorem injective_shiftOdd_fn : Function.Injective (fun v : ℕ => v + v + 1) := by
   intro a b h

Complexity/Computability/Complexity/Problems/SAT/PolyTime.lean

@@ -61,30 +61,30 @@ open ComputableTidilyInPolyTime
 @[fun_prop]
 theorem computableTidilyInPolyTime_vars :
     ComputableTidilyInPolyTime (CNF.vars (V := ℕ)) encCNF (encList encNat) :=
-  CNF.computableTidilyInPolyTime_vars encNat
+  (CNF.computableInPolyTime_vars encNat).tidy
 
 /-- The number of literals of a polynomial-time clause, in unary, is polynomial-time. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_clause_length {α : Type} {input : α ↪ List Bool}
     {c : α → Clause ℕ}
     (hc : ComputableTidilyInPolyTime c input (encList (encPair encNat encBool))) :
     ComputableTidilyInPolyTime (fun a => (c a).length) input encUnary :=
-  Clause.computableTidilyInPolyTime_length hc
+  (Clause.computableInPolyTime_length (.of_tidy hc)).tidy
 
 /-- The number of clauses of a polynomial-time formula, in unary, is polynomial-time. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_length {α : Type} {input : α ↪ List Bool} {φ : α → CNF ℕ}
     (hφ : ComputableTidilyInPolyTime φ input encCNF) :
     ComputableTidilyInPolyTime (fun a => (φ a).length) input encUnary :=
-  CNF.computableTidilyInPolyTime_length (encV := encNat) hφ
+  (CNF.computableInPolyTime_length (encV := encNat) (.of_tidy hφ)).tidy
 
 /-- The number of variable occurrences of a polynomial-time formula, in unary, is
 polynomial-time. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_vars_length {α : Type} {input : α ↪ List Bool}
     {φ : α → CNF ℕ} (hφ : ComputableTidilyInPolyTime φ input encCNF) :
     ComputableTidilyInPolyTime (fun a => (φ a).vars.length) input encUnary :=
-  CNF.computableTidilyInPolyTime_vars_length (encV := encNat) hφ
+  (CNF.computableInPolyTime_vars_length (encV := encNat) (.of_tidy hφ)).tidy
 
 /-- Reading the certificate at the first occurrence of a variable is polynomial-time. -/
 @[fun_prop]

Complexity/Computability/Complexity/Problems/ThreeSAT.lean

@@ -157,8 +157,8 @@ theorem computableTidilyInPolyTime_splitVarToNat :
 @[fun_prop]
 theorem computableTidilyInPolyTime_toThreeSAT :
     ComputableTidilyInPolyTime toThreeSAT encCNF encCNF :=
-  (CNF.computableTidilyInPolyTime_relabel computableTidilyInPolyTime_splitVarToNat).comp
-    (CNF.isPolyTime_to3CNF encNat)
+  (CNF.computableInPolyTime_relabel (.of_tidy computableTidilyInPolyTime_splitVarToNat)).tidy.comp
+    (CNF.isPolyTime_to3CNF encNat).tidy
 
 namespace ThreeSAT
 

Complexity/Computability/PCP/Encoded/GapTheorem.lean

@@ -12,6 +12,7 @@ public import Complexity.Computability.PCP.Encoded.SelectedComposition.Enumerati
 public import Complexity.Computability.PCP.Encoded.Amplification.Arithmetic
 public import Complexity.Logics.Propositional.CNF.ThreeCNF
 import Complexity.Logics.Propositional.CNF.ThreeCNF.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # An executable constant-gap reduction from SAT
@@ -71,7 +72,7 @@ theorem isPolyTime_gapGraph {V Input : Type} [DecidableEq V]
   unfold gapGraph
   apply Graph.isPolyTime_arithmeticAmplify
   · exact Graph.isPolyTime_composeSelectedEnumerated
-      (Graph.isPolyTime_ofCompactCNF ((CNF.isPolyTime_to3CNF enc).comp hformula))
+      (Graph.isPolyTime_ofCompactCNF ((CNF.isPolyTime_to3CNF enc).tidy.comp hformula))
   · exact fun x => (Graph.wellFormed_ofCompactCNF (formula x).to3CNF).composeSelectedEnumerated
 
 /-- Every output edge has endpoints in the declared finite vertex range. -/

Complexity/Computability/PCP/Encoded/ThreeSAT.lean

@@ -127,6 +127,7 @@ theorem isPolyTime_ofCNF :
   unfold ofCNF
   fun_prop
 
+attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- The complete construction accepts any variable encoding and charges compact renaming. -/
 @[fun_prop]
 theorem isPolyTime_ofCompactCNF {V Input : Type} [DecidableEq V]