Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
⊢ UInt.getBit (UInt.lsb a)
      (toNat
        (Nat.fold
          (fun n x => UInt.when (decide ¬UInt.lsb a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
cases UInt.lsb_singleton a ha with | intro i hi =>
generalize UInt.lsb a = x at *; clear ‹a≠0› a ‹x≠0›
let f (i : Nat) (y : α) : α := UInt.when (x &&& bitmask (OfNat.ofNat i) ≠ 0) ((1 : α) <<< OfNat.ofNat i) ||| y
conv =>
  change UInt.getBit x (toNat $ Nat.fold f (Nat.log2RU $ length α) 0) = true
have : UInt.getBit x i = true := (decide_eq_true (Eq.refl i) ▸ hi i)
have : i < length α := by
  cases Nat.lt_or_ge i (length α)
  case inl hlt => exact hlt
  case inr hge =>
    have := calc
      false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
      _     = true := ‹_›
    cases this
have : 0 < length α := trans i.zero_le ‹i < length α›
suffices UInt.toNat (Nat.fold f (Nat.log2RU $ length α) 0) = i
  by rw [this]; assumption
have foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false := by
  intro n k hnk
  induction n generalizing k
  case zero => dsimp [Nat.fold]; exact UInt.getBit_zero k
  case succ n h_ind =>
    dsimp [Nat.fold]
    rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), Bool.or_false]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case true =>
      rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
      have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
        rw [UInt.toNat_ofNat]
        have := calc
          n % 2^length α % length α
            ≤ n % 2^length α := Nat.mod_le ..
          _ ≤ n := Nat.mod_le ..
          _ < n.succ := n.lt_succ_self
          _ ≤ k := hnk
        have : k - n % 2^length α % length α > 0 :=
          Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
        rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
      simp only [this, Bool.and_false]
    case false =>
      exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
suffices ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = i.getBit k by
  have what_is_shown :=
    this (Nat.log2RU $ length α) (Nat.log2RU_lt_self _ ‹0 < length α›)
  apply Nat.bitext; intro k
  cases Nat.lt_or_ge k (Nat.log2RU $ length α)
  case a.inl hlt => exact what_is_shown k hlt
  case a.inr hge =>
    unfold UInt.getBit at foldf_high; rw [foldf_high _ _ hge]
    suffices Nat.getBit i k = false
      from Eq.symm this
    apply Nat.getBit_high ?_ k hge
    calc
      i < length α := ‹_›
      _ ≤ 2^Nat.log2RU (length α) := Nat.le_pow2_log2RU_self _
intro n hn k hk
induction n generalizing k
case zero => cases hk
case succ n h_ind =>
  unfold Nat.fold
  conv =>
    lhs; arg 1;
    change UInt.when (x &&& bitmask (OfNat.ofNat n) ≠ 0) ((1 : α) <<< OfNat.ofNat n) ||| Nat.fold f n 0
  rw [UInt.getBit_lor]
  have : n < length α := Nat.lt_of_succ_lt hn
  have : n < 2^length α := trans this (Nat.exp_lt_pow _ .refl)
  cases hk
  case step hlt =>
    rw [h_ind (Nat.lt_of_succ_lt hn) k hlt]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case false => rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
    case true =>
      simp only [
        UInt.when_true_eq, UInt.getBit_shiftLeft, UInt.toNat_ofNat,
        Nat.mod_eq_of_lt ‹n < 2^length α›,
        Nat.mod_eq_of_lt ‹n < length α›
      ]
      rw [decide_eq_false (Nat.not_le_of_lt hlt)]
      simp only [Bool.false_and, Bool.and_false, Bool.false_or]
  case refl =>
    rw [foldf_high n n .refl, Bool.or_false]
    have : ∀ b, UInt.getBit (UInt.when b ((1 : α) <<< OfNat.ofNat n)) n = b := by
      intro b; cases b
      case true =>
        simp only [
          UInt.when_true_eq, UInt.getBit_shiftLeft,
          UInt.toNat_ofNat,
          Nat.mod_eq_of_lt ‹n < 2^length α›,
          Nat.mod_eq_of_lt ‹n < length α›
        ]
        rw [decide_eq_true ‹n < length α›, decide_eq_true (p:=n≥n) .refl]
        rw [Nat.sub_self, UInt.getBit_one, decide_eq_true ‹0 < length α›, decide_eq_true rfl]
        simp only [Bool.true_and]
      case false => rw [UInt.when_false_eq, UInt.getBit_zero]
    rw [this]; clear this
    suffices ∀ y, decide ((x &&& y) ≠ 0) = UInt.getBit y i by
      rw [this]
      have hgetbit := UInt.getBit_bitmask (OfNat.ofNat (α:=α) n) i
      simp only [UInt.toNat_ofNat, Nat.mod_eq_of_lt ‹n < 2^length α›] at hgetbit
      rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
      exact hgetbit ‹n < length α›
    intro y
    cases hyi : UInt.getBit y i
    case true =>
      apply decide_eq_true; intro hcontra
      have := calc
        true = (true && true) := rfl
        _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
        _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
        _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
        _    = false := UInt.getBit_zero i
      cases this
    case false =>
      apply decide_eq_false; apply not_not_intro
      apply UInt.bitext; intro j hj
      rw [UInt.getBit_zero, UInt.getBit_land, hi j]
      if hij : i = j
      then cases hij; rw [hyi, Bool.and_false]
      else rw [decide_eq_false hij, Bool.false_and]
Proof state after:
no goals