feat: add comparison lemmas to bv_normalize (#6788)

This PR teaches bv_normalize that !(x < x) and !(x < 0).

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -291,6 +291,14 @@ theorem BitVec.zero_ult' (a : BitVec w) : (BitVec.ult 0#w a) = (!a == 0#w) := by
   | true => simp_all
   | false => simp_all
 
+@[bv_normalize]
+theorem BitVec.lt_irrefl (a : BitVec n) : (BitVec.ult a a) = false := by
+  rw [← Bool.not_eq_true, ← BitVec.lt_ult]
+  exact _root_.BitVec.lt_irrefl _
+
+@[bv_normalize]
+theorem BitVec.not_lt_zero (a : BitVec n) : (BitVec.ult a 0#n) = false := by rfl
+
 theorem BitVec.max_ult (a : BitVec w) : ¬ ((-1#w) < a) := by
   rcases w with rfl | w
   · simp [bv_toNat, BitVec.toNat_of_zero_length]

tests/lean/run/bv_counterexample.lean

@@ -114,5 +114,5 @@ error: The prover found a counterexample, consider the following assignment:
 x = 0x3#2
 -/
 #guard_msgs in
-example (x : BitVec 2) : (bif x.ult 0#2 then 1#2 else 2#2) == 3#2 := by
+example (x : BitVec 2) : (bif x.ult 1#2 then 1#2 else 2#2) == 3#2 := by
   bv_decide

tests/lean/run/bv_decide_rewriter.lean

@@ -25,7 +25,6 @@ def mem_subset (a1 a2 b1 b2 : BitVec 64) : Bool :=
 theorem mem_subset_refl : mem_subset a1 a2 a1 a2 := by
   unfold mem_subset
   bv_normalize
-  sorry
 
 example {x : BitVec 16} : 0#16 + x = x := by bv_normalize
 example {x : BitVec 16} : x + 0#16 = x := by bv_normalize
@@ -88,6 +87,16 @@ example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize
 example {x y : Bool} (h1 : x && y) : x || y := by bv_normalize
 example (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by bv_normalize
 
+-- lt_irrefl
+example (x : BitVec 16) : ¬x < x := by bv_normalize
+example (x : BitVec 16) : !(x.ult x) := by bv_normalize
+example (x : BitVec 16) : !(x.slt x) := by bv_normalize
+
+-- not_lt_zero
+example (x : BitVec 16) : ¬x < 0 := by bv_normalize
+example (x : BitVec 16) : x ≥ 0 := by bv_normalize
+example (x : BitVec 16) : !(x.ult 0) := by bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by