From 9e0702b5f5de4abc97aa83d903afda36b336acae Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 27 Jun 2026 19:49:13 -0500 Subject: [PATCH] Replace AboveBelow lattice-axiom case bashes with aesop The six lattice axioms (sup/inf comm/assoc, absorption) all close with a uniform `rcases <;> aesop`, removing the per-lemma simp-lemma lists that had to be kept in sync with the Max/Min definitions. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Lattice/AboveBelow.lean | 26 ++++++-------------------- 1 file changed, 6 insertions(+), 20 deletions(-) diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index 29e8946..c7f1f10 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -49,36 +49,22 @@ instance : Min (AboveBelow α) where (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by - rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only - [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] - split_ifs with h₁ h₂ h₂ <;> simp_all + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by - rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> - simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk] - split_ifs <;> simp_all + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> aesop protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by - rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only - [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] - split_ifs with h₁ h₂ h₂ <;> simp_all + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by - rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> - simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] - split_ifs <;> simp_all + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;> aesop protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by - rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> - simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, - bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> - try (split_ifs <;> simp_all) + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by - rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> - simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk, - bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;> - try (split_ifs <;> simp_all) + rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> aesop instance : Lattice (AboveBelow α) := Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc