From 8ce6e5e4e4269b3d5d7abf35d2c6677b00461cd1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Jun 2026 13:01:53 -0500 Subject: [PATCH] Have LatticeInterpretation extend Interp MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- lean/Spa/Analysis/Constant.lean | 16 +++------------- lean/Spa/Analysis/Sign.lean | 22 ++++++---------------- lean/Spa/Language/Semantics.lean | 4 ++-- 3 files changed, 11 insertions(+), 31 deletions(-) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index ad03af2..c644132 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/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) diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 51c2fed..876ada0 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/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 diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean index 848c7fd..2fa1234 100644 --- a/lean/Spa/Language/Semantics.lean +++ b/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),