refactor(Complexity/Problems): migrate cycles, games, and drawings to structures (#4385)

CslibFrontier/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean

@@ -386,8 +386,8 @@ with `B` arcs and `n` declared vertex entries, replay `n + 1` blocks of `2 * B`
 from the start vertex, the first player to move; the existential player wins when the first player
 does. -/
 def verifier (x : GeneralizedGeographyInstance × List Bool) : Bool :=
-  ((blocks x.1.graph.2.length (x.1.graph.1.length + 1) x.2).foldl
-    (step x.1.graph x.1.graph.2.length) (none, true, [x.1.start], x.1.start)).1.getD false
+  ((blocks x.1.graph.edges.length (x.1.graph.vertices.length + 1) x.2).foldl
+    (step x.1.graph x.1.graph.edges.length) (none, true, [x.1.start], x.1.start)).1.getD false
 
 /-- The arcs and the declared vertex entries of a graph are no more than the length of the encoded
 instance. -/
@@ -536,18 +536,18 @@ theorem computableInPolyTime_verifier :
       (fun x : GeneralizedGeographyInstance × List Bool => x.1.graph) encInput encGraph := by
     fun_prop
   have hB : ComputableInPolyTime
-      (fun x : GeneralizedGeographyInstance × List Bool => x.1.graph.2.length) encInput
-      encUnary := (length_list _).comp ((snd _ _).comp hG)
+      (fun x : GeneralizedGeographyInstance × List Bool => x.1.graph.edges.length) encInput
+      encUnary := (length_list _).comp (encGraph_edges_polyTime hG)
   have hR : ComputableInPolyTime
-      (fun x : GeneralizedGeographyInstance × List Bool => x.1.graph.1.length + 1)
+      (fun x : GeneralizedGeographyInstance × List Bool => x.1.graph.vertices.length + 1)
       encInput encUnary :=
-    unary_add.comp (((length_list _).comp ((fst _ _).comp hG)).prod (const 1))
+    unary_add.comp (((length_list _).comp (encGraph_vertices_polyTime hG)).prod (const 1))
   have hblocks : ComputableInPolyTime
       (fun x : GeneralizedGeographyInstance × List Bool =>
-        blocks x.1.graph.2.length (x.1.graph.1.length + 1) x.2)
+        blocks x.1.graph.edges.length (x.1.graph.vertices.length + 1) x.2)
       encInput (encList encBits) := by
     have h2B : ComputableInPolyTime
-        (fun p : (GeneralizedGeographyInstance × List Bool) × ℕ => 2 * p.1.1.graph.2.length)
+        (fun p : (GeneralizedGeographyInstance × List Bool) × ℕ => 2 * p.1.1.graph.edges.length)
         (encPair encInput encUnary) encUnary :=
       unary_mul.comp ((const 2).prod (hB.comp (fst _ _)))
     unfold blocks
@@ -560,7 +560,7 @@ theorem computableInPolyTime_verifier :
     fun_prop
   have hstep : ComputableInPolyTime
       (fun p : (((GeneralizedGeographyInstance × List Bool) × Play) × List Bool) =>
-        step p.1.1.1.graph p.1.1.1.graph.2.length p.1.2 p.2)
+        step p.1.1.1.graph p.1.1.1.graph.edges.length p.1.2 p.2)
       encStep encPlay := by
     have hst : ComputableInPolyTime
         (fun p : (((GeneralizedGeographyInstance × List Bool) × Play) × List Bool) => p.1.2)
@@ -570,19 +570,19 @@ theorem computableInPolyTime_verifier :
         encStep encInput := by fun_prop
     have hbits : ComputableInPolyTime
         (fun p : (((GeneralizedGeographyInstance × List Bool) × Play) × List Bool) =>
-          moverBits p.1.1.1.graph.2.length p.1.2.2.1 p.2)
+          moverBits p.1.1.1.graph.edges.length p.1.2.2.1 p.2)
         encStep (encList encBool) :=
       computableInPolyTime_moverBits (hB.comp hX) (by fun_prop) (snd _ _)
     have hpair : ComputableInPolyTime
         (fun p : (((GeneralizedGeographyInstance × List Bool) × Play) × List Bool) =>
-          ((p.1.1.1.graph, p.1.2), moverBits p.1.1.1.graph.2.length p.1.2.2.1 p.2))
+          ((p.1.1.1.graph, p.1.2), moverBits p.1.1.1.graph.edges.length p.1.2.2.1 p.2))
         encStep
         (encPair (encPair encGraph encPlay) (encList encBool)) :=
       ((hG.comp hX).prod hst).prod hbits
     have hnext : ComputableInPolyTime
         (fun p : (((GeneralizedGeographyInstance × List Bool) × Play) × List Bool) =>
           next p.1.1.1.graph p.1.2.2.1 p.1.2.2.2.1 p.1.2.2.2.2
-            (moverBits p.1.1.1.graph.2.length p.1.2.2.1 p.2))
+            (moverBits p.1.1.1.graph.edges.length p.1.2.2.1 p.2))
         encStep encPlay := by
       have h := computableInPolyTime_next.comp hpair
       simp only [Function.comp_def] at h
