internlm/Lean-Github huggingface dataset:
Theorem: Nat.odd_xor_one
Proof state before:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n ^^^ 1 = n - 1
Tactic:
conv =>
  lhs; change bitwise bne n 1
  unfold bitwise; simp [this, hodd]
  change (n/2 ^^^ 0) + (n/2 ^^^ 0)
  rw [Nat.xor_zero, ←Nat.mul_two]
Proof state after:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n / 2 * 2 = n - 1
Theorem: Nat.odd_xor_one
Proof state before:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n / 2 * 2 = n - 1
Tactic:
conv =>
  rhs; rw [←Nat.div_add_mod n 2, hodd, Nat.add_sub_cancel, Nat.mul_comm]
Proof state after:
no goals
Theorem: Nat.odd_xor_one
Proof state before:
n : Nat
hodd : n % 2 = 1
h : n = 0
⊢ False
Tactic:
cases h
Proof state after:
case refl
hodd : 0 % 2 = 1
⊢ False
Theorem: Nat.odd_xor_one
Proof state before:
case refl
hodd : 0 % 2 = 1
⊢ False
Tactic:
cases hodd
Proof state after:
no goals
Theorem: Nat.xor_one
Proof state before:
n : Nat
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
cases n.mod_two_eq_zero_or_one
Proof state after:
case inl
n : Nat
h✝ : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1

