From 3452a8a2e5744b9efb4ed1a4877e2bc0b169e210 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Mon, 2 Jun 2025 22:11:59 +0200
Subject: [PATCH] feat: improve BitVec.extractLsb' lemma on appended vectors
 (#8585)

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`.
---
 src/Init/Data/BitVec/Lemmas.lean                  | 15 +++++++++------
 .../BVDecide/Frontend/Normalize/Simproc.lean      |  6 +++---
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5b167259e6..79f0d946bc 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -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`.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index 643708bc89..7e9befd989 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -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