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

@@ -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
+Concretely, every embedding here is a *constant index shift*: `∙` and `⤳` lay
-    preserves node payloads and edges. -/
+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
+  off : ℕ
-  nodes_eq : ∀ i, h.nodes (f i) = g.nodes i
+  size_le : g.size + off ≤ h.size
-  edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges
+  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
+    Embed g₁ g₃ :=
-  f := e₂.f ∘ e₁.f
+  .ofIndexMap (e₂.off + e₁.off) (fun i => e₂.f (e₁.f i))
-  nodes_eq i := (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)
+    (fun i => (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i))
-  edges_mem he := e₂.edges_mem (e₁.edges_mem he)
+    (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
+def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) :=
-  f i := i.castAdd g₂.size
+  .ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes)
-  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
+    (fun he => List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he)))
-  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
+def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) :=
-  f i := i.natAdd g₁.size
+  .ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes)
-  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
+    (fun he => List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he)))
-  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
+def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) :=
-  f i := i.castAdd g₂.size
+  .ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes)
-  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
+    (fun he => List.mem_append_left _ (List.mem_map_of_mem _ he))
-  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
+def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) :=
-  f i := i.natAdd g₁.size
+  .ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes)
-  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
+    (fun he => List.mem_append_right _ (List.mem_map_of_mem _ he))
-  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
+def Embed.loop (g : GGraph (Option β)) : Embed g (GGraph.loop g) :=
-  f i := i.natAdd 2
+  .ofIndexMap 2 (fun i => i.natAdd 2) (Fin.append_right (fun _ : Fin 2 => none) g.nodes)
-  nodes_eq i := Fin.append_right (fun _ : Fin 2 => none) g.nodes i
+    (fun he => List.mem_append_left _ (List.mem_append_left _
-  edges_mem he := List.mem_append_left _ (List.mem_append_left _
+      (List.mem_append_left _ (List.mem_map_of_mem _ he))))
-    (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 α)
 

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) ρ₁ ρ₂ :=
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
+  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) ρ₁ ρ₂ :=
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
+  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. -/