From 2044d4b2b6511961730500a3cb60af12c604a7c6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Jun 2026 10:23:44 -0500 Subject: [PATCH] Start working on notation for formalization Per convention, create a new instance for 'interpretable' thing, with an fundep'ed semantic domain. I feel at peace with this notation even though it conflicts with Mathlib's quotients. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Analysis/Constant.lean | 34 +++++++++++++++------------- lean/Spa/Analysis/Sign.lean | 40 ++++++++++++++++++--------------- lean/Spa/Interp.lean | 10 +++++++++ 3 files changed, 51 insertions(+), 33 deletions(-) create mode 100644 lean/Spa/Interp.lean diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index f72aa86..9ec3707 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -26,6 +26,7 @@ Correspondence: -/ import Spa.Analysis.Forward import Spa.Analysis.Utils +import Spa.Interp import Spa.Showable namespace Spa @@ -86,9 +87,12 @@ def interpConst : ConstLattice → Value → Prop | .top, _ => True | .mk z, v => v = .int z +/-- Agda: `⟦_⟧ᶜ` is registered for the `⟦_⟧` interpretation notation. -/ +instance : Interp ConstLattice (Value → Prop) := ⟨interpConst⟩ + /-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/ theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} : - ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by + ¬(⟦(.mk z₁ : ConstLattice)⟧ v ∧ ⟦(.mk z₂ : ConstLattice)⟧ v) := by rintro ⟨h₁, h₂⟩ rw [h₁] at h₂ injection h₂ with hz @@ -96,12 +100,12 @@ theorem interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Val /-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨` (via the factored flat-lattice lemma). -/ theorem interpConst_sup {s₁ s₂ : ConstLattice} (v : Value) - (h : interpConst s₁ v ∨ interpConst s₂ v) : interpConst (s₁ ⊔ s₂) v := + (h : ⟦s₁⟧ v ∨ ⟦s₂⟧ v) : ⟦s₁ ⊔ s₂⟧ v := AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h /-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧` (via the factored flat-lattice lemma). -/ theorem interpConst_inf {s₁ s₂ : ConstLattice} (v : Value) - (h : interpConst s₁ v ∧ interpConst s₂ v) : interpConst (s₁ ⊓ s₂) v := + (h : ⟦s₁⟧ v ∧ ⟦s₂⟧ v) : ⟦s₁ ⊓ s₂⟧ v := AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h /-- Agda: `latticeInterpretationᶜ` (an instance there too). -/ @@ -153,8 +157,8 @@ def output : String := /-- Agda: `plus-valid`. -/ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} - (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) : - interpConst (plus g₁ g₂) (.int (z₁ + z₂)) := by + (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : + ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by rcases g₁ with _ | _ | c₁ · exact h₁.elim · rcases g₂ with _ | _ | c₂ @@ -171,8 +175,8 @@ theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} /-- Agda: `minus-valid`. -/ theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ} - (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) : - interpConst (minus g₁ g₂) (.int (z₁ - z₂)) := by + (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : + ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by rcases g₁ with _ | _ | c₁ · exact h₁.elim · rcases g₂ with _ | _ | c₂ @@ -194,11 +198,11 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by induction hev with | num n => intro _ - show interpConst (eval prog (.num n) vs) (.int n) + show ⟦eval prog (.num n) vs⟧ (.int n) rfl | var x v hxv => intro hvs - show interpConst (eval prog (.var x) vs) v + show ⟦eval prog (.var x) vs⟧ v simp only [eval] by_cases hk : FiniteMap.MemKey x vs · rw [dif_pos hk] @@ -207,15 +211,15 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by exact trivial | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => intro hvs - have h₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs - have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs - show interpConst (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂)) + have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs + have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs + show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂)) exact plus_valid h₁ h₂ | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => intro hvs - have h₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs - have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs - show interpConst (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂)) + have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs + have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs + show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂)) exact minus_valid h₁ h₂ /-- Agda: `WithProg.analyze-correct`. -/ diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 10cc95f..6485839 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -1,5 +1,6 @@ import Spa.Analysis.Forward import Spa.Analysis.Utils +import Spa.Interp import Spa.Showable namespace Spa @@ -85,11 +86,14 @@ def interpSign : SignLattice → Value → Prop | .mk .zero, v => v = .int 0 | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1)) +/-- Agda: `⟦_⟧ᵍ` is registered for the `⟦_⟧` interpretation notation. -/ +instance signInterp : Interp SignLattice (Value → Prop) := ⟨interpSign⟩ + theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} : - ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by + ¬(⟦(.mk s₁ : SignLattice)⟧ v ∧ ⟦(.mk s₂ : SignLattice)⟧ v) := by rintro ⟨h₁, h₂⟩ rcases s₁ <;> rcases s₂ <;> try exact hne rfl - all_goals simp only [interpSign] at h₁ h₂ + all_goals simp only [signInterp, interpSign] at h₁ h₂ · obtain ⟨n₁, rfl⟩ := h₁ obtain ⟨n₂, hv⟩ := h₂ injection hv with hz @@ -114,11 +118,11 @@ theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Val omega theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value) - (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v := + (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 : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v := + (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 @@ -167,8 +171,8 @@ def output : String := show' (result SignLattice prog) theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} - (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) : - interpSign (plus g₁ g₂) (.int (z₁ + z₂)) := by + (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : + ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by rcases g₁ with _ | _ | s₁ · exact h₁.elim · rcases g₂ with _ | _ | s₂ @@ -179,7 +183,7 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} · exact h₂.elim · rcases s₁ <;> exact trivial · rcases s₁ <;> rcases s₂ <;> - simp only [plus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;> + simp only [plus, signInterp, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;> try trivial · obtain ⟨n₁, rfl⟩ := h₁ obtain ⟨n₂, rfl⟩ := h₂ @@ -204,8 +208,8 @@ theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} omega theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} - (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) : - interpSign (minus g₁ g₂) (.int (z₁ - z₂)) := by + (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : + ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by rcases g₁ with _ | _ | s₁ · exact h₁.elim · rcases g₂ with _ | _ | s₂ @@ -216,7 +220,7 @@ theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} · exact h₂.elim · rcases s₁ <;> exact trivial · rcases s₁ <;> rcases s₂ <;> - simp only [minus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;> + simp only [minus, signInterp, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;> try trivial · obtain ⟨n₁, rfl⟩ := h₁ obtain ⟨n₂, rfl⟩ := h₂ @@ -246,13 +250,13 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by induction hev with | num n => intro _ - show interpSign (eval prog (.num n) vs) (.int n) + show ⟦eval prog (.num n) vs⟧ (.int n) cases n with | zero => rfl | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩ | var x v hxv => intro hvs - show interpSign (eval prog (.var x) vs) v + show ⟦eval prog (.var x) vs⟧ v simp only [eval] by_cases hk : FiniteMap.MemKey x vs · rw [dif_pos hk] @@ -261,15 +265,15 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by exact trivial | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => intro hvs - have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs - have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs - show interpSign (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂)) + have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs + have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs + show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂)) exact plus_valid h₁ h₂ | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ => intro hvs - have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs - have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs - show interpSign (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂)) + have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs + have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs + show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂)) exact minus_valid h₁ h₂ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : diff --git a/lean/Spa/Interp.lean b/lean/Spa/Interp.lean new file mode 100644 index 0000000..97f0e24 --- /dev/null +++ b/lean/Spa/Interp.lean @@ -0,0 +1,10 @@ +import Mathlib.Tactic.TypeStar + +namespace Spa + +class Interp (α : Type*) (dom : outParam Type*) where + interp : α → dom + +notation:max (priority := high) "⟦" v "⟧" => Interp.interp v + +end Spa