From c0542d0811f15b8e6137ac007ebfe3dd76a069ff Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 9 Aug 2026 17:51:58 -0500
Subject: [PATCH] Allow negative numbers in expressions

---
 lean/Spa/Analysis/Sign.lean      | 27 +++++++++++++++++++++------
 lean/Spa/Language/Base.lean      |  2 +-
 lean/Spa/Language/Semantics.lean |  2 +-
 3 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean
index bc69ced..02aa356 100644
--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -111,13 +111,16 @@ namespace SignAnalysis
 
 variable (prog : Program)
 
+/-- The sign of an integer literal. -/
+def signOf (z : ℤ) : SignLattice :=
+  if z = 0 then .mk .zero else if 0 < z then .mk .plus else .mk .minus
+
 def eval : Expr → VariableValues SignLattice prog → SignLattice
   | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
   | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
   | .var k, vs =>
     if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
-  | .num 0, _ => .mk .zero
-  | .num (_ + 1), _ => .mk .plus
+  | .num z, _ => signOf z
 
 lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
   induction e with
@@ -139,7 +142,7 @@ lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
           dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
   | num n =>
     intro vs₁ vs₂ _
-    cases n <;> exact le_refl _
+    exact le_refl _
 
 instance exprEvaluator : ExprEvaluator SignLattice prog :=
   ⟨eval prog, eval_mono prog⟩
@@ -159,6 +162,20 @@ private lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z
   · rintro ⟨n, rfl⟩; omega
   · intro h; exact ⟨(-z - 1).toNat, by omega⟩
 
+/-- `signOf` really does describe the literal it was computed from. -/
+lemma interp_signOf (z : ℤ) : ⟦signOf z⟧ (Value.int z) := by
+  unfold signOf
+  split
+  · case isTrue h => subst h; rfl
+  · rename_i hne
+    split
+    · case isTrue hpos =>
+        simp only [signInterpretation, interpSign, Value.int.injEq, int_pos_iff]
+        exact hpos
+    · case isFalse hnpos =>
+        simp only [signInterpretation, interpSign, Value.int.injEq, int_neg_iff]
+        omega
+
 lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
     ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
@@ -184,9 +201,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
   | num n =>
     intro _
     show ⟦eval prog (.num n) vs⟧ (.int n)
-    cases n with
-    | zero => rfl
-    | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
+    exact interp_signOf n
   | var x v hxv =>
     intro hvs
     show ⟦eval prog (.var x) vs⟧ v
diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean
index 1da64ea..447783f 100644
--- a/lean/Spa/Language/Base.lean
+++ b/lean/Spa/Language/Base.lean
@@ -22,7 +22,7 @@ inductive Expr where
   | add (e₁ e₂ : Expr)
   | sub (e₁ e₂ : Expr)
   | var (x : String)
-  | num (n : ℕ)
+  | num (z : ℤ)
   deriving DecidableEq
 
 /-- A statement that cannot alter control flow (and thus, can be part of a basic block).
diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean
index 19a3925..cb5fc3b 100644
--- a/lean/Spa/Language/Semantics.lean
+++ b/lean/Spa/Language/Semantics.lean
@@ -33,7 +33,7 @@ inductive Env.Mem : String × Value → Env → Prop
 /-- Inference rules for evaluating an expression (`Spa.Expr`) in a given
     environment. Pretty standard big-step expression evaluation. -/
 inductive EvalExpr : Env → Expr → Value → Prop
-  | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
+  | num (ρ : Env) (z : ℤ) : EvalExpr ρ (.num z) (.int z)
   | var (ρ : Env) (x : String) (v : Value) :
       Env.Mem (x, v) ρ → EvalExpr ρ (.var x) v
   | add (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :