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

feat: improve BitVec.extractLsb' lemma on appended vectors (#8585)

Browse source 
This PR makes the lemma `BitVec.extractLsb'_append_eq_ite` more usable
by using the "simple case" more often, and uses this simplification to
make `BitVec.extractLsb'_append_eq_of_add_lt` stronger, renaming it to
`BitVec.extractLsb'_append_eq_of_add_le`.
This commit is contained in:
Jakob von Raumer 2025-06-02 22:11:59 +02:00 • committed by GitHub
parent fcc97fe49f
commit 3452a8a2e5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Data/BitVec/Lemmas.lean
View file

@ -2974,7 +2974,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
extractLsb' start len (xhi ++ xlo) =
if hstart : start < w
then
if hlen : start + len < w
if hlen : start + len ≤ w
then extractLsb' start len xlo
else
(((extractLsb' (start - w) (len - (w - start)) xhi) ++
@ -2983,7 +2983,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
extractLsb' (start - w) len xhi := by
by_cases hstart : start < w
· simp only [hstart, ↓reduceDIte]
by_cases hlen : start + len < w
by_cases hlen : start + len ≤ w
· simp only [hlen, ↓reduceDIte]
ext i hi
simp only [getElem_extractLsb', getLsbD_append, ite_eq_left_iff, Nat.not_lt]
@ -3006,11 +3006,14 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
/-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
the bits from `xlo` when `start + len` is within `xlo`.
-/
theorem extractLsb'_append_eq_of_lt {v w} {xhi : BitVec v} {xlo : BitVec w}
{start len : Nat} (h : start + len < w) :
theorem extractLsb'_append_eq_of_add_le {v w} {xhi : BitVec v} {xlo : BitVec w}
{start len : Nat} (h : start + len ≤ w) :
extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo := by
simp [extractLsb'_append_eq_ite, h]
omega
simp only [extractLsb'_append_eq_ite, h, ↓reduceDIte, dite_eq_ite, ite_eq_left_iff, Nat.not_lt]
intro h'
have : len = 0 := by omega
subst this
simp
/-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
the bits from `xhi` when `start` is outside `xlo`.

6
src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
View file

@ -652,18 +652,18 @@ builtin_simproc [bv_normalize] bv_extract_concat
let some start ← getNatValue? startExpr | return .continue
let some len ← getNatValue? lenExpr | return .continue
let some rhsWidth ← getNatValue? rhsWidthExpr | return .continue
if start + len < rhsWidth then
if start + len ≤ rhsWidth then
let expr := mkApp4 (mkConst ``BitVec.extractLsb') rhsWidthExpr startExpr lenExpr rhsExpr
let proof :=
mkApp7
(mkConst ``BitVec.extractLsb'_append_eq_of_lt)
(mkConst ``BitVec.extractLsb'_append_eq_of_add_le)
lhsWidthExpr
rhsWidthExpr
lhsExpr
rhsExpr
startExpr
lenExpr
(← mkDecideProof (← mkLt (toExpr (start + len)) rhsWidthExpr))
(← mkDecideProof (← mkLe (toExpr (start + len)) rhsWidthExpr))
return .visit { expr := expr, proof? := some proof }
else if rhsWidth ≤ start then
let expr := mkApp4 (mkConst ``BitVec.extractLsb') lhsWidthExpr (toExpr (start - rhsWidth)) lenExpr lhsExpr