case inr
n : Nat
h✝ : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Theorem: Nat.xor_one
Proof state before:
n : Nat
h : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
case inl h => simp [h, n.even_xor_one h]
Proof state after:
no goals
Theorem: Nat.xor_one
Proof state before:
n : Nat
h : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
case inr h => simp [h, n.odd_xor_one h]
Proof state after:
no goals
Theorem: Nat.xor_one
Proof state before:
n : Nat
h : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
simp [h, n.even_xor_one h]
Proof state after:
no goals
Theorem: Nat.xor_one
Proof state before:
n : Nat
h : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
simp [h, n.odd_xor_one h]
Proof state after:
no goals
Theorem: Nat.xor_getBit
Proof state before:
m n i : Nat
⊢ getBit (m ^^^ n) i = (getBit m i != getBit n i)
Tactic:
conv => lhs; change (bitwise bne m n).getBit i; rw [bitwise_getBit]
Proof state after:
no goals
Theorem: Nat.lor_land
Proof state before:
l m n : Nat
⊢ (l ||| m) &&& n = l &&& n ||| m &&& n
Tactic:
apply bitext
Proof state after:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i
Theorem: Nat.lor_land
Proof state before:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i
Tactic:
intro i
Proof state after:
case a
l m n i : Nat
⊢ getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i
Theorem: Nat.lor_land
Proof state before:
case a
l m n i : Nat
⊢ getBit ((l ||| m) &&& n) i = getBit (l &&& n ||| m &&& n) i
Tactic:
simp [Nat.lor_getBit, Nat.land_getBit]
Proof state after:
case a
l m n i : Nat
⊢ ((getBit l i || getBit m i) && getBit n i) = (getBit l i && getBit n i || getBit m i && getBit n i)
Theorem: Nat.lor_land
Proof state before:
case a
l m n i : Nat
⊢ ((getBit l i || getBit m i) && getBit n i) = (getBit l i && getBit n i || getBit m i && getBit n i)
Tactic:
cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
Proof state after:
no goals
Theorem: Nat.land_lor
Proof state before:
l m n : Nat
⊢ l &&& (m ||| n) = l &&& m ||| l &&& n
Tactic:
apply bitext
Proof state after:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit (l &&& (m ||| n)) i = getBit (l &&& m ||| l &&& n) i
Theorem: Nat.land_lor
Proof state before:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit (l &&& (m ||| n)) i = getBit (l &&& m ||| l &&& n) i
Tactic:
intro i
Proof state after:
case a
l m n i : Nat
⊢ getBit (l &&& (m ||| n)) i = getBit (l &&& m ||| l &&& n) i
Theorem: Nat.land_lor
Proof state before:
case a
l m n i : Nat
⊢ getBit (l &&& (m ||| n)) i = getBit (l &&& m ||| l &&& n) i
Tactic:
simp [Nat.lor_getBit, Nat.land_getBit]
Proof state after:
case a
l m n i : Nat
⊢ (getBit l i && (getBit m i || getBit n i)) = (getBit l i && getBit m i || getBit l i && getBit n i)
Theorem: Nat.land_lor
Proof state before:
case a
l m n i : Nat
⊢ (getBit l i && (getBit m i || getBit n i)) = (getBit l i && getBit m i || getBit l i && getBit n i)
Tactic:
cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
Proof state after:
no goals
Theorem: Nat.xor_and
Proof state before:
l m n : Nat
⊢ (l ^^^ m) &&& n = l &&& n ^^^ m &&& n
Tactic:
apply bitext
Proof state after:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i
Theorem: Nat.xor_and
Proof state before:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i
Tactic:
intro i
Proof state after:
case a
l m n i : Nat
⊢ getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i
Theorem: Nat.xor_and
Proof state before:
case a
l m n i : Nat
⊢ getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i
Tactic:
conv => lhs; change (bitwise and (bitwise bne l m) n).getBit i
Proof state after:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (l &&& n ^^^ m &&& n) i
Theorem: Nat.xor_and
Proof state before:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (l &&& n ^^^ m &&& n) i
Tactic:
conv => rhs; change (bitwise bne (bitwise and l n) (bitwise and m n)).getBit i
Proof state after:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (bitwise bne (bitwise and l n) (bitwise and m n)) i
Theorem: Nat.xor_and
Proof state before:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (bitwise bne (bitwise and l n) (bitwise and m n)) i
Tactic:
simp [bitwise_getBit]
Proof state after:
case a
l m n i : Nat
⊢ (getBit l i != getBit m i && getBit n i) = ((getBit l i && getBit n i) != (getBit m i && getBit n i))
Theorem: Nat.xor_and
Proof state before:
case a
l m n i : Nat
⊢ (getBit l i != getBit m i && getBit n i) = ((getBit l i && getBit n i) != (getBit m i && getBit n i))
Tactic:
cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
Proof state after:
no goals
Theorem: Nat.and_xor
Proof state before:
l m n : Nat
⊢ l &&& (m ^^^ n) = l &&& m ^^^ l &&& n
Tactic:
apply bitext
Proof state after:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit (l &&& (m ^^^ n)) i = getBit (l &&& m ^^^ l &&& n) i
Theorem: Nat.and_xor
Proof state before:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit (l &&& (m ^^^ n)) i = getBit (l &&& m ^^^ l &&& n) i
Tactic:
intro i
Proof state after:
case a
l m n i : Nat
⊢ getBit (l &&& (m ^^^ n)) i = getBit (l &&& m ^^^ l &&& n) i
Theorem: Nat.and_xor
Proof state before:
case a
l m n i : Nat
⊢ getBit (l &&& (m ^^^ n)) i = getBit (l &&& m ^^^ l &&& n) i
Tactic:
conv => lhs; change (bitwise and l (bitwise bne m n)).getBit i
Proof state after:
case a
l m n i : Nat
⊢ getBit (bitwise and l (bitwise bne m n)) i = getBit (l &&& m ^^^ l &&& n) i
Theorem: Nat.and_xor
Proof state before:
case a
l m n i : Nat
⊢ getBit (bitwise and l (bitwise bne m n)) i = getBit (l &&& m ^^^ l &&& n) i
Tactic:
conv => rhs; change (bitwise bne (bitwise and l m) (bitwise and l n)).getBit i
Proof state after:
case a
l m n i : Nat
⊢ getBit (bitwise and l (bitwise bne m n)) i = getBit (bitwise bne (bitwise and l m) (bitwise and l n)) i
Theorem: Nat.and_xor
Proof state before:
case a
l m n i : Nat
⊢ getBit (bitwise and l (bitwise bne m n)) i = getBit (bitwise bne (bitwise and l m) (bitwise and l n)) i
Tactic:
simp [bitwise_getBit]
Proof state after:
case a
l m n i : Nat
⊢ (getBit l i && getBit m i != getBit n i) = ((getBit l i && getBit m i) != (getBit l i && getBit n i))
Theorem: Nat.and_xor
Proof state before:
case a
l m n i : Nat
⊢ (getBit l i && getBit m i != getBit n i) = ((getBit l i && getBit m i) != (getBit l i && getBit n i))
Tactic:
cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
Proof state after:
no goals
Theorem: Nat.lor_mod_two_pow
Proof state before:
m n k : Nat
⊢ (false || false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_mod_two_pow
Proof state before:
m n k : Nat
⊢ (false && false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.xor_mod_two_pow
Proof state before:
m n k : Nat
⊢ (false != false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.shiftLeft_succ
Proof state before:
n k : Nat
⊢ n <<< succ k = 2 * n <<< k
Tactic:
simp
Proof state after:
n k : Nat
⊢ n * 2 ^ succ k = 2 * (n * 2 ^ k)
Theorem: Nat.shiftLeft_succ
Proof state before:
n k : Nat
⊢ n * 2 ^ succ k = 2 * (n * 2 ^ k)
Tactic:
rw [←Nat.mul_assoc, Nat.mul_comm 2, Nat.mul_assoc, Nat.mul_comm 2]
Proof state after:
n k : Nat
⊢ n * 2 ^ succ k = n * (2 ^ k * 2)
Theorem: Nat.shiftLeft_succ
Proof state before:
n k : Nat
⊢ n * 2 ^ succ k = n * (2 ^ k * 2)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftLeft
Proof state before:
n k l : Nat
⊢ n <<< k <<< l = n <<< (k + l)
Tactic:
induction l
Proof state after:
case zero
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)

case succ
n k n✝ : Nat
n_ih✝ : n <<< k <<< n✝ = n <<< (k + n✝)
⊢ n <<< k <<< succ n✝ = n <<< (k + succ n✝)
Theorem: Nat.shiftLeft_shiftLeft
Proof state before:
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftLeft
Proof state before:
n k l : Nat
h_ind : n <<< k <<< l = n <<< (k + l)
⊢ n <<< k <<< succ l = n <<< (k + succ l)
Tactic:
case succ l h_ind =>
  conv =>
    rw [add_succ, shiftLeft_succ, shiftLeft_succ, h_ind]
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftLeft
Proof state before:
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftLeft
Proof state before:
n k l : Nat
h_ind : n <<< k <<< l = n <<< (k + l)
⊢ n <<< k <<< succ l = n <<< (k + succ l)
Tactic:
conv =>
  rw [add_succ, shiftLeft_succ, shiftLeft_succ, h_ind]
Proof state after:
no goals
Theorem: Nat.shiftRight_shiftRight
Proof state before:
n k l : Nat
⊢ n >>> k >>> l = n >>> (k + l)
Tactic:
induction l
Proof state after:
case zero
n k : Nat
⊢ n >>> k >>> zero = n >>> (k + zero)

case succ
n k n✝ : Nat
n_ih✝ : n >>> k >>> n✝ = n >>> (k + n✝)
⊢ n >>> k >>> succ n✝ = n >>> (k + succ n✝)
Theorem: Nat.shiftRight_shiftRight
Proof state before:
n k : Nat
⊢ n >>> k >>> zero = n >>> (k + zero)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.shiftRight_shiftRight
Proof state before:
n k l : Nat
h_ind : n >>> k >>> l = n >>> (k + l)
⊢ n >>> k >>> succ l = n >>> (k + succ l)
Tactic:
case succ l h_ind =>
  conv =>
    rw [add_succ, shiftRight_succ, shiftRight_succ, h_ind]
Proof state after:
no goals
Theorem: Nat.shiftRight_shiftRight
Proof state before:
n k : Nat
⊢ n >>> k >>> zero = n >>> (k + zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftRight_shiftRight
Proof state before:
n k l : Nat
h_ind : n >>> k >>> l = n >>> (k + l)
⊢ n >>> k >>> succ l = n >>> (k + succ l)
Tactic:
conv =>
  rw [add_succ, shiftRight_succ, shiftRight_succ, h_ind]
Proof state after:
no goals
Theorem: Nat.zero_shiftLeft
Proof state before:
k : Nat
⊢ 0 <<< k = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.zero_shiftRight
Proof state before:
k : Nat
⊢ 0 >>> k = 0
Tactic:
induction k
Proof state after:
case zero

⊢ 0 >>> zero = 0

case succ
n✝ : Nat
n_ih✝ : 0 >>> n✝ = 0
⊢ 0 >>> succ n✝ = 0
Theorem: Nat.zero_shiftRight
Proof state before:
⊢ 0 >>> zero = 0
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.zero_shiftRight
Proof state before:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 >>> succ k = 0
Tactic:
case succ k h_ind => rw [shiftRight_succ, h_ind]; rfl
Proof state after:
no goals
Theorem: Nat.zero_shiftRight
Proof state before:
⊢ 0 >>> zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.zero_shiftRight
Proof state before:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 >>> succ k = 0
Tactic:
rw [shiftRight_succ, h_ind]
Proof state after:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 / 2 = 0
Theorem: Nat.zero_shiftRight
Proof state before:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 / 2 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftRight_self
Proof state before:
n k : Nat
⊢ n <<< k >>> k = n
Tactic:
induction k generalizing n
Proof state after:
case zero
n : Nat
⊢ n <<< zero >>> zero = n

case succ
n✝ : Nat
n_ih✝ : ∀ (n : Nat), n <<< n✝ >>> n✝ = n
n : Nat
⊢ n <<< succ n✝ >>> succ n✝ = n
Theorem: Nat.shiftLeft_shiftRight_self
Proof state before:
n : Nat
⊢ n <<< zero >>> zero = n
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftRight_self
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ n <<< succ k >>> succ k = n
Tactic:
case succ k h_ind =>
  conv =>
    lhs; simp; change (n * (2^k*2)) >>> k / 2
    rw [Nat.mul_comm (2^k) 2, ←Nat.mul_assoc]
    rw [←Nat.shiftLeft_eq (n*2) k, h_ind (n*2), Nat.mul_div_cancel n (n:=2) (by decide)]
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftRight_self
Proof state before:
n : Nat
⊢ n <<< zero >>> zero = n
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftRight_self
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ n <<< succ k >>> succ k = n
Tactic:
conv =>
  lhs; simp; change (n * (2^k*2)) >>> k / 2
  rw [Nat.mul_comm (2^k) 2, ←Nat.mul_assoc]
  rw [←Nat.shiftLeft_eq (n*2) k, h_ind (n*2), Nat.mul_div_cancel n (n:=2) (by decide)]
Proof state after:
no goals
Theorem: Nat.shiftLeft_shiftRight_self
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
n k i : Nat
⊢ i < k → getBit (n <<< k) i = false
Tactic:
intro h
Proof state after:
n k i : Nat
h : i < k
⊢ getBit (n <<< k) i = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
n k i : Nat
h : i < k
⊢ getBit (n <<< k) i = false
Tactic:
induction i generalizing n k
Proof state after:
case zero
n k : Nat
h : zero < k
⊢ getBit (n <<< k) zero = false

case succ
n✝ : Nat
n_ih✝ : ∀ (n k : Nat), n✝ < k → getBit (n <<< k) n✝ = false
n k : Nat
h : succ n✝ < k
⊢ getBit (n <<< k) (succ n✝) = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
n k : Nat
h : zero < k
⊢ getBit (n <<< k) zero = false
Tactic:
case zero =>
  have : k.pred.succ = k := Nat.succ_pred_eq_of_pos h
  rw [←this, Nat.shiftLeft_succ]
  conv => lhs; change decide ((2*n <<< k.pred) % 2 = 1); simp
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
⊢ getBit (n <<< k) (succ i) = false
Tactic:
case succ i h_ind =>
  have : k.pred.succ = k := Nat.succ_pred_eq_of_pos (trans i.zero_lt_succ h)
  rw [←this, Nat.shiftLeft_succ]
  conv =>
    lhs; change getBit ((2 * n <<< k.pred) / 2) i
    rw [Nat.mul_div_cancel_left _ (Nat.zero_lt_succ 1)]
  apply h_ind
  exact Nat.lt_of_succ_lt_succ (trans h this.symm)
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
n k : Nat
h : zero < k
⊢ getBit (n <<< k) zero = false
Tactic:
have : k.pred.succ = k := Nat.succ_pred_eq_of_pos h
Proof state after:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (n <<< k) zero = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (n <<< k) zero = false
Tactic:
rw [←this, Nat.shiftLeft_succ]
Proof state after:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) zero = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) zero = false
Tactic:
conv => lhs; change decide ((2*n <<< k.pred) % 2 = 1); simp
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
⊢ getBit (n <<< k) (succ i) = false
Tactic:
have : k.pred.succ = k := Nat.succ_pred_eq_of_pos (trans i.zero_lt_succ h)
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< k) (succ i) = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< k) (succ i) = false
Tactic:
rw [←this, Nat.shiftLeft_succ]
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) (succ i) = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) (succ i) = false
Tactic:
conv =>
  lhs; change getBit ((2 * n <<< k.pred) / 2) i
  rw [Nat.mul_div_cancel_left _ (Nat.zero_lt_succ 1)]
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< pred k) i = false
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< pred k) i = false
Tactic:
apply h_ind
Proof state after:
case h
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ i < pred k
Theorem: Nat.shiftLeft_getBit_lt
Proof state before:
case h
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ i < pred k
Tactic:
exact Nat.lt_of_succ_lt_succ (trans h this.symm)
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
n k i : Nat
⊢ i ≥ k → getBit (n <<< k) i = getBit n (i - k)
Tactic:
intro h
Proof state after:
n k i : Nat
h : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
n k i : Nat
h : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
Tactic:
induction k generalizing n i
Proof state after:
case zero
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n : Nat) {i : Nat}, i ≥ n✝ → getBit (n <<< n✝) i = getBit n (i - n✝)
n i : Nat
h : i ≥ succ n✝
⊢ getBit (n <<< succ n✝) i = getBit n (i - succ n✝)
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Tactic:
case succ k h_ind =>
  have : i-k = (i-k.succ).succ := by
    rw [Nat.sub_succ i k]
    apply (Nat.succ_pred_eq_of_pos ?_).symm
    exact Nat.zero_lt_sub_of_lt h
  conv =>
    lhs; change (n <<< (k+1)).getBit i
    rw [Nat.add_comm, ←Nat.shiftLeft_shiftLeft]
    rw [h_ind (n <<< 1) (Nat.le_of_succ_le h), this]
    change ((2*n)/2).getBit (i-k.succ)
    simp
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Tactic:
have : i-k = (i-k.succ).succ := by
  rw [Nat.sub_succ i k]
  apply (Nat.succ_pred_eq_of_pos ?_).symm
  exact Nat.zero_lt_sub_of_lt h
