Theorem: Nat.land_exp2_sub_one (Algdata/Data/Nat/Bits.lean)

State before:
k : Nat
⊢ ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
Tactic:
intro n
State after:
k n : Nat
⊢ n &&& 2 ^ k - 1 = n % 2 ^ k

State before:
k n : Nat
⊢ n &&& 2 ^ k - 1 = n % 2 ^ k
Tactic:
induction k generalizing n
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✝

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
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)

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
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

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)
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

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]
State after:
no goals

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]
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

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))]
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

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)]
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

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)
State after:
no goals

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]
State after:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ 0 < 2 ^ k * 2

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)
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ 0 < 2
Tactic:
decide
State after:
no goals

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)]
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

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
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

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]
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

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))]
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

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 _]
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

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]
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (false && false) = false
Tactic:
decide
State after:
no goals

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
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

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
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

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals