English
The cast commutes with right shift: (m >>> n) cast equals cast(m) right-shifted by n.
Русский
Приведение коммутирует с побитовым сдвигом вправо: cast(m >>> n) = cast(m) >> n.
LaTeX
$$$\mathrm{castNum}(\mathrm{shiftr}\, m \\text{ by } n) = (m : \mathbb{Z}) \\text{shiftRight } n$$$
Lean4
@[simp, norm_cast]
theorem castNum_shiftRight (m : Num) (n : Nat) : ↑(m >>> n) = (m : ℕ) >>> (n : ℕ) :=
by
obtain - | m := m <;> dsimp only [← shiftr_eq_shiftRight, shiftr]
· symm
apply Nat.zero_shiftRight
induction n generalizing m with
| zero => cases m <;> rfl
| succ n IH => ?_
have hdiv2 : ∀ m, Nat.div2 (m + m) = m := by intro; rw [Nat.div2_val]; omega
obtain - | m | m := m <;> dsimp only [PosNum.shiftr, ← PosNum.shiftr_eq_shiftRight]
· rw [Nat.shiftRight_eq_div_pow]
symm
apply Nat.div_eq_of_lt
simp
· trans
· apply IH
change Nat.shiftRight m n = Nat.shiftRight (m + m + 1) (n + 1)
rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
apply congr_arg fun x => Nat.shiftRight x n
simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]
· trans
· apply IH
change Nat.shiftRight m n = Nat.shiftRight (m + m) (n + 1)
rw [add_comm n 1, @Nat.shiftRight_eq _ (1 + n), Nat.shiftRight_add]
apply congr_arg fun x => Nat.shiftRight x n
simp [-add_assoc, Nat.shiftRight_succ, Nat.shiftRight_zero, ← Nat.div2_val, hdiv2]
