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

Clean up Sign correctness proofs

Browse Source 
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-23 11:44:33 -05:00
parent 2044d4b2b6
commit 20daf817e4
1 changed files with 22 additions and 66 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -170,78 +170,34 @@ instance exprEvaluator : ExprEvaluator SignLattice prog :=
def output : String := def output : String :=
show' (result SignLattice prog) show' (result SignLattice prog)
/-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
private theorem int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
constructor
· rintro ⟨n, rfl⟩; omega
· intro h; exact ⟨(z - 1).toNat, by omega⟩
/-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
private theorem int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
constructor
· rintro ⟨n, rfl⟩; omega
· intro h; exact ⟨(-z - 1).toNat, by omega⟩
theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
rcases g₁ with _ | _ | s₁ rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
· exact h₁.elim (try rcases s₁) <;> (try rcases s₂) <;>
· rcases g₂ with _ | _ | s₂ simp only [plus, signInterp, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
· exact h₂.elim at h₁ h₂ ⊢ <;>
· exact trivial
· exact trivial
· rcases g₂ with _ | _ | s₂
· exact h₂.elim
· rcases s₁ <;> exact trivial
· rcases s₁ <;> rcases s₂ <;>
simp only [plus, signInterp, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
try trivial
· obtain ⟨n₁, rfl⟩ := h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₁ + n₂ + 1, by omega⟩
· obtain ⟨n₁, rfl⟩ := h₁
subst h₂
exact ⟨n₁, by omega⟩
· obtain ⟨n₁, rfl⟩ := h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₁ + n₂ + 1, by omega⟩
· obtain ⟨n₁, rfl⟩ := h₁
subst h₂
exact ⟨n₁, by omega⟩
· subst h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₂, by omega⟩
· subst h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₂, by omega⟩
· subst h₁
subst h₂
omega omega
theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
(h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) : (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
rcases g₁ with _ | _ | s₁ rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
· exact h₁.elim (try rcases s₁) <;> (try rcases s₂) <;>
· rcases g₂ with _ | _ | s₂ simp only [minus, signInterp, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
· exact h₂.elim at h₁ h₂ ⊢ <;>
· exact trivial
· exact trivial
· rcases g₂ with _ | _ | s₂
· exact h₂.elim
· rcases s₁ <;> exact trivial
· rcases s₁ <;> rcases s₂ <;>
simp only [minus, signInterp, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
try trivial
· obtain ⟨n₁, rfl⟩ := h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₁ + n₂ + 1, by omega⟩
· obtain ⟨n₁, rfl⟩ := h₁
subst h₂
exact ⟨n₁, by omega⟩
· obtain ⟨n₁, rfl⟩ := h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₁ + n₂ + 1, by omega⟩
· obtain ⟨n₁, rfl⟩ := h₁
subst h₂
exact ⟨n₁, by omega⟩
· subst h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₂, by omega⟩
· subst h₁
obtain ⟨n₂, rfl⟩ := h₂
exact ⟨n₂, by omega⟩
· subst h₁
subst h₂
omega omega
instance eval_valid : ValidExprEvaluator SignLattice prog := by instance eval_valid : ValidExprEvaluator SignLattice prog := by