internlm/Lean-Github huggingface dataset:
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != Nat.getBit ((k >>> toNat n &&& 1) <<< k % 2 ^ length α) i) = ?m.37836
Tactic:
have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
  calc (k >>> toNat n &&& 1) <<< k
    _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
    _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
    _ = 2^k := Nat.one_mul _
    _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝² : k < 2 ^ length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
this : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != Nat.getBit ((k >>> toNat n &&& 1) <<< k % 2 ^ length α) i) = ?m.37836
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ k >>> toNat n &&& 1 ≤ 1
Tactic:
rw [Nat.land_one]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ k >>> toNat n % 2 ≤ 1
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ k >>> toNat n % 2 ≤ 1
Tactic:
exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝² : k < 2 ^ length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
this : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
Tactic:
have : 0 = i-k ↔ i ≤ k :=
  ⟨Nat.le_of_sub_eq_zero ∘ Eq.symm, Eq.symm ∘ Nat.sub_eq_zero_of_le⟩
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
Tactic:
have : (i ≥ k ∧ i ≤ k) ↔ i = k :=
  ⟨λ h => Nat.le_antisymm h.right h.left, λ h => by cases h; exact ⟨Nat.le.refl, Nat.le.refl⟩⟩
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝⁴ : k < 2 ^ length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
this✝¹ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this✝ : 0 = i - k ↔ i ≤ k
this : i ≥ k ∧ i ≤ k ↔ i = k
⊢ (decide (i ≥ k) && (Nat.getBit k (0 + toNat n) && decide (0 = i - k))) = ?m.39484
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝³ : k < 2 ^ length α
this✝² : 2 ^ toNat n < 2 ^ length α
this✝¹ : 1 < 2 ^ length α
this✝ : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
this : 0 = i - k ↔ i ≤ k
h : i = k
⊢ i ≥ k ∧ i ≤ k
Tactic:
cases h
Proof state after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this✝¹ : i < 2 ^ length α
this✝ : (i >>> toNat n &&& 1) <<< i < 2 ^ length α
this : 0 = i - i ↔ i ≤ i
⊢ i ≥ i ∧ i ≤ i
Theorem: UInt.getBit_bitmask
Proof state before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝³ : 2 ^ toNat n < 2 ^ length α
this✝² : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this✝¹ : i < 2 ^ length α
this✝ : (i >>> toNat n &&& 1) <<< i < 2 ^ length α
this : 0 = i - i ↔ i ≤ i
⊢ i ≥ i ∧ i ≤ i
Tactic:
exact ⟨Nat.le.refl, Nat.le.refl⟩
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
rw [decide_eq_true hlt, decide_eq_false (Nat.ne_of_lt hlt), decide_eq_true (Nat.lt_succ_of_lt hlt)]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (true != false && Nat.getBit i (toNat n)) = (true && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hlt : i < k
⊢ (true != false && Nat.getBit i (toNat n)) = (true && Nat.getBit i (toNat n))
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
cases Nat.lt_or_eq_of_le hge
Proof state after:
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
h✝ : k < i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
h✝ : k = i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inl hgt =>
  rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
  rfl
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
heq : k = i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
case inr heq => cases heq; simp
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
rw [decide_eq_false (Nat.not_lt_of_le (Nat.le_of_lt hgt)), decide_eq_false (Nat.ne_of_gt hgt), decide_eq_false (Nat.not_lt_of_le hgt)]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (false != false && Nat.getBit i (toNat n)) = (false && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
hgt : k < i
⊢ (false != false && Nat.getBit i (toNat n)) = (false && Nat.getBit i (toNat n))
Tactic:
rfl
Proof state after:
no goals
Theorem: UInt.getBit_bitmask
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
hge : i ≥ k
heq : k = i
⊢ (decide (i < k) != decide (i = k) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ k) && Nat.getBit i (toNat n))
Tactic:
cases heq
Proof state after:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this : i < 2 ^ length α
hge : i ≥ i
⊢ (decide (i < i) != decide (i = i) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ i) && Nat.getBit i (toNat n))
Theorem: UInt.getBit_bitmask
Proof state before:
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this : i < 2 ^ length α
hge : i ≥ i
⊢ (decide (i < i) != decide (i = i) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ i) && Nat.getBit i (toNat n))
Tactic:
simp
Proof state after:
no goals
Theorem: UInt.maskTable_size
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ Array.size maskTable = Nat.log2RU (length α)
Tactic:
unfold maskTable
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ Array.size (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)) = Nat.log2RU (length α)
Theorem: UInt.maskTable_size
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ Array.size (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)) = Nat.log2RU (length α)
Tactic:
rw [Array.size_ofFn]
Proof state after:
no goals
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
⊢ ∀ (n i : Nat) {x : n < Array.size maskTable}, UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
intro n i h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
have : n < Nat.log2RU (length α) := maskTable_size (α:=α) ▸ h
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this : n < Nat.log2RU (length α)
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this : n < Nat.log2RU (length α)
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
have := calc
  n < Nat.log2RU (length α) := this
  _ ≤ length α := Nat.log2RU_le_self (length α)
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝ : n < Nat.log2RU (length α)
this : n < length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝ : n < Nat.log2RU (length α)
this : n < length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
have := calc
  n < length α := this
  _ < 2^(length α) := Nat.exp_lt_pow (length α) .refl
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
unfold maskTable
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i))[n] i = (decide (i < length α) && Nat.getBit i n)
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i))[n] i = (decide (i < length α) && Nat.getBit i n)
Tactic:
rw [Array.getElem_ofFn', getBit_bitmask (OfNat.ofNat n) i (toNat_ofNat (α:=α) n ▸ (Nat.mod_eq_of_lt ‹n < 2^length α›).symm ▸ ‹_›)]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n))) = (decide (i < length α) && Nat.getBit i n)
Theorem: UInt.maskTable_spec
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n))) = (decide (i < length α) && Nat.getBit i n)
Tactic:
rw [toNat_ofNat (α:=α), Nat.mod_eq_of_lt ‹n < 2^length α›]
Proof state after:
no goals
Theorem: UInt.bitcnt_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
have : bitcnt x = (Prod.fst $ (x,1) |> Fin.foldAll λ (i : Fin (Nat.log2RU (length α))) ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i.1)) + ((x &&& bitmask (OfNat.ofNat i.1)) >>> k), k <<< 1)) := by
  unfold bitcnt; unfold maskTable
  simp only [Array.foldl_ofFn_eq]; rfl
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Theorem: UInt.bitcnt_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
rw [this]
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Theorem: UInt.bitcnt_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
clear this
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Theorem: UInt.bitcnt_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
apply Eq.trans $ congrArg Prod.fst $ Fin.foldAll_comp_val (n:=Nat.log2RU (length α)) (f:=λ (i : Nat) ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i)) + ((x &&& bitmask (OfNat.ofNat i)) >>> k), k <<< 1)) (init:=(x,1))
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Theorem: UInt.bitcnt_eq
Proof state before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
Tactic:
generalize hn : Nat.log2RU (length α) = n
Proof state after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x