internlm/Lean-Github huggingface dataset:
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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Tactic:
cases hk
Proof state after:
case refl
α : 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
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n ||
      UInt.getBit (Nat.fold f n 0) n) =
    Nat.getBit i n

case step
α : 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
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
a✝ : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f 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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Tactic:
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]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n ||
      UInt.getBit (Nat.fold f n 0) n) =
    Nat.getBit i n
Tactic:
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
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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k ||
      UInt.getBit (Nat.fold f n 0) k) =
    Nat.getBit i k
Tactic:
rw [h_ind (Nat.lt_of_succ_lt hn) k hlt]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k || Nat.getBit i 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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) =
    Nat.getBit i k
Tactic:
cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
Proof state after:
case false
α : 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
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k

case true
α : 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
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k || Nat.getBit i 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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
case false => rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
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]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
rw [UInt.when_false_eq, UInt.getBit_zero, Bool.false_or]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k || Nat.getBit i k) = Nat.getBit i k
Tactic:
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 α›
]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && decide (k ≥ n) && UInt.getBit 1 (k - n) || Nat.getBit i 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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && decide (k ≥ n) && UInt.getBit 1 (k - n) || Nat.getBit i k) = Nat.getBit i k
Tactic:
rw [decide_eq_false (Nat.not_le_of_lt hlt)]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && false && UInt.getBit 1 (k - n) || Nat.getBit i 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
n : Nat
h_ind : 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
this✝ : n < length α
this : n < 2 ^ length α
hlt : Nat.le (Nat.succ k) n
⊢ (decide (k < length α) && false && UInt.getBit 1 (k - n) || Nat.getBit i k) = Nat.getBit i k
Tactic:
simp only [Bool.false_and, Bool.and_false, Bool.false_or]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
⊢ (UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n ||
      UInt.getBit (Nat.fold f n 0) n) =
    Nat.getBit i n
Tactic:
rw [foldf_high n n .refl, Bool.or_false]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n
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
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n
Tactic:
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]
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n
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
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ UInt.getBit (UInt.when (decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n)) n = Nat.getBit i n
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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n
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
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (b : Bool), UInt.getBit (UInt.when b (1 <<< OfNat.ofNat n)) n = b
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n
Tactic:
clear 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 α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
⊢ decide (x &&& bitmask (OfNat.ofNat n) ≠ 0) = Nat.getBit i n