-- Generated by extract_lean.lua from graceful_lean.md
-- Foundation fragment: foundation.lean
-- Do not edit this file by hand.

/-
Lightweight foundations for labelled graphs.

This file intentionally stays close to Lean core.  It gives the blog post a
small vocabulary for graphs, normalized undirected edges, graceful labelings,
and list-based certificates without importing Mathlib.
-/

namespace GracefulLean

notation "ℕ" => Nat

structure Vertex where
  -- This identifies the vertex itself; it is not the graceful label.
  id : ℕ
deriving Repr, DecidableEq

abbrev Label := ℕ

structure Edge where
  a : Vertex
  b : Vertex
deriving Repr, DecidableEq

namespace Edge

def norm (e : Edge) : Edge :=
  if e.a.id <= e.b.id then
    { a := e.a, b := e.b }
  else
    { a := e.b, b := e.a }

def Same (e f : Edge) : Prop :=
  e.norm = f.norm

end Edge

structure Graph where
  vertices : List Vertex
  edges : List Edge
deriving Repr

-- TODO: Consider renaming to avoid confusion with Mathlib
namespace Graph

def edgeCount (G : Graph) : ℕ :=
  G.edges.length

def normalizedEdges (G : Graph) : List Edge :=
  G.edges.map Edge.norm

def hasEdge (G : Graph) (a b : Vertex) : Prop :=
  Exists (fun e : Edge =>
    e ∈ G.edges ∧ Edge.Same e { a := a, b := b })

def edgeWellFormed (G : Graph) (e : Edge) : Prop :=
  e.a ≠ e.b ∧
  e.a ∈ G.vertices ∧
  e.b ∈ G.vertices

def IsLeafAt (G : Graph) (parent leaf : Vertex) : Prop :=
  parent ∈ G.vertices ∧
  leaf ∈ G.vertices ∧
  hasEdge G parent leaf ∧
  ∀ x, hasEdge G leaf x → x = parent

end Graph

def SameMembers (xs ys : List Vertex) : Prop :=
  ∀ x, x ∈ xs ↔ x ∈ ys

def SubsetList (xs ys : List Vertex) : Prop :=
  ∀ x, x ∈ xs → x ∈ ys

end GracefulLean

namespace GracefulLean

open Graph


-- Lean block 1
namespace Graph

def Simple (G : Graph) : Prop :=
  List.Nodup G.vertices ∧
  List.Nodup (normalizedEdges G) ∧
  ∀ e, e ∈ G.edges → edgeWellFormed G e

inductive Walk (G : Graph) : Vertex → Vertex → Prop where
  | stay (v : Vertex) : v ∈ G.vertices → Walk G v v
  | cons {u v w : Vertex} :
      hasEdge G u v → Walk G v w → Walk G u w

def Connected (G : Graph) : Prop :=
  ∀ u, u ∈ G.vertices →
  ∀ v, v ∈ G.vertices →
  Walk G u v

end Graph


-- Lean block 2
namespace Graph

def IsAcyclic (G : Graph) : Prop :=
  edgeCount G + 1 = G.vertices.length

def IsTree (G : Graph) : Prop :=
  Simple G ∧ Connected G ∧ IsAcyclic G

end Graph


-- Lean block 3
namespace Graph

def degree (G : Graph) (v : Vertex) : ℕ :=
  (List.filter (fun e : Edge ↦ decide (e.a = v ∨ e.b = v)) G.edges).length

def IsPathGraph (G : Graph) : Prop :=
  IsTree G ∧
  ∀ v, v ∈ G.vertices → degree G v ≤ 2

end Graph


-- Lean block 4
namespace Graph

-- Evidence that a proposed caterpillar spine walks along edges of `G`.
inductive SpineWalk (G : Graph) : List Vertex → Prop where
  | empty : SpineWalk G []
  | single (v : Vertex) : v ∈ G.vertices → SpineWalk G [v]
  | step {u v : Vertex} {rest : List Vertex} :
      u ∈ G.vertices →
      hasEdge G u v →
      SpineWalk G (v :: rest) →
      SpineWalk G (u :: v :: rest)

