Have LatticeInterpretation extend Interp

LatticeInterpretation now extends Interp L (Value → Prop), so each analysis
defines only its LatticeInterpretation instance and gets the ⟦⟧ notation for
free. Drops the standalone per-analysis Interp instances (signInterp and the
anonymous constInterp). The Interp class is kept for other uses.

The interp*_mk_disjoint bootstrap lemmas now state on the raw interp function
since they feed the instance and run before any Interp instance exists; the
trivial sup/inf wrappers are inlined into the instance.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lean/Spa/Analysis/Constant.lean

@@ -42,27 +42,17 @@ def interpConst : ConstLattice → Value → Prop
   | .top, _ => True
   | .mk z, v => v = .int z
 
-instance : Interp ConstLattice (Value → Prop) := ⟨interpConst⟩
-
 theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
-    ¬(⟦(.mk z₁ : ConstLattice)⟧ v ∧ ⟦(.mk z₂ : ConstLattice)⟧ v) := by
+    ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
   rintro ⟨h₁, h₂⟩
   rw [h₁] at h₂
   injection h₂ with hz
   exact hne hz
 
-theorem interpConst_sup {s₁ s₂ : ConstLattice} (v : Value)
-    (h : ⟦s₁⟧ v ∨ ⟦s₂⟧ v) : ⟦s₁ ⊔ s₂⟧ v :=
-  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
-
-theorem interpConst_inf {s₁ s₂ : ConstLattice} (v : Value)
-    (h : ⟦s₁⟧ v ∧ ⟦s₂⟧ v) : ⟦s₁ ⊓ s₂⟧ v :=
-  AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h
-
 instance constInterpretation : LatticeInterpretation ConstLattice where
   interp := interpConst
-  interp_sup := fun {l₁ l₂} v h => interpConst_sup (s₁ := l₁) (s₂ := l₂) v h
-  interp_inf := fun {l₁ l₂} v h => interpConst_inf (s₁ := l₁) (s₂ := l₂) v h
+  interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+  interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h
 
 variable (prog : Program)
 

lean/Spa/Analysis/Sign.lean

@@ -78,13 +78,11 @@ def interpSign : SignLattice → Value → Prop
   | .mk .zero, v => v = .int 0
   | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
 
-instance signInterp : Interp SignLattice (Value → Prop) := ⟨interpSign⟩
-
 theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
-    ¬(⟦(.mk s₁ : SignLattice)⟧ v ∧ ⟦(.mk s₂ : SignLattice)⟧ v) := by
+    ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
   rintro ⟨h₁, h₂⟩
   rcases s₁ <;> rcases s₂ <;> try exact hne rfl
-  all_goals simp only [signInterp, interpSign] at h₁ h₂
+  all_goals simp only [interpSign] at h₁ h₂
   · obtain ⟨n₁, rfl⟩ := h₁
     obtain ⟨n₂, hv⟩ := h₂
     injection hv with hz
@@ -108,18 +106,10 @@ theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Val
     injection hv with hz
     omega
 
-theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value)
-    (h : ⟦s₁⟧ v ∨ ⟦s₂⟧ v) : ⟦s₁ ⊔ s₂⟧ v :=
-  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
-
-theorem interpSign_inf {s₁ s₂ : SignLattice} (v : Value)
-    (h : ⟦s₁⟧ v ∧ ⟦s₂⟧ v) : ⟦s₁ ⊓ s₂⟧ v :=
-  AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
-
 instance signInterpretation : LatticeInterpretation SignLattice where
   interp := interpSign
-  interp_sup := fun {l₁ l₂} v h => interpSign_sup (s₁ := l₁) (s₂ := l₂) v h
-  interp_inf := fun {l₁ l₂} v h => interpSign_inf (s₁ := l₁) (s₂ := l₂) v h
+  interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+  interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
 
 namespace SignAnalysis
 
@@ -178,7 +168,7 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
   rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
     (try rcases s₁) <;> (try rcases s₂) <;>
-    simp only [plus, signInterp, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
+    simp only [plus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
       at h₁ h₂ ⊢ <;>
     omega
 
@@ -187,7 +177,7 @@ theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
     ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
   rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
     (try rcases s₁) <;> (try rcases s₂) <;>
-    simp only [minus, signInterp, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
+    simp only [minus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
       at h₁ h₂ ⊢ <;>
     omega
 

lean/Spa/Language/Semantics.lean

@@ -1,5 +1,6 @@
 import Spa.Language.Base
 import Spa.Lattice
+import Spa.Interp
 
 namespace Spa
 
@@ -56,8 +57,7 @@ inductive EvalStmt : Env → Stmt → Env → Prop
       EvalExpr ρ e (.int 0) →
       EvalStmt ρ (.whileLoop e s) ρ
 
-class LatticeInterpretation (L : Type*) [Lattice L] where
-  interp : L → Value → Prop
+class LatticeInterpretation (L : Type*) [Lattice L] extends Interp L (Value → Prop) where
   interp_sup : ∀ {l₁ l₂ : L} (v : Value),
     interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v
   interp_inf : ∀ {l₁ l₂ : L} (v : Value),