@@ -595,7 +595,7 @@ theorem computableInPolyTime_verifier :
     exact ite' hsome hst hnext
   have hfold := foldlWithInput_of_bounded_growth (encA := encBits) (encL := encList encBits)
     (step := fun x : GeneralizedGeographyInstance × List Bool =>
-      step x.1.graph x.1.graph.2.length)
+      step x.1.graph x.1.graph.edges.length)
     hinit ⟨hblocks, hstep, inferInstance, inferInstance⟩
     (growth := fun x => 5 * (encInput x).length + 4)
     ⟨((PolyBounded.const 5).mul .self).add (.const 4),

CslibFrontier/Computability/Complexity/Problems/FeedbackArcSet.lean

@@ -87,7 +87,7 @@ structure FeedbackArcSetInstance where
   graph : Graph
   /-- The maximum number of arcs to remove. -/
   bound : ℕ
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Encoding of `FeedbackArcSetInstance` as a pair `(graph, bound)`. -/
 enc_structure encFeedbackArcSet : FeedbackArcSetInstance where

CslibFrontier/Computability/Complexity/Problems/FeedbackVertexSet.lean

@@ -81,7 +81,7 @@ structure FeedbackVertexSetInstance where
   graph : Graph
   /-- The maximum number of vertices to remove. -/
   bound : ℕ
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Encoding of `FeedbackVertexSetInstance` as a pair `(graph, bound)`. -/
 enc_structure encFeedbackVertexSet : FeedbackVertexSetInstance where

CslibFrontier/Computability/Complexity/Problems/GeneralizedGeography.lean

@@ -130,7 +130,7 @@ structure GeneralizedGeographyInstance where
   graph : Graph
   /-- The starting vertex of the token. -/
   start : ℕ
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Encoding of `GeneralizedGeographyInstance` as a pair `(graph, start)`. -/
 enc_structure encGeneralizedGeography : GeneralizedGeographyInstance where

CslibFrontier/Computability/Complexity/Problems/GraphIsomorphism.lean

@@ -95,7 +95,7 @@ structure GraphIsomorphismInstance where
   first : Graph
   /-- The second graph in the pair. -/
   second : Graph
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Encoding of `GraphIsomorphismInstance` as a pair `(first, second)`. -/
 enc_structure encGraphIsomorphism : GraphIsomorphismInstance where

CslibFrontier/Computability/Complexity/Problems/LongPath.lean

@@ -77,7 +77,7 @@ structure LongPathInstance where
   graph : Graph
   /-- The target number of vertices on the path. -/
   target : ℕ
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Encoding of `LongPathInstance` as `(graph, target)` with `target` in binary. -/
 enc_structure encLongPath : LongPathInstance where

CslibFrontier/Computability/Complexity/Problems/PlanarPositiveOneInThreeSAT.lean

@@ -75,13 +75,17 @@ paired with a finite integer orthogonal drawing of its incidence graph. -/
   formula : CNF ℕ
   /-- The supplied integer orthogonal incidence drawing. -/
   drawing : Graph.OrthogonalDrawing
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Binary encoding of a CNF formula and its supplied orthogonal incidence drawing. -/
 enc_structure encDrawnPlanarPositiveOneInExactThreeSATThree :
     DrawnPlanarPositiveOneInExactThreeSATThreeInstance where
   formula : encCNF, drawing : Graph.encOrthogonalDrawing
 
+attribute [fun_prop] encDrawnPlanarPositiveOneInExactThreeSATThree_formula_polyTime
+  encDrawnPlanarPositiveOneInExactThreeSATThree_drawing_polyTime
+  encDrawnPlanarPositiveOneInExactThreeSATThree_mk_polyTime
+
 /-- Positive exact-three, occurrence-three exact-one formulas with an integer orthogonal
 incidence drawing whose full real segments meet only at common incident endpoints. -/
 @[expose] def PlanarPositiveOneInExactThreeSATThree : Set (CNF ℕ) :=