def SpinePath (G : Graph) (spine : List Vertex) : Prop :=
  List.Nodup spine ∧
  SpineWalk G spine

end Graph


-- Lean block 5
namespace Graph

def IsCaterpillarGraph (G : Graph) : Prop :=
  IsTree G ∧
  ∃ spine : List Vertex,
    SpinePath G spine ∧
    ∀ v, v ∈ G.vertices →
      v ∈ spine ∨
      ∃ s, s ∈ spine ∧ IsLeafAt G s v

end Graph


-- Lean block 6
-- Avoid a gotcha with ℕ in Lean, where negative numbers get clamped to zero.
def absoluteDifference (a b : Label) : Label :=
  Int.natAbs ((a : Int) - (b : Int))

def VertexLabelsValid (G : Graph) (label : Vertex → Label) : Prop :=
  (∀ v, v ∈ G.vertices → label v ≤ edgeCount G) ∧
  ∀ a b, a ∈ G.vertices → b ∈ G.vertices →
    (label a = label b) → a = b

def EdgeLabelsValid (xs : List Label) (n : ℕ) : Prop :=
  List.Nodup xs ∧
  ∀ k, k ∈ xs ↔ 1 ≤ k ∧ k ≤ n

structure GracefulCertificate (G : Graph) where
  label : Vertex → Label
  simple : Simple G
  vertex_labels : VertexLabelsValid G label
  edge_labels :
    EdgeLabelsValid
      (G.edges.map (fun e ↦ absoluteDifference (label e.a) (label e.b)))
      (edgeCount G)


-- Lean block 7
def IsGraceful (T : Graph) : Prop :=
  Nonempty (GracefulCertificate T)


-- Lean block 8
def extremeSprout (T : Graph) (anchor newLeaf : Vertex) : Graph :=
  { vertices := newLeaf :: T.vertices,
    edges := { a := anchor, b := newLeaf } :: T.edges }


-- Lean block 9
inductive ExtremeSide where
  | zero
  | max

def flipSide : ExtremeSide → ExtremeSide
  | .zero => .max
  | .max => .zero

inductive PathRecipe : Graph → Vertex → ExtremeSide → Type where
  | seed (root : Vertex) :
      PathRecipe { vertices := [root], edges := [] } root .zero
  | sprout {T : Graph} {endpoint : Vertex} {side : ExtremeSide}
      (prev : PathRecipe T endpoint side)
      (newLeaf : Vertex)
      (fresh : newLeaf ∉ T.vertices) :
      PathRecipe
        (extremeSprout T endpoint newLeaf)
        newLeaf
        (flipSide side)


-- Lean block 10
inductive CaterpillarRecipe : ℕ → Graph → Vertex → ExtremeSide → Type where
  | start (root : Vertex) :
      CaterpillarRecipe 0 { vertices := [root], edges := [] } root .zero
  | leg {i : ℕ} {T : Graph} {spine : Vertex} {side : ExtremeSide}
      (prev : CaterpillarRecipe i T spine side)
      (leg : Vertex)
      (fresh : leg ∉ T.vertices) :
      CaterpillarRecipe i
        (extremeSprout T spine leg)
        spine
        side
  | next {i : ℕ} {T : Graph} {spine : Vertex} {side : ExtremeSide}
      (prev : CaterpillarRecipe i T spine side)
      (nextSpine : Vertex)
      (fresh : nextSpine ∉ T.vertices) :
      CaterpillarRecipe (i + 1)
        (extremeSprout T spine nextSpine)
        nextSpine
        (flipSide side)


-- Lean block 11
def PathRecipeTree (T : Graph) : Prop :=
  ∃ endpoint : Vertex, ∃ side : ExtremeSide,
    Nonempty (PathRecipe T endpoint side)

def CaterpillarRecipeTree (T : Graph) : Prop :=
  ∃ i : ℕ, ∃ spine : Vertex, ∃ side : ExtremeSide,
    Nonempty (CaterpillarRecipe i T spine side)

axiom path_graph_has_recipe
    (T : Graph)
    (h_path : IsPathGraph T) :
    PathRecipeTree T

