import HardnessReductions.Graph.Encoding
import HardnessReductions.Graph.SubgraphIsomorphism.Encoding
import HardnessReductions.Graph.VertexCover.FromIndepSet.Certified

/-!
# Representation: the bundled graph problems are their concrete encodings

The missing leg of the triangle between the mathematical layer and the
certificate layer. Each concrete problem is *defined* as the pullback of its
bundled problem along `decodeGraph`, so a certified reduction is, on its face,
a statement about decoded instances only; that the concrete problem faithfully
*represents* the bundled one — that no instance is lost, and none invented —
would otherwise be a reading of the decoder, not a theorem. This file makes it
a theorem, once per problem of the domain:

* `encodeGraph` maps a bundled instance to concrete data by numbering its
  vertices (`Fintype.equivFin`), listing its adjacencies as index pairs, and
  passing the threshold through.
* `encodeGraph_adj` is the round trip: the decoded encoding is the original
  graph, up to the vertex bijection `encodeEquiv`. This is exactly the
  adjacency-correspondence hypothesis that each entry's renaming-invariance
  lemma consumes, so every representation pair below is one application of one
  existing lemma.
* `<problem>ToConcrete : P ⟶ᵣ Concrete.P` and `concreteTo<Problem> :
  Concrete.P ⟶ᵣ P` — the two reductions of the representation theorem. The
  decode direction is definitional (`Concrete.P` *is* `P.comap decodeGraph`);
  all content is in the encode direction.

With both directions, a certified reduction between concrete problems induces
the reduction between the bundled problems by composition — see the closing
example, which recovers INDEPENDENT SET → VERTEX COVER through the certified
program. A degenerate decoder could not support this: encode-then-decode must
reproduce every bundled instance up to isomorphism.

## Why `encodeGraph` is noncomputable, and deliberately not a `Code` program

Cost is charged where it belongs: on the concrete side, whose instances are
strings of first-order data. A bundled instance contains an arbitrary
`Fintype`, which is not `Ty`-data, so "encode" is not a computational step of
any reduction pipeline — it is the mathematical statement that the concrete
side speaks about all graphs. `Fintype.equivFin`'s choice of numbering is
noncomputable, and nothing here needs it to be otherwise.
-/

namespace Hardness
namespace Cert

/-! ## The encoding map -/

/-- Encode a bundled graph instance concretely: number the vertices by
`Fintype.equivFin`, list every adjacent pair of numbers as an edge, pass the
threshold through. Vertex labels are irrelevant under the decoding — only the
length of the vertex list matters — so the list is a run of zeros. -/
noncomputable def encodeGraph (x : GraphThresholdInstance) : GraphTy.denote :=
  (List.replicate (Fintype.card x.V) 0,
    ((Finset.univ.filter fun p : x.V × x.V ↦ x.G.Adj p.1 p.2).toList.map
        (fun p ↦ ((Fintype.equivFin x.V p.1 : ℕ), (Fintype.equivFin x.V p.2 : ℕ))),
      x.k))

theorem length_encodeGraph_verts (x : GraphThresholdInstance) :
    (encodeGraph x).1.length = Fintype.card x.V := by
  simp [encodeGraph]

/-- The vertex bijection underlying the encoding: `Fintype.equivFin`'s
numbering, read as positions of the encoded vertex list. -/
noncomputable def encodeEquiv (x : GraphThresholdInstance) :
    x.V ≃ Fin (encodeGraph x).1.length :=
  (Fintype.equivFin x.V).trans (finCongr (length_encodeGraph_verts x).symm)

@[simp] theorem encodeEquiv_val (x : GraphThresholdInstance) (v : x.V) :
    (encodeEquiv x v : ℕ) = (Fintype.equivFin x.V v : ℕ) := rfl

