internlm/Lean-Github huggingface dataset:
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      let n' := m / 2;
      let m' := n / 2;
      let b₁ := m % 2 = 1;
      let b₂ := n % 2 = 1;
      let r := bitwise (flip f) n' m';
      if flip f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    if n = 0 then if f false true = true then m else 0
    else
      let n' := n / 2;
      let m' := m / 2;
      let b₁ := n % 2 = 1;
      let b₂ := m % 2 = 1;
      let r := bitwise f n' m';
      if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
Tactic:
dsimp
Proof state after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Tactic:
have : m > 0 := Nat.pos_of_ne_zero hm
Proof state after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this : m > 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this : m > 0
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Tactic:
have : m/2 < m := Nat.div_lt_self ‹m>0› (Nat.lt_succ_self 1)
Proof state after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this✝ : m > 0
this : m / 2 < m
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this✝ : m > 0
this : m / 2 < m
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2) + 1
      else bitwise (flip f) (m / 2) (n / 2) + bitwise (flip f) (m / 2) (n / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Tactic:
rw [bitwise_flip (m:=m/2) (n:=n/2)]
Proof state after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this✝ : m > 0
this : m / 2 < m
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
this✝ : m > 0
this : m / 2 < m
⊢ (if n = 0 then if flip f true false = true then m else 0
    else
      if flip f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)) =
    if n = 0 then if f false true = true then m else 0
    else
      if f (decide (n % 2 = 1)) (decide (m % 2 = 1)) = true then
        bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1
      else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.bitwise_comm
Proof state before:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m
Tactic:
have : flip f = f := funext (λ a => funext (λ b => h b a))
Proof state after:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m
Theorem: Nat.bitwise_comm
Proof state before:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
⊢ ∀ {m n : Nat}, bitwise f m n = bitwise f n m
Tactic:
intro m n
Proof state after:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
m n : Nat
⊢ bitwise f m n = bitwise f n m
Theorem: Nat.bitwise_comm
Proof state before:
f : Bool → Bool → Bool
h : ∀ (a b : Bool), f a b = f b a
this : flip f = f
m n : Nat
⊢ bitwise f m n = bitwise f n m
Tactic:
rw [←bitwise_flip (m:=m) (n:=n), this]
Proof state after:
no goals
Theorem: Nat.lor_comm
Proof state before:
m n : Nat
a b : Bool
⊢ (a || b) = (b || a)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Nat.lor_assoc
Proof state before:
l m n : Nat
⊢ (false || false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.lor_zero
Proof state before:
n : Nat
⊢ n ||| 0 = n
Tactic:
apply bitext
Proof state after:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n ||| 0) i = getBit n i
Theorem: Nat.lor_zero
Proof state before:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n ||| 0) i = getBit n i
Tactic:
intro i
Proof state after:
case a
n i : Nat
⊢ getBit (n ||| 0) i = getBit n i
Theorem: Nat.lor_zero
Proof state before:
case a
n i : Nat
⊢ getBit (n ||| 0) i = getBit n i
Tactic:
conv =>
  change (bitwise or n 0).getBit i = n.getBit i
  rw [bitwise_getBit, zero_getBit, Bool.or_false]
Proof state after:
no goals
Theorem: Nat.zero_lor
Proof state before:
n : Nat
⊢ 0 ||| n = n
Tactic:
rw [Nat.lor_comm, Nat.lor_zero]
Proof state after:
no goals
Theorem: Nat.lor_getBit
Proof state before:
m n i : Nat
⊢ getBit (m ||| n) i = (getBit m i || getBit n i)
Tactic:
conv => lhs; change (bitwise or m n).getBit i; rw [bitwise_getBit]
Proof state after:
no goals
Theorem: Nat.land_comm
Proof state before:
m n : Nat
a b : Bool
⊢ (a && b) = (b && a)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Nat.land_assoc
Proof state before:
l m n : Nat
⊢ (false && false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_zero
Proof state before:
n : Nat
⊢ n &&& 0 = 0
Tactic:
apply bitext
Proof state after:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n &&& 0) i = getBit 0 i
Theorem: Nat.land_zero
Proof state before:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n &&& 0) i = getBit 0 i
Tactic:
intro i
Proof state after:
case a
n i : Nat
⊢ getBit (n &&& 0) i = getBit 0 i
Theorem: Nat.land_zero
Proof state before:
case a
n i : Nat
⊢ getBit (n &&& 0) i = getBit 0 i
Tactic:
conv =>
  change (bitwise and n 0).getBit i = getBit 0 i
  rw [bitwise_getBit, zero_getBit, Bool.and_false]
Proof state after:
no goals
Theorem: Nat.zero_land
Proof state before:
n : Nat
⊢ 0 &&& n = 0
Tactic:
rw [Nat.land_comm, Nat.land_zero]
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
⊢ ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
Tactic:
intro n
Proof state after:
k n : Nat
⊢ n &&& 2 ^ k - 1 = n % 2 ^ k
Theorem: Nat.land_exp2_sub_one
Proof state before:
k n : Nat
⊢ n &&& 2 ^ k - 1 = n % 2 ^ k
Tactic:
induction k generalizing n
Proof state after:
case zero
n : Nat
⊢ n &&& 2 ^ zero - 1 = n % 2 ^ zero

case succ
n✝ : Nat
n_ih✝ : ∀ (n : Nat), n &&& 2 ^ n✝ - 1 = n % 2 ^ n✝
n : Nat
⊢ n &&& 2 ^ succ n✝ - 1 = n % 2 ^ succ n✝
Theorem: Nat.land_exp2_sub_one
Proof state before:
n : Nat
⊢ n &&& 2 ^ zero - 1 = n % 2 ^ zero
Tactic:
case zero => calc
  n &&& 2^0 - 1 = n &&& 0 := rfl
  _             = 0 := Nat.land_zero n
  _             = n % 1 := n.mod_one.symm
  _             = n % 2^0 := rfl
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ n &&& 2 ^ succ k - 1 = n % 2 ^ succ k
Tactic:
case succ k h_ind =>
  conv =>
    change bitwise and n (2^k*2 - 1) = n % (2^k*2)
    rw [Nat.mul_comm _ 2]
  apply eq_of_div_mod_two_eq
  . rw [bitwise_div_two]
    rw [Nat.mul_sub_div 0 2 (2^k) (by rw [Nat.mul_comm]; exact Nat.pos_pow_of_pos (n:=2) (k+1) (by decide))]
    rw [Nat.mod_mul_div_left n 2 (2^k)]
    exact h_ind (n/2)
  . rw [bitwise_mod_two and (by decide)]
    simp
    have : ∀ (l : Nat), l > 0 → (2*l - 1) % 2 = 1 := by
      intro l hl
      cases l
      case zero => cases hl
      case succ l =>
        conv =>
          lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
          rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
    simp [this (2^k) (Nat.pos_pow_of_pos k (by decide))]
    rw [Nat.mod_mul_mod_left n 2 _]
    apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
n : Nat
⊢ n &&& 2 ^ zero - 1 = n % 2 ^ zero
Tactic:
calc
n &&& 2^0 - 1 = n &&& 0 := rfl
_             = 0 := Nat.land_zero n
_             = n % 1 := n.mod_one.symm
_             = n % 2^0 := rfl
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ n &&& 2 ^ succ k - 1 = n % 2 ^ succ k
Tactic:
conv =>
  change bitwise and n (2^k*2 - 1) = n % (2^k*2)
  rw [Nat.mul_comm _ 2]
Proof state after:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) = n % (2 * 2 ^ k)
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) = n % (2 * 2 ^ k)
Tactic:
apply eq_of_div_mod_two_eq
Proof state after:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) / 2 = n % (2 * 2 ^ k) / 2

case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) / 2 = n % (2 * 2 ^ k) / 2

case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
Tactic:
. rw [bitwise_div_two]
  rw [Nat.mul_sub_div 0 2 (2^k) (by rw [Nat.mul_comm]; exact Nat.pos_pow_of_pos (n:=2) (k+1) (by decide))]
  rw [Nat.mod_mul_div_left n 2 (2^k)]
  exact h_ind (n/2)
Proof state after:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
Tactic:
. rw [bitwise_mod_two and (by decide)]
  simp
  have : ∀ (l : Nat), l > 0 → (2*l - 1) % 2 = 1 := by
    intro l hl
    cases l
    case zero => cases hl
    case succ l =>
      conv =>
        lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
        rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
  simp [this (2^k) (Nat.pos_pow_of_pos k (by decide))]
  rw [Nat.mod_mul_mod_left n 2 _]
  apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) / 2 = n % (2 * 2 ^ k) / 2
