From 3e3ff31864267a83f829f2c445a7bf1f9f9ec554 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 27 Mar 2025 13:32:27 +0100 Subject: [PATCH] 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 | 20 +++++++++++------- src/Init/Data/BitVec/Lemmas.lean | 25 ++++++++++++++++++++++- src/Init/Data/Int/LemmasAux.lean | 5 +++++ src/Init/Data/Nat/Bitwise/Lemmas.lean | 6 ++++++ src/Std/Data/DHashMap/Internal/Index.lean | 2 +- 5 files changed, 49 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 3aa5d898e1..b06e5fa171 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/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 -/ /-- diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 416314de2e..b2dc42f326 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/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] diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean index 5e03cfbc50..9217b192ed 100644 --- a/src/Init/Data/Int/LemmasAux.lean +++ b/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) : diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 8e46e450ec..6e91b8c795 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/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) diff --git a/src/Std/Data/DHashMap/Internal/Index.lean b/src/Std/Data/DHashMap/Internal/Index.lean index dcb98d9f02..89e44a14d0 100644 --- a/src/Std/Data/DHashMap/Internal/Index.lean +++ b/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']