feat: support material for finite type theory (#7694)

This PR contains additional material on `BitVec`, `Int` and `Nat`, split
off from #7592.

src/Init/Data/BitVec/Bitblast.lean

@@ -567,19 +567,19 @@ theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
   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) :
+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) :
+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
+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 zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : BitVec.sle 0#w x = !x.msb := by
@@ -588,14 +588,14 @@ theorem zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : BitVec.sle 0#w x = !x.msb
 theorem zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} : BitVec.sle 0#w x ↔ x.msb = false := by
   simp [zero_sle_eq_not_msb]
 
-theorem toNat_toInt_of_sle {w : Nat} (x : BitVec w) (hx : BitVec.sle 0#w x) : x.toInt.toNat = x.toNat :=
+theorem toNat_toInt_of_sle {w : Nat} {x : BitVec w} (hx : BitVec.sle 0#w x) : x.toInt.toNat = x.toNat :=
   toNat_toInt_of_msb x (zero_sle_iff_msb_eq_false.1 hx)
 
-theorem sle_eq_carry (x y : BitVec w) :
+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]
 
-theorem neg_slt_zero (h : 0 < w) (x : BitVec w) :
+theorem neg_slt_zero (h : 0 < w) {x : BitVec w} :
     (-x).slt 0#w = ((x == intMin w) || (0#w).slt x) := by
   rw [slt_zero_eq_msb, msb_neg, slt_eq_sle_and_ne, zero_sle_eq_not_msb]
   apply Bool.eq_iff_iff.2
@@ -608,11 +608,17 @@ theorem neg_slt_zero (h : 0 < w) (x : BitVec w) :
     rintro rfl
     simp at hmsb
 
-theorem neg_sle_zero (h : 0 < w) (x : BitVec w) :
+theorem neg_sle_zero (h : 0 < w) {x : BitVec w} :
     (-x).sle 0#w = (x == intMin w || (0#w).sle x) := by
   rw [sle_eq_slt_or_eq, neg_slt_zero h, sle_eq_slt_or_eq]
   simp [Bool.beq_eq_decide_eq (-x), Bool.beq_eq_decide_eq _ x, Eq.comm (a := x), Bool.or_assoc]
 
+theorem sle_eq_ule {x y : BitVec w} : x.sle y = (x.msb != y.msb ^^ x.ule y) := by
+  rw [sle_eq_not_slt, slt_eq_ult, ← Bool.xor_not, ← ule_eq_not_ult, bne_comm]
+
+theorem sle_eq_ule_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) : x.sle y = x.ule y := by
+  simp [BitVec.sle_eq_ule, h]
+
 /-! ### mul recurrence for bitblasting -/
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -756,12 +756,36 @@ theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
 theorem slt_zero_eq_msb {w : Nat} {x : BitVec  w} : x.slt 0#w = x.msb := by
   rw [Bool.eq_iff_iff, BitVec.slt_zero_iff_msb_cond]
 
+theorem sle_eq_decide {x y : BitVec w} : x.sle y = decide (x.toInt ≤ y.toInt) := rfl
+
+theorem slt_eq_decide {x y : BitVec w} : x.slt y = decide (x.toInt < y.toInt) := rfl
+
+theorem ule_eq_decide {x y : BitVec w} : x.ule y = decide (x.toNat ≤ y.toNat) := rfl
+
+theorem ult_eq_decide {x y : BitVec w} : x.ult y = decide (x.toNat < y.toNat) := rfl
+
+theorem ule_eq_decide_le {x y : BitVec w} : x.ule y = decide (x ≤ y) := rfl
+
+theorem ult_eq_decide_lt {x y : BitVec w} : x.ult y = decide (x < y) := rfl
+
+theorem ule_iff_le {x y : BitVec w} : x.ule y ↔ x ≤ y :=
+  decide_eq_true_iff
+
+theorem ult_iff_lt {x y : BitVec w} : x.ult y ↔ x < y :=
+  decide_eq_true_iff
+
 theorem sle_iff_toInt_le {w : Nat} {x y : BitVec w} : x.sle y ↔ x.toInt ≤ y.toInt :=
   decide_eq_true_iff
 
 theorem slt_iff_toInt_lt {w : Nat} {x y : BitVec w} : x.slt y ↔ x.toInt < y.toInt :=
   decide_eq_true_iff
 
+theorem ule_iff_toNat_le {x y : BitVec w} : x.ule y ↔ x.toNat ≤ y.toNat :=
+  decide_eq_true_iff
+
+theorem ult_iff_toNat_lt {x y : BitVec w} : x.ult y ↔ x.toNat < y.toNat :=
+  decide_eq_true_iff
+
 theorem sle_eq_slt_or_eq {x y : BitVec w} : x.sle y = (x.slt y || x == y) := by
   apply Bool.eq_iff_iff.2
   simp only [BitVec.sle, decide_eq_true_eq, BitVec.slt, Bool.or_eq_true, beq_iff_eq, ← toInt_inj]
@@ -2504,7 +2528,6 @@ theorem toInt_signExtend_eq_toInt_bmod_of_le (x : BitVec w) (h : v ≤ w) :
     (x.signExtend v).toInt = x.toInt.bmod (2 ^ v) := by
   rw [BitVec.toInt_signExtend, Nat.min_eq_left h]
 
-
 theorem toFin_signExtend_of_le {x : BitVec w} (hv : v ≤ w):
     (x.signExtend v).toFin = Fin.ofNat' (2 ^ v) x.toNat := by
   simp [signExtend_eq_setWidth_of_le _ hv]

src/Init/Data/Int/LemmasAux.lean

@@ -76,6 +76,11 @@ theorem neg_lt_self_iff {n : Int} : -n < n ↔ 0 < n := by
 theorem pos_iff_toNat_pos {n : Int} : 0 < n ↔ 0 < n.toNat := by
   omega
 
+theorem ofNat_toNat_eq_self {a : Int} : a.toNat = a ↔ 0 ≤ a := by omega
+theorem eq_ofNat_toNat {a : Int} : a = a.toNat ↔ 0 ≤ a := by omega
+theorem toNat_le_toNat {n m : Int} (h : n ≤ m) : n.toNat ≤ m.toNat := by omega
+theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m := by omega
+
 /-! ### natAbs -/
 
 theorem eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) :

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -828,3 +828,9 @@ theorem and_le_left {n m : Nat} : n &&& m ≤ n :=
 
 theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
   le_of_testBit (by simp)
+
+theorem left_le_or {n m : Nat} : n ≤ n ||| m :=
+  le_of_testBit (by simpa using fun i => Or.inl)
+
+theorem right_le_or {n m : Nat} : m ≤ n ||| m :=
+  le_of_testBit (by simpa using fun i => Or.inr)

src/Std/Data/DHashMap/Internal/Index.lean

@@ -45,7 +45,7 @@ cf. https://github.com/leanprover/lean4/issues/4157
 -/
 @[irreducible, inline] def mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
     { u : USize // u.toNat < sz } :=
-  ⟨(scrambleHash hash).toUSize &&& (sz.toUSize - 1), by
+  ⟨(scrambleHash hash).toUSize &&& (USize.ofNat sz - 1), by
     -- This proof is a good test for our USize API
     by_cases h' : sz < USize.size
     · rw [USize.toNat_and, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt' h']