From 445187837c2fa57082cee5a8418ff215e698b469 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 27 Jun 2026 19:45:45 -0500 Subject: [PATCH] Add Trace.concat notation and apply at call sites MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce `tr₁ ++< he >++ tr₂` scoped notation for `Trace.concat` (precedence 65, right-associative, mirroring `++`) and use it throughout Properties.lean. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Language/Properties.lean | 12 ++++++------ lean/Spa/Language/Traces.lean | 2 ++ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean index 5ebfa67..0e40f2b 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -120,7 +120,7 @@ noncomputable def EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂ refine ⟨i₁.castAdd g₂.size, List.mem_map_of_mem _ h₁, j₂.natAdd g₁.size, List.mem_map_of_mem _ k₂, - Trace.concat tr₁.sequence_left ?_ tr₂.sequence_right⟩ + tr₁.sequence_left ++< ?_ >++ tr₂.sequence_right⟩ exact List.mem_append_right _ (List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩) @@ -168,8 +168,8 @@ noncomputable def EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) : refine List.mem_append_left _ (List.mem_append_right _ ?_) exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₂) refine ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, ?_⟩ - exact Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none)) hin - (Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none))) + exact Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hin >++ + tr.loop ++< hout >++ Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none) /-- The zero-or-more times loop has an edge to return back to the top, to continue after an iteration. -/ private lemma loop_edge_out_in : @@ -186,15 +186,15 @@ noncomputable def EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop simp only [Graph.loop_inputs, Graph.loop_outputs, List.mem_singleton] at h₁ h₂ k₁ k₂ subst h₁; subst h₂; subst k₁; subst k₂ exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, - Trace.concat tr₁ loop_edge_out_in tr₂⟩ + tr₁ ++< loop_edge_out_in >++ tr₂⟩ /-- A loop can be executed zero times. -/ noncomputable def EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _)) exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, - Trace.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none)) hedge - (Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none))⟩ + Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hedge >++ + Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)⟩ end Loop diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 712f66a..71bc13f 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -48,6 +48,8 @@ noncomputable def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Inde | single hbs => exact Trace.edge hbs he tr₂ | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂) +scoped notation:65 tr₁:66 " ++< " he " >++ " tr₂:65 => Trace.concat tr₁ he tr₂ + /-- A beginning-to-end trace corresponding to the CFG `g`. -/ inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)