From f86901844726222f026b8cf345f3ac67abc8f7f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 10 Sep 2024 14:32:44 +0200
Subject: [PATCH] feat: `BitVec` unsigned order theoretic results (#5297)

Proves that `<` and `<=` on `BitVec` are (strict) (total) partial
orders. This is required for the `UInt` as `BitVec` refactor.

This does open the question how to state these theorems "correctly" for
`BitVec`, we have both `<` living in `Prop` and `BitVec.ult` living in
`Bool`. We might of course say to always use `<` but: Once we start
adding `IntX` we need to prove the same results for `BitVec.slt` to
provide an equivalent API. So it would appear that it is unavoidable to
have a `= true` variant of these theorems there?

Question answered: Use `<` and `slt`.
---
 src/Init/Data/BitVec/Lemmas.lean | 41 +++++++++++++++++++++++++++-----
 1 file changed, 35 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a537d40707..8ad6753d66 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1631,12 +1631,41 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
 @[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2^n < y % 2^n := by
   simp [lt_def]
 
-protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x < y := by
-  revert h1 h2
-  let ⟨x, lt⟩ := x
-  let ⟨y, lt⟩ := y
-  simp
-  exact Nat.lt_of_le_of_ne
+@[simp] protected theorem not_le {x y : BitVec n} : ¬ x ≤ y ↔ y < x := by
+  simp [le_def, lt_def]
+
+@[simp] protected theorem not_lt {x y : BitVec n} : ¬ x < y ↔ y ≤ x := by
+  simp [le_def, lt_def]
+
+@[simp] protected theorem le_refl (x : BitVec n) : x ≤ x := by
+  simp [le_def]
+
+@[simp] protected theorem lt_irrefl (x : BitVec n) : ¬x < x := by
+  simp [lt_def]
+
+protected theorem le_trans {x y z : BitVec n} : x ≤ y → y ≤ z → x ≤ z := by
+  simp only [le_def]
+  apply Nat.le_trans
+
+protected theorem lt_trans {x y z : BitVec n} : x < y → y < z → x < z := by
+  simp only [lt_def]
+  apply Nat.lt_trans
+
+protected theorem le_total (x y : BitVec n) : x ≤ y ∨ y ≤ x := by
+  simp only [le_def]
+  apply Nat.le_total
+
+protected theorem le_antisymm {x y : BitVec n} : x ≤ y → y ≤ x → x = y := by
+  simp only [le_def, BitVec.toNat_eq]
+  apply Nat.le_antisymm
+
+protected theorem lt_asymm {x y : BitVec n} : x < y → ¬ y < x := by
+  simp only [lt_def]
+  apply Nat.lt_asymm
+
+protected theorem lt_of_le_ne {x y : BitVec n} : x ≤ y → ¬ x = y → x < y := by
+  simp only [lt_def, le_def, BitVec.toNat_eq]
+  apply Nat.lt_of_le_of_ne
 
 /-! ### ofBoolList -/