internlm/Lean-Github huggingface dataset:
Theorem: Nat.bitwise_shiftLeft
Proof state before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ bitwise f m n <<< k = bitwise f (m <<< k) (n <<< k)
Tactic:
apply bitext
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n <<< k) i = getBit (bitwise f (m <<< k) (n <<< k)) i
Theorem: Nat.bitwise_shiftLeft
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n <<< k) i = getBit (bitwise f (m <<< k) (n <<< k)) i
Tactic:
intro i
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n <<< k) i = getBit (bitwise f (m <<< k) (n <<< k)) i
Theorem: Nat.bitwise_shiftLeft
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n <<< k) i = getBit (bitwise f (m <<< k) (n <<< k)) i
Tactic:
simp only [shiftLeft_getBit, bitwise_getBit f f_stable]
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i ≥ k) && f (getBit m (i - k)) (getBit n (i - k))) =
    f (decide (i ≥ k) && getBit m (i - k)) (decide (i ≥ k) && getBit n (i - k))
Theorem: Nat.bitwise_shiftLeft
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i ≥ k) && f (getBit m (i - k)) (getBit n (i - k))) =
    f (decide (i ≥ k) && getBit m (i - k)) (decide (i ≥ k) && getBit n (i - k))
Tactic:
cases decide (i ≥ k) <;> simp [f_stable]
Proof state after:
no goals
Theorem: Nat.lor_shiftLeft
Proof state before:
m n k : Nat
⊢ (false || false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_shiftLeft
Proof state before:
m n k : Nat
⊢ (false && false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.xor_shiftLeft
Proof state before:
m n k : Nat
⊢ (false != false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.bitwise_shiftRight
Proof state before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ bitwise f m n >>> k = bitwise f (m >>> k) (n >>> k)
Tactic:
apply bitext
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n >>> k) i = getBit (bitwise f (m >>> k) (n >>> k)) i
Theorem: Nat.bitwise_shiftRight
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n >>> k) i = getBit (bitwise f (m >>> k) (n >>> k)) i
Tactic:
intro i
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n >>> k) i = getBit (bitwise f (m >>> k) (n >>> k)) i
Theorem: Nat.bitwise_shiftRight
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n >>> k) i = getBit (bitwise f (m >>> k) (n >>> k)) i
Tactic:
simp [bitwise_getBit f f_stable]
Proof state after:
no goals
Theorem: Nat.lor_shiftRight
Proof state before:
m n k : Nat
⊢ (false || false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_shiftRight
Proof state before:
m n k : Nat
⊢ (false && false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.xor_shiftRight
Proof state before:
m n k : Nat
⊢ (false != false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
cases n.mod_two_eq_zero_or_one
Proof state after:
case inl
n : Nat
h✝ : n % 2 = 0
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1

case inr
n : Nat
h✝ : n % 2 = 1
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : n % 2 = 0
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
case inl h => simp [Nat.even_xor_one h, h]
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : n % 2 = 1
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
case inr h =>
  simp [Nat.odd_xor_one h, h]
  cases n
  case zero => cases h
  case succ n => rfl
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : n % 2 = 0
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
simp [Nat.even_xor_one h, h]
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : n % 2 = 1
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
simp [Nat.odd_xor_one h, h]
Proof state after:
n : Nat
h : n % 2 = 1
⊢ n = n - 1 + 1
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : n % 2 = 1
⊢ n = n - 1 + 1
Tactic:
cases n
Proof state after:
case zero
h : zero % 2 = 1
⊢ zero = zero - 1 + 1

case succ
n✝ : Nat
h : succ n✝ % 2 = 1
⊢ succ n✝ = succ n✝ - 1 + 1
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
h : zero % 2 = 1
⊢ zero = zero - 1 + 1
Tactic:
case zero => cases h
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : succ n % 2 = 1
⊢ succ n = succ n - 1 + 1
Tactic:
case succ n => rfl
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
h : zero % 2 = 1
⊢ zero = zero - 1 + 1
Tactic:
cases h
Proof state after:
no goals
Theorem: Nat.succ_eq_xor_add_land_shiftLeft
Proof state before:
n : Nat
h : succ n % 2 = 1
⊢ succ n = succ n - 1 + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.add_getBit_zero
Proof state before:
m n : Nat
⊢ getBit (m + n) 0 = getBit (m ^^^ n) 0
Tactic:
conv =>
  rhs; change (bitwise bne m n).getBit 0
  rw [bitwise_getBit bne (by decide)]
Proof state after:
m n : Nat
⊢ getBit (m + n) 0 = (getBit m 0 != getBit n 0)
Theorem: Nat.add_getBit_zero
Proof state before:
m n : Nat
⊢ getBit (m + n) 0 = (getBit m 0 != getBit n 0)
Tactic:
unfold getBit
Proof state after:
m n : Nat
⊢ decide ((m + n) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Theorem: Nat.add_getBit_zero
Proof state before:
m n : Nat
⊢ decide ((m + n) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
rw [Nat.add_mod m n 2]
Proof state after:
m n : Nat
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Theorem: Nat.add_getBit_zero
Proof state before:
m n : Nat
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
apply m.mod_two_eq_zero_or_one.elim
<;> apply n.mod_two_eq_zero_or_one.elim
<;> (intro hn hm; rw [hn, hm]; decide)
Proof state after:
no goals
Theorem: Nat.add_getBit_zero
Proof state before:
m n : Nat
⊢ (false != false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.add_getBit_zero
Proof state before:
case right.right
m n : Nat
⊢ n % 2 = 1 → m % 2 = 1 → decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
intro hn hm
Proof state after:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Theorem: Nat.add_getBit_zero
Proof state before:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
rw [hn, hm]
Proof state after:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((1 + 1) % 2 = 1) = (decide (1 = 1) != decide (1 = 1))
Theorem: Nat.add_getBit_zero
Proof state before:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((1 + 1) % 2 = 1) = (decide (1 = 1) != decide (1 = 1))
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.add_div_two
Proof state before:
m n : Nat
⊢ (m + n) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0
Tactic:
conv =>
  lhs; rw [←m.div_add_mod 2, ←n.div_add_mod 2]
  rw [←Nat.add_assoc, Nat.add_assoc _ (m%2), Nat.add_comm (m%2), ←Nat.add_assoc]
  rw [←Nat.mul_add 2, Nat.add_assoc, Nat.mul_add_div_left (x:=2) (y:=m/2+n/2) (z:=m%2+n%2) (by decide)]
Proof state after:
m n : Nat
⊢ m / 2 + n / 2 + (m % 2 + n % 2) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0
Theorem: Nat.add_div_two
Proof state before:
m n : Nat
⊢ m / 2 + n / 2 + (m % 2 + n % 2) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0
Tactic:
apply congrArg
Proof state after:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if getBit (m &&& n) 0 = true then 1 else 0
Theorem: Nat.add_div_two
Proof state before:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if getBit (m &&& n) 0 = true then 1 else 0
Tactic:
conv =>
  rhs; change if (bitwise and m n).getBit 0 = true then 1 else 0
  rw [bitwise_getBit and (by decide)]
Proof state after:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (getBit m 0 && getBit n 0) = true then 1 else 0
Theorem: Nat.add_div_two
Proof state before:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (getBit m 0 && getBit n 0) = true then 1 else 0
Tactic:
unfold getBit
Proof state after:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Theorem: Nat.add_div_two
Proof state before:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Tactic:
apply m.mod_two_eq_zero_or_one.elim <;> apply n.mod_two_eq_zero_or_one.elim
<;> (intro hn hm; rw [hn, hm]; decide)
Proof state after:
no goals
Theorem: Nat.add_div_two
Proof state before:
m n : Nat
⊢ 2 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.add_div_two
Proof state before:
m n : Nat
⊢ (false && false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.add_div_two
Proof state before:
case h.right.right
m n : Nat
⊢ n % 2 = 1 → m % 2 = 1 → (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Tactic:
intro hn hm
Proof state after:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Theorem: Nat.add_div_two
Proof state before:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Tactic:
rw [hn, hm]
Proof state after:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (1 + 1) / 2 = if (decide (1 = 1) && decide (1 = 1)) = true then 1 else 0
Theorem: Nat.add_div_two
Proof state before:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (1 + 1) / 2 = if (decide (1 = 1) && decide (1 = 1)) = true then 1 else 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.add_eq_xor
Proof state before:
m n : Nat
disjoint : m &&& n = 0
⊢ m + n = m ^^^ n
Tactic:
apply (Nat.eq_zero_or_pos m).elim
Proof state after:
case left
m n : Nat
disjoint : m &&& n = 0
⊢ m = 0 → m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Theorem: Nat.add_eq_xor
Proof state before:
case left
m n : Nat
disjoint : m &&& n = 0
⊢ m = 0 → m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
(intro hm; cases hm; simp)
Proof state after:
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Theorem: Nat.add_eq_xor
Proof state before:
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
intro hm
Proof state after:
case right
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ m + n = m ^^^ n
Theorem: Nat.add_eq_xor
Proof state before:
case right
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ m + n = m ^^^ n
Tactic:
apply eq_of_div_mod_two_eq
Proof state after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2

case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Theorem: Nat.add_eq_xor
Proof state before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2

case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Tactic:
. have : (m &&& n).getBit 0 = false := by simp [disjoint]
  conv => lhs; simp [add_div_two, this]; change (m >>> 1) + (n >>> 1)
  conv => rhs; change (m ^^^ n) >>> 1; rw [xor_shiftRight]
  have : m >>> 1 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
  exact add_eq_xor (m:=m >>> 1) (n:=n >>> 1) (by rw [←land_shiftRight, disjoint]; rfl)
Proof state after:
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Theorem: Nat.add_eq_xor
Proof state before:
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Tactic:
. exact eq_mod2_of_decide (add_getBit_zero m n)
Proof state after:
no goals
Theorem: Nat.add_eq_xor
Proof state before:
case left
m n : Nat
disjoint : m &&& n = 0
⊢ m = 0 → m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
intro hm
Proof state after:
case left
m n : Nat
disjoint : m &&& n = 0
hm : m = 0
⊢ m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Theorem: Nat.add_eq_xor
Proof state before:
case left
m n : Nat
disjoint : m &&& n = 0
hm : m = 0
⊢ m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
cases hm
Proof state after:
case left.refl
n : Nat
disjoint : 0 &&& n = 0
⊢ 0 + n = 0 ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Theorem: Nat.add_eq_xor
Proof state before:
case left.refl
n : Nat
disjoint : 0 &&& n = 0
⊢ 0 + n = 0 ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
simp
Proof state after:
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Theorem: Nat.add_eq_xor
Proof state before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2
Tactic:
have : (m &&& n).getBit 0 = false := by simp [disjoint]
Proof state after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ (m + n) / 2 = (m ^^^ n) / 2
Theorem: Nat.add_eq_xor
Proof state before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ (m + n) / 2 = (m ^^^ n) / 2
Tactic:
conv => lhs; simp [add_div_two, this]; change (m >>> 1) + (n >>> 1)
Proof state after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = (m ^^^ n) / 2
Theorem: Nat.add_eq_xor
Proof state before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = (m ^^^ n) / 2
Tactic:
conv => rhs; change (m ^^^ n) >>> 1; rw [xor_shiftRight]
Proof state after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1
Theorem: Nat.add_eq_xor
Proof state before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1
Tactic:
have : m >>> 1 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
Proof state after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1
Theorem: Nat.add_eq_xor
Proof state before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1
Tactic:
exact add_eq_xor (m:=m >>> 1) (n:=n >>> 1) (by rw [←land_shiftRight, disjoint]; rfl)
Proof state after:
no goals
Theorem: Nat.add_eq_xor
Proof state before:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ getBit (m &&& n) 0 = false
Tactic:
simp [disjoint]
Proof state after:
no goals
Theorem: Nat.add_eq_xor
Proof state before:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 &&& n >>> 1 = 0
Tactic:
rw [←land_shiftRight, disjoint]
Proof state after:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ 0 >>> 1 = 0
Theorem: Nat.add_eq_xor
Proof state before:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ 0 >>> 1 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.add_eq_xor
Proof state before:
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Tactic:
exact eq_mod2_of_decide (add_getBit_zero m n)
Proof state after:
no goals
Theorem: Nat.sub_eq_xor
Proof state before:
m n : Nat
incl : m &&& n = n
⊢ m - n = m ^^^ n
Tactic:
apply Nat.sub_eq_of_eq_add
Proof state after:
case h
m n : Nat
incl : m &&& n = n
⊢ m = (m ^^^ n) + n
Theorem: Nat.sub_eq_xor
Proof state before:
case h
m n : Nat
incl : m &&& n = n
⊢ m = (m ^^^ n) + n
Tactic:
have := calc
  (m ^^^ n) &&& n
    = (m &&& n) ^^^ (n &&& n) := Nat.xor_and m n n
  _ = n ^^^ n := by rw [incl, Nat.land_self n]
  _ = 0 := Nat.xor_self n
Proof state after:
case h
m n : Nat
incl : m &&& n = n
this : (m ^^^ n) &&& n = 0
⊢ m = (m ^^^ n) + n
Theorem: Nat.sub_eq_xor
Proof state before:
case h
m n : Nat
incl : m &&& n = n
this : (m ^^^ n) &&& n = 0
⊢ m = (m ^^^ n) + n
Tactic:
simp [add_eq_xor this, Nat.xor_assoc]
Proof state after:
no goals
Theorem: Nat.sub_eq_xor
Proof state before:
m n : Nat
incl : m &&& n = n
⊢ m &&& n ^^^ n &&& n = n ^^^ n
Tactic:
rw [incl, Nat.land_self n]
Proof state after:
no goals
Theorem: Nat.bitdivide
Proof state before:
n k : Nat
⊢ n = (n ^^^ n &&& k) + (n &&& k)
Tactic:
have : (n ^^^ (n &&& k)) &&& (n &&& k) = 0 := by
  simp [←Nat.land_assoc n n k]
Proof state after:
n k : Nat
this : (n ^^^ n &&& k) &&& (n &&& k) = 0
⊢ n = (n ^^^ n &&& k) + (n &&& k)
Theorem: Nat.bitdivide
Proof state before:
n k : Nat
this : (n ^^^ n &&& k) &&& (n &&& k) = 0
⊢ n = (n ^^^ n &&& k) + (n &&& k)
Tactic:
conv =>
  rhs; simp [add_eq_xor this, Nat.xor_assoc]
Proof state after:
no goals
Theorem: Nat.bitdivide
Proof state before:
n k : Nat
⊢ (n ^^^ n &&& k) &&& (n &&& k) = 0
Tactic:
simp [←Nat.land_assoc n n k]
Proof state after:
no goals
Theorem: Nat.setminus_land_setminus
Proof state before:
m n : Nat
⊢ (m ^^^ m &&& n) &&& (n ^^^ m &&& n) = 0
Tactic:
simp [Nat.land_assoc m n n, ←Nat.land_assoc m m n]
Proof state after:
no goals
Theorem: Nat.setminus_add_setminus
Proof state before:
m n : Nat
⊢ (m ^^^ m &&& n) + (n ^^^ m &&& n) = m ^^^ n
Tactic:
rw [add_eq_xor (setminus_land_setminus m n)]
Proof state after:
m n : Nat
⊢ m ^^^ m &&& n ^^^ (n ^^^ m &&& n) = m ^^^ n
Theorem: Nat.setminus_add_setminus
Proof state before:
m n : Nat
⊢ m ^^^ m &&& n ^^^ (n ^^^ m &&& n) = m ^^^ n
Tactic:
rw [Nat.xor_assoc, ←Nat.xor_assoc (m &&& n), Nat.xor_comm (m &&& n), Nat.xor_assoc]
Proof state after:
m n : Nat
⊢ m ^^^ (n ^^^ (m &&& n ^^^ m &&& n)) = m ^^^ n
Theorem: Nat.setminus_add_setminus
Proof state before:
m n : Nat
⊢ m ^^^ (n ^^^ (m &&& n ^^^ m &&& n)) = m ^^^ n
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.add_eq_xor_add_carry
Proof state before:
m n : Nat
⊢ m + n = (m ^^^ n) + (m &&& n) <<< 1
Tactic:
conv =>
  lhs; congr
  . rw [bitdivide m n]
  . rw [bitdivide n m]
Proof state after:
m n : Nat
⊢ (m ^^^ m &&& n) + (m &&& n) + ((n ^^^ n &&& m) + (n &&& m)) = (m ^^^ n) + (m &&& n) <<< 1
Theorem: Nat.add_eq_xor_add_carry
Proof state before:
m n : Nat
⊢ (m ^^^ m &&& n) + (m &&& n) + ((n ^^^ n &&& m) + (n &&& m)) = (m ^^^ n) + (m &&& n) <<< 1
Tactic:
conv =>
  lhs; rw [Nat.land_comm n m]
  rw [Nat.add_assoc, ←Nat.add_assoc (m &&& n), Nat.add_comm (m &&& n), Nat.add_assoc]
  rw [←Nat.two_mul, ←Nat.add_assoc]
  change (m ^^^ (m &&& n)) + (n ^^^ (m &&& n)) + ((m &&& n) <<< 1)
  rw [setminus_add_setminus]
Proof state after:
no goals
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
⊢ n % 2 = 1 → Nat.lsb n = 1
Tactic:
intro h
Proof state after:
n : Nat
h : n % 2 = 1
⊢ Nat.lsb n = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
h : n % 2 = 1
⊢ Nat.lsb n = 1
Tactic:
unfold Nat.lsb
Proof state after:
n : Nat
h : n % 2 = 1
⊢ n ^^^ n &&& n - 1 = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
h : n % 2 = 1
⊢ n ^^^ n &&& n - 1 = 1
Tactic:
have : n = 2*(n/2) + 1 :=
  Eq.symm $ Nat.add_comm .. ▸ h ▸ Nat.mod_add_div n 2
Proof state after:
n : Nat
h : n % 2 = 1
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
h : n % 2 = 1
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1
Tactic:
clear h
Proof state after:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ n ^^^ n &&& n - 1 = 1
Tactic:
rw [this, Nat.add_sub_cancel]
Proof state after:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1
Tactic:
have : 2*(n/2) + 1 = 2*(n/2) ^^^ 1 := by
  apply Nat.add_eq_xor
  rw [Nat.land_one, Nat.mul_mod_right]
Proof state after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) + 1 ^^^ 2 * (n / 2) + 1 &&& 2 * (n / 2) = 1
Tactic:
simp only [this]
Proof state after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1) &&& 2 * (n / 2) = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1) &&& 2 * (n / 2) = 1
Tactic:
rw [Nat.xor_and, Nat.land_self]
Proof state after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1 &&& 2 * (n / 2)) = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1 &&& 2 * (n / 2)) = 1
Tactic:
rw [←Nat.xor_assoc, Nat.xor_comm _ 1, Nat.xor_assoc 1, Nat.xor_self, Nat.xor_zero]
Proof state after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
Tactic:
have : ∀ k, 1 &&& 2 * k = 0 := by
  intro k; rw [Nat.land_comm, Nat.land_one, Nat.mul_mod_right]
Proof state after:
n : Nat
this✝¹ : n = 2 * (n / 2) + 1
this✝ : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
this : ∀ (k : Nat), 1 &&& 2 * k = 0
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝¹ : n = 2 * (n / 2) + 1
this✝ : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
this : ∀ (k : Nat), 1 &&& 2 * k = 0
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
Tactic:
rw [this, Nat.xor_zero]
Proof state after:
no goals
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
Tactic:
apply Nat.add_eq_xor
Proof state after:
case disjoint
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) &&& 1 = 0
Theorem: Nat.lsb_of_odd
Proof state before:
case disjoint
n : Nat
this : n = 2 * (n / 2) + 1
⊢ 2 * (n / 2) &&& 1 = 0
Tactic:
rw [Nat.land_one, Nat.mul_mod_right]
Proof state after:
no goals
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ ∀ (k : Nat), 1 &&& 2 * k = 0
Tactic:
intro k
Proof state after:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
k : Nat
⊢ 1 &&& 2 * k = 0
Theorem: Nat.lsb_of_odd
Proof state before:
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
k : Nat
⊢ 1 &&& 2 * k = 0
Tactic:
rw [Nat.land_comm, Nat.land_one, Nat.mul_mod_right]
Proof state after:
no goals
Theorem: Nat.lsb_shiftLeft
Proof state before:
⊢ ∀ (n k : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
Tactic:
suffices ∀ n, 2*n.lsb = (2*n).lsb by
  intro n k
  induction k generalizing n
  case zero => rfl
  case succ k h_ind =>
    simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
    conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
    rw [this]
Proof state after:
⊢ ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)