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

Slightly tweak AboveBelow proofs

Browse Source
This commit is contained in:
Danila Fedorin
2026-06-29 08:16:55 -05:00
parent 47d54f5b4b
commit 2598df690c
1 changed files with 4 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
lean/Spa/Lattice/AboveBelow.lean
View File

@@ -32,6 +32,7 @@ any inherent structure beyond "matching exactly".
namespace Spa namespace Spa
/-- The above-below lattice, with bottom element `bot` and top element `top`. -/ /-- The above-below lattice, with bottom element `bot` and top element `top`. -/
@[aesop safe cases]
inductive AboveBelow (α : Type*) where inductive AboveBelow (α : Type*) where
| bot | bot
| top | top
@@ -40,8 +41,6 @@ inductive AboveBelow (α : Type*) where
namespace AboveBelow namespace AboveBelow
attribute [aesop safe cases] AboveBelow
instance {α : Type*} [ToString α] : ToString (AboveBelow α) where instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
toString toString
| bot => "⊥" | bot => "⊥"
@@ -108,14 +107,9 @@ instance : OrderTop (AboveBelow α) where
top := top top := top
le_top := le_top' le_top := le_top'
lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
lt_of_le_of_ne (bot_le' _) (by simp) lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)
lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
lt_of_le_of_ne (le_top' _) (by simp)
lemma bot_lt_top : (bot : AboveBelow α) < top :=
lt_of_le_of_ne (bot_le' _) (by simp)
lemma le_cases {a b : AboveBelow α} (h : a ≤ b) : lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
a = bot ∨ b = top ∨ a = b := by a = bot ∨ b = top ∨ a = b := by