/-- Membership in the encoded edge list: exactly the images of adjacent
pairs. -/
theorem mem_encodeGraph_edges (x : GraphThresholdInstance) (a b : ℕ) :
    (a, b) ∈ (encodeGraph x).2.1 ↔
      ∃ u v : x.V, x.G.Adj u v ∧
        (Fintype.equivFin x.V u : ℕ) = a ∧ (Fintype.equivFin x.V v : ℕ) = b := by
  simp only [encodeGraph, List.mem_map, Finset.mem_toList, Finset.mem_filter,
    Finset.mem_univ, true_and, Prod.mk.injEq, Prod.exists]

/-- **The round trip**: adjacency of the bundled graph is adjacency of the
decoded encoding, across `encodeEquiv`. Together with the definitional
equality of the thresholds, this is the adjacency-correspondence hypothesis
that every renaming-invariance lemma consumes. -/
theorem encodeGraph_adj (x : GraphThresholdInstance) (u v : x.V) :
    x.G.Adj u v ↔
      (decodeGraph (encodeGraph x)).G.Adj (encodeEquiv x u) (encodeEquiv x v) := by
  rw [decodeGraph_adj]
  constructor
  · intro h
    refine ⟨fun hc ↦ h.ne ((encodeEquiv x).injective hc), Or.inl ?_⟩
    exact (mem_encodeGraph_edges x _ _).mpr ⟨u, v, h, rfl, rfl⟩
  · rintro ⟨hne, hor⟩
    rcases hor with hm | hm <;> rw [mem_encodeGraph_edges] at hm <;>
      obtain ⟨u', v', hadj, hu, hv⟩ := hm
    · obtain rfl : u' = u :=
        (Fintype.equivFin x.V).injective (Fin.val_injective hu)
      obtain rfl : v' = v :=
        (Fintype.equivFin x.V).injective (Fin.val_injective hv)
      exact hadj
    · obtain rfl : u' = v :=
        (Fintype.equivFin x.V).injective (Fin.val_injective hu)
      obtain rfl : v' = u :=
        (Fintype.equivFin x.V).injective (Fin.val_injective hv)
      exact hadj.symm

/-! ## The representation pairs

One per catalog entry of the domain. Each encode direction is one application
of the entry's renaming-invariance lemma to the round trip; each decode
direction is definitional, because the concrete problem *is* the comap. -/

/-- CLIQUE is faithfully represented by its concrete encoding. -/
noncomputable def cliqueToConcrete : CLIQUE ⟶ᵣ Concrete.CLIQUE :=
  ⟨encodeGraph, fun x ↦ exists_clique_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete CLIQUE interprets back: definitional. -/
def concreteToClique : Concrete.CLIQUE ⟶ᵣ CLIQUE :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- INDEPENDENT SET is faithfully represented by its concrete encoding. -/
noncomputable def indepSetToConcrete : INDEPENDENT_SET ⟶ᵣ Concrete.INDEPENDENT_SET :=
  ⟨encodeGraph, fun x ↦ exists_indepSet_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete INDEPENDENT SET interprets back: definitional. -/
def concreteToIndepSet : Concrete.INDEPENDENT_SET ⟶ᵣ INDEPENDENT_SET :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- VERTEX COVER is faithfully represented by its concrete encoding. -/
noncomputable def vertexCoverToConcrete : VERTEX_COVER ⟶ᵣ Concrete.VERTEX_COVER :=
  ⟨encodeGraph, fun x ↦ exists_vertexCover_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete VERTEX COVER interprets back: definitional. -/
def concreteToVertexCover : Concrete.VERTEX_COVER ⟶ᵣ VERTEX_COVER :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- Degree-bounded VERTEX COVER is faithfully represented by its concrete
encoding: the restriction's side condition transfers by renaming invariance of
the degree bound, the yes-instance condition by that of the cover. -/
noncomputable def vertexCoverDeg3ToConcrete :
    VERTEX_COVER_DEG3 ⟶ᵣ Concrete.VERTEX_COVER_DEG3 :=
  ⟨encodeGraph, fun x ↦ and_congr
    (forall_degree_le_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) 3)
    (exists_vertexCover_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k)⟩

