import Mathlib.Combinatorics.SimpleGraph.Basic
import HardnessReductions.Core
import HardnessReductions.Graph.Defs

/-!
# SUBGRAPH ISOMORPHISM

Does the host graph `G` contain a subgraph isomorphic to the pattern graph
`H`? Garey–Johnson phrase the question as a choice of `V ⊆ V₁` and `E ⊆ E₁`
with `|V| = |V₂|`, `|E| = |E₂|` and a one-to-one `f : V₂ → V` matching the two
edge sets; choosing `E` to be the image of `E₂` shows that this is exactly an
*injective homomorphism* `H → G`, which is the form stated here. The subgraph
is not required to be induced: `f` must carry edges of `H` to edges of `G`, but
may carry non-edges anywhere.

Hardness proof (in `SubgraphIsomorphism/`): from CLIQUE
(`FromClique.lean`, the pattern is a complete graph; certified in
`FromClique/Certified.lean`).
-/

namespace Hardness

/-- SUBGRAPH ISOMORPHISM: does the host graph contain a (not necessarily
induced) subgraph isomorphic to the pattern graph — equivalently, is there an
injective homomorphism from the pattern to the host? -/
def SUBGRAPH_ISOMORPHISM : Problem GraphPairInstance :=
  fun x ↦ ∃ f : x.pattern.V → x.host.V, Function.Injective f ∧
    ∀ u v : x.pattern.V, x.pattern.G.Adj u v → x.host.G.Adj (f u) (f v)

/-- Existence of an injective homomorphism transfers across bijections that
match the two adjacency relations — one bijection per graph, since the question
names two of them. -/
theorem exists_injHom_iff_of_equiv {V W V' W' : Type*} {G : SimpleGraph V}
    {H : SimpleGraph W} {G' : SimpleGraph V'} {H' : SimpleGraph W'}
    (e : V ≃ V') (d : W ≃ W')
    (hG : ∀ a b : V, G.Adj a b ↔ G'.Adj (e a) (e b))
    (hH : ∀ a b : W, H.Adj a b ↔ H'.Adj (d a) (d b)) :
    (∃ f : W → V, Function.Injective f ∧ ∀ u v : W, H.Adj u v → G.Adj (f u) (f v)) ↔
      ∃ f : W' → V', Function.Injective f ∧
        ∀ u v : W', H'.Adj u v → G'.Adj (f u) (f v) := by
  constructor
  · rintro ⟨f, hinj, hf⟩
    refine ⟨fun w ↦ e (f (d.symm w)), fun a b hab ↦ ?_, fun u v huv ↦ ?_⟩
    · exact d.symm.injective (hinj (e.injective hab))
    · exact (hG _ _).mp (hf _ _ ((hH _ _).mpr (by rwa [d.apply_symm_apply, d.apply_symm_apply])))
  · rintro ⟨f, hinj, hf⟩
    refine ⟨fun w ↦ e.symm (f (d w)), fun a b hab ↦ ?_, fun u v huv ↦ ?_⟩
    · exact d.injective (hinj (e.symm.injective hab))
    · rw [hG]
      simp only [Equiv.apply_symm_apply]
      exact hf _ _ ((hH _ _).mp huv)

end Hardness