-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
    (x.sshiftRight s) = ~~~((~~~x) >>> s)

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) / 2 ^ s < 2 ^ (w + 1)

Tactic:
apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega)

Result:
no goals

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (BitVec.ofInt (w + 1) ((if 2 * x.toNat < 2 ^ (w + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (w + 1))) >>> s)).toNat =
    (~~~(~~~x >>> s)).toNat

Tactic:
simp only [hxbound, ↓reduceIte, toNat_ofInt, toNat_not, toNat_ushiftRight]

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ ((↑x.toNat - ↑(2 ^ (w + 1))) >>> s % ↑(2 ^ (w + 1))).toNat = 2 ^ (w + 1) - 1 - (2 ^ (w + 1) - 1 - x.toNat) >>> s

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
⊢ (BitVec.ofInt (w + 1) ((if 2 * x.toNat < 2 ^ (w + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (w + 1))) >>> s)).toNat =
    (~~~(~~~x >>> s)).toNat

Tactic:
have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := BitVec.msb_eq_true_iff_two_mul_ge.mp h

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : 2 * x.toNat ≥ 2 ^ (w + 1)
⊢ (BitVec.ofInt (w + 1) ((if 2 * x.toNat < 2 ^ (w + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (w + 1))) >>> s)).toNat =
    (~~~(~~~x >>> s)).toNat

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ 2 ^ (w + 1) - ((2 ^ (w + 1) - 1 - x.toNat) >>> s + 1) = 2 ^ (w + 1) - 1 - (2 ^ (w + 1) - 1 - x.toNat) >>> s

case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) >>> s < 2 ^ (w + 1)

Tactic:
omega

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) >>> s < 2 ^ (w + 1)

Proof state:
w : Nat
x : BitVec w
s : Nat
h : x.msb = true
⊢ x.sshiftRight s = ~~~(~~~x >>> s)

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = true
⊢ (x.sshiftRight s).toNat = (~~~(~~~x >>> s)).toNat

Proof state:
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : 2 * x.toNat ≥ 2 ^ (w + 1)
⊢ ¬2 * x.toNat < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
⊢ (x.sshiftRight s).toNat = (~~~(~~~x >>> s)).toNat

Tactic:
rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
⊢ (BitVec.ofInt (w + 1) ((if 2 * x.toNat < 2 ^ (w + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (w + 1))) >>> s)).toNat =
    (~~~(~~~x >>> s)).toNat

Proof state:
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ x.toNat < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ ((↑x.toNat - ↑(2 ^ (w + 1))) >>> s % ↑(2 ^ (w + 1))).toNat = 2 ^ (w + 1) - 1 - (2 ^ (w + 1) - 1 - x.toNat) >>> s

Tactic:
rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (by omega),
    Nat.pred_eq_sub_one, Int.negSucc_shiftRight,
    Int.emod_negSucc, Int.natAbs_ofNat, Nat.succ_eq_add_one,
    Int.subNatNat_of_le (by omega), Int.toNat_ofNat, Nat.mod_eq_of_lt,
    Nat.sub_right_comm]

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ 2 ^ (w + 1) - ((2 ^ (w + 1) - 1 - x.toNat) >>> s + 1) = 2 ^ (w + 1) - 1 - (2 ^ (w + 1) - 1 - x.toNat) >>> s

case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) >>> s < 2 ^ (w + 1)

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : 2 * x.toNat ≥ 2 ^ (w + 1)
⊢ (BitVec.ofInt (w + 1) ((if 2 * x.toNat < 2 ^ (w + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (w + 1))) >>> s)).toNat =
    (~~~(~~~x >>> s)).toNat

Tactic:
replace hxbound : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (BitVec.ofInt (w + 1) ((if 2 * x.toNat < 2 ^ (w + 1) then ↑x.toNat else ↑x.toNat - ↑(2 ^ (w + 1))) >>> s)).toNat =
    (~~~(~~~x >>> s)).toNat

Proof state:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) >>> s < 2 ^ (w + 1)

Tactic:
rw [Nat.shiftRight_eq_div_pow]

Result:
case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) / 2 ^ s < 2 ^ (w + 1)

Proof state:
case a.zero
s : Nat
x : BitVec 0
h : x.msb = true
⊢ (x.sshiftRight s).toNat = (~~~(~~~x >>> s)).toNat

Tactic:
simp [toNat_of_zero_length]

Result:
no goals

Proof state:
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ (2 ^ (w + 1) - x.toNat - 1) >>> s % 2 ^ (w + 1) + 1 ≤ 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = true
⊢ (x.sshiftRight s).toNat = (~~~(~~~x >>> s)).toNat

Tactic:
rcases w with rfl | w

Result:
case a.zero
s : Nat
x : BitVec 0
h : x.msb = true
⊢ (x.sshiftRight s).toNat = (~~~(~~~x >>> s)).toNat

case a.succ
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
⊢ (x.sshiftRight s).toNat = (~~~(~~~x >>> s)).toNat

Proof state:
s w : Nat
x : BitVec (w + 1)
h : x.msb = true
hxbound : ¬2 * x.toNat < 2 ^ (w + 1)
⊢ 2 ^ (w + 1) - x.toNat - 1 < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals