From 43e8288e3f073737f4b9f2283f455f0635a0f72e Mon Sep 17 00:00:00 2001 From: Siddharth Date: Fri, 2 May 2025 11:32:01 +0100 Subject: [PATCH] feat: Bitvector 0 equals bitvector 1 iff width is zero (#8202) This PR adds an inference that was repeatedly needed when proving `BitVec.msb_sdiv`, and is the symmetric version of `BitVec.one_eq_zero_iff` --- src/Init/Data/BitVec/Bitblast.lean | 1 - src/Init/Data/BitVec/Lemmas.lean | 4 ++++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index b5fe987149..b196173b70 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1501,7 +1501,6 @@ theorem sdiv_intMin {x : BitVec w} : by_cases h : x = intMin w · subst h simp - omega · simp only [sdiv_eq, msb_intMin, show 0 < w by omega, h] have := Nat.two_pow_pos (w-1) by_cases hx : x.msb diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3db766f82f..650aa9929e 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -518,6 +518,10 @@ theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by · rintro rfl simp +/-- `0#w = 1#w` iff the width is zero. -/ +@[simp] theorem zero_eq_one_iff (w : Nat) : (0#w = 1#w) ↔ (w = 0) := by + rw [← one_eq_zero_iff, eq_comm] + /-! ### msb -/ @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]