Add computation lemmas on GGraphs + map to Graphs.lean

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lean/Spa/Language/Graphs.lean

@@ -101,6 +101,37 @@ def singleton (a : α) : GGraph α where
 def wrap (g : GGraph (List β)) : GGraph (List β) :=
   singleton [] ⤳ g ⤳ singleton []
 
+@[simp] theorem map_singleton (f : α → β) (a : α) :
+    (singleton a).map f = singleton (f a) := rfl
+
+@[simp] theorem map_comp (f : α → β) (g₁ g₂ : GGraph α) :
+    (g₁ ∙ g₂).map f = g₁.map f ∙ g₂.map f := by
+  rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
+  simp only [GGraph.map, GGraph.comp]
+  congr 1
+  funext i
+  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
+
+@[simp] theorem map_link (f : α → β) (g₁ g₂ : GGraph α) :
+    (g₁ ⤳ g₂).map f = g₁.map f ⤳ g₂.map f := by
+  rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
+  simp only [GGraph.map, GGraph.link]
+  congr 1
+  funext i
+  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
+
+@[simp] theorem map_loop (h : β → γ) (g : GGraph (List β)) :
+    (loop g).map (List.map h) = loop (g.map (List.map h)) := by
+  rcases g with ⟨n, nd, e, i, o⟩
+  simp only [GGraph.map, GGraph.loop]
+  congr 1
+  funext i
+  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
+
+@[simp] theorem map_wrap (h : β → γ) (g : GGraph (List β)) :
+    (wrap g).map (List.map h) = wrap (g.map (List.map h)) := by
+  simp [GGraph.wrap, GGraph.map_link, GGraph.map_singleton]
+
 variable (g : GGraph α)
 
 def indices : List g.Index := List.finRange g.size