From c6feffa2bdabc0fbd75e3f8c2f9f681fbb7b41f5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 26 Aug 2024 14:12:40 +0100 Subject: [PATCH] feat: add Bitvec.ofInt_ofNat (#5081) We use `no_index` to work around special-handling of `OfNat.ofNat` in `DiscrTree`, which has been reported as an issue in https://github.com/leanprover/lean4/issues/2867 and is currently in the process of being fixed in https://github.com/leanprover/lean4/pull/3684. As the potential fix seems non-trivial and might need some time to arrive in-tree, we meanwhile add the `no_index` keyword to the problematic subterm. --------- Co-authored-by: Eric Wieser --- src/Init/Data/BitVec/Lemmas.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d41d236a8a..7b744b8ebf 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -303,6 +303,9 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : @[simp] theorem ofInt_natCast (w n : Nat) : BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl +@[simp] theorem ofInt_ofNat (w n : Nat) : + BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl + theorem toInt_neg_iff {w : Nat} {x : BitVec w} : BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by simp [toInt_eq_toNat_cond]; omega