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

State before:
f : Bool → Bool → Bool
m n : Nat
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
by_cases m = 0
State after:
case pos
f : Bool → Bool → Bool
m n : Nat
h✝ : m = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)

case neg
f : Bool → Bool → Bool
m n : Nat
h✝ : ¬m = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)

State before:
f : Bool → Bool → Bool
m n : Nat
hm : m = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
case pos hm =>
  cases hm; unfold bitwise; simp
  cases hfft : f false true <;> simp [hfft]
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : m = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
cases hm
State after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise f 0 n / 2 = bitwise f (0 / 2) (n / 2)

State before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise f 0 n / 2 = bitwise f (0 / 2) (n / 2)
Tactic:
unfold bitwise
State after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if 0 = 0 then if f false true = true then n else 0
      else
        if n = 0 then if f true false = true then 0 else 0
        else
          let n' := 0 / 2;
          let m' := n / 2;
          let b₁ := 0 % 2 = 1;
          let b₂ := n % 2 = 1;
          let r := bitwise f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) /
      2 =
    if 0 / 2 = 0 then if f false true = true then n / 2 else 0
    else
      if n / 2 = 0 then if f true false = true then 0 / 2 else 0
      else
        let n' := 0 / 2 / 2;
        let m' := n / 2 / 2;
        let b₁ := 0 / 2 % 2 = 1;
        let b₂ := n / 2 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r

State before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if 0 = 0 then if f false true = true then n else 0
      else
        if n = 0 then if f true false = true then 0 else 0
        else
          let n' := 0 / 2;
          let m' := n / 2;
          let b₁ := 0 % 2 = 1;
          let b₂ := n % 2 = 1;
          let r := bitwise f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) /
      2 =
    if 0 / 2 = 0 then if f false true = true then n / 2 else 0
    else
      if n / 2 = 0 then if f true false = true then 0 / 2 else 0
      else
        let n' := 0 / 2 / 2;
        let m' := n / 2 / 2;
        let b₁ := 0 / 2 % 2 = 1;
        let b₂ := n / 2 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
Tactic:
simp
State after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if f false true = true then n else 0) / 2 = if f false true = true then n / 2 else 0

State before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if f false true = true then n else 0) / 2 = if f false true = true then n / 2 else 0
Tactic:
cases hfft : f false true <;> simp [hfft]
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
by_cases n = 0
State after:
case pos
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
h✝ : n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)

case neg
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
h✝ : ¬n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
case pos hn =>
  cases hn
  unfold bitwise; simp; simp [if_neg hm]
  cases hftf : f true false <;> by_cases hm2 : m / 2 = 0 <;> simp [hftf, hm2]
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
cases hn
State after:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ bitwise f m 0 / 2 = bitwise f (m / 2) (0 / 2)

State before:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ bitwise f m 0 / 2 = bitwise f (m / 2) (0 / 2)
Tactic:
unfold bitwise
State after:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if m = 0 then if f false true = true then 0 else 0
      else
        if 0 = 0 then if f true false = true then m else 0
        else
          let n' := m / 2;
          let m' := 0 / 2;
          let b₁ := m % 2 = 1;
          let b₂ := 0 % 2 = 1;
          let r := bitwise f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) /
      2 =
    if m / 2 = 0 then if f false true = true then 0 / 2 else 0
    else
      if 0 / 2 = 0 then if f true false = true then m / 2 else 0
      else
        let n' := m / 2 / 2;
        let m' := 0 / 2 / 2;
        let b₁ := m / 2 % 2 = 1;
        let b₂ := 0 / 2 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r

State before:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if m = 0 then if f false true = true then 0 else 0
      else
        if 0 = 0 then if f true false = true then m else 0
        else
          let n' := m / 2;
          let m' := 0 / 2;
          let b₁ := m % 2 = 1;
          let b₂ := 0 % 2 = 1;
          let r := bitwise f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) /
      2 =
    if m / 2 = 0 then if f false true = true then 0 / 2 else 0
    else
      if 0 / 2 = 0 then if f true false = true then m / 2 else 0
      else
        let n' := m / 2 / 2;
        let m' := 0 / 2 / 2;
        let b₁ := m / 2 % 2 = 1;
        let b₂ := 0 / 2 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
Tactic:
simp
State after:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if m = 0 then 0 else if f true false = true then m else 0) / 2 =
    if m / 2 = 0 then 0 else if f true false = true then m / 2 else 0

State before:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if m = 0 then 0 else if f true false = true then m else 0) / 2 =
    if m / 2 = 0 then 0 else if f true false = true then m / 2 else 0
Tactic:
simp [if_neg hm]
State after:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if f true false = true then m else 0) / 2 = if m / 2 = 0 then 0 else if f true false = true then m / 2 else 0

State before:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if f true false = true then m else 0) / 2 = if m / 2 = 0 then 0 else if f true false = true then m / 2 else 0
Tactic:
cases hftf : f true false <;> by_cases hm2 : m / 2 = 0 <;> simp [hftf, hm2]
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
Tactic:
conv => lhs; unfold bitwise; simp [if_neg hm, if_neg hn]
State after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) + bitwise f (m / 2) (n / 2) + 1
      else bitwise f (m / 2) (n / 2) + bitwise f (m / 2) (n / 2)) /
      2 =
    bitwise f (m / 2) (n / 2)

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then (bitwise f (m / 2) (n / 2) * 2 + 1) / 2
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)
Tactic:
rw [Nat.add_comm, Nat.add_mul_div_right 1 _ (z:=2) (Nat.zero_lt_succ 1)]
State after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 / 2 + bitwise f (m / 2) (n / 2)
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 / 2 + bitwise f (m / 2) (n / 2)
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)
Tactic:
have : 1/2 = 0 := by decide
State after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
this : 1 / 2 = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 / 2 + bitwise f (m / 2) (n / 2)
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
this : 1 / 2 = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 / 2 + bitwise f (m / 2) (n / 2)
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)
Tactic:
rw [this, Nat.zero_add]
State after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
this : 1 / 2 = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2)
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
this : 1 / 2 = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2)
    else bitwise f (m / 2) (n / 2)) =
    bitwise f (m / 2) (n / 2)
Tactic:
simp
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ 1 / 2 = 0
Tactic:
decide
State after:
no goals