Proof state after:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
this : i - k = succ (i - succ k)
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
this : i - k = succ (i - succ k)
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Tactic:
conv =>
  lhs; change (n <<< (k+1)).getBit i
  rw [Nat.add_comm, ←Nat.shiftLeft_shiftLeft]
  rw [h_ind (n <<< 1) (Nat.le_of_succ_le h), this]
  change ((2*n)/2).getBit (i-k.succ)
  simp
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ i - k = succ (i - succ k)
Tactic:
rw [Nat.sub_succ i k]
Proof state after:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ i - k = succ (pred (i - k))
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ i - k = succ (pred (i - k))
Tactic:
apply (Nat.succ_pred_eq_of_pos ?_).symm
Proof state after:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ 0 < i - k
Theorem: Nat.shiftLeft_getBit_ge
Proof state before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ 0 < i - k
Tactic:
exact Nat.zero_lt_sub_of_lt h
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
cases Nat.lt_or_ge i k
Proof state after:
case inl
n k i : Nat
h✝ : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))

case inr
n k i : Nat
h✝ : i ≥ k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
case inl hlt =>
  rw [decide_eq_false (Nat.not_le_of_gt hlt), Bool.false_and]
  exact shiftLeft_getBit_lt n k hlt
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
case inr hge =>
  rw [decide_eq_true hge, Bool.true_and]
  exact shiftLeft_getBit_ge n k hge
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
rw [decide_eq_false (Nat.not_le_of_gt hlt), Bool.false_and]
Proof state after:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = false
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = false
Tactic:
exact shiftLeft_getBit_lt n k hlt
Proof state after:
no goals
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
rw [decide_eq_true hge, Bool.true_and]
Proof state after:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
Theorem: Nat.shiftLeft_getBit
Proof state before:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
Tactic:
exact shiftLeft_getBit_ge n k hge
Proof state after:
no goals
Theorem: Nat.shiftRight_getBit
Proof state before:
n k i : Nat
⊢ getBit (n >>> k) i = getBit n (i + k)
Tactic:
induction k generalizing n i
Proof state after:
case zero
n i : Nat
⊢ getBit (n >>> zero) i = getBit n (i + zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n i : Nat), getBit (n >>> n✝) i = getBit n (i + n✝)
n i : Nat
⊢ getBit (n >>> succ n✝) i = getBit n (i + succ n✝)
Theorem: Nat.shiftRight_getBit
Proof state before:
n i : Nat
⊢ getBit (n >>> zero) i = getBit n (i + zero)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Nat.shiftRight_getBit
Proof state before:
k : Nat
h_ind : ∀ (n i : Nat), getBit (n >>> k) i = getBit n (i + k)
n i : Nat
⊢ getBit (n >>> succ k) i = getBit n (i + succ k)
Tactic:
case succ k h_ind =>
  conv =>
    lhs; rw [Nat.succ_eq_add_one, Nat.add_comm, ←Nat.shiftRight_shiftRight]
    rw [h_ind]
Proof state after:
no goals
Theorem: Nat.shiftRight_getBit
Proof state before:
n i : Nat
⊢ getBit (n >>> zero) i = getBit n (i + zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.shiftRight_getBit
Proof state before:
k : Nat
h_ind : ∀ (n i : Nat), getBit (n >>> k) i = getBit n (i + k)
n i : Nat
⊢ getBit (n >>> succ k) i = getBit n (i + succ k)
Tactic:
conv =>
  lhs; rw [Nat.succ_eq_add_one, Nat.add_comm, ←Nat.shiftRight_shiftRight]
  rw [h_ind]
Proof state after:
no goals