CslibFrontier/Computability/Complexity/Problems/PlanarThreeSATThree.lean

@@ -84,12 +84,15 @@ orthogonal drawing of its incidence graph. -/
   formula : CNF ℕ
   /-- The supplied integer orthogonal incidence drawing. -/
   drawing : Graph.OrthogonalDrawing
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Inhabited
 
 /-- Binary encoding of a CNF formula and its supplied orthogonal incidence drawing. -/
 enc_structure encDrawnPlanarThreeSATThree : DrawnPlanarThreeSATThreeInstance where
   formula : encCNF, drawing : Graph.encOrthogonalDrawing
 
+attribute [fun_prop] encDrawnPlanarThreeSATThree_formula_polyTime
+  encDrawnPlanarThreeSATThree_drawing_polyTime encDrawnPlanarThreeSATThree_mk_polyTime
+
 /-- Satisfiable width-three, occurrence-three formulas whose actual incidence graph admits an
 integer orthogonal drawing with continuous endpoint-only contacts. -/
 @[expose] def PlanarThreeSATThree : Set (CNF ℕ) :=

CslibFrontierTests/FeedbackArcSet.lean

@@ -49,6 +49,7 @@ example : ComputableInPolyTime (fun p : Graph × ℕ => (⟨p.1, p.2⟩ : Feedba
     (encPair encGraph encNat) encFeedbackArcSet := by
   fun_prop
 
+example : (default : FeedbackArcSetInstance) = ⟨default, default⟩ := rfl
 
 /-! ### Feedback arc sets -/
 

CslibFrontierTests/FeedbackVertexSet.lean

@@ -48,6 +48,7 @@ example : ComputableInPolyTime (fun p : Graph × ℕ => (⟨p.1, p.2⟩ : Feedba
     (encPair encGraph encNat) encFeedbackVertexSet := by
   fun_prop
 
+example : (default : FeedbackVertexSetInstance) = ⟨default, default⟩ := rfl
 
 /-! ### Directed cycles -/
 

CslibFrontierTests/GapGraphsGeography.lean

@@ -172,4 +172,6 @@ example : ComputableInPolyTime
     (encPair encGraph encNat) encGeneralizedGeography := by
   fun_prop
 
+example : (default : GeneralizedGeographyInstance) = ⟨default, default⟩ := rfl
+
 end CslibFrontierTests.GapGraphsGeography

CslibFrontierTests/InteractiveProofs.lean

@@ -65,6 +65,8 @@ example :
       (encPair encGraph encGraph) encGraphIsomorphism := by
   fun_prop
 
+example : (default : GraphIsomorphismInstance) = ⟨default, default⟩ := rfl
+
 -- The certificate decoding `[7, 5, 9]` (positions `0, 1, 2` of
 -- `path'.vertices = [7, 5, 9, 5]` in unary
 -- blocks of width `4`) maps positions `0, 1, 2` of `path` to `7, 5, 9` and is accepted.

CslibFrontierTests/LongPathHardness.lean

@@ -52,6 +52,8 @@ example {x y : LongPathInstance} (hG : x.graph = y.graph) (hk : x.target = y.tar
     x = y :=
   LongPathInstance.ext hG hk
 
+example : (default : LongPathInstance) = ⟨default, default⟩ := rfl
+
 /-- `encLongPath` exposes polynomial-time projections and constructor to `fun_prop`. -/
 example : ComputableInPolyTime LongPathInstance.graph encLongPath encGraph := by fun_prop
 

CslibFrontierTests/PlanarPositiveOneInThreeSAT.lean

@@ -97,4 +97,6 @@ example : Turing.MultiTapeTM.ComputableInPolyTime
     encDrawnPlanarPositiveOneInExactThreeSATThree := by
   fun_prop
 
+example : (default : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) = ⟨default, default⟩ := rfl
+
 end CslibFrontierTests.PlanarPositiveOneInThreeSAT

CslibFrontierTests/PlanarThreeSATThree.lean

@@ -89,6 +89,8 @@ example : Turing.MultiTapeTM.ComputableInPolyTime
     encDrawnPlanarThreeSATThree := by
   fun_prop
 
+example : (default : DrawnPlanarThreeSATThreeInstance) = ⟨default, default⟩ := rfl
+
 -- The paired-port variable and placed-clause encodings are computable via `FinEnum`.
 example : SAT.ParsimoniousPlanar.encVariable ((0, 0), .inl (0, 0)) ≠
     SAT.ParsimoniousPlanar.encVariable ((0, 0), .inr .center) := by decide +kernel