Complexity Theory Definitions and Axioms

Stream: Program verification

[Essam Abadir]

I'm new to Lean and working on a proof that requires the standard foundations. Below are the definitions I'm seeking to port. Any and all help recasting them into more standard or accepted Lean idioms is greatly appreciated.

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.List.Basic
import Mathlib.Data.Set.Defs
/- ComplexityDefs.lean -/
namespace PprobablyEqualsNP.ComplexityDefs
/-!
  Section 1: Foundational Definitions (Complexity, SAT, Entropy)
  This module gathers key abstract types, complexity class definitions, and axioms.
-/

open Classical
-- Core Computational Primitives
axiom Word : Type
instance : Inhabited Word := ⟨sorry⟩

axiom Machine : Type
instance : Inhabited Machine := ⟨sorry⟩

axiom wordLength (w : Word) : Nat
axiom combineInput (input cert : Word) : Word
axiom successWord : Word
axiom compute (m : Machine) (w : Word) : Option Word
axiom timeComplexity (m : Machine) (w : Word) : Nat
-- Polynomial Time Definitions
def PolyTime (f : Nat → Nat) : Prop :=
  ∃ (c k : Nat), ∀ n, f n ≤ c * n^k + c

def RunsInPolyTime (m : Machine) : Prop :=
  ∃ (p : Nat → Nat), PolyTime p ∧ ∀ w, timeComplexity m w ≤ p (wordLength w)
-- Complexity Class Definitions
def Lang : Type := Word → Prop

def P : Set Lang :=
  { L | ∃ (m : Machine), RunsInPolyTime m ∧
         ∀ w, L w ↔ compute m w = some successWord }

def NP : Set Lang :=
  { L | ∃ (m : Machine) (p : Nat → Nat), PolyTime p ∧ RunsInPolyTime m ∧
         ∀ w, L w ↔ ∃ cert, wordLength cert ≤ p (wordLength w) ∧
                        compute m (combineInput w cert) = some successWord }
-- Reducibility Definition
def PolyTimeReducible (L1 L2 : Lang) : Prop :=
  ∃ (f : Word → Word) (m : Machine), RunsInPolyTime m ∧
    (∀ w, compute m w = some (f w)) ∧ (∀ w, L1 w ↔ L2 (f w))

infix:50 " <=p " => PolyTimeReducible

theorem polyTimeReducible_trans {L1 L2 L3 : Lang} :
  (L1 <=p L2) → (L2 <=p L3) → (L1 <=p L3) := by sorry

theorem reduction_in_P {L1 L2 : Lang} : (L1 <=p L2) → L2 ∈ P → L1 ∈ P := by sorry
theorem reducible_in_NP {L1 L2 : Lang} : (L1 <=p L2) → L2 ∈ NP → L1 ∈ NP := by sorry
-- Boolean Circuits and SAT
axiom Circuit : Type
instance : Inhabited Circuit := ⟨sorry⟩

axiom encodeCircuit (c : Circuit) : Word
axiom decodeCircuit (w : Word) : Option Circuit
axiom evalCircuit (c : Circuit) (assignment : Word) : Bool

def SAT_problem : Lang :=
  fun w_c => ∃ (c : Circuit) (assignment : Word),
      decodeCircuit w_c = some c ∧ evalCircuit c assignment = true

def NPComplete (L : Lang) : Prop :=
  L ∈ NP ∧ ∀ L' ∈ NP, L' <=p L

axiom CookLevin_SAT_in_NP : SAT_problem ∈ NP
axiom CookLevin_SAT_is_NP_hard : ∀ (L : Lang), L ∈ NP → L <=p SAT_problem

lemma CookLevin : NPComplete SAT_problem :=
  ⟨CookLevin_SAT_in_NP, CookLevin_SAT_is_NP_hard⟩
-- Information Theory and Physics Definitions
noncomputable def ShannonEntropy (p : List Real) : Real :=
  - (p.map (fun pi => if pi > 0 then pi * (Real.logb 2 pi) else 0)).sum

axiom ShannonEntropyProblem : Lang
axiom ShannonCodingTheorem : ShannonEntropyProblem ∈ P

axiom PhysicalSystemDesc : Type
instance : Inhabited PhysicalSystemDesc := ⟨sorry⟩
axiom decodeDesc (w : Word) : Option PhysicalSystemDesc
axiom IsPhysicalSystem (desc : PhysicalSystemDesc) : Prop
axiom PhysicalSystemProperty (desc : PhysicalSystemDesc) (h_phys : IsPhysicalSystem desc) : Prop

def PhysicalSystemEntropyProblem : Lang :=
  fun w => ∃ (desc : PhysicalSystemDesc) (h : IsPhysicalSystem desc),
             decodeDesc w = some desc ∧ PhysicalSystemProperty desc h

axiom ProgramProblem : Lang
axiom CircuitProblem : Lang
axiom ShannonEntropyProblemToProgram : ShannonEntropyProblem <=p ProgramProblem
axiom ProgramToCircuitProblem : ProgramProblem <=p CircuitProblem
axiom CircuitProblemToSAT : CircuitProblem <=p SAT_problem

axiom P_and_NPComplete_implies_P_eq_NP (L : Lang) :
  L ∈ P → NPComplete L → P = NP

[Mario Carneiro]

There are too many sorries here. More precisely, if you sorry the definitions involved in sorried theorems, it becomes unclear what you are even talking about (and obviously it's not possible to prove the theorem while it has a compromised statement). Here are the definitions I think you should not be sorrying and should just give definitions:

• axiom Word : Type
• axiom ShannonEntropyProblem : Lang
• axiom PhysicalSystemDesc : Type
• axiom IsPhysicalSystem (desc : PhysicalSystemDesc) : Prop
• axiom PhysicalSystemProperty (desc : PhysicalSystemDesc) (h_phys : IsPhysicalSystem desc) : Prop
• axiom ProgramProblem : Lang
• axiom CircuitProblem : Lang

[Mario Carneiro]

If you think the ones about physical systems are unformalizable, then I would challenge whether the poly-time reduction theorem has in fact been proved in the literature. Proving a theorem such as this necessarily entails making formally precise what is meant by the problems involved in the reduction.