From 1a49689edcf57e74efd0d6924e07841671816dec Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 27 Jun 2026 19:30:01 -0500
Subject: [PATCH] Apply aesop to reduce proofs

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 lean/Spa/Analysis/Reaching.lean | 39 +++++----------------------------
 1 file changed, 6 insertions(+), 33 deletions(-)

diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean
index e156b7b..8f90264 100644
--- a/lean/Spa/Analysis/Reaching.lean
+++ b/lean/Spa/Analysis/Reaching.lean
@@ -51,6 +51,7 @@ inductive Run (prog : Program) where
   | cons (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
       (rest : Run prog) : Run prog
 
+@[aesop unsafe cases]
 inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop
   | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e))
       (rest : Run prog) :
@@ -60,22 +61,6 @@ inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId 
       (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
       LastAssign prog x (Run.cons s bs hc rest) n
 
-lemma lastAssign_cons_here {x : String} {s : prog.State} {e : Expr}
-    {hc : prog.code s = some (.assign x e)} {rest : Run prog} {n : prog.NodeId}
-    (h : LastAssign prog x (Run.cons s (.assign x e) hc rest) n) :
-    n = prog.nodeIdOfNonempty s hc := by
-  cases h with
-  | here _ _ _ _ => rfl
-  | there _ _ _ _ hne _ => exact absurd rfl (hne e)
-
-lemma lastAssign_cons_of_ne {x : String} {s : prog.State} {bs : BasicStmt}
-    {hc : prog.code s = some bs} {rest : Run prog} {n : prog.NodeId}
-    (h : LastAssign prog x (Run.cons s bs hc rest) n)
-    (hne : ∀ e, bs ≠ .assign x e) : LastAssign prog x rest n := by
-  cases h with
-  | here _ e' _ _ => exact absurd rfl (hne e')
-  | there _ _ _ _ _ hp => exact hp
-
 instance stateInterp : StateInterp (DefSet prog) prog where
   St := fun _ => Run prog
   init := Run.nil
@@ -84,14 +69,10 @@ instance stateInterp : StateInterp (DefSet prog) prog where
   interp_sup := by
     intro vs₁ vs₂ ρ run h x assigners hmem n hla
     obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
-    rw [Pi.sup_apply]
-    rcases h with h | h
-    · aesop
-    · aesop
+    aesop
   interp_inf := by
     intro vs₁ vs₂ ρ run h x assigners hmem n hla
     obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
-    rw [Pi.inf_apply]
     aesop
 
 instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
@@ -99,10 +80,7 @@ instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
   valid := by
     intro s ρ₁ ρ₂ bs vs st hcode hbs hvs
     cases hbs with
-    | noop =>
-      intro x assigners hmem n hla
-      exact hvs x assigners hmem n
-        (lastAssign_cons_of_ne prog hla (fun _ h => BasicStmt.noConfusion h))
+    | noop => intro x assigners hmem n hla; aesop
     | assign x e v hev =>
       intro k assigners hmem n hla
       have hmem2 : (k, assigners) ∈
@@ -110,15 +88,10 @@ instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
       by_cases hx : k = x
       · subst hx
         have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem2
-        have hn := lastAssign_cons_here prog hla
-        subst hd
-        rw [hn]
-        simp only [genSet, Function.update_self]
-      · have hp := lastAssign_cons_of_ne prog hla
-          (by intro e' h; injection h with h1 _; exact hx h1.symm)
-        have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
+        aesop (add simp genSet)
+      · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
           (fun hc => hx (List.mem_singleton.mp hc)) hmem2
-        exact hvs k assigners hmem' n hp
+        aesop
   botV_init := by intro x assigners _ n hla; cases hla
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :