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

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
Tactic:
intro i
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m n i : Nat
⊢ getBit (bitwise f m n) i = f (getBit m i) (getBit n i)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n i : Nat
⊢ getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
Tactic:
induction i generalizing m n
State after:
case zero
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)

case succ
f : Bool → Bool → Bool
f_stable : f false false = false
n✝ : Nat
n_ih✝ : ∀ (m n : Nat), getBit (bitwise f m n) n✝ = f (getBit m n✝) (getBit n n✝)
m n : Nat
⊢ getBit (bitwise f m n) (succ n✝) = f (getBit m (succ n✝)) (getBit n (succ n✝))

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
i : Nat
h_ind : ∀ (m n : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
m n : Nat
⊢ getBit (bitwise f m n) (succ i) = f (getBit m (succ i)) (getBit n (succ i))
Tactic:
case succ i h_ind =>
  dsimp [getBit]; rw [bitwise_div_two, h_ind]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
Tactic:
by_cases m = 0
State after:
case pos
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)

case neg
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : ¬m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
Tactic:
case pos hm =>
  cases hm; simp
  unfold bitwise; simp
  cases hft : f false true
  case false =>
    have : ∀ b, f false b = false := by intro b; cases b <;> assumption
    simp [this]
  case true =>
    have : ∀ b, f false b = b := by intro b; cases b <;> assumption
    simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
Tactic:
cases hm
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (bitwise f 0 n) zero = f (getBit 0 zero) (getBit n zero)

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (bitwise f 0 n) zero = f (getBit 0 zero) (getBit n zero)
Tactic:
simp
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (bitwise f 0 n) 0 = f false (getBit n 0)

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (bitwise f 0 n) 0 = f false (getBit n 0)
Tactic:
unfold bitwise
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit
      (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)
      0 =
    f false (getBit n 0)

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit
      (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)
      0 =
    f false (getBit n 0)
Tactic:
simp
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (if f false true = true then n else 0) 0 = f false (getBit n 0)

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ getBit (if f false true = true then n else 0) 0 = f false (getBit n 0)
Tactic:
cases hft : f false true
State after:
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
⊢ getBit (if false = true then n else 0) 0 = f false (getBit n 0)

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
⊢ getBit (if true = true then n else 0) 0 = f false (getBit n 0)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
⊢ getBit (if false = true then n else 0) 0 = f false (getBit n 0)
Tactic:
case false =>
  have : ∀ b, f false b = false := by intro b; cases b <;> assumption
  simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
⊢ getBit (if true = true then n else 0) 0 = f false (getBit n 0)
Tactic:
case true =>
  have : ∀ b, f false b = b := by intro b; cases b <;> assumption
  simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
⊢ getBit (if false = true then n else 0) 0 = f false (getBit n 0)
Tactic:
have : ∀ b, f false b = false := by intro b; cases b <;> assumption
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
this : ∀ (b : Bool), f false b = false
⊢ getBit (if false = true then n else 0) 0 = f false (getBit n 0)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
this : ∀ (b : Bool), f false b = false
⊢ getBit (if false = true then n else 0) 0 = f false (getBit n 0)
Tactic:
simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
⊢ ∀ (b : Bool), f false b = false
Tactic:
intro b
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
b : Bool
⊢ f false b = false

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = false
b : Bool
⊢ f false b = false
Tactic:
cases b <;> assumption
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
⊢ getBit (if true = true then n else 0) 0 = f false (getBit n 0)
Tactic:
have : ∀ b, f false b = b := by intro b; cases b <;> assumption
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
this : ∀ (b : Bool), f false b = b
⊢ getBit (if true = true then n else 0) 0 = f false (getBit n 0)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
this : ∀ (b : Bool), f false b = b
⊢ getBit (if true = true then n else 0) 0 = f false (getBit n 0)
Tactic:
simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
⊢ ∀ (b : Bool), f false b = b
Tactic:
intro b
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
b : Bool
⊢ f false b = b

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hft : f false true = true
b : Bool
⊢ f false b = b
Tactic:
cases b <;> assumption
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
Tactic:
unfold bitwise
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit
      (if m = 0 then if f false true = true then n else 0
      else
        if n = 0 then if 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 f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r)
      zero =
    f (getBit m zero) (getBit n zero)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit
      (if m = 0 then if f false true = true then n else 0
      else
        if n = 0 then if 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 f n' m';
          if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r)
      zero =
    f (getBit m zero) (getBit n zero)
Tactic:
simp [if_neg hm]
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)
Tactic:
by_cases n = 0
State after:
case pos
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
h✝ : n = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)

case neg
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
h✝ : ¬n = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)
Tactic:
case pos hn =>
  cases hn; simp
  cases htf : f true false
  case false =>
    have : ∀ b, f b false = false := by intro b; cases b <;> assumption
    simp [this]
  case true =>
    have : ∀ b, f b false = b := by intro b; cases b <;> assumption
    simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)
