feat: simprocs for applying shiftLeft_shiftLeft and shiftRight_shiftRight

only when the shifts are literals

src/Init/Data/BitVec/Lemmas.lean

@@ -705,7 +705,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsb_append, cond_eq_if]
   split <;> simp [*]
 
-theorem shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) :
+theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
     (x >>> n) >>> m = x >>> (n + m) := by
   ext i
   simp [Nat.add_assoc n m i]

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -191,8 +191,6 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have test_false := p _ i_ge_n
   simp only [test_true] at test_false
 
-/-! ### testBit -/
-
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with
   | zero =>
@@ -236,7 +234,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [Nat.pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -260,7 +258,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
             exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
       simp only [hyp y y_lt_x]
       if i_lt_j : i < j then
-        rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
+        rw [Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
       else
         simp [i_lt_j]
 

src/Init/Data/Nat/Lemmas.lean

@@ -478,6 +478,7 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b
 
 theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by
   rw [succ_mul, mul_succ]; rfl
+
 theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by
   match k with
   | 0 =>

src/Init/Data/Nat/Linear.lean

@@ -714,10 +714,4 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
   simp [Expr.toNormPoly, Poly.norm] at h
   assumption
 
-end Linear
-
-def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α := by
-  simp_arith at h₁
-  exact h₂ h₁
-
-end Nat
+end Nat.Linear

src/Lean/Meta/Tactic/Cases.lean

@@ -200,7 +200,7 @@ private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name
     { ctorName           := ctorName,
       toInductionSubgoal := s }
 
-partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
+partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := do
   if numEqs == 0 then
     return some (mvarId, subst)
   else

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -8,6 +8,7 @@ import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Lemmas
 
 namespace BitVec
 open Lean Meta Simp
@@ -78,6 +79,16 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate
   let some i ← Nat.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op v.value i)
 
+/--
+Helper function for reducing `x <<< i` and `x >>> i` where `i` is a bitvector literal,
+into one that is a natural number literal.
+-/
+@[inline] def reduceShiftWithBitVecLit (declName : Name) (e : Expr) : SimpM DStep := do
+  unless e.isAppOfArity declName 6 do return .continue
+  let v := e.appFn!.appArg!
+  let some i ← fromExpr? e.appArg! | return .continue
+  return .visit (← mkAppM declName #[v, toExpr i.value.toNat])
+
 /--
 Helper function for reducing bitvector predicates.
 -/
@@ -158,9 +169,15 @@ builtin_dsimproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
 /-- Simplification procedure for shift left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
   reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/
+builtin_dsimproc [simp, seval] reduceHShiftLeft' ((_ <<< (_ : BitVec _) : BitVec _)) :=
+  reduceShiftWithBitVecLit ``HShiftLeft.hShiftLeft
 /-- Simplification procedure for shift right on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) :=
   reduceShift ``HShiftRight.hShiftRight 6 (· >>> ·)
+/-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/
+builtin_dsimproc [simp, seval] reduceHShiftRight' ((_ >>> (_ : BitVec _) : BitVec _)) :=
+  reduceShiftWithBitVecLit ``HShiftRight.hShiftRight
 /-- Simplification procedure for rotate left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) :=
   reduceShift ``BitVec.rotateLeft 3 BitVec.rotateLeft
@@ -287,4 +304,25 @@ builtin_dsimproc [simp, seval] reduceBitVecToFin (BitVec.toFin _)  := fun e => d
   let some ⟨_, v⟩ ← getBitVecValue? v | return .continue
   return .done <| toExpr v.toFin
 
