Graceful Lean

In the previous post, Graceful Graph Moves, I described constructive proof moves for graceful trees.

This post makes a small start at formalizing the proofs for paths and caterpillars; it also gave me an excuse to learn Lean. It is an exercise in literate programming; I wrote it primarily to teach myself, but maybe other folks who are learning Lean will find it useful.

Graphs & Trees

First some foundational stuff to support simple labeled graphs:

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

abbrev Label := ℕ

The keyword deriving asks Lean to generate boilerplate code: Repr gives Lean a way to print values for debugging, and DecidableEq gives Lean a computed equality test.

On the way to defining the notion of a tree, let’s spell out three graph predicates:

• Simple rules out duplicate vertices (i.e., “no dup”), duplicate undirected edges, loops, and malformed edges.
• Walk is reachability evidence: either a vertex reaches itself, or one edge plus a shorter walk gives a longer walk.
• Connected says every listed vertex can reach every other listed vertex.

All three are propositions (Prop): something that can be true or false, but not data to perform computation with.

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

I’ve omitted definitions for small helpers like hasEdge, but the complete Lean code can be downloaded at the end of the post.

The type Walk takes a graph and two vertices. Walk G u v means “there is a walk in graph G from vertex u to vertex v.”

An inductive declaration defines a type by listing its constructors. Each branch is a named constructor. Here the constructor names we’ve chosen are stay and cons.

After the constructor name come the inputs needed to build that case. Named inputs look like (v : Vertex). Unnamed inputs can be written with arrows. For example:

• Walk.stay says: choose a vertex v, provide evidence that v ∈ G.vertices, and you get evidence of Walk G v v.
• Walk.cons says: provide an edge from u to v and a walk from v to w, and you get a walk from u to w.

One tree condition we haven’t tackled yet is acyclicity. In this finite connected-simple setting, we can use an edge-count trick: a connected simple graph is acyclic exactly when it has one fewer edge than vertex.

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

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

Now we can go over the two graph families of interest: paths and caterpillars. Both of them are, of course, trees.

A finite tree is a path exactly when every vertex has degree at most two. In Lean, the definition is a conjunction: IsTree G supplies the tree condition, and the ∀ v line says “for every vertex v in the graph, the degree of v is at most two.”

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

A caterpillar is a tree with a central spine. Every vertex is either on that spine or is a leaf attached to it.

The SpineWalk helper says that the listed spine vertices form a walk through edges of G. A SpinePath is the stricter version we want here: it is a spine walk with no repeated vertices.

-- 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

The double-colon operators build a list by adding an element to the front. The expression u :: v :: rest is parsed as u :: (v :: rest), so the step constructor says: if u is connected to v, and the list starting at v is already a spine walk, then the longer list starting with u, v is also a spine walk.

Now we can define the actual predicate for caterpillars:

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

In plain English, this means that a graph is a caterpillar if it’s a tree and if you can call some list-of-vertices a “spine” such that:

• the spine is a path through G (it walks through graph edges without crossing itself), and
• for every vertex v in the graph, v is either a member of the spine, or a leaf attached to the spine.

Proof Targets

Recall from my earlier post that a graceful labeling for a simple graph with $q$ edges assigns a natural number to every vertex so that:

• each label is between $0$ and $q$,
• no two vertices receive the same label, and
• the edge differences are exactly $1,2,\ldots,q$, with no repeats.

Let’s define a certificate for gracefulness: a package containing an actual candidate labeling plus proof that the labeling is valid.

-- 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)

Read the fields of GracefulCertificate as the graceful-labeling checklist:

• label is the actual proposed labeling function, assigning a natural-number label to every vertex.
• simple proves that G has no duplicate vertices, duplicate undirected edges, loops, or malformed edges.
• vertex_labels proves that every vertex label lies between 0 and the number of edges, and no two listed vertices receive the same label. The lower bound is automatic because labels are natural numbers.
• edge_labels proves the induced edge-label condition: if computed via differences, then they have no duplicates and they cover the expected numeric range.

GracefulCertificate T is a data-carrying type. A value of this type supplies a specific labeling function label : Vertex → Label, together with proof that this labeling satisfies the graceful-labeling rules. It does not merely say that a valid labeling could exist; it contains one.

The next definition deliberately forgets the concrete data and keeps only the existence guarantee. IsGraceful T is a proposition saying that the certificate type is inhabited.

def IsGraceful (T : Graph) : Prop :=
  Nonempty (GracefulCertificate T)

Nonempty is Lean’s standard proposition for saying that a type has at least one value. So Nonempty (GracefulCertificate T) reads as: the type of graceful certificates for T has some member.

In other words,

• GracefulCertificate G means: “here is one labeling of G and proof that it is graceful.”
• IsGraceful G means: “there exists some graceful labeling of G.”

