max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make bv_decide work on simp normal forms of shifts (#7976)

Browse source 
This PR ensure that `bv_decide` can handle the simp normal form of a
shift.

Consider:
```lean
theorem test1 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0)
  : b <<< s = 0 := by
  bv_decide
```
This works out, however:
```lean
theorem test2 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0)
  : b <<< s = 0 := by
  simp
  bv_decide
```
this fails because the `simp` normal form adds `toNat` to the right hand
argument of the `<<<` and `bv_decide` cannot deal with shifts by
non-constant `Nat`.

Discovered by @spdskatr
This commit is contained in:
Henrik Böving 2025-04-15 19:26:19 +02:00 • committed by GitHub
parent 525fd2697c
commit 712bb070f9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 31 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
View file

@ -5,6 +5,7 @@ Authors: Henrik Böving
-/
prelude
import Init.Data.BitVec
import Std.Tactic.BVDecide.Syntax
/-!
This contains theorems responsible for turning both `Bool` and `BitVec` goals into the
@ -97,6 +98,9 @@ attribute [bv_normalize] BitVec.neg_eq
attribute [bv_normalize] BitVec.mul_eq
attribute [bv_normalize] BitVec.udiv_eq
attribute [bv_normalize] BitVec.umod_eq
attribute [bv_normalize ←] BitVec.shiftLeft_eq'
attribute [bv_normalize ←] BitVec.sshiftRight_eq'
attribute [bv_normalize ←] BitVec.ushiftRight_eq'
end Normalize
end Std.Tactic.BVDecide

6
src/Std/Tactic/BVDecide/Syntax.lean
View file

@ -95,6 +95,12 @@ syntax (name := bvNormalize) "bv_normalize" optConfig : tactic
end Tactic
/--
Theorems tagged with the `bv_normalize` attribute are used during the rewriting step of the
`bv_decide` tactic.
-/
syntax (name := bv_normalize) "bv_normalize" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
/--
Auxiliary attribute for builtin `bv_normalize` simprocs.
-/

21
tests/lean/run/bv_decide_shift_to_nat.lean Normal file
View file

@ -0,0 +1,21 @@
import Std.Tactic.BVDecide
theorem test2 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
b <<< s.toNat = 0 := by
bv_decide
theorem test2' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
b >>> s.toNat = 0 := by
bv_decide
theorem test2'' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
BitVec.sshiftRight b s.toNat = 0 := by
bv_decide
theorem test2''' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
BitVec.shiftLeft b s.toNat = 0 := by
bv_decide
theorem test2'''' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
BitVec.ushiftRight b s.toNat = 0 := by
bv_decide