Clean up and document AboveBelow

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
+protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
-  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 sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
+protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
-  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 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
+/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
-`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
+    (against any non-`⊥` argument), it is monotone in both arguments.
-monotone in both arguments — regardless of its values on plain elements.
+    The values of the the elements in `α` are irrelevant since they
-`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
+    are always incomparable. This makes it easy to prove monotonicity
-monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
+    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
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop
-  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
 
+/-- 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
+  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> try aesop
-  · rw [bot_inf]; exact h.1
+  exfalso; exact (hdisj h v left right)
-  · 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)
 
 end Interp
 
-/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
+/-- synthetic rank of an element, used to prove chain bounds. -/
-(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
+private def rank : AboveBelow α → ℕ
-def rank : AboveBelow α → ℕ
   | bot => 0
   | mk _ => 1
   | top => 2
 
-/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
+/-- It's not possible for any two lifted flat-domain elements to be less
-`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
+    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