axiom caterpillar_graph_has_recipe
    (T : Graph)
    (h_caterpillar : IsCaterpillarGraph T) :
    CaterpillarRecipeTree T


-- Lean block 12
-- A vertex is attachable when it has a graceful certificate and an extreme label.
structure ExtremeSproutCertificate
    (T : Graph)
    (anchor : Vertex)
    (side : ExtremeSide) where
  cert : GracefulCertificate T
  anchor_belongs_to_tree : anchor ∈ T.vertices
  anchor_zero : side = ExtremeSide.zero → cert.label anchor = 0
  anchor_max : side = ExtremeSide.max → cert.label anchor = edgeCount T

-- The two facts returned by an extreme sprout move.
structure ExtremeSproutResult
    (T : Graph)
    (anchor newLeaf : Vertex)
    (side : ExtremeSide) where
  new_leaf_attachable :
    ExtremeSproutCertificate
      (extremeSprout T anchor newLeaf)
      newLeaf
      (flipSide side)
  old_anchor_attachable :
    ExtremeSproutCertificate
      (extremeSprout T anchor newLeaf)
      anchor
      side

-- The move lemma for adding a fresh leaf at an extreme-labeled vertex.
axiom extreme_sprout_theorem
    {T : Graph}
    {anchor newLeaf : Vertex}
    {side : ExtremeSide}
    (ready : ExtremeSproutCertificate T anchor side)
    (fresh : newLeaf ∉ T.vertices) :
    ExtremeSproutResult T anchor newLeaf side


-- Lean block 13
def seedGraph (v : Vertex) : Graph :=
  { vertices := [v], edges := [] }

-- Base certificate used by every induction proof below.  It proclaims that
-- the one-vertex seed tree is graceful with only one possible labeling.
def seed_is_graceful (v : Vertex) :
    GracefulCertificate (seedGraph v) where
  label := fun _ ↦ 0
  simple := by simp [seedGraph, Simple, normalizedEdges]
  vertex_labels := by simp [seedGraph, VertexLabelsValid, edgeCount]
  edge_labels := by
    simp [seedGraph, EdgeLabelsValid, edgeCount]
    intro k h hk
    simp_all

def seed_ready (v : Vertex) :
    ExtremeSproutCertificate (seedGraph v) v ExtremeSide.zero where
  cert := seed_is_graceful v
  anchor_belongs_to_tree := by simp [seedGraph]
  anchor_zero := by simp [seed_is_graceful]
  anchor_max := by simp


-- Lean block 14
noncomputable def PathRecipe.ready
    {T : Graph}
    {endpoint : Vertex}
    {side : ExtremeSide}
    (proof : PathRecipe T endpoint side) :
    ExtremeSproutCertificate T endpoint side := by
  induction proof with
  | seed root =>
      exact seed_ready root
  | sprout prev newLeaf fresh ih =>
      exact (extreme_sprout_theorem ih fresh).new_leaf_attachable

theorem path_graph_is_graceful
    (T : Graph)
    (h_path : IsPathGraph T) :
    IsGraceful T := by
  rcases path_graph_has_recipe T h_path with ⟨_, _, ⟨recipe⟩⟩
  exact ⟨recipe.ready.cert⟩


-- Lean block 15
noncomputable def CaterpillarRecipe.ready
    {i : ℕ}
    {T : Graph}
    {spine : Vertex}
    {side : ExtremeSide}
    (proof : CaterpillarRecipe i T spine side) :
    ExtremeSproutCertificate T spine side := by
  induction proof with
  | start root =>
      exact seed_ready root
  | leg prev leg fresh ih =>
      exact (extreme_sprout_theorem ih fresh).old_anchor_attachable
  | next prev nextSpine fresh ih =>
      exact (extreme_sprout_theorem ih fresh).new_leaf_attachable

theorem caterpillar_graph_is_graceful
    (T : Graph)
    (h_caterpillar : IsCaterpillarGraph T) :
    IsGraceful T := by
  let recipeTree := caterpillar_graph_has_recipe T h_caterpillar
  rcases recipeTree with ⟨_, _, _, ⟨recipe⟩⟩
  exact ⟨recipe.ready.cert⟩


end GracefulLean