Tactic:
rw [bitwise_div_two]
Proof state after:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and (n / 2) ((2 * 2 ^ k - 1) / 2) = n % (2 * 2 ^ k) / 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and (n / 2) ((2 * 2 ^ k - 1) / 2) = n % (2 * 2 ^ k) / 2
Tactic:
rw [Nat.mul_sub_div 0 2 (2^k) (by rw [Nat.mul_comm]; exact Nat.pos_pow_of_pos (n:=2) (k+1) (by decide))]
Proof state after:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and (n / 2) (2 ^ k - succ (0 / 2)) = n % (2 * 2 ^ k) / 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and (n / 2) (2 ^ k - succ (0 / 2)) = n % (2 * 2 ^ k) / 2
Tactic:
rw [Nat.mod_mul_div_left n 2 (2^k)]
Proof state after:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and (n / 2) (2 ^ k - succ (0 / 2)) = n / 2 % 2 ^ k
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and (n / 2) (2 ^ k - succ (0 / 2)) = n / 2 % 2 ^ k
Tactic:
exact h_ind (n/2)
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ 0 < 2 * 2 ^ k
Tactic:
rw [Nat.mul_comm]
Proof state after:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ 0 < 2 ^ k * 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ 0 < 2 ^ k * 2
Tactic:
exact Nat.pos_pow_of_pos (n:=2) (k+1) (by decide)
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
Tactic:
rw [bitwise_mod_two and (by decide)]
Proof state after:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (if (decide (n % 2 = 1) && decide ((2 * 2 ^ k - 1) % 2 = 1)) = true then 1 else 0) = n % (2 * 2 ^ k) % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (if (decide (n % 2 = 1) && decide ((2 * 2 ^ k - 1) % 2 = 1)) = true then 1 else 0) = n % (2 * 2 ^ k) % 2
Tactic:
simp
Proof state after:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (if n % 2 = 1 ∧ (2 * 2 ^ k - 1) % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (if n % 2 = 1 ∧ (2 * 2 ^ k - 1) % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
Tactic:
have : ∀ (l : Nat), l > 0 → (2*l - 1) % 2 = 1 := by
  intro l hl
  cases l
  case zero => cases hl
  case succ l =>
    conv =>
      lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
      rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
Proof state after:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 ∧ (2 * 2 ^ k - 1) % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 ∧ (2 * 2 ^ k - 1) % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
Tactic:
simp [this (2^k) (Nat.pos_pow_of_pos k (by decide))]
Proof state after:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
Tactic:
rw [Nat.mod_mul_mod_left n 2 _]
Proof state after:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 then 1 else 0) = n % 2
Theorem: Nat.land_exp2_sub_one
Proof state before:
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 then 1 else 0) = n % 2
Tactic:
apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (false && false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
Tactic:
intro l hl
Proof state after:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n l : Nat
hl : l > 0
⊢ (2 * l - 1) % 2 = 1
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n l : Nat
hl : l > 0
⊢ (2 * l - 1) % 2 = 1
Tactic:
cases l
Proof state after:
case zero
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
hl : zero > 0
⊢ (2 * zero - 1) % 2 = 1

case succ
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n n✝ : Nat
hl : succ n✝ > 0
⊢ (2 * succ n✝ - 1) % 2 = 1
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
hl : zero > 0
⊢ (2 * zero - 1) % 2 = 1
Tactic:
case zero => cases hl
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n l : Nat
hl : succ l > 0
⊢ (2 * succ l - 1) % 2 = 1
Tactic:
case succ l =>
  conv =>
    lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
    rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
hl : zero > 0
⊢ (2 * zero - 1) % 2 = 1
Tactic:
cases hl
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n l : Nat
hl : succ l > 0
⊢ (2 * succ l - 1) % 2 = 1
Tactic:
conv =>
  lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
  rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: Nat.land_exp2_sub_one
Proof state before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.land_getBit
Proof state before:
m n i : Nat
⊢ getBit (m &&& n) i = (getBit m i && getBit n i)
Tactic:
conv => lhs; change (bitwise and m n).getBit i; rw [bitwise_getBit]
Proof state after:
no goals
Theorem: Nat.xor_self
Proof state before:
n : Nat
b : Bool
⊢ (b != b) = false
Tactic:
cases b <;> decide
Proof state after:
no goals
Theorem: Nat.xor_comm
Proof state before:
m n : Nat
a b : Bool
⊢ (a != b) = (b != a)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Nat.xor_assoc
Proof state before:
l m n : Nat
⊢ (false != false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.xor_assoc
Proof state before:
l m n : Nat
a b c : Bool
⊢ ((a != b) != c) = (a != (b != c))
Tactic:
cases a <;> cases b <;> cases c <;> decide
Proof state after:
no goals
Theorem: Nat.xor_zero
Proof state before:
n : Nat
⊢ n ^^^ 0 = n
Tactic:
apply bitext
Proof state after:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n ^^^ 0) i = getBit n i
Theorem: Nat.xor_zero
Proof state before:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n ^^^ 0) i = getBit n i
Tactic:
intro i
Proof state after:
case a
n i : Nat
⊢ getBit (n ^^^ 0) i = getBit n i
Theorem: Nat.xor_zero
Proof state before:
case a
n i : Nat
⊢ getBit (n ^^^ 0) i = getBit n i
Tactic:
conv =>
  change (bitwise bne n 0).getBit i = n.getBit i
  rw [Nat.bitwise_getBit, Nat.zero_getBit]