+/--
+Helper function for reducing `(x <<< i) <<< j` (and `(x >>> i) >>> j`) where `i` and `j` are
+natural number literals.
+-/
+@[inline] def reduceShiftShift (declName : Name) (thmName : Name) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName 6 do return .continue
+  let aux := e.appFn!.appArg!
+  let some i ← Nat.fromExpr? e.appArg! | return .continue
+  unless aux.isAppOfArity declName 6 do return .continue
+  let x := aux.appFn!.appArg!
+  let some j ← Nat.fromExpr? aux.appArg! | return .continue
+  let i_add_j := toExpr (i + j)
+  let expr ← mkAppM declName #[x, i_add_j]
+  let proof ← mkAppM thmName #[x, aux.appArg!, e.appArg!]
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc reduceShiftLeftShiftLeft (((_ <<< _ : BitVec _) <<< _ : BitVec _)) :=
+  reduceShiftShift ``HShiftLeft.hShiftLeft ``shiftLeft_shiftLeft
+builtin_simproc reduceShiftRightShiftRight (((_ >>> _ : BitVec _) >>> _ : BitVec _)) :=
+  reduceShiftShift ``HShiftRight.hShiftRight ``shiftRight_shiftRight
+
 end BitVec

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -21,11 +21,6 @@ structure UnifyEqResult where
   subst     : FVarSubst
   numNewEqs : Nat := 0
 
-private def toOffset? (e : Expr) : MetaM (Option (Expr × Nat)) := do
-  match (← evalNat e) with
-  | some k => return some (mkNatLit 0, k)
-  | none => isOffset? e
-
 /--
   Helper method for methods such as `Cases.unifyEqs?`.
   Given the given goal `mvarId` containing the local hypothesis `eqFVarId`, it performs the following operations:
@@ -74,30 +69,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
             return none -- this alternative has been solved
           else
             throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
-        /- Special support for offset equalities -/
-        let injectionOffset? (a b : Expr) := do
-          unless (← getEnv).contains ``Nat.elimOffset do return none
-          let some (xa, ka) ← toOffset? a | return none
-          let some (xb, kb) ← toOffset? b | return none
-          if ka == 0 || kb == 0 then return none -- use default noConfusion
-          let (x, y, k) ← if ka < kb then
-            pure (xa, (← mkAdd xb (mkNatLit (kb - ka))), ka)
-          else if ka = kb then
-            pure (xa, xb, ka)
-          else
-            pure ((← mkAdd xa (mkNatLit (ka - kb))), xb, kb)
-          let target ← mvarId.getType
-          let u ← getLevel target
-          let newTarget ← mkArrow (← mkEq x y) target
-          let tag ← mvarId.getTag
-          let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
-          let val := mkAppN (mkConst ``Nat.elimOffset [u]) #[target, x, y, mkNatLit k, eqDecl.toExpr, newMVar]
-          mvarId.assign val
-          let mvarId ← newMVar.mvarId!.tryClear eqDecl.fvarId
-          return some mvarId
         let rec injection (a b : Expr) := do
-          if let some mvarId ← injectionOffset? a b then
-            return some { mvarId, numNewEqs := 1, subst }
           if (← isConstructorApp a <&&> isConstructorApp b) then
             /- ctor_i ... = ctor_j ... -/
             match (← injectionCore mvarId eqFVarId) with

tests/lean/run/4219.lean

@@ -1,9 +0,0 @@
-example (h : 2000 = 2001) : False := by
-  cases h
-
-example (h : 20000 = 20001) : False := by
-  cases h
-
-example (h : x + 20000 = 20001) : x = 1 := by
-  cases h
-  rfl

tests/lean/run/bitvec_simproc.lean

@@ -113,3 +113,27 @@ example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ1019#10 = x; assumption
 example (h : 5#10 = x) : -signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ5#10 = x; assumption
+example (h : 40#32 = b) : 10#32 <<< 2#32 = b := by
+  simp; guard_target =ₛ 40#32 = b; assumption
+example (h : 3#32 = b) : 12#32 >>> 2#32 = b := by
+  simp; guard_target =ₛ 3#32 = b; assumption
+example (a : BitVec 32) (h : a >>> 2 = b) : a >>> 2#32 = b := by
+  simp; guard_target =ₛ a >>> 2 = b; assumption
+example (a : BitVec 32) (h : a <<< 2 = b) : a <<< 2#32 = b := by
+  simp; guard_target =ₛ a <<< 2 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1#32) <<< 2#32 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1) <<< 2#32 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1) <<< 2 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a <<< 3 = b) : (a <<< 1#32) <<< 2 = b := by
+  simp; guard_target =ₛ a <<< 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1#32) >>> 2#32 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1) >>> 2#32 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1) >>> 2 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption
+example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1#32) >>> 2 = b := by
+  simp; guard_target =ₛ a >>> 3 = b; assumption