diff --git a/Complexity/Computability/Complexity/Classes/Space/TQBF/PolyTime.lean b/Complexity/Computability/Complexity/Classes/Space/TQBF/PolyTime.lean index 407e51d203..1160cfc28c 100644 --- a/Complexity/Computability/Complexity/Classes/Space/TQBF/PolyTime.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Classes/Space/TQBF/Prenex.lean b/Complexity/Computability/Complexity/Classes/Space/TQBF/Prenex.lean index 68ba2a297d..cd0253f468 100644 --- a/Complexity/Computability/Complexity/Classes/Space/TQBF/Prenex.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean b/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean index 7c4b42cf4f..463dcb762a 100644 --- a/Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/CookLevin/Clauses.lean b/Complexity/Computability/Complexity/CookLevin/Clauses.lean index ab4ca61fc0..78c3feea21 100644 --- a/Complexity/Computability/Complexity/CookLevin/Clauses.lean +++ b/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,6 +88,7 @@ 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 : @@ -94,6 +96,7 @@ theorem computableTidilyInPolyTime_sitClauses : (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] : @@ -101,6 +104,7 @@ theorem computableTidilyInPolyTime_uniqueClauses [DecidableEq State] : (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) diff --git a/Complexity/Computability/Complexity/CookLevin/Encoding.lean b/Complexity/Computability/Complexity/CookLevin/Encoding.lean index a1ccfed80f..63e1cbd7e5 100644 --- a/Complexity/Computability/Complexity/CookLevin/Encoding.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/FineGrained/Sparsification.lean b/Complexity/Computability/Complexity/FineGrained/Sparsification.lean index 7e88f141d3..d529574bae 100644 --- a/Complexity/Computability/Complexity/FineGrained/Sparsification.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Problems/CountingSAT.lean b/Complexity/Computability/Complexity/Problems/CountingSAT.lean index fe7afc92b0..1ceef33a6a 100644 --- a/Complexity/Computability/Complexity/Problems/CountingSAT.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Problems/SAT/PolyTime.lean b/Complexity/Computability/Complexity/Problems/SAT/PolyTime.lean index 1930587654..e6fb553f2c 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/PolyTime.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/PolyTime.lean @@ -61,7 +61,7 @@ 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] @@ -69,14 +69,14 @@ theorem computableTidilyInPolyTime_clause_length {α : Type} {input : α ↪ Lis {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. -/ @@ -84,7 +84,7 @@ polynomial-time. -/ 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] diff --git a/Complexity/Computability/Complexity/Problems/ThreeSAT.lean b/Complexity/Computability/Complexity/Problems/ThreeSAT.lean index 5faea60b28..677ba8023a 100644 --- a/Complexity/Computability/Complexity/Problems/ThreeSAT.lean +++ b/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 diff --git a/Complexity/Computability/PCP/Encoded/GapTheorem.lean b/Complexity/Computability/PCP/Encoded/GapTheorem.lean index 00a50e68a3..e034ccc240 100644 --- a/Complexity/Computability/PCP/Encoded/GapTheorem.lean +++ b/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. -/ diff --git a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean index 74a6f97411..fac5fb1cf0 100644 --- a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean +++ b/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] diff --git a/Complexity/Logics/Propositional/CNF/PolyTime.lean b/Complexity/Logics/Propositional/CNF/PolyTime.lean index 232ec76c84..2764a6690a 100644 --- a/Complexity/Logics/Propositional/CNF/PolyTime.lean +++ b/Complexity/Logics/Propositional/CNF/PolyTime.lean @@ -11,7 +11,9 @@ public import Complexity.Logics.Propositional.CNF.Compact public import Complexity.Logics.Propositional.CNF.ExactlyOne public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Polynomial-time CNF construction @@ -27,15 +29,15 @@ needed separately when transferring satisfiability. ## Main results -* `Cslib.Logic.PL.Clause.computableTidilyInPolyTime_impLits`, +* `Cslib.Logic.PL.Clause.computableInPolyTime_impLits`, `.computableTidilyInPolyTime_imp`: implication clauses. -* `Cslib.Logic.PL.Clause.computableTidilyInPolyTime_relabel`, - `Cslib.Logic.PL.CNF.computableTidilyInPolyTime_relabel`: renaming variables. -* `Cslib.Logic.PL.CNF.computableTidilyInPolyTime_exactlyOne`: exactly-one constraints. -* `Cslib.Logic.PL.CNF.computableTidilyInPolyTime_vars`: listing variable occurrences. -* `Cslib.Logic.PL.Clause.computableTidilyInPolyTime_length`, - `Cslib.Logic.PL.CNF.computableTidilyInPolyTime_length`, - `Cslib.Logic.PL.CNF.computableTidilyInPolyTime_vars_length`: clause, formula and +* `Cslib.Logic.PL.Clause.computableInPolyTime_relabel`, + `Cslib.Logic.PL.CNF.computableInPolyTime_relabel`: renaming variables. +* `Cslib.Logic.PL.CNF.computableInPolyTime_exactlyOne`: exactly-one constraints. +* `Cslib.Logic.PL.CNF.computableInPolyTime_vars`: listing variable occurrences. +* `Cslib.Logic.PL.Clause.computableInPolyTime_length`, + `Cslib.Logic.PL.CNF.computableInPolyTime_length`, + `Cslib.Logic.PL.CNF.computableInPolyTime_vars_length`: clause, formula and variable-occurrence counts in unary. * `Cslib.Logic.PL.CNF.isPolyTime_compact`: compact unary indices for arbitrary variable names. @@ -54,78 +56,85 @@ variable {V W : Type} {encV : V ↪ List Bool} {encW : W ↪ List Bool} /-- Negating a literal changes only its polarity. -/ @[fun_prop] -theorem Literal.computableTidilyInPolyTime_negate (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime Std.Sat.Literal.negate +theorem Literal.computableInPolyTime_negate (enc : V ↪ List Bool) : + ComputableInPolyTime Std.Sat.Literal.negate (encPair enc encBool) (encPair enc encBool) := by unfold Std.Sat.Literal.negate fun_prop +attribute [local fun_prop] ComputableInPolyTime.tidy in /-- Construct an implication from literals, with a positive conclusion. -/ @[fun_prop] -theorem Clause.computableTidilyInPolyTime_impLits (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (fun p : List (Literal V) × V => Clause.impLits p.1 p.2) +theorem Clause.computableInPolyTime_impLits (enc : V ↪ List Bool) : + ComputableInPolyTime (fun p : List (Literal V) × V => Clause.impLits p.1 p.2) (encPair (encList (encPair enc encBool)) enc) (encList (encPair enc encBool)) := by + refine .of_tidy ?_ unfold Clause.impLits fun_prop /-- Construct an implication from positive hypotheses and a positive conclusion. -/ @[fun_prop] -theorem Clause.computableTidilyInPolyTime_imp (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (fun p : List V × V => Clause.imp p.1 p.2) +theorem Clause.computableInPolyTime_imp (enc : V ↪ List Bool) : + ComputableInPolyTime (fun p : List V × V => Clause.imp p.1 p.2) (encPair (encList enc) enc) (encList (encPair enc encBool)) := by unfold Clause.imp fun_prop /-- Relabelling a clause is polynomial-time whenever the renaming function is. -/ @[fun_prop] -theorem Clause.computableTidilyInPolyTime_relabel {f : V → W} - (hf : ComputableTidilyInPolyTime f encV encW) : - ComputableTidilyInPolyTime (Clause.relabel f) - (encList (encPair encV encBool)) (encList (encPair encW encBool)) := - map ((hf.comp (fst encV encBool)).prod (snd encV encBool)) +theorem Clause.computableInPolyTime_relabel {f : V → W} + (hf : ComputableInPolyTime f encV encW) : + ComputableInPolyTime (Clause.relabel f) + (encList (encPair encV encBool)) (encList (encPair encW encBool)) := by + have hf := hf.tidy + exact .of_tidy (map ((hf.comp (fst encV encBool)).prod (snd encV encBool))) /-- Relabelling a formula is polynomial-time whenever the renaming function is. -/ @[fun_prop] -theorem CNF.computableTidilyInPolyTime_relabel {f : V → W} - (hf : ComputableTidilyInPolyTime f encV encW) : - ComputableTidilyInPolyTime (CNF.relabel f) +theorem CNF.computableInPolyTime_relabel {f : V → W} + (hf : ComputableInPolyTime f encV encW) : + ComputableInPolyTime (CNF.relabel f) (encList (encList (encPair encV encBool))) - (encList (encList (encPair encW encBool))) := - map (Clause.computableTidilyInPolyTime_relabel hf) + (encList (encList (encPair encW encBool))) := by + have hf := hf.tidy + exact .of_tidy (map (Clause.computableInPolyTime_relabel (.of_tidy hf)).tidy) /-- List the variables of a formula in order, including repetitions. -/ @[fun_prop] -theorem CNF.computableTidilyInPolyTime_vars (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (CNF.vars (V := V)) +theorem CNF.computableInPolyTime_vars (enc : V ↪ List Bool) : + ComputableInPolyTime (CNF.vars (V := V)) (encList (encList (encPair enc encBool))) (encList enc) := - (map (fst enc encBool)).comp (flatten (encPair enc encBool)) + .of_tidy ((map (fst enc encBool)).comp (flatten (encPair enc encBool))) /-- The number of literals in a polynomial-time clause, in unary, is polynomial-time. -/ -theorem Clause.computableTidilyInPolyTime_length {α : Type} {input : α ↪ List Bool} +theorem Clause.computableInPolyTime_length {α : Type} {input : α ↪ List Bool} {c : α → Clause V} - (hc : ComputableTidilyInPolyTime c input (encList (encPair encV encBool))) : - ComputableTidilyInPolyTime (fun a => (c a).length) input encUnary := - (length (encPair encV encBool)).comp hc + (hc : ComputableInPolyTime c input (encList (encPair encV encBool))) : + ComputableInPolyTime (fun a => (c a).length) input encUnary := by + have hc := hc.tidy + exact .of_tidy ((length (encPair encV encBool)).comp hc) /-- The number of clauses in a polynomial-time formula, in unary, is polynomial-time. -/ -theorem CNF.computableTidilyInPolyTime_length {α : Type} {input : α ↪ List Bool} +theorem CNF.computableInPolyTime_length {α : Type} {input : α ↪ List Bool} {φ : α → CNF V} - (hφ : ComputableTidilyInPolyTime φ input (encList (encList (encPair encV encBool)))) : - ComputableTidilyInPolyTime (fun a => (φ a).length) input encUnary := - (length (encList (encPair encV encBool))).comp hφ + (hφ : ComputableInPolyTime φ input (encList (encList (encPair encV encBool)))) : + ComputableInPolyTime (fun a => (φ a).length) input encUnary := by + have hφ := hφ.tidy + exact .of_tidy ((length (encList (encPair encV encBool))).comp hφ) /-- The number of variable occurrences in a polynomial-time formula, in unary, is polynomial-time. -/ -theorem CNF.computableTidilyInPolyTime_vars_length {α : Type} {input : α ↪ List Bool} +theorem CNF.computableInPolyTime_vars_length {α : Type} {input : α ↪ List Bool} {φ : α → CNF V} - (hφ : ComputableTidilyInPolyTime φ input (encList (encList (encPair encV encBool)))) : - ComputableTidilyInPolyTime (fun a => (φ a).vars.length) input encUnary := - (length encV).comp ((CNF.computableTidilyInPolyTime_vars encV).comp hφ) + (hφ : ComputableInPolyTime φ input (encList (encList (encPair encV encBool)))) : + ComputableInPolyTime (fun a => (φ a).vars.length) input encUnary := by + have hφ := hφ.tidy + exact .of_tidy ((length encV).comp ((PL.CNF.computableInPolyTime_vars encV).tidy.comp hφ)) /-- Construct the clause requiring at least one listed variable to hold. -/ @[fun_prop] -theorem CNF.computableTidilyInPolyTime_atLeastOne (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (CNF.atLeastOne (V := V)) +theorem CNF.computableInPolyTime_atLeastOne (enc : V ↪ List Bool) : + ComputableInPolyTime (CNF.atLeastOne (V := V)) (encList enc) (encList (encList (encPair enc encBool))) := by unfold CNF.atLeastOne fun_prop @@ -133,26 +142,29 @@ theorem CNF.computableTidilyInPolyTime_atLeastOne (enc : V ↪ List Bool) : /-- Construct the clauses forbidding two distinct listed variables from both holding. The list may contain repeated variables. -/ @[fun_prop] -theorem CNF.computableTidilyInPolyTime_atMostOne [DecidableEq V] (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (CNF.atMostOne (V := V)) +theorem CNF.computableInPolyTime_atMostOne [DecidableEq V] (enc : V ↪ List Bool) : + ComputableInPolyTime (CNF.atMostOne (V := V)) (encList enc) (encList (encList (encPair enc encBool))) := by + refine .of_tidy ?_ fun_prop [CNF.atMostOne] /-- Construct exactly-one constraints in polynomial time, including for empty or repeated lists. -/ @[fun_prop] -theorem CNF.computableTidilyInPolyTime_exactlyOne [DecidableEq V] (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (CNF.exactlyOne (V := V)) +theorem CNF.computableInPolyTime_exactlyOne [DecidableEq V] (enc : V ↪ List Bool) : + ComputableInPolyTime (CNF.exactlyOne (V := V)) (encList enc) (encList (encList (encPair enc encBool))) := by unfold CNF.exactlyOne fun_prop +attribute [local fun_prop] ComputableInPolyTime.tidy in /-- The entire input-dependent renaming is polynomial-time for any original variable encoding. Its output indices use unary encoding and are bounded by the input's number of occurrences. -/ @[fun_prop] theorem CNF.isPolyTime_compact [DecidableEq V] (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (CNF.compact (V := V)) + ComputableInPolyTime (CNF.compact (V := V)) (encList (encList (encPair enc encBool))) (encList (encList (encPair encUnary encBool))) := by + refine .of_tidy ?_ unfold CNF.compact CNF.relabel Clause.relabel Prod.map fun_prop diff --git a/Complexity/Logics/Propositional/CNF/ThreeCNF/PolyTime.lean b/Complexity/Logics/Propositional/CNF/ThreeCNF/PolyTime.lean index 11c87cff79..19334b9738 100644 --- a/Complexity/Logics/Propositional/CNF/ThreeCNF/PolyTime.lean +++ b/Complexity/Logics/Propositional/CNF/ThreeCNF/PolyTime.lean @@ -10,11 +10,13 @@ module public import Complexity.Logics.Propositional.CNF.ThreeCNF public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Sum +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime import Complexity.Logics.Propositional.CNF.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Sum import Mathlib.Data.List.GetD +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Polynomial-time clause splitting @@ -86,13 +88,18 @@ private theorem splitAux_eq_map (fresh : ℕ → W) (j : ℕ) (carry : Literal W theorem Clause.isPolyTime_splitAux {input : Input ↪ List Bool} {enc : W ↪ List Bool} {fresh : Input → ℕ → W} {index : Input → ℕ} {carry : Input → Literal W} {rest : Input → Clause W} - (hrest : ComputableTidilyInPolyTime rest input (encList (encPair enc encBool))) - (hcarry : ComputableTidilyInPolyTime carry input (encPair enc encBool)) - (hindex : ComputableTidilyInPolyTime index input encUnary) - (hfresh : ComputableTidilyInPolyTime (fun p : Input × ℕ => fresh p.1 p.2) + (hrest : ComputableInPolyTime rest input (encList (encPair enc encBool))) + (hcarry : ComputableInPolyTime carry input (encPair enc encBool)) + (hindex : ComputableInPolyTime index input encUnary) + (hfresh : ComputableInPolyTime (fun p : Input × ℕ => fresh p.1 p.2) (encPair input encUnary) enc) : - ComputableTidilyInPolyTime (fun x => Clause.splitAux (fresh x) (index x) (carry x) (rest x)) + ComputableInPolyTime (fun x => Clause.splitAux (fresh x) (index x) (carry x) (rest x)) input (encList (encList (encPair enc encBool))) := by + have hrest := hrest.tidy + have hcarry := hcarry.tidy + have hindex := hindex.tidy + have hfresh := hfresh.tidy + refine .of_tidy ?_ have hdrop : ComputableTidilyInPolyTime (fun x => (rest x).drop ((rest x).length - 2)) input (encList (encPair enc encBool)) := (dropUnary (encA := encPair enc encBool)).comp (hrest.prod (by fun_prop)) @@ -103,26 +110,43 @@ theorem Clause.isPolyTime_splitAux {input : Input ↪ List Bool} {enc : W ↪ Li @[fun_prop] theorem Clause.isPolyTime_split3 {input : Input ↪ List Bool} {enc : W ↪ List Bool} {fresh : Input → ℕ → W} {index : Input → ℕ} {clause : Input → Clause W} - (hclause : ComputableTidilyInPolyTime clause input (encList (encPair enc encBool))) - (hindex : ComputableTidilyInPolyTime index input encUnary) - (hfresh : ComputableTidilyInPolyTime (fun p : Input × ℕ => fresh p.1 p.2) + (hclause : ComputableInPolyTime clause input (encList (encPair enc encBool))) + (hindex : ComputableInPolyTime index input encUnary) + (hfresh : ComputableInPolyTime (fun p : Input × ℕ => fresh p.1 p.2) (encPair input encUnary) enc) : - ComputableTidilyInPolyTime (fun x => Clause.split3 (fresh x) (index x) (clause x)) + ComputableInPolyTime (fun x => Clause.split3 (fresh x) (index x) (clause x)) input (encList (encList (encPair enc encBool))) := by + have hclause := hclause.tidy + have hindex := hindex.tidy + have hfresh := hfresh.tidy + refine .of_tidy ?_ have heq (f : ℕ → W) (j : ℕ) (c : Clause W) : Clause.split3 f j c = c.head?.elim [[]] (fun carry => Clause.splitAux f j carry c.tail) := by cases c <;> rfl simp_rw [heq] apply optionElimWithInput (encB := encPair enc encBool) (by fun_prop) (by fun_prop) - fun_prop + exact (Clause.isPolyTime_splitAux (input := encPair input (encPair enc encBool)) + (fresh := fun p => fresh p.1) (index := fun p => index p.1) (carry := fun p => p.2) + (rest := fun p => (clause p.1).tail) (.of_tidy (by fun_prop)) (.of_tidy (by fun_prop)) + (.of_tidy (by fun_prop)) (.of_tidy (by fun_prop))).tidy /-- Convert an arbitrary CNF formula to 3CNF, encoding fresh variables by unary clause and chain indices. The certificate includes relabelling, clause traversal, and all output copying. -/ @[fun_prop] theorem CNF.isPolyTime_to3CNF (enc : V ↪ List Bool) : - ComputableTidilyInPolyTime (CNF.to3CNF (V := V)) + ComputableInPolyTime (CNF.to3CNF (V := V)) (encList (encList (encPair enc encBool))) (encList (encList (encPair (encSum enc (encPair encUnary encUnary)) encBool))) := by + refine .of_tidy ?_ + have hsplit : ComputableTidilyInPolyTime + (fun p : CNF V × (Clause V × ℕ) => Clause.split3 (fun j => Sum.inr (p.2.2, j)) 0 + (Clause.relabel Sum.inl p.2.1)) + (encPair (encList (encList (encPair enc encBool))) + (encPair (encList (encPair enc encBool)) encUnary)) + (encList (encList (encPair (encSum enc (encPair encUnary encUnary)) encBool))) := + ComputableInPolyTime.tidy <| Clause.isPolyTime_split3 + ((Clause.computableInPolyTime_relabel (.of_tidy (by fun_prop))).comp + (.of_tidy (by fun_prop))) (.of_tidy (by fun_prop)) (.of_tidy (by fun_prop)) unfold CNF.to3CNF fun_prop diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean index b5f5eda7e7..74bdac9678 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean @@ -11,9 +11,11 @@ public import Complexity.Logics.Propositional.ClauseSet.Sparsification.List public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Bounds public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Sparsification -- the step is polynomial-time @@ -24,15 +26,15 @@ sparseness (`Cslib.Logic.PL.CNF.Sparsification.isSparse`) and normalization formulas, for any encoding of the variables. The width `k` is fixed, so a clause has a constant number of candidate hearts; the thresholds enter only through comparisons `θ j ≤ n`, which must themselves be polynomial-time in unary. They are for the explicit thresholds -(`Cslib.Logic.PL.ClauseSet.Sparsification.computableTidilyInPolyTime_threshold_le`). +(`Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_threshold_le`). ## Main results -* `Cslib.Logic.PL.CNF.Sparsification.computableTidilyInPolyTime_next`: the step. -* `Cslib.Logic.PL.CNF.Sparsification.computableTidilyInPolyTime_isSparse`: the test for +* `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_next`: the step. +* `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparse`: the test for sparseness. -* `Cslib.Logic.PL.CNF.Sparsification.computableTidilyInPolyTime_normalize`: normalization. -* `Cslib.Logic.PL.ClauseSet.Sparsification.computableTidilyInPolyTime_threshold_le`: comparisons +* `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_normalize`: normalization. +* `Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_threshold_le`: comparisons with the explicit thresholds. ## References @@ -48,8 +50,8 @@ open Turing.MultiTapeTM ComputableTidilyInPolyTime namespace Cslib.Logic.PL.ClauseSet.Sparsification /-- Comparing the explicit thresholds with a number is polynomial-time in unary. -/ -theorem computableTidilyInPolyTime_threshold_le (k α : ℕ) : - ComputableTidilyInPolyTime (fun p : ℕ × ℕ => decide (threshold k α p.1 ≤ p.2)) +theorem computableInPolyTime_threshold_le (k α : ℕ) : + ComputableInPolyTime (fun p : ℕ × ℕ => decide (threshold k α p.1 ≤ p.2)) (encPair encUnary encUnary) encBool := by have h : (fun p : ℕ × ℕ => decide (threshold k α p.1 ≤ p.2)) = fun p => if p.1 = 0 then decide (1 ≤ p.2) else decide (α * base k α ^ (2 * p.1 - 1) ≤ p.2) := by @@ -130,20 +132,24 @@ private theorem computableTidilyInPolyTime_choice {θ : ℕ → ℕ} (encL := encList (encPair encUnary encC))).comp hb) (const (0, [])) /-- The list-level test for sparseness is polynomial-time. -/ -theorem computableTidilyInPolyTime_isSparse {θ : ℕ → ℕ} - (hθ : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) +theorem computableInPolyTime_isSparse {θ : ℕ → ℕ} + (hθ : ComputableInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) (encPair encUnary encUnary) encBool) (k : ℕ) : - ComputableTidilyInPolyTime (isSparse (V := V) θ k) encF encBool := by + ComputableInPolyTime (isSparse (V := V) θ k) encF encBool := by + have hθ := hθ.tidy + refine .of_tidy ?_ unfold isSparse exact bool_not.comp (anyWithInput (computableTidilyInPolyTime_candidates encV k) (computableTidilyInPolyTime_heavy encV hθ)) /-- **The list-level step is polynomial-time.** -/ -theorem computableTidilyInPolyTime_next {θ : ℕ → ℕ} - (hθ : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) +theorem computableInPolyTime_next {θ : ℕ → ℕ} + (hθ : ComputableInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) (encPair encUnary encUnary) encBool) (k : ℕ) : - ComputableTidilyInPolyTime (fun p : CNF V × Bool => next θ k p.1 p.2) + ComputableInPolyTime (fun p : CNF V × Bool => next θ k p.1 p.2) (encPair encF encBool) encF := by + have hθ := hθ.tidy + refine .of_tidy ?_ have := computableTidilyInPolyTime_choice encV hθ k have := computableTidilyInPolyTime_reduce encV have := computableTidilyInPolyTime_flower encV @@ -151,8 +157,9 @@ theorem computableTidilyInPolyTime_next {θ : ℕ → ℕ} fun_prop /-- Normalization is polynomial-time. -/ -theorem computableTidilyInPolyTime_normalize : - ComputableTidilyInPolyTime (normalize (V := V)) encF encF := by +theorem computableInPolyTime_normalize : + ComputableInPolyTime (normalize (V := V)) encF encF := by + refine .of_tidy ?_ have := computableTidilyInPolyTime_reduce encV have hdedup : ComputableTidilyInPolyTime (dedup (V := V)) encC encC := by unfold dedup diff --git a/ComplexityTests/Axioms.lean b/ComplexityTests/Axioms.lean index 55cca21d0e..68c1627fb9 100644 --- a/ComplexityTests/Axioms.lean +++ b/ComplexityTests/Axioms.lean @@ -4154,58 +4154,58 @@ info: 'Turing.MultiTapeTM.ComputableTidilyInPolyTime.filter' depends on axioms: #print axioms Turing.MultiTapeTM.ComputableTidilyInPolyTime.filter /-- -info: 'Cslib.Logic.PL.Literal.computableTidilyInPolyTime_negate' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.Literal.computableInPolyTime_negate' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.Literal.computableTidilyInPolyTime_negate +#print axioms Cslib.Logic.PL.Literal.computableInPolyTime_negate /-- -info: 'Cslib.Logic.PL.Clause.computableTidilyInPolyTime_impLits' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.Clause.computableInPolyTime_impLits' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.Clause.computableTidilyInPolyTime_impLits +#print axioms Cslib.Logic.PL.Clause.computableInPolyTime_impLits /-- -info: 'Cslib.Logic.PL.Clause.computableTidilyInPolyTime_imp' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.Clause.computableInPolyTime_imp' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.Clause.computableTidilyInPolyTime_imp +#print axioms Cslib.Logic.PL.Clause.computableInPolyTime_imp /-- -info: 'Cslib.Logic.PL.Clause.computableTidilyInPolyTime_relabel' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.Clause.computableInPolyTime_relabel' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.Clause.computableTidilyInPolyTime_relabel +#print axioms Cslib.Logic.PL.Clause.computableInPolyTime_relabel /-- -info: 'Cslib.Logic.PL.CNF.computableTidilyInPolyTime_relabel' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.CNF.computableInPolyTime_relabel' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.CNF.computableTidilyInPolyTime_relabel +#print axioms Cslib.Logic.PL.CNF.computableInPolyTime_relabel /-- -info: 'Cslib.Logic.PL.CNF.computableTidilyInPolyTime_vars' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.CNF.computableInPolyTime_vars' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.CNF.computableTidilyInPolyTime_vars +#print axioms Cslib.Logic.PL.CNF.computableInPolyTime_vars /-- -info: 'Cslib.Logic.PL.CNF.computableTidilyInPolyTime_atLeastOne' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.CNF.computableInPolyTime_atLeastOne' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.CNF.computableTidilyInPolyTime_atLeastOne +#print axioms Cslib.Logic.PL.CNF.computableInPolyTime_atLeastOne /-- -info: 'Cslib.Logic.PL.CNF.computableTidilyInPolyTime_atMostOne' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.CNF.computableInPolyTime_atMostOne' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.CNF.computableTidilyInPolyTime_atMostOne +#print axioms Cslib.Logic.PL.CNF.computableInPolyTime_atMostOne /-- -info: 'Cslib.Logic.PL.CNF.computableTidilyInPolyTime_exactlyOne' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Cslib.Logic.PL.CNF.computableInPolyTime_exactlyOne' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.CNF.computableTidilyInPolyTime_exactlyOne +#print axioms Cslib.Logic.PL.CNF.computableInPolyTime_exactlyOne /-- info: 'Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_enc_eq' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ComplexityTests/CNFPolyTime.lean b/ComplexityTests/CNFPolyTime.lean index db46388787..b9679c6c1e 100644 --- a/ComplexityTests/CNFPolyTime.lean +++ b/ComplexityTests/CNFPolyTime.lean @@ -21,6 +21,7 @@ namespace ComplexityTests.CNFPolyTime open Cslib.Logic.PL Cslib.Complexity Turing.MultiTapeTM +attribute [local fun_prop] ComputableInPolyTime.tidy in example {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : ComputableTidilyInPolyTime (fun p : List V × V => CNF.exactlyOne p.1 ++ [Clause.imp p.1 p.2]) @@ -30,12 +31,13 @@ example {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : -- Enumeration uses unary indices, while the resulting SAT instance has binary labels. example : ComputableTidilyInPolyTime (fun n => CNF.exactlyOne (List.range n)) encUnary encCNF := by - have h := (CNF.computableTidilyInPolyTime_relabel (f := id) - ComputableTidilyInPolyTime.unary_to_binary).comp - ((CNF.computableTidilyInPolyTime_exactlyOne encUnary).comp + have h := (CNF.computableInPolyTime_relabel (f := id) + (.of_tidy ComputableTidilyInPolyTime.unary_to_binary)).tidy.comp + ((CNF.computableInPolyTime_exactlyOne encUnary).tidy.comp ComputableTidilyInPolyTime.range) simpa only [Function.comp_def, CNF.relabel_id, encCNF] using h +attribute [local fun_prop] ComputableInPolyTime.tidy in -- Computability of relabelling does not require the renaming to be injective. example : ComputableTidilyInPolyTime (CNF.relabel fun _ : ℕ => 0) encCNF encCNF := by fun_prop diff --git a/ComplexityTests/CookLevinPolyTime.lean b/ComplexityTests/CookLevinPolyTime.lean index 0ecb225acd..771e60021d 100644 --- a/ComplexityTests/CookLevinPolyTime.lean +++ b/ComplexityTests/CookLevinPolyTime.lean @@ -59,6 +59,7 @@ example : ComputableTidilyInPolyTime (fun T => (initClauses finish T).relabel Var.index) encUnary encCNF := by fun_prop +attribute [local fun_prop] ComputableInPolyTime.tidy in example : ComputableTidilyInPolyTime (fun n => (oneHotClauses (k := 0) (State := Unit) [] n n n).relabel Var.index) encUnary encCNF := by diff --git a/ComplexityTests/FineGrained/Sparsification.lean b/ComplexityTests/FineGrained/Sparsification.lean index 150efa1127..3a14b6c6f4 100644 --- a/ComplexityTests/FineGrained/Sparsification.lean +++ b/ComplexityTests/FineGrained/Sparsification.lean @@ -127,11 +127,11 @@ info: 'Cslib.Logic.PL.CNF.Sparsification.choice_spec' depends on axioms: #print axioms Cslib.Logic.PL.CNF.Sparsification.choice_spec /-- -info: 'Cslib.Logic.PL.CNF.Sparsification.computableTidilyInPolyTime_next' depends on axioms: +info: 'Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_next' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in -#print axioms Cslib.Logic.PL.CNF.Sparsification.computableTidilyInPolyTime_next +#print axioms Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_next /-- info: 'Cslib.Complexity.Sparsify.search_eq_true_iff' depends on axioms: diff --git a/ComplexityTests/ThreeCNFPolyTime.lean b/ComplexityTests/ThreeCNFPolyTime.lean index 06ad31b03b..a4c72f04aa 100644 --- a/ComplexityTests/ThreeCNFPolyTime.lean +++ b/ComplexityTests/ThreeCNFPolyTime.lean @@ -23,33 +23,33 @@ example : Clause.split3 (fun i : ℕ => i + 100) 7 [(0, true), (1, false), (2, true), (3, false)] = [[(0, true), (1, false), (107, true)], [(107, false), (2, true), (3, false)]] := rfl -example : ComputableTidilyInPolyTime +example : ComputableInPolyTime (fun p : ℕ × Clause ℕ => Clause.split3 (fun i => p.1 + i) p.1 p.2) (encPair encUnary (encList (encPair encUnary encBool))) - (encList (encList (encPair encUnary encBool))) := by polytime + (encList (encList (encPair encUnary encBool))) := by fun_prop -- Binary original names coexist with unary fresh clause and chain indices. -example : ComputableTidilyInPolyTime (CNF.to3CNF (V := ℕ)) +example : ComputableInPolyTime (CNF.to3CNF (V := ℕ)) (encList (encList (encPair encNat encBool))) (encList (encList (encPair (encSum encNat (encPair encUnary encUnary)) encBool))) := by fun_prop -- No inhabitant of the original variable type is required. -example (empty : Empty ↪ List Bool) : ComputableTidilyInPolyTime (CNF.to3CNF (V := Empty)) +example (empty : Empty ↪ List Bool) : ComputableInPolyTime (CNF.to3CNF (V := Empty)) (encList (encList (encPair empty encBool))) (encList (encList (encPair (encSum empty (encPair encUnary encUnary)) encBool))) := by - polytime + fun_prop section Captured variable {W Input : Type} (input : Input ↪ List Bool) (enc : W ↪ List Bool) (fresh : Input → ℕ → W) (index : Input → ℕ) (clause : Input → Clause W) - (hclause : ComputableTidilyInPolyTime clause input (encList (encPair enc encBool))) - (hindex : ComputableTidilyInPolyTime index input encUnary) - (hfresh : ComputableTidilyInPolyTime (fun p : Input × ℕ => fresh p.1 p.2) + (hclause : ComputableInPolyTime clause input (encList (encPair enc encBool))) + (hindex : ComputableInPolyTime index input encUnary) + (hfresh : ComputableInPolyTime (fun p : Input × ℕ => fresh p.1 p.2) (encPair input encUnary) enc) -example : ComputableTidilyInPolyTime +example : ComputableInPolyTime (fun x => Clause.split3 (fresh x) (index x) (clause x)) input (encList (encList (encPair enc encBool))) := by fail_if_success (clear hclause; fun_prop) @@ -57,20 +57,20 @@ example : ComputableTidilyInPolyTime fail_if_success (clear hfresh; fun_prop) fun_prop -example : ComputableTidilyInPolyTime +example : ComputableInPolyTime (fun x => let c := clause x; let start := index x; Clause.split3 (fresh x) start (c ++ c)) - input (encList (encList (encPair enc encBool))) := by polytime + input (encList (encList (encPair enc encBool))) := by fun_prop end Captured example {V Input : Type} (enc : V ↪ List Bool) (input : Input ↪ List Bool) (formula : Input → CNF V) - (hformula : ComputableTidilyInPolyTime formula input + (hformula : ComputableInPolyTime formula input (encList (encList (encPair enc encBool)))) : - ComputableTidilyInPolyTime (fun x => let φ := formula x; φ.to3CNF) + ComputableInPolyTime (fun x => let φ := formula x; φ.to3CNF) input (encList (encList (encPair (encSum enc (encPair encUnary encUnary)) encBool))) := by fail_if_success (clear hformula; fun_prop) - polytime + fun_prop example (φ : CNF ℕ) : φ.to3CNF.Satisfiable ↔ φ.Satisfiable := CNF.satisfiable_to3CNF φ diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 92b904a0a7..1049fe2f61 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -421,8 +421,5 @@ "Complexity/Crypto/Computational/Stretch.lean": 8, "Complexity/Crypto/Computational/Stretch/Quantitative.lean": 9, "Complexity/Crypto/Computational/UniformChoice.lean": 2, - "Complexity/Logics/Propositional/CNF/PolyTime.lean": 13, - "Complexity/Logics/Propositional/CNF/ThreeCNF/PolyTime.lean": 3, - "Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean": 4, "Complexity/Tactic/PolyTime.lean": 3 }