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

State before:
f : Bool → Bool → Bool
⊢ ∀ {m n : Nat}, bitwise (flip f) m n = bitwise f n m
Tactic:
intro m n
State after:
f : Bool → Bool → Bool
m n : Nat
⊢ bitwise (flip f) m n = bitwise f n m

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

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

State before:
f : Bool → Bool → Bool
m n : Nat
hm : m = 0
⊢ bitwise (flip f) m n = bitwise f n m
Tactic:
case pos hm =>
  cases hm
  unfold bitwise
  simp [flip]
  by_cases n = 0
  case pos hn =>
    cases hn; rw [if_pos (Eq.refl 0)]
    by_cases f true false <;> simp
  case neg hn => rw [if_neg hn]
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ bitwise (flip f) m n = bitwise f n m
Tactic:
case neg hm =>
  unfold bitwise
  rw [if_neg hm, if_neg hm]
  dsimp
  have : m > 0 := Nat.pos_of_ne_zero hm
  have : m/2 < m := Nat.div_lt_self ‹m>0› (Nat.lt_succ_self 1)
  rw [bitwise_flip (m:=m/2) (n:=n/2)]
  rfl
State after:
no goals

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

State before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise (flip f) 0 n = bitwise f n 0
Tactic:
unfold bitwise
State after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if 0 = 0 then if flip f false true = true then n else 0
    else
      if n = 0 then if flip 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 (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 0 else 0
    else
      if 0 = 0 then if f true false = true then n else 0
      else
        let n' := n / 2;
        let m' := 0 / 2;
        let b₁ := n % 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

State before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if 0 = 0 then if flip f false true = true then n else 0
    else
      if n = 0 then if flip 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 (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 0 else 0
    else
      if 0 = 0 then if f true false = true then n else 0
      else
        let n' := n / 2;
        let m' := 0 / 2;
        let b₁ := n % 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
Tactic:
simp [flip]
State after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0

State before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0
Tactic:
by_cases n = 0
State after:
case pos
f : Bool → Bool → Bool
n : Nat
h✝ : n = 0
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0

case neg
f : Bool → Bool → Bool
n : Nat
h✝ : ¬n = 0
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0

State before:
f : Bool → Bool → Bool
n : Nat
hn : n = 0
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0
Tactic:
case pos hn =>
  cases hn; rw [if_pos (Eq.refl 0)]
  by_cases f true false <;> simp
State after:
no goals

State before:
f : Bool → Bool → Bool
n : Nat
hn : ¬n = 0
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0
Tactic:
case neg hn => rw [if_neg hn]
State after:
no goals

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

State before:
case refl
f : Bool → Bool → Bool
⊢ (if f true false = true then 0 else 0) = if 0 = 0 then 0 else if f true false = true then 0 else 0
Tactic:
rw [if_pos (Eq.refl 0)]
State after:
case refl
f : Bool → Bool → Bool
⊢ (if f true false = true then 0 else 0) = 0

State before:
case refl
f : Bool → Bool → Bool
⊢ (if f true false = true then 0 else 0) = 0
Tactic:
by_cases f true false <;> simp
State after:
no goals

State before:
f : Bool → Bool → Bool
n : Nat
hn : ¬n = 0
⊢ (if f true false = true then n else 0) = if n = 0 then 0 else if f true false = true then n else 0
Tactic:
rw [if_neg hn]
State after:
no goals

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ bitwise (flip f) m n = bitwise f n m
Tactic:
unfold bitwise
State after:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ (if m = 0 then if flip f false true = true then n else 0
    else
      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
      if m = 0 then if f true false = true then n 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

State before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ (if m = 0 then if flip f false true = true then n else 0
    else
      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
      if m = 0 then if f true false = true then n 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:
rw [if_neg hm, if_neg hm]
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
      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

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

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

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

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

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