DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Start working on notation for formalization

Browse Source 
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 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-23 10:23:44 -05:00
parent 8c37a4c049
commit 2044d4b2b6
3 changed files with 51 additions and 33 deletions
Download Patch File Download Diff File Expand all files Collapse all files

40
lean/Spa/Analysis/Sign.lean
View File

@@ -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 ρ) :