feat: bitblasting theorems for signed comparisons (#4201)

Prove theorems that relate `BitVec.slt` and `sle` to `carry`, so that
these signed comparisons may be bitblasted in LeanSAT.

This PR is stacked on top of #4200. For the diff without changes from
that PR, see:
https://github.com/opencompl/lean4/compare/opencompl:lean4:bitvec-toInt-iff-msb...bitvec-slt-blast

---------

Co-authored-by: Kim Morrison <scott@tqft.net>

src/Init/Data/BitVec/Bitblast.lean

@@ -198,4 +198,41 @@ theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
 theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
   simp [ule_eq_not_ult, ult_eq_not_carry]
 
+/-- If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide -/
+theorem slt_eq_ult_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) :
+    x.slt y = x.ult y := by
+  simp only [BitVec.slt, toInt_eq_msb_cond, BitVec.ult, decide_eq_decide, h]
+  cases y.msb <;> simp
+
+/-- If two bitvectors have different `msb`s, then unsigned comparison is determined by this bit -/
+theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
+    x.ult y = y.msb := by
+  simp only [BitVec.ult, msb_eq_decide, ne_eq, decide_eq_decide] at *
+  omega
+
+/-- If two bitvectors have different `msb`s, then signed and unsigned comparisons are opposites -/
+theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
+    x.slt y = !x.ult y := by
+  simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h]
+  cases y.msb <;> (simp; omega)
+
+theorem slt_eq_ult (x y : BitVec w) :
+    x.slt y = (x.msb != y.msb).xor (x.ult y) := by
+  by_cases h : x.msb = y.msb
+  · simp [h, slt_eq_ult_of_msb_eq]
+  · have h' : x.msb != y.msb := by simp_all
+    simp [slt_eq_not_ult_of_msb_neq h, h']
+
+theorem slt_eq_not_carry (x y : BitVec w) :
+    x.slt y = (x.msb == y.msb).xor (carry w x (~~~y) true) := by
+  simp only [slt_eq_ult, bne, ult_eq_not_carry]
+  cases x.msb == y.msb <;> simp
+
+theorem sle_eq_not_slt (x y : BitVec w) : x.sle y = !y.slt x := by
+  simp only [BitVec.sle, BitVec.slt, ← decide_not, decide_eq_decide]; omega
+
+theorem sle_eq_carry (x y : BitVec w) :
+    x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
+  rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
+
 end BitVec

src/Init/Data/Bool.lean

@@ -227,6 +227,8 @@ instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 @[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
 @[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide
 
+theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
+
 /-! ### coercision related normal forms -/
 
 theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :

src/Init/Data/Int/Order.lean

@@ -813,6 +813,20 @@ protected theorem sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b
 protected theorem sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c :=
   Int.add_lt_add hab (Int.neg_lt_neg hcd)
 
+protected theorem lt_of_sub_lt_sub_left {a b c : Int} (h : c - a < c - b) : b < a :=
+  Int.lt_of_neg_lt_neg <| Int.lt_of_add_lt_add_left h
+
+protected theorem lt_of_sub_lt_sub_right {a b c : Int} (h : a - c < b - c) : a < b :=
+  Int.lt_of_add_lt_add_right h
+
+@[simp] protected theorem sub_lt_sub_left_iff (a b c : Int) :
+    c - a < c - b ↔ b < a :=
+  ⟨Int.lt_of_sub_lt_sub_left, (Int.sub_lt_sub_left · c)⟩
+
+@[simp] protected theorem sub_lt_sub_right_iff (a b c : Int) :
+    a - c < b - c ↔ a < b :=
+  ⟨Int.lt_of_sub_lt_sub_right, (Int.sub_lt_sub_right · c)⟩
+
 protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int}
   (hab : a ≤ b) (hcd : c < d) : a - d < b - c :=
   Int.add_lt_add_of_le_of_lt hab (Int.neg_lt_neg hcd)