internlm/Lean-Github huggingface dataset:
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n % 2 ^ length α = n
this : 1 % 2 ^ length α = 1
⊢ n % 2 ^ length α + 1 % 2 ^ length α = n + 1
Tactic:
rw [‹n % 2^length α = n›, ‹1 % 2^length α = 1›]
Proof state after:
no goals
Theorem: UInt.ctz_eq_ctz'
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
this✝ : n < length α
this : toNat (OfNat.ofNat n) + toNat 1 = n + 1
⊢ y <<< (OfNat.ofNat n + 1) = y <<< OfNat.ofNat (n + 1)
Tactic:
rw [UInt.ofNat_add]
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
⊢ a ≠ 0 → UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true
Tactic:
intro ha
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
⊢ UInt.getBit (UInt.lsb a) (toNat (UInt.ctz a)) = true
Tactic:
have : UInt.lsb a ≠ 0 := λ h => absurd (UInt.eq_zero_of_lsb_eq_zero a h) ha
Proof state after:
α : 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 (UInt.ctz a)) = true
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 (UInt.ctz a)) = true
Tactic:
rw [UInt.ctz_eq_ctz']
Proof state after:
α : 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 (UInt.ctz' a)) = true
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 (UInt.ctz' a)) = true
Tactic:
dsimp [UInt.ctz']
Proof state after:
α : 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 α)) (UInt.when (decide (UInt.lsb a = 0)) (OfNat.ofNat (length α))))) =
    true
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 α)) (UInt.when (decide (UInt.lsb a = 0)) (OfNat.ofNat (length α))))) =
    true
Tactic:
rw [decide_eq_false this, UInt.when_false_eq]
Proof state after:
α : 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
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
this : UInt.lsb a ≠ 0
i : Nat
hi : ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i = j)
⊢ 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:
generalize UInt.lsb a = x at *
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
i : Nat
x : α
this : x ≠ 0
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
ha : a ≠ 0
i : Nat
x : α
this : x ≠ 0
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
clear ‹a≠0› a ‹x≠0›
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
let f (i : Nat) (y : α) : α := UInt.when (x &&& bitmask (OfNat.ofNat i) ≠ 0) ((1 : α) <<< OfNat.ofNat i) ||| y
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
Tactic:
conv =>
  change UInt.getBit x (toNat $ Nat.fold f (Nat.log2RU $ length α) 0) = true
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
have : UInt.getBit x i = true := (decide_eq_true (Eq.refl i) ▸ hi i)
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
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
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝ : UInt.getBit x i = true
this : i < length α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝ : UInt.getBit x i = true
this : i < length α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
have : 0 < length α := trans i.zero_le ‹i < length α›
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
suffices UInt.toNat (Nat.fold f (Nat.log2RU $ length α) 0) = i
  by rw [this]; assumption
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
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
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
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 _
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
⊢ ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
⊢ ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
Tactic:
intro n hn k hk
Proof state after:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
hn : n < length α
k : Nat
hk : k < n
⊢ UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
hn : n < length α
k : Nat
hk : k < n
⊢ UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
Tactic:
induction n generalizing k
Proof state after:
case intro.zero
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
hn : Nat.zero < length α
k : Nat
hk : k < Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = Nat.getBit i k

case intro.succ
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n✝ : Nat
n_ih✝ : n✝ < length α → ∀ (k : Nat), k < n✝ → UInt.getBit (Nat.fold f n✝ 0) k = Nat.getBit i k
hn : Nat.succ n✝ < length α
k : Nat
hk : k < Nat.succ n✝
⊢ UInt.getBit (Nat.fold f (Nat.succ n✝) 0) k = Nat.getBit i k
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
hn : Nat.zero < length α
k : Nat
hk : k < Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = Nat.getBit i k
Tactic:
case zero => cases hk
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
⊢ i < length α
Tactic:
cases Nat.lt_or_ge i (length α)
Proof state after:
case inl
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
h✝ : i < length α
⊢ i < length α

case inr
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
h✝ : i ≥ length α
⊢ i < length α
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
hlt : i < length α
⊢ i < length α
Tactic:
case inl hlt => exact hlt
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
hge : i ≥ length α
⊢ i < length α
Tactic:
case inr hge =>
  have := calc
    false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
    _     = true := ‹_›
  cases this
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
hlt : i < length α
⊢ i < length α
Tactic:
exact hlt
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this : UInt.getBit x i = true
hge : i ≥ length α
⊢ i < length α
Tactic:
have := calc
  false = UInt.getBit x i := (UInt.getBit_high x i hge).symm
  _     = true := ‹_›
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝ : UInt.getBit x i = true
hge : i ≥ length α
this : false = true
⊢ i < length α
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝ : UInt.getBit x i = true
hge : i ≥ length α
this : false = true
⊢ i < length α
Tactic:
cases this
Proof state after:
no goals
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
this : toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true
Tactic:
rw [this]
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
this : toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
⊢ UInt.getBit x i = true
Theorem: UInt.getBit_lsb_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
this : toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
⊢ UInt.getBit x i = true
Tactic:
assumption
Proof state after:
no goals