From 20daf817e414c55185faea6fdae0d1940197ba28 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Jun 2026 11:44:33 -0500 Subject: [PATCH] Clean up Sign correctness proofs Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Analysis/Sign.lean | 88 ++++++++++--------------------------- 1 file changed, 22 insertions(+), 66 deletions(-) diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 6485839..0629c09 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -170,79 +170,35 @@ instance exprEvaluator : ExprEvaluator SignLattice prog := def output : String := 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₂ : ℤ} (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₂ - · exact h₂.elim - · 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 + 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] + at h₁ h₂ ⊢ <;> + omega theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ} (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₂ - · exact h₂.elim - · 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 + 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] + at h₁ h₂ ⊢ <;> + omega instance eval_valid : ValidExprEvaluator SignLattice prog := by constructor