From 827d55c6b657184a75445248eb755ddbf8b56fd5 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 9 Aug 2026 17:23:46 -0500 Subject: [PATCH] Switch embeddings to index-offset. This is a special case of an embedding, but it has the nice property for checking inclusion. --- lean/Spa/Language/Graphs.lean | 128 ++++++++++++++++++++++-------- lean/Spa/Language/Properties.lean | 10 ++- 2 files changed, 102 insertions(+), 36 deletions(-) diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean index 5d0b28b..9c68457 100644 --- a/lean/Spa/Language/Graphs.lean +++ b/lean/Spa/Language/Graphs.lean @@ -225,52 +225,116 @@ operator. 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. -/ +inclusion is meant. -/-- An embedding of graph `g` into graph `h`: an index translation that - preserves node payloads and edges. -/ +Concretely, every embedding here is a *constant index shift*: `∙` and `⤳` lay +their operands out in consecutive blocks via `Fin.append`, and `loop` prepends its +two synthetic nodes. Storing the offset rather than an arbitrary function makes +the range of an embedding an interval by construction (`Embed.mem_range_iff`), +which is the "is this node inside that subgraph?" test. -/ + +/-- Translate an index of `g` into `h` by a constant offset. -/ +def shift {g h : GGraph α} (off : ℕ) (hle : g.size + off ≤ h.size) (i : g.Index) : + h.Index := ⟨off + i.val, by omega⟩ + +@[simp] lemma shift_val {g h : GGraph α} {off : ℕ} (hle : g.size + off ≤ h.size) + (i : g.Index) : (shift (h := h) off hle i).val = off + i.val := rfl + +/-- An embedding of `g` into `h`: a constant index shift preserving 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 + off : ℕ + size_le : g.size + off ≤ h.size + nodes_eq : ∀ i, h.nodes (shift off size_le i) = g.nodes i + edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → + (shift off size_le e.1, shift off size_le e.2) ∈ h.edges -/-- Embeddings compose. -/ +/-- The index translation of an embedding. -/ +abbrev Embed.f {g h : GGraph α} (e : Embed g h) (i : g.Index) : h.Index := + shift e.off e.size_le i + +lemma Embed.f_inj {g h : GGraph α} (e : Embed g h) : Function.Injective e.f := + fun _ _ hij => Fin.ext (by simpa using congrArg Fin.val hij) + +/-- An embedding's range is the interval `[off, off + g.size)`. -/ +lemma Embed.mem_range_iff {g h : GGraph α} (e : Embed g h) (j : h.Index) : + (∃ i, e.f i = j) ↔ e.off ≤ j.val ∧ j.val < e.off + g.size := by + constructor + · rintro ⟨i, rfl⟩; have := i.isLt; simp only [Embed.f, shift_val]; omega + · rintro ⟨hlo, hhi⟩ + exact ⟨⟨j.val - e.off, by omega⟩, Fin.ext (by simp only [Embed.f, shift_val]; omega)⟩ + +/-- Build an embedding from an index map that is pointwise the shift. The five + inclusions below are naturally written with `Fin.castAdd`/`Fin.natAdd` — the form + the `Fin.append` lemmas are stated in — so this lets them keep those proofs + verbatim while `Embed` stores only the offset. The trailing two arguments are + boilerplate at every call site and default to discharging themselves. -/ +def Embed.ofIndexMap {g h : GGraph α} (off : ℕ) (k : g.Index → h.Index) + (hn : ∀ i, h.nodes (k i) = g.nodes i) + (hem : ∀ {e : g.Edge}, e ∈ g.edges → (k e.1, k e.2) ∈ h.edges) + (hle : g.size + off ≤ h.size := by + first | omega | (simp [GGraph.sequence, GGraph.overlay, GGraph.loop] <;> omega)) + (hk : ∀ i, (k i).val = off + i.val := by intro i; simp) : + Embed g h where + off := off + size_le := hle + nodes_eq i := by rw [show shift off hle i = k i from Fin.ext (by simp [hk])]; exact hn i + edges_mem hmem := by + have hs : ∀ i, shift (h := h) off hle i = k i := fun i => Fin.ext (by simp [hk]) + rw [hs, hs]; exact hem hmem + +/-- Embeddings compose; offsets add. -/ 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) + Embed g₁ g₃ := + .ofIndexMap (e₂.off + e₁.off) (fun i => e₂.f (e₁.f i)) + (fun i => (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)) + (fun he => e₂.edges_mem (e₁.edges_mem he)) + (hle := by have := e₁.size_le; have := e₂.size_le; omega) + (hk := fun i => by simp; omega) + +/-! The five inclusions `Stmt.cfg` uses, one per composition operator. Each `_f` +lemma recovers the `Fin.castAdd`/`Fin.natAdd` form for callers stating indices +that way (`Spa/Language/Properties.lean`). -/ /-- 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)) +def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) := + .ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes) + (fun 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)) +def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) := + .ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes) + (fun 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) +def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) := + .ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes) + (fun 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) +def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) := + .ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes) + (fun 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))) +def Embed.loop (g : GGraph (Option β)) : Embed g (GGraph.loop g) := + .ofIndexMap 2 (fun i => i.natAdd 2) (Fin.append_right (fun _ : Fin 2 => none) g.nodes) + (fun he => List.mem_append_left _ (List.mem_append_left _ + (List.mem_append_left _ (List.mem_map_of_mem _ he)))) + +/-! `shift` puts the offset on the left (`off + i.val`), matching `Fin.natAdd`, so +every right inclusion is *definitionally* the form `Spa/Language/Properties.lean` +states its trace indices in. Only the left inclusions need a bridge, since their +offset is `0` and `0 + i.val` does not reduce. + +Deliberately not `@[simp]`: they rewrite `Embed.f` back into `Fin.castAdd` form, +discarding the offset that `Embed.mem_range_iff` — and the subgraph-containment +tests built on it — reason with. -/ + +lemma Embed.sequenceLeft_f (g₁ g₂ : GGraph α) (i : g₁.Index) : + (Embed.sequenceLeft g₁ g₂).f i = i.castAdd g₂.size := Fin.ext (Nat.zero_add _) +lemma Embed.overlayLeft_f (g₁ g₂ : GGraph α) (i : g₁.Index) : + (Embed.overlayLeft g₁ g₂).f i = i.castAdd g₂.size := Fin.ext (Nat.zero_add _) variable (g : GGraph α) diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean index 08caeb6..e1deca2 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -41,8 +41,9 @@ noncomputable def Trace.embed {g h : Graph} (e : GGraph.Embed g h) 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) ρ₁ ρ₂ := - tr.embed (GGraph.Embed.overlayLeft g₁ g₂) + Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by + have h := tr.embed (GGraph.Embed.overlayLeft g₁ g₂) + rwa [GGraph.Embed.overlayLeft_f, GGraph.Embed.overlayLeft_f] at h /-- When two graphs are overlaid, for each trace in the right graph, a corresponding trace exists in the combined graph. -/ @@ -55,8 +56,9 @@ noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index} 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) ρ₁ ρ₂ := - tr.embed (GGraph.Embed.sequenceLeft g₁ g₂) + Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by + have h := tr.embed (GGraph.Embed.sequenceLeft g₁ g₂) + rwa [GGraph.Embed.sequenceLeft_f, GGraph.Embed.sequenceLeft_f] at h /-- When two graphs are sequenced, for each trace in the second graph, a corresponding trace exists in the combined graph. -/