From d66a7d0e3e0f2e9fdf56504a7af5ad71ac456a48 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Jun 2026 14:31:27 -0500 Subject: [PATCH] Clean up and document AboveBelow --- lean/Spa/Lattice/AboveBelow.lean | 109 ++++++++++++++++--------------- 1 file changed, 56 insertions(+), 53 deletions(-) diff --git a/lean/Spa/Lattice/AboveBelow.lean b/lean/Spa/Lattice/AboveBelow.lean index 1148792..7cf7dc0 100644 --- a/lean/Spa/Lattice/AboveBelow.lean +++ b/lean/Spa/Lattice/AboveBelow.lean @@ -1,7 +1,37 @@ import Spa.Lattice +/-! + +# The Above-Below Lattice + +This file defines the `AboveBelow` lattice, which takes a flat domain +$a_1, \ldots, a_n \in \alpha$ and lifts it into a lattice bounded +above by a synthetic $\top$ element, and below by a synthetic $\bot$ +element. + +$$ +\begin{array}{ccccc} + && \top && \\ + & \swarrow & \downarrow & \searrow & \\ + a_1 & & … & & a_n \\ + & \searrow & \downarrow & \swarrow & \\ + && \bot && +\end{array} +$$ + +This lattice is also a `Spa.FiniteHeightLattice`, because no chain can +exceed the bottom-to-top chain $\bot < a_i < \top$. + +The above-below lattice is helpful for for analyses such as +`Spa/Analysis/Sign.lean` and `Spa/Analysis/Constant.lean`, whose +classifications of values (by sign or by exact value) do not have +any inherent structure beyond "matching exactly". + +-/ + namespace Spa +/-- The above-below lattice, with bottom element `bot` and top element `top`. -/ inductive AboveBelow (α : Type*) where | bot | top @@ -50,23 +80,12 @@ instance : Min (AboveBelow α) where @[simp] lemma mk_inf_mk (x y : α) : (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 - aesop - -protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by - aesop - -protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by - aesop - -protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by - aesop - -protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by - aesop - -protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by - aesop +protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop +protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by aesop +protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by aesop +protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop +protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by aesop +protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by aesop instance : Lattice (AboveBelow α) := Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc @@ -116,11 +135,11 @@ lemma le_cases {a b : AboveBelow α} (h : a ≤ b) : · rw [if_neg hxy] at hsup exact absurd hsup (by simp) -/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to -`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is -monotone in both arguments — regardless of its values on plain elements. -`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these -monotonicity facts for their `plus`/`minus`, all of which have this shape. -/ +/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤` + (against any non-`⊥` argument), it is monotone in both arguments. + The values of the the elements in `α` are irrelevant since they + are always incomparable. This makes it easy to prove monotonicity + for operations that "just" combine their flat elements, or give up. -/ lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ] (f : AboveBelow α → AboveBelow β → AboveBelow γ) (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot) @@ -144,68 +163,52 @@ lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ] · rw [htopr x hx]; exact le_top' _ · exact le_rfl -/-! ### Interpretations of flat lattices -/ - section Interp variable {V : Type*} {P : AboveBelow α → V → Prop} +/-- As long as the interpretation of a the above-below lattice respects the + fact that `bot` means "impossible", interpreting the above-below + lattice agrees with its `⊔`. -/ lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v) - {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by - rcases s₁ with _ | _ | x - · rw [bot_sup]; exact h.resolve_left (hbot v) - · rw [top_sup]; exact htop v - · rcases s₂ with _ | _ | y - · rw [sup_bot]; exact h.resolve_right (hbot v) - · rw [sup_top]; exact htop v - · rw [mk_sup_mk] - split - · next heq => subst heq; exact h.elim id id - · exact htop v + {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop +/-- As long as two distinct values in the flat domain don't overlap, + interpreting the above-below lattice agrees with its `⊔` -/ lemma interp_inf_of (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v)) {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by - rcases s₁ with _ | _ | x - · rw [bot_inf]; exact h.1 - · rw [top_inf]; exact h.2 - · rcases s₂ with _ | _ | y - · rw [inf_bot]; exact h.2 - · rw [inf_top]; exact h.1 - · rw [mk_inf_mk] - split - · next heq => subst heq; exact h.1 - · next hne => exact absurd h (hdisj hne v) + rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> try aesop + exfalso; exact (hdisj h v left right) end Interp -/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains -(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/ -def rank : AboveBelow α → ℕ +/-- synthetic rank of an element, used to prove chain bounds. -/ +private def rank : AboveBelow α → ℕ | bot => 0 | mk _ => 1 | top => 2 -/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and -`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/ +/-- It's not possible for any two lifted flat-domain elements to be less + than one another. -/ lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by intro h obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h rcases le_cases hle with h | h | h <;> simp_all +/-- The rank of elements is strictly monotonic. -/ lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by intro a b hab rcases a with _ | _ | x <;> rcases b with _ | _ | y + <;> try simp [rank] · exact absurd hab (lt_irrefl _) - · simp [rank] - · simp [rank] · exact absurd hab (bot_le' _).not_lt · exact absurd hab (lt_irrefl _) · exact absurd hab (le_top' _).not_lt · exact absurd hab (bot_le' _).not_lt - · simp [rank] · exact absurd hab (not_mk_lt_mk x y) +/-- All chains in the above-below lattice have at most 2 comparisons. -/ lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono) rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h