From 904f6375be5737026337f188afd903074c4fbcff Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 2 Jul 2026 15:06:40 -0500 Subject: [PATCH] Consolidate per-operator trace lifting into GGraph.Embed + Trace.embed Each graph-composition operator includes its operands via an index translation preserving node payloads and edges. Capture that once as GGraph.Embed (a structure, not a class: for g ; g both inclusions share the type Embed g (g <~> g), so instance resolution could pick the wrong copy) with five named witnesses, and replace the five structurally identical trace-lifting inductions in Properties.lean with a single generic Trace.embed plus one-line corollaries. The same witnesses' nodes_eq fields will back the upcoming AST-id/CFG label bijection, so the per-operator content is stated exactly once. Co-Authored-By: Claude Fable 5 --- lean/Spa/Language/Graphs.lean | 59 ++++++++++++++++++++++++++ lean/Spa/Language/Properties.lean | 69 +++++++++---------------------- 2 files changed, 79 insertions(+), 49 deletions(-) diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index 81bd5ee..5d0b28b 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -213,6 +213,65 @@ lemma wrap_outputs (g : GGraph (Option β)) : (Option.map h) <$> wrap g = wrap (Option.map h <$> g) := by simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton] +/-! ### Embeddings + +Each composition operator includes its operands into the result via an index +translation that preserves node payloads and edges. `Embed` captures exactly +those two facts, so anything defined from `nodes` and `edges` (traces, node +labels, …) can be transported along an embedding once, instead of once per +operator. + +`Embed` is deliberately a structure rather than a class: for `g ⤳ g`, both the +left and the right inclusion inhabit the same type `Embed g (g ⤳ g)`, so +instance resolution could silently pick the wrong copy. Embeddings into a +composed graph are non-canonical by design; a named witness says which +inclusion is meant. -/ + +/-- An embedding of graph `g` into graph `h`: an index translation that + preserves node payloads and edges. -/ +structure Embed (g h : GGraph α) where + f : g.Index → h.Index + nodes_eq : ∀ i, h.nodes (f i) = g.nodes i + edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges + +/-- Embeddings compose. -/ +def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) : + Embed g₁ g₃ where + f := e₂.f ∘ e₁.f + nodes_eq i := (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i) + edges_mem he := e₂.edges_mem (e₁.edges_mem he) + +/-- The left operand's inclusion into a sequenced graph. -/ +def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) where + f i := i.castAdd g₂.size + nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i + edges_mem he := List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he)) + +/-- The right operand's inclusion into a sequenced graph. -/ +def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) where + f i := i.natAdd g₁.size + nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i + edges_mem he := List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he)) + +/-- The left operand's inclusion into an overlaid graph. -/ +def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) where + f i := i.castAdd g₂.size + nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i + edges_mem he := List.mem_append_left _ (List.mem_map_of_mem _ he) + +/-- The right operand's inclusion into an overlaid graph. -/ +def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) where + f i := i.natAdd g₁.size + nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i + edges_mem he := List.mem_append_right _ (List.mem_map_of_mem _ he) + +/-- The body's inclusion into a `loop` graph. -/ +def Embed.loop (g : GGraph (Option β)) : Embed g (loop g) where + f i := i.natAdd 2 + nodes_eq i := Fin.append_right (fun _ : Fin 2 => none) g.nodes i + edges_mem he := List.mem_append_left _ (List.mem_append_left _ + (List.mem_append_left _ (List.mem_map_of_mem _ he))) + variable (g : GGraph α) /-- All the nodes in the graph. -/ diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean index 8a03684..08caeb6 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -27,62 +27,43 @@ section Embeddings variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} +/-- Transport a trace along a graph embedding: an embedding preserves node + payloads and edges, which is everything a trace is made of. This is the + single induction behind all the per-operator lifting corollaries below. -/ +noncomputable def Trace.embed {g h : Graph} (e : GGraph.Embed g h) + {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) : + Trace h (e.f idx₁) (e.f idx₂) ρ₁ ρ₂ := by + induction tr with + | single hbs => exact Trace.single (by rwa [e.nodes_eq]) + | edge hbs he _ ih => exact Trace.edge (by rwa [e.nodes_eq]) (e.edges_mem he) ih + /-- When two graphs are overlaid, for each trace in the left graph, a corresponding trace exists in the combined graph. -/ noncomputable def Trace.overlay_left {idx₁ idx₂ : g₁.Index} (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : - Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by - induction tr with - | single hbs => - exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, - Fin.append_left]) - | edge hbs he _ ih => - refine Trace.edge ?_ ?_ ih - · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left] - · exact List.mem_append_left _ (List.mem_map_of_mem _ he) + Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := + tr.embed (GGraph.Embed.overlayLeft g₁ g₂) /-- When two graphs are overlaid, for each trace in the right graph, a corresponding trace exists in the combined graph. -/ noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index} (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : - Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by - induction tr with - | single hbs => - exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, - Fin.append_right]) - | edge hbs he _ ih => - refine Trace.edge ?_ ?_ ih - · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right] - · exact List.mem_append_right _ (List.mem_map_of_mem _ he) + Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := + tr.embed (GGraph.Embed.overlayRight g₁ g₂) /-- When two graphs are sequenced, for each trace in the first graph, a corresponding trace exists in the combined graph. -/ noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index} (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) : - Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by - induction tr with - | single hbs => - exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, - Fin.append_left]) - | edge hbs he _ ih => - refine Trace.edge ?_ ?_ ih - · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left] - · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he)) + Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := + tr.embed (GGraph.Embed.sequenceLeft g₁ g₂) /-- When two graphs are sequenced, for each trace in the second graph, a corresponding trace exists in the combined graph. -/ noncomputable def Trace.sequence_right {idx₁ idx₂ : g₂.Index} (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) : - Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by - induction tr with - | single hbs => - exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, - Fin.append_right]) - | edge hbs he _ ih => - refine Trace.edge ?_ ?_ ih - · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right] - · exact List.mem_append_left _ - (List.mem_append_right _ (List.mem_map_of_mem _ he)) + Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := + tr.embed (GGraph.Embed.sequenceRight g₁ g₂) /-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/ noncomputable def EndToEndTrace.overlay_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) : @@ -125,18 +106,8 @@ variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} /-- A trace through a body CFG still exists (up to reindexing) in a zero-or-more loop CFG. -/ noncomputable def Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) : - Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by - induction tr with - | single hbs => - exact Trace.single (by - rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => none) g.nodes from rfl, - Fin.append_right]) - | edge hbs he _ ih => - refine Trace.edge ?_ ?_ ih - · rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => none) g.nodes from rfl, - Fin.append_right] - · exact List.mem_append_left _ (List.mem_append_left _ - (List.mem_append_left _ (List.mem_map_of_mem _ he))) + Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := + tr.embed (GGraph.Embed.loop g) /-- The beginning node of a loop graph is empty. -/ private lemma loop_nodes_at_in :