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 α
⊢ ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
Tactic:
intro n k hnk
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 α
n k : Nat
hnk : k ≥ n
⊢ UInt.getBit (Nat.fold f n 0) k = false
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 α
n k : Nat
hnk : k ≥ n
⊢ UInt.getBit (Nat.fold f n 0) k = false
Tactic:
induction n generalizing k
Proof state after:
case 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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = false

case 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 α
n✝ : Nat
n_ih✝ : ∀ (k : Nat), k ≥ n✝ → UInt.getBit (Nat.fold f n✝ 0) k = false
k : Nat
hnk : k ≥ Nat.succ n✝
⊢ UInt.getBit (Nat.fold f (Nat.succ n✝) 0) k = false
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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = false
Tactic:
case zero => dsimp [Nat.fold]; exact UInt.getBit_zero k
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (Nat.fold f (Nat.succ n) 0) k = false
Tactic:
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:
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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit (Nat.fold f Nat.zero 0) k = false
Tactic:
dsimp [Nat.fold]
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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit 0 k = false
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 α
k : Nat
hnk : k ≥ Nat.zero
⊢ UInt.getBit 0 k = false
Tactic:
exact UInt.getBit_zero k
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (Nat.fold f (Nat.succ n) 0) k = false
Tactic:
dsimp [Nat.fold]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit
      (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) |||
        Nat.fold (fun i y => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat i) = 0) (1 <<< OfNat.ofNat i) ||| y) n 0)
      k =
    false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit
      (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) |||
        Nat.fold (fun i y => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat i) = 0) (1 <<< OfNat.ofNat i) ||| y) n 0)
      k =
    false
Tactic:
rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), 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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n)) k = false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n)) k = false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k = false

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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false
Tactic:
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]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k = false
Tactic:
case false =>
  exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when true (1 <<< OfNat.ofNat n)) k = false
Tactic:
rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false
Tactic:
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]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α) = false
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α) = false
⊢ (decide (k < length α) && decide (k ≥ toNat (OfNat.ofNat n) % length α) &&
      UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α)) =
    false
Tactic:
simp only [this, Bool.and_false]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit 1 (k - toNat (OfNat.ofNat n) % length α) = false
Tactic:
rw [UInt.toNat_ofNat]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
Tactic:
have := calc
  n % 2^length α % length α
    ≤ n % 2^length α := Nat.mod_le ..
  _ ≤ n := Nat.mod_le ..
  _ < n.succ := n.lt_succ_self
  _ ≤ k := hnk
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : n % 2 ^ length α % length α < k
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this : n % 2 ^ length α % length α < k
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
Tactic:
have : k - n % 2^length α % length α > 0 :=
  Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ 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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this✝ : n % 2 ^ length α % length α < k
this : k - n % 2 ^ length α % length α > 0
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
this✝ : n % 2 ^ length α % length α < k
this : k - n % 2 ^ length α % length α > 0
⊢ UInt.getBit 1 (k - n % 2 ^ length α % length α) = false
Tactic:
rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
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 α
n : Nat
h_ind : ∀ (k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
k : Nat
hnk : k ≥ Nat.succ n
⊢ UInt.getBit (UInt.when false (1 <<< OfNat.ofNat n)) k = false
Tactic:
exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
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
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
have what_is_shown :=
  this (Nat.log2RU $ length α) (Nat.log2RU_lt_self _ ‹0 < 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
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
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
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
Tactic:
apply Nat.bitext
Proof state after:
case a
α : 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
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
⊢ ∀ (i_1 : Nat), Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) i_1 = Nat.getBit i i_1