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 α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
this : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = (decide (i < length α) && Nat.getBit i n)
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
Tactic:
rw [decide_eq_true ‹i < length α›, Bool.true_and] at hgetbit
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 : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = 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 : ∀ (y : α), decide (x &&& y ≠ 0) = UInt.getBit y i
hgetbit : n < length α → UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
⊢ UInt.getBit (bitmask (OfNat.ofNat n)) i = Nat.getBit i n
Tactic:
exact hgetbit ‹n < length α›
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 α
y : α
hyi : UInt.getBit y i = true
⊢ decide (x &&& y ≠ 0) = true
Tactic:
apply decide_eq_true
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
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 α
y : α
hyi : UInt.getBit y i = true
⊢ x &&& y ≠ 0
Theorem: UInt.getBit_lsb_ctz
Proof state before:
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
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 α
y : α
hyi : UInt.getBit y i = true
⊢ x &&& y ≠ 0
Tactic:
intro hcontra
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
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ False
Theorem: UInt.getBit_lsb_ctz
Proof state before:
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
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ False
Tactic:
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
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
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
this : true = false
⊢ False
Theorem: UInt.getBit_lsb_ctz
Proof state before:
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
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
this : true = false
⊢ False
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 α
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ (true && true) = (UInt.getBit x i && UInt.getBit y i)
Tactic:
rw [hi i, decide_eq_true rfl, hyi]
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ (UInt.getBit x i && UInt.getBit y i) = UInt.getBit (x &&& y) i
Tactic:
rw [UInt.getBit_land]
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 α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ UInt.getBit (x &&& y) i = UInt.getBit 0 i
Tactic:
rw [hcontra]
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 α
y : α
hyi : UInt.getBit y i = false
⊢ decide (x &&& y ≠ 0) = false
Tactic:
apply decide_eq_false
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
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 α
y : α
hyi : UInt.getBit y i = false
⊢ ¬x &&& y ≠ 0
Theorem: UInt.getBit_lsb_ctz
Proof state before:
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
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 α
y : α
hyi : UInt.getBit y i = false
⊢ ¬x &&& y ≠ 0
Tactic:
apply not_not_intro
Proof state after:
case a.h
α : 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 α
y : α
hyi : UInt.getBit y i = false
⊢ x &&& y = 0
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case a.h
α : 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 α
y : α
hyi : UInt.getBit y i = false
⊢ x &&& y = 0
Tactic:
apply UInt.bitext
Proof state after:
case a.h.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
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 α
y : α
hyi : UInt.getBit y i = false
⊢ ∀ (i : Nat), i < length α → UInt.getBit (x &&& y) i = UInt.getBit 0 i
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case a.h.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
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 α
y : α
hyi : UInt.getBit y i = false
⊢ ∀ (i : Nat), i < length α → UInt.getBit (x &&& y) i = UInt.getBit 0 i
Tactic:
intro j hj
Proof state after:
case a.h.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
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 α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ UInt.getBit (x &&& y) j = UInt.getBit 0 j
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case a.h.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
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 α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ UInt.getBit (x &&& y) j = UInt.getBit 0 j
Tactic:
rw [UInt.getBit_zero, UInt.getBit_land, hi j]
Proof state after:
case a.h.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
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 α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ (decide (i = j) && UInt.getBit y j) = false
Theorem: UInt.getBit_lsb_ctz
Proof state before:
case a.h.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
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 α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
⊢ (decide (i = j) && UInt.getBit y j) = false
Tactic:
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 α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
hij : i = j
⊢ (decide (i = j) && UInt.getBit y j) = false
Tactic:
cases hij
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 α
y : α
hyi : UInt.getBit y i = false
hj : i < length α
⊢ (decide (i = i) && UInt.getBit y i) = false
Theorem: UInt.getBit_lsb_ctz
Proof state before:
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 α
y : α
hyi : UInt.getBit y i = false
hj : i < length α
⊢ (decide (i = i) && UInt.getBit y i) = false
Tactic:
rw [hyi, 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 α
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 α
y : α
hyi : UInt.getBit y i = false
j : Nat
hj : j < length α
hij : ¬i = j
⊢ (decide (i = j) && UInt.getBit y j) = false
Tactic:
rw [decide_eq_false hij, Bool.false_and]
Proof state after:
no goals
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
if ha : a = 0
then intros; rw [ha, UInt.getBit_zero]
else
  have : ∃ i₀, ∀ j, UInt.getBit (UInt.lsb a) j = decide (i₀=j) := UInt.lsb_singleton a ha
  cases this with | intro i₀ hi₀ =>
  have : UInt.getBit (UInt.lsb a) i₀ = true := decide_eq_true (Eq.refl i₀) ▸ (hi₀ i₀)
  have ⟨_, (halow: ∀ j, j < i₀ → UInt.getBit a j = false)⟩ :=
    (UInt.getBit_lsb_iff a).mp this
  suffices UInt.toNat (UInt.ctz a) = i₀ by
    rw [this]; intro hi; exact halow _ hi
  have : decide (i₀ = toNat (UInt.ctz a)) = true :=
    hi₀ _ ▸ UInt.getBit_lsb_ctz a ha
  apply Eq.symm; exact of_decide_eq_true this
Proof state after:
no goals
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : a = 0
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
intros
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : a = 0
a✝ : i < toNat (UInt.ctz a)
⊢ UInt.getBit a i = false
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : a = 0
a✝ : i < toNat (UInt.ctz a)
⊢ UInt.getBit a i = false
Tactic:
rw [ha, UInt.getBit_zero]
Proof state after:
no goals
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
have : ∃ i₀, ∀ j, UInt.getBit (UInt.lsb a) j = decide (i₀=j) := UInt.lsb_singleton a ha
Proof state after:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
this : ∃ i₀, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Theorem: UInt.getBit_lsb_of_lt_ctz
Proof state before:
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
i : Nat
ha : ¬a = 0
this : ∃ i₀, ∀ (j : Nat), UInt.getBit (UInt.lsb a) j = decide (i₀ = j)
⊢ i < toNat (UInt.ctz a) → UInt.getBit a i = false
Tactic:
cases this with | intro i₀ hi₀ =>
have : UInt.getBit (UInt.lsb a) i₀ = true := decide_eq_true (Eq.refl i₀) ▸ (hi₀ i₀)
have ⟨_, (halow: ∀ j, j < i₀ → UInt.getBit a j = false)⟩ :=
  (UInt.getBit_lsb_iff a).mp this
suffices UInt.toNat (UInt.ctz a) = i₀ by
  rw [this]; intro hi; exact halow _ hi
have : decide (i₀ = toNat (UInt.ctz a)) = true :=
  hi₀ _ ▸ UInt.getBit_lsb_ctz a ha
apply Eq.symm; exact of_decide_eq_true this
Proof state after:
no goals