Proof state after:
case a
n i : Nat
⊢ (getBit n i != false) = getBit n i
Theorem: Nat.xor_zero
Proof state before:
case a
n i : Nat
⊢ (getBit n i != false) = getBit n i
Tactic:
cases n.getBit i <;> decide
Proof state after:
no goals
Theorem: Nat.zero_xor
Proof state before:
n : Nat
⊢ 0 ^^^ n = n
Tactic:
rw [Nat.xor_comm, Nat.xor_zero]
Proof state after:
no goals
Theorem: Nat.even_xor_one
Proof state before:
n : Nat
⊢ n % 2 = 0 → n ^^^ 1 = n + 1
Tactic:
intro heven
Proof state after:
n : Nat
heven : n % 2 = 0
⊢ n ^^^ 1 = n + 1
Theorem: Nat.even_xor_one
Proof state before:
n : Nat
heven : n % 2 = 0
⊢ n ^^^ 1 = n + 1
Tactic:
by_cases n = 0
Proof state after:
case pos
n : Nat
heven : n % 2 = 0
h✝ : n = 0
⊢ n ^^^ 1 = n + 1

case neg
n : Nat
heven : n % 2 = 0
h✝ : ¬n = 0
⊢ n ^^^ 1 = n + 1
Theorem: Nat.even_xor_one
Proof state before:
n : Nat
heven : n % 2 = 0
h : n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
case pos h => cases h; decide
Proof state after:
no goals
Theorem: Nat.even_xor_one
Proof state before:
n : Nat
heven : n % 2 = 0
h : ¬n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
case neg h =>
  conv =>
    lhs; change bitwise bne n 1
    unfold bitwise; simp [h, heven]
    change (n/2 ^^^ 0) + (n/2 ^^^ 0) + 1
    rw [Nat.xor_zero, ←Nat.mul_two, Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
Proof state after:
no goals
Theorem: Nat.even_xor_one
Proof state before:
n : Nat
heven : n % 2 = 0
h : n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
cases h
Proof state after:
case refl
heven : 0 % 2 = 0
⊢ 0 ^^^ 1 = 0 + 1
Theorem: Nat.even_xor_one
Proof state before:
case refl
heven : 0 % 2 = 0
⊢ 0 ^^^ 1 = 0 + 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.even_xor_one
Proof state before:
n : Nat
heven : n % 2 = 0
h : ¬n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
conv =>
  lhs; change bitwise bne n 1
  unfold bitwise; simp [h, heven]
  change (n/2 ^^^ 0) + (n/2 ^^^ 0) + 1
  rw [Nat.xor_zero, ←Nat.mul_two, Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
Proof state after:
no goals
Theorem: Nat.odd_xor_one
Proof state before:
n : Nat
⊢ n % 2 = 1 → n ^^^ 1 = n - 1
Tactic:
intro hodd
Proof state after:
n : Nat
hodd : n % 2 = 1
⊢ n ^^^ 1 = n - 1
Theorem: Nat.odd_xor_one
Proof state before:
n : Nat
hodd : n % 2 = 1
⊢ n ^^^ 1 = n - 1
Tactic:
have : n ≠ 0 := λ h => by cases h; cases hodd
Proof state after:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n ^^^ 1 = n - 1