From f6aed0c42ac808bc898e243229df9784de29115d Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 3 Oct 2024 10:43:42 -0500 Subject: [PATCH 1/2] chore: add bv_toNat tags for toNat_{ofInt, sub} These were missing from the `bv_toNat` simp-set, discovered when refactoring LNSym's simp-set: https://github.com/leanprover/LNSym/pull/208 --- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 61e68c58cbc9..b87a73210e88 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -433,7 +433,7 @@ theorem toInt_inj {x y : BitVec n} : x.toInt = y.toInt ↔ x = y := theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y := by rw [Ne, toInt_inj] -@[simp] theorem toNat_ofInt {n : Nat} (i : Int) : +@[simp, bv_toNat] theorem toNat_ofInt {n : Nat} (i : Int) : (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by unfold BitVec.ofInt simp @@ -1741,7 +1741,7 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) = theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl -@[simp] theorem toNat_sub {n} (x y : BitVec n) : +@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) : (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set. From 6dfbb51542d87c9a982ef2cba3c314f18c316fee Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 3 Oct 2024 12:30:12 -0500 Subject: [PATCH 2/2] chore: remove BitVec.toNat_sub from simp-set --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index b87a73210e88..0b7657c1d901 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1741,7 +1741,7 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) = theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl -@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) : +@[simp] theorem toNat_sub {n} (x y : BitVec n) : (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.