Tactic:
cases hn
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ getBit
      (if 0 = 0 then if f true false = true then m else 0
      else
        if f (decide (m % 2 = 1)) (decide (0 % 2 = 1)) = true then
          bitwise f (m / 2) (0 / 2) + bitwise f (m / 2) (0 / 2) + 1
        else bitwise f (m / 2) (0 / 2) + bitwise f (m / 2) (0 / 2))
      0 =
    f (getBit m 0) (getBit 0 0)

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ getBit
      (if 0 = 0 then if f true false = true then m else 0
      else
        if f (decide (m % 2 = 1)) (decide (0 % 2 = 1)) = true then
          bitwise f (m / 2) (0 / 2) + bitwise f (m / 2) (0 / 2) + 1
        else bitwise f (m / 2) (0 / 2) + bitwise f (m / 2) (0 / 2))
      0 =
    f (getBit m 0) (getBit 0 0)
Tactic:
simp
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ getBit (if f true false = true then m else 0) 0 = f (getBit m 0) false

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ getBit (if f true false = true then m else 0) 0 = f (getBit m 0) false
Tactic:
cases htf : f true false
State after:
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
⊢ getBit (if false = true then m else 0) 0 = f (getBit m 0) false

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
⊢ getBit (if true = true then m else 0) 0 = f (getBit m 0) false

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
⊢ getBit (if false = true then m else 0) 0 = f (getBit m 0) false
Tactic:
case false =>
  have : ∀ b, f b false = false := by intro b; cases b <;> assumption
  simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
⊢ getBit (if true = true then m else 0) 0 = f (getBit m 0) false
Tactic:
case true =>
  have : ∀ b, f b false = b := by intro b; cases b <;> assumption
  simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
⊢ getBit (if false = true then m else 0) 0 = f (getBit m 0) false
Tactic:
have : ∀ b, f b false = false := by intro b; cases b <;> assumption
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
this : ∀ (b : Bool), f b false = false
⊢ getBit (if false = true then m else 0) 0 = f (getBit m 0) false

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
this : ∀ (b : Bool), f b false = false
⊢ getBit (if false = true then m else 0) 0 = f (getBit m 0) false
Tactic:
simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
⊢ ∀ (b : Bool), f b false = false
Tactic:
intro b
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
b : Bool
⊢ f b false = false

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = false
b : Bool
⊢ f b false = false
Tactic:
cases b <;> assumption
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
⊢ getBit (if true = true then m else 0) 0 = f (getBit m 0) false
Tactic:
have : ∀ b, f b false = b := by intro b; cases b <;> assumption
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ getBit (if true = true then m else 0) 0 = f (getBit m 0) false

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ getBit (if true = true then m else 0) 0 = f (getBit m 0) false
Tactic:
simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
⊢ ∀ (b : Bool), f b false = b
Tactic:
intro b
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
b : Bool
⊢ f b false = b

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
htf : f true false = true
b : Bool
⊢ f b false = b
Tactic:
cases b <;> assumption
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ getBit
      (if n = 0 then if f true false = true then m else 0
      else
        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))
      0 =
    f (getBit m 0) (getBit n 0)
Tactic:
simp [if_neg hn]
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ getBit
      (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))
      0 =
    f (getBit m 0) (getBit n 0)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then getBit (1 + bitwise f (m / 2) (n / 2) * 2) 0
    else getBit (bitwise f (m / 2) (n / 2) * 2) 0) =
    f (getBit m 0) (getBit n 0)
Tactic:
dsimp [getBit]
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then decide ((1 + bitwise f (m / 2) (n / 2) * 2) % 2 = 1)
    else decide (bitwise f (m / 2) (n / 2) * 2 % 2 = 1)) =
    f (decide (m % 2 = 1)) (decide (n % 2 = 1))

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then decide ((1 + bitwise f (m / 2) (n / 2) * 2) % 2 = 1)
    else decide (bitwise f (m / 2) (n / 2) * 2 % 2 = 1)) =
    f (decide (m % 2 = 1)) (decide (n % 2 = 1))
Tactic:
cases hf : f (decide (m%2 = 1)) (decide (n%2 = 1)) <;> simp [hf]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
i : Nat
h_ind : ∀ (m n : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
m n : Nat
⊢ getBit (bitwise f m n) (succ i) = f (getBit m (succ i)) (getBit n (succ i))
Tactic:
dsimp [getBit]
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
i : Nat
h_ind : ∀ (m n : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
m n : Nat
⊢ getBit (bitwise f m n / 2) i = f (getBit (m / 2) i) (getBit (n / 2) i)

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
i : Nat
h_ind : ∀ (m n : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
m n : Nat
⊢ getBit (bitwise f m n / 2) i = f (getBit (m / 2) i) (getBit (n / 2) i)
Tactic:
rw [bitwise_div_two, h_ind]
State after:
no goals