/-- Concrete degree-bounded VERTEX COVER interprets back: definitional. -/
def concreteToVertexCoverDeg3 : Concrete.VERTEX_COVER_DEG3 ⟶ᵣ VERTEX_COVER_DEG3 :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- DOMINATING SET is faithfully represented by its concrete encoding. -/
noncomputable def dominatingSetToConcrete : DOMINATING_SET ⟶ᵣ Concrete.DOMINATING_SET :=
  ⟨encodeGraph, fun x ↦
    exists_dominatingSet_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete DOMINATING SET interprets back: definitional. -/
def concreteToDominatingSet : Concrete.DOMINATING_SET ⟶ᵣ DOMINATING_SET :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- GRAPH K-COLORABILITY is faithfully represented by its concrete encoding. -/
noncomputable def colorabilityToConcrete : GRAPH_COLORABILITY ⟶ᵣ Concrete.GRAPH_COLORABILITY :=
  ⟨encodeGraph, fun x ↦ colorable_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete K-COLORABILITY interprets back: definitional. -/
def concreteToColorability : Concrete.GRAPH_COLORABILITY ⟶ᵣ GRAPH_COLORABILITY :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- GRAPH 3-COLORABILITY is faithfully represented by its concrete encoding:
the restriction's side condition (`k = 3`) passes through the encoding
definitionally. -/
noncomputable def threeColorToConcrete :
    GRAPH_3_COLORABILITY ⟶ᵣ Concrete.GRAPH_3_COLORABILITY :=
  ⟨encodeGraph, fun x ↦
    and_congr Iff.rfl (colorable_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k)⟩

/-- Concrete 3-COLORABILITY interprets back: definitional. -/
def concreteToThreeColor : Concrete.GRAPH_3_COLORABILITY ⟶ᵣ GRAPH_3_COLORABILITY :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- GRAPH CLIQUE COVER is faithfully represented by its concrete encoding. -/
noncomputable def cliqueCoverToConcrete :
    GRAPH_CLIQUE_COVER ⟶ᵣ Concrete.GRAPH_CLIQUE_COVER :=
  ⟨encodeGraph, fun x ↦ cliqueCoverable_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete CLIQUE COVER interprets back: definitional. -/
def concreteToCliqueCover : Concrete.GRAPH_CLIQUE_COVER ⟶ᵣ GRAPH_CLIQUE_COVER :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-- SIMPLE MAX CUT is faithfully represented by its concrete encoding — through
the *counting* invariance lemma `exists_cut_iff_of_equiv`, where every earlier
entry transported a witness set. -/
noncomputable def simpleMaxCutToConcrete : SIMPLE_MAX_CUT ⟶ᵣ Concrete.SIMPLE_MAX_CUT :=
  ⟨encodeGraph, fun x ↦ exists_cut_iff_of_equiv (encodeEquiv x) (encodeGraph_adj x) x.k⟩

/-- Concrete SIMPLE MAX CUT interprets back: definitional. -/
def concreteToSimpleMaxCut : Concrete.SIMPLE_MAX_CUT ⟶ᵣ SIMPLE_MAX_CUT :=
  ⟨decodeGraph, fun _ ↦ Iff.rfl⟩

/-! ### The thresholdless entry

HAMILTONIAN CIRCUIT states no threshold, so its representation goes through the
same graph encoding with the threshold coordinate carrying junk. Both halves of
that junk-tolerance are theorems here rather than readings of a definition: the
encode direction picks `0` and the round trip does not see it, and the decode
direction forgets whatever the concrete instance happened to carry. -/

/-- Encode a thresholdless instance: the graph encoding at an arbitrary
threshold. -/
noncomputable def encodeGraphInstance (x : GraphInstance) : GraphTy.denote :=
  encodeGraph (x.withThreshold 0)

/-- HAMILTONIAN CIRCUIT is faithfully represented by its concrete encoding. -/
noncomputable def hamiltonianCircuitToConcrete :
    HAMILTONIAN_CIRCUIT ⟶ᵣ Concrete.HAMILTONIAN_CIRCUIT :=
  ⟨encodeGraphInstance, fun x ↦ exists_isHamiltonianCycle_iff_of_equiv
    (encodeEquiv (x.withThreshold 0)) (encodeGraph_adj (x.withThreshold 0))⟩

/-- …and represents it: decoding is the identity on the problem. -/
def concreteToHamiltonianCircuit : Concrete.HAMILTONIAN_CIRCUIT ⟶ᵣ HAMILTONIAN_CIRCUIT :=
  ⟨fun y ↦ (decodeGraph y).forgetThreshold, fun _ ↦ Iff.rfl⟩

/-- HAMILTONIAN PATH is faithfully represented by its concrete encoding — the
same thresholdless passage. -/
noncomputable def hamiltonianPathToConcrete :
    HAMILTONIAN_PATH ⟶ᵣ Concrete.HAMILTONIAN_PATH :=
  ⟨encodeGraphInstance, fun x ↦ exists_isHamiltonian_iff_of_equiv
    (encodeEquiv (x.withThreshold 0)) (encodeGraph_adj (x.withThreshold 0))⟩

/-- …and represents it. -/
def concreteToHamiltonianPath : Concrete.HAMILTONIAN_PATH ⟶ᵣ HAMILTONIAN_PATH :=
  ⟨fun y ↦ (decodeGraph y).forgetThreshold, fun _ ↦ Iff.rfl⟩

/-! ### The two-graph entry

SUBGRAPH ISOMORPHISM poses its question about a pair of graphs, so its
representation is the graph encoding applied twice — each half thresholdless,
as for HAMILTONIAN CIRCUIT — and the entry's invariance lemma consumes one
round trip per graph. -/

/-- Encode a bundled graph-pair instance: each half through the thresholdless
graph encoding. -/
noncomputable def encodeGraphPair (x : GraphPairInstance) : GraphPairTy.denote :=
  (encodeGraphInstance x.host, encodeGraphInstance x.pattern)

/-- SUBGRAPH ISOMORPHISM is faithfully represented by its concrete
encoding. -/
noncomputable def subgraphIsoToConcrete :
    SUBGRAPH_ISOMORPHISM ⟶ᵣ Concrete.SUBGRAPH_ISOMORPHISM :=
  ⟨encodeGraphPair, fun x ↦ exists_injHom_iff_of_equiv
    (encodeEquiv (x.host.withThreshold 0)) (encodeEquiv (x.pattern.withThreshold 0))
    (encodeGraph_adj (x.host.withThreshold 0)) (encodeGraph_adj (x.pattern.withThreshold 0))⟩

/-- Concrete SUBGRAPH ISOMORPHISM interprets back: definitional. -/
def concreteToSubgraphIso : Concrete.SUBGRAPH_ISOMORPHISM ⟶ᵣ SUBGRAPH_ISOMORPHISM :=
  ⟨decodeGraphPair, fun _ ↦ Iff.rfl⟩

/-! ## The loop, closed -/

/-- The payoff of the representation pairs: a certified reduction between
concrete problems induces the reduction between the *bundled* problems, by
composing through the representation. Here the abstract INDEPENDENT SET →
VERTEX COVER reduction is recovered from the certified program `isToVcCode` —
no appeal to the mathematical-layer reduction, only to the certificate. -/
noncomputable example : INDEPENDENT_SET ⟶ᵣ VERTEX_COVER :=
  indepSetToConcrete.comp (isToVcCertified.toReduction.comp concreteToVertexCover)

end Cert
end Hardness