lt_of_testBit — Mathlib

English

If at position i a_n has 0 and b_n has 1, and all higher positions agree, then n < m.

Русский

Если в позиции i у n бит равен 0, у m равен 1, и во всех более старших позициях биты совпадают, то n < m.

LaTeX

$$$\forall n\,m\,i\; (testBit(n,i)=\text{false}) \rightarrow (testBit(m,i)=\text{true}) \rightarrow (\forall j, i

Lean4

theorem lt_of_testBit {n m : ℕ} (i : ℕ) (hn : testBit n i = false) (hm : testBit m i = true)
    (hnm : ∀ j, i < j → testBit n j = testBit m j) : n < m := by
  induction n using Nat.binaryRec generalizing i m with
  | zero =>
    rw [Nat.pos_iff_ne_zero]
    rintro rfl
    simp at hm
  | bit b n hn' =>
    induction m using Nat.binaryRec generalizing i with
    | zero => exact False.elim (Bool.false_ne_true ((zero_testBit i).symm.trans hm))
    | bit b' m hm' =>
      by_cases hi : i = 0
      · subst hi
        simp only [testBit_bit_zero] at hn hm
        have : n = m :=
          eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1 <;> rw [testBit_bit_succ]
        rw [hn, hm, this, bit_false, bit_true]
        exact Nat.lt_succ_self _
      · obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
        simp only [testBit_bit_succ] at hn hm
        have := hn' _ hn hm fun j hj => by convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_bit_succ]
        exact bit_lt_bit b b' this

Похожие утверждения