If we claim “all caterpillars are graceful”, we mean that every caterpillar has at least one graceful labeling.

Next let’s make the actual conjectures that we wish to prove:

theorem path_graph_is_graceful
    (T : Graph)
    (h_path : IsPathGraph T) :
    IsGraceful T := by
  sorry

theorem caterpillar_graph_is_graceful
    (T : Graph)
    (h_caterpillar : IsCaterpillarGraph T) :
    IsGraceful T := by
  sorry

In Lean, a named hypothesis such as h_path is evidence that the arbitrary graph belongs to the corresponding family. The sorry is a commonly used placeholder for the actual proof. From here on, the post is devoted to what it would take to replace those sorry lines.

Here’s what’s cool about Lean: if the statements above have been formalized correctly, and every sorry or provisional axiom is eventually replaced by proof code that Lean accepts, then you can be confident in your proof story, no matter how complicated it is.

Construction Recipes

The proofs covered in my previous post are inductive. They start from a small fixed seed and apply a number of graph moves. To formalize that style of argument, we introduce construction recipes: inductive requirements that say how a particular tree was built.

The upcoming recipes are very different from the above tree-family predicates. The predicate IsPathGraph says what T looks like, whereas a value of PathRecipe says how T can be constructed, and it remembers attachment points that could be used by a subsequent move. That extra information is what will make our final gracefulness proof possible: Lean can recurse over the recipe, one constructor at a time, and apply the matching move theorem at each step.

The path and caterpillar recipes both use The Extreme Sprout so let’s go ahead and formalize it. The extremeSprout function takes a graph and two vertices (attachment + leaf) and produces a new graph.

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

Next let’s define the path construction recipe that uses the above move. This simply formalizes what was described in my previous post:

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)

The above inductive has two constructors. The seed constructor builds the one-vertex path. The sprout constructor takes a previous path recipe, attaches a fresh leaf at the current endpoint, and records the new leaf as the new endpoint on the flipped extreme side.

Next, let’s cover caterpillar construction:

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)

The caterpillar recipe follows the same idea as the path recipe, but the current attachment point is a spine vertex. A leg step attaches a leaf while staying at the same spine vertex. A next step attaches the next spine vertex and flips the extreme side for the next round.

The two bridge axioms below are the recognition step: they say that a graph in the path or caterpillar family has a matching construction recipe.

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

Proof: Paths are graceful.

The move lemma says exactly what evidence a move needs and exactly what evidence it gives back. Here the reusable state is ExtremeSproutCertificate: a graceful certificate, proof that the attachment vertex is present, and proof that its label is at the requested extreme.

The lemma says that if an anchor is ready and the new vertex is fresh, then the sprouted graph has both of the continuation states that the recipes need: the new leaf is ready on the flipped side, and the old anchor is still ready on the same side. The result structure gives names to those two pieces of evidence.

We’re cheating a bit here by making it an axiom, which lets us avoid proving it formally in Lean. However this is a lemma from my previous post that is surely obvious and non-controversial.

-- 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

The Seed Tree

The one-vertex tree is the seed for most of the inductive proofs that we’ll be covering.

The proof below first names the one-vertex, zero-edge graph, then uses record literals. Each field says which small fact Lean needs, and the short by blocks discharge those facts for the seed graph.

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

The proof is short because the seed tree has only one vertex and no edges. Expanding Simple, VertexLabelsValid, and EdgeLabelsValid leaves only list facts about [v] and [], plus the impossible edge-label case 1 ≤ 0. The seed_ready helper adds the fact that this lone vertex is ready for the first extreme sprout.

With the sprout theorem and seed proof in place, the path induction is short. The recipe carries the endpoint side, so the induction hypothesis is already the exact ExtremeSproutCertificate needed by the next sprout move.

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⟩

The rcases tactic is Lean’s compact way to take apart nested evidence. In the path proof, path_graph_has_recipe gives a value shaped like “there exists an endpoint, there exists a side, and there exists a recipe.” The pattern ⟨_, _, ⟨recipe⟩⟩ tells Lean to unpack that evidence all at once: ignore the endpoint, ignore the side, and keep only the actual recipe. The caterpillar proof is the same idea with one more ignored value, the spine index.

The angle brackets are constructor patterns. For existential proofs, ⟨x, h⟩ means “a witness x together with evidence h.” For Nonempty, ⟨recipe⟩ means “there is at least one recipe, and here is one.” After rcases creates the local name recipe, the last line simply extracts its ready certificate: recipe.ready.cert is a GracefulCertificate T, and wrapping it in ⟨...⟩ turns that certificate into the required IsGraceful T.

Proof: Caterpillars are graceful.

For caterpillars, the current rightmost spine vertex stays extreme while its legs are attached. When the next spine vertex is attached, the new spine vertex becomes the extreme vertex for the next round.

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⟩

The checked Lean source for this post is available as GracefulLean.lean.