internlm/Lean-Github huggingface dataset:
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
this : n / 2 < 2 ^ k
⊢ getBit n i = false
Tactic:
cases hi
Proof state after:
case refl
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false

case step
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
m✝ : Nat
a✝ : Nat.le (succ k) m✝
⊢ getBit n (succ m✝) = false
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false
Tactic:
case refl =>
  dsimp [getBit]
  exact h_ind ‹n/2 < 2^k› k Nat.le.refl
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit n (succ i) = false
Tactic:
case step i hstep =>
  dsimp [getBit]
  exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false
Tactic:
dsimp [getBit]
Proof state after:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit (n / 2) k = false
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit (n / 2) k = false
Tactic:
exact h_ind ‹n/2 < 2^k› k Nat.le.refl
Proof state after:
no goals
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit n (succ i) = false
Tactic:
dsimp [getBit]
Proof state after:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit (n / 2) i = false
Theorem: Nat.getBit_high
Proof state before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit (n / 2) i = false
Tactic:
exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
k i : Nat
⊢ getBit (2 ^ k) i = decide (k = i)
Tactic:
induction i generalizing k
Proof state after:
case zero
k : Nat
⊢ getBit (2 ^ k) zero = decide (k = zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (k : Nat), getBit (2 ^ k) n✝ = decide (k = n✝)
k : Nat
⊢ getBit (2 ^ k) (succ n✝) = decide (k = succ n✝)
Theorem: Nat.getBit_two_pow
Proof state before:
k : Nat
⊢ getBit (2 ^ k) zero = decide (k = zero)
Tactic:
case zero =>
  dsimp [getBit]
  cases k
  case zero => decide
  case succ k => conv => lhs; change decide (2^k*2%2 = 1); simp
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) (succ i) = decide (k = succ i)
Tactic:
case succ i h_ind =>
  dsimp [getBit]
  cases k
  case zero =>
    conv => change getBit 0 i = false
    simp
  case succ k =>
    conv => lhs; arg 1; change 2^k*2/2; simp
    have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
    rw [h_ind, decide_eq_decide.mpr this]
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
k : Nat
⊢ getBit (2 ^ k) zero = decide (k = zero)
Tactic:
dsimp [getBit]
Proof state after:
k : Nat
⊢ decide (2 ^ k % 2 = 1) = decide (k = 0)
Theorem: Nat.getBit_two_pow
Proof state before:
k : Nat
⊢ decide (2 ^ k % 2 = 1) = decide (k = 0)
Tactic:
cases k
Proof state after:
case zero

⊢ decide (2 ^ zero % 2 = 1) = decide (zero = 0)

case succ
n✝ : Nat
⊢ decide (2 ^ succ n✝ % 2 = 1) = decide (succ n✝ = 0)
Theorem: Nat.getBit_two_pow
Proof state before:
⊢ decide (2 ^ zero % 2 = 1) = decide (zero = 0)
Tactic:
case zero => decide
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
k : Nat
⊢ decide (2 ^ succ k % 2 = 1) = decide (succ k = 0)
Tactic:
case succ k => conv => lhs; change decide (2^k*2%2 = 1); simp
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
⊢ decide (2 ^ zero % 2 = 1) = decide (zero = 0)
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
k : Nat
⊢ decide (2 ^ succ k % 2 = 1) = decide (succ k = 0)
Tactic:
conv => lhs; change decide (2^k*2%2 = 1); simp
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) (succ i) = decide (k = succ i)
Tactic:
dsimp [getBit]
Proof state after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k / 2) i = decide (k = succ i)
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k / 2) i = decide (k = succ i)
Tactic:
cases k
Proof state after:
case zero
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)

case succ
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
n✝ : Nat
⊢ getBit (2 ^ succ n✝ / 2) i = decide (succ n✝ = succ i)
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)
Tactic:
case zero =>
  conv => change getBit 0 i = false
  simp
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ succ k / 2) i = decide (succ k = succ i)
Tactic:
case succ k =>
  conv => lhs; arg 1; change 2^k*2/2; simp
  have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
  rw [h_ind, decide_eq_decide.mpr this]
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)
Tactic:
conv => change getBit 0 i = false
Proof state after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit 0 i = false
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit 0 i = false
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ succ k / 2) i = decide (succ k = succ i)
Tactic:
conv => lhs; arg 1; change 2^k*2/2; simp
Proof state after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) i = decide (succ k = succ i)
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) i = decide (succ k = succ i)
Tactic:
have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
Proof state after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
this : k = i ↔ succ k = succ i
⊢ getBit (2 ^ k) i = decide (succ k = succ i)
Theorem: Nat.getBit_two_pow
Proof state before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
this : k = i ↔ succ k = succ i
⊢ getBit (2 ^ k) i = decide (succ k = succ i)
Tactic:
rw [h_ind, decide_eq_decide.mpr this]
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k i : Nat
⊢ getBit (2 ^ k - 1) i = decide (i < k)
Tactic:
induction k generalizing i
Proof state after:
case zero
i : Nat
⊢ getBit (2 ^ zero - 1) i = decide (i < zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (i : Nat), getBit (2 ^ n✝ - 1) i = decide (i < n✝)
i : Nat
⊢ getBit (2 ^ succ n✝ - 1) i = decide (i < succ n✝)
Theorem: Nat.getBit_pred_two_pow
Proof state before:
i : Nat
⊢ getBit (2 ^ zero - 1) i = decide (i < zero)
Tactic:
case zero =>
  conv => lhs; rw [Nat.pow_zero]; change getBit 0 i; rw [Nat.zero_getBit]
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) i = decide (i < succ k)
Tactic:
case succ k h_ind =>
  cases i
  case zero =>
    dsimp [Nat.getBit]; apply decide_eq_decide.mpr
    have := calc
      (2^k.succ - 1) % 2
        = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
      _ = (2-1)%2 :=
        Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
      _ = 1 := rfl
    rw [this]
    constructor <;> intros; exact k.zero_lt_succ; rfl
  case succ i =>
    have := calc
      (2^k.succ - 1).getBit i.succ
        = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
      _ = (2^k - 1).getBit i :=
        by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
    rw [this, h_ind]; apply decide_eq_decide.mpr
    exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
i : Nat
⊢ getBit (2 ^ zero - 1) i = decide (i < zero)
Tactic:
conv => lhs; rw [Nat.pow_zero]; change getBit 0 i; rw [Nat.zero_getBit]
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) i = decide (i < succ k)
Tactic:
cases i
Proof state after:
case zero
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)

case succ
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
n✝ : Nat
⊢ getBit (2 ^ succ k - 1) (succ n✝) = decide (succ n✝ < succ k)
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)
Tactic:
case zero =>
  dsimp [Nat.getBit]; apply decide_eq_decide.mpr
  have := calc
    (2^k.succ - 1) % 2
      = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
    _ = (2-1)%2 :=
      Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
    _ = 1 := rfl
  rw [this]
  constructor <;> intros; exact k.zero_lt_succ; rfl
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Tactic:
case succ i =>
  have := calc
    (2^k.succ - 1).getBit i.succ
      = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
    _ = (2^k - 1).getBit i :=
      by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
  rw [this, h_ind]; apply decide_eq_decide.mpr
  exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)
Tactic:
dsimp [Nat.getBit]
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ decide ((2 ^ succ k - 1) % 2 = 1) = decide (0 < succ k)
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ decide ((2 ^ succ k - 1) % 2 = 1) = decide (0 < succ k)
Tactic:
apply decide_eq_decide.mpr
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
Tactic:
have := calc
  (2^k.succ - 1) % 2
    = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
  _ = (2-1)%2 :=
    Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
  _ = 1 := rfl
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
Tactic:
rw [this]
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ 1 = 1 ↔ 0 < succ k
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ 1 = 1 ↔ 0 < succ k
Tactic:
constructor <;> intros
Proof state after:
case mp
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 1 = 1
⊢ 0 < succ k

case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1
Theorem: Nat.getBit_pred_two_pow
Proof state before:
case mp
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 1 = 1
⊢ 0 < succ k

case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1
Tactic:
exact k.zero_lt_succ
Proof state after:
case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1
Theorem: Nat.getBit_pred_two_pow
Proof state before:
case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = (2 ^ k * 2 - 1) % 2
Tactic:
rw [Nat.pow_succ]
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Tactic:
have := calc
  (2^k.succ - 1).getBit i.succ
    = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
  _ = (2^k - 1).getBit i :=
    by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Tactic:
rw [this, h_ind]
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ decide (i < k) = decide (succ i < succ k)
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ decide (i < k) = decide (succ i < succ k)
Tactic:
apply decide_eq_decide.mpr
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ i < k ↔ succ i < succ k
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ i < k ↔ succ i < succ k
Tactic:
exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) (succ i) = getBit ((2 ^ k * 2 - 1) / 2) i
Tactic:
rw [Nat.pow_succ, Nat.getBit]
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit ((2 ^ k * 2 - 1) / 2) i = getBit (2 ^ k - 1) i
Tactic:
rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]
Proof state after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ k - succ (0 / 2)) i = getBit (2 ^ k - 1) i
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ k - succ (0 / 2)) i = getBit (2 ^ k - 1) i
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ 2 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.getBit_pred_two_pow
Proof state before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n k i : Nat
⊢ getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
Tactic:
induction i generalizing n k
Proof state after:
case zero
n k : Nat
⊢ getBit (n % 2 ^ k) zero = (decide (zero < k) && getBit n zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n k : Nat), getBit (n % 2 ^ k) n✝ = (decide (n✝ < k) && getBit n n✝)
n k : Nat
⊢ getBit (n % 2 ^ k) (succ n✝) = (decide (succ n✝ < k) && getBit n (succ n✝))
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n k : Nat
⊢ getBit (n % 2 ^ k) zero = (decide (zero < k) && getBit n zero)
Tactic:
case zero =>
  cases k
  case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
  case succ k =>
    conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
    conv => rhs; simp [decide_eq_true k.zero_lt_succ]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ k) (succ i) = (decide (succ i < k) && getBit n (succ i))
Tactic:
case succ i h_ind =>
  cases k
  case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
  case succ k =>
    unfold getBit
    have : i.succ < k.succ ↔ i < k :=
      ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
    rw [decide_eq_decide.mpr this]
    conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
    exact h_ind (n/2) k
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n k : Nat
⊢ getBit (n % 2 ^ k) zero = (decide (zero < k) && getBit n zero)
Tactic:
cases k
Proof state after:
case zero
n : Nat
⊢ getBit (n % 2 ^ zero) zero = (decide (zero < zero) && getBit n zero)

case succ
n n✝ : Nat
⊢ getBit (n % 2 ^ succ n✝) zero = (decide (zero < succ n✝) && getBit n zero)
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n : Nat
⊢ getBit (n % 2 ^ zero) zero = (decide (zero < zero) && getBit n zero)
Tactic:
case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n k : Nat
⊢ getBit (n % 2 ^ succ k) zero = (decide (zero < succ k) && getBit n zero)
Tactic:
case succ k =>
  conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
  conv => rhs; simp [decide_eq_true k.zero_lt_succ]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n : Nat
⊢ getBit (n % 2 ^ zero) zero = (decide (zero < zero) && getBit n zero)
Tactic:
conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n k : Nat
⊢ getBit (n % 2 ^ succ k) zero = (decide (zero < succ k) && getBit n zero)
Tactic:
conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
Proof state after:
n k : Nat
⊢ decide (n % 2 = 1) = (decide (zero < succ k) && getBit n zero)
Theorem: Nat.getBit_mod_two_pow
Proof state before:
n k : Nat
⊢ decide (n % 2 = 1) = (decide (zero < succ k) && getBit n zero)
Tactic:
conv => rhs; simp [decide_eq_true k.zero_lt_succ]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ k) (succ i) = (decide (succ i < k) && getBit n (succ i))
Tactic:
cases k
Proof state after:
case zero
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n : Nat
⊢ getBit (n % 2 ^ zero) (succ i) = (decide (succ i < zero) && getBit n (succ i))

case succ
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n n✝ : Nat
⊢ getBit (n % 2 ^ succ n✝) (succ i) = (decide (succ i < succ n✝) && getBit n (succ i))
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n : Nat
⊢ getBit (n % 2 ^ zero) (succ i) = (decide (succ i < zero) && getBit n (succ i))
Tactic:
case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k) (succ i) = (decide (succ i < succ k) && getBit n (succ i))
Tactic:
case succ k =>
  unfold getBit
  have : i.succ < k.succ ↔ i < k :=
    ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
  rw [decide_eq_decide.mpr this]
  conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
  exact h_ind (n/2) k
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n : Nat
⊢ getBit (n % 2 ^ zero) (succ i) = (decide (succ i < zero) && getBit n (succ i))
Tactic:
conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
Proof state after:
no goals
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k) (succ i) = (decide (succ i < succ k) && getBit n (succ i))
Tactic:
unfold getBit
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
Tactic:
have : i.succ < k.succ ↔ i < k :=
  ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
Tactic:
rw [decide_eq_decide.mpr this]
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (i < k) && getBit (n / 2) i)