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

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
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
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0

case neg
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : ¬m = 0
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : m = 0
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
case pos hm =>
  cases hm; unfold bitwise; simp
  cases hfft : f false true
  case false =>
    have : ∀ b, f false b = false := λ b => by cases b; exact f_stable; exact hfft
    simp [this]
  case true =>
    have : ∀ b, f false b = b := λ b => by cases b; exact f_stable; exact hfft
    simp [this]
    apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
State after:
no goals

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

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

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

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
⊢ (if f false true = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
cases hfft : f false true
State after:
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ (if false = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ (if true = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ (if false = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
case false =>
  have : ∀ b, f false b = false := λ b => by cases b; exact f_stable; exact hfft
  simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ (if true = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
case true =>
  have : ∀ b, f false b = b := λ b => by cases b; exact f_stable; exact hfft
  simp [this]
  apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ (if false = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
have : ∀ b, f false b = false := λ b => by cases b; exact f_stable; exact hfft
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
this : ∀ (b : Bool), f false b = false
⊢ (if false = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0

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

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
b : Bool
⊢ f false b = false
Tactic:
cases b
State after:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ f false true = false

State before:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ f false true = false
Tactic:
exact f_stable
State after:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ f false true = false

State before:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = false
⊢ f false true = false
Tactic:
exact hfft
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ (if true = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
have : ∀ b, f false b = b := λ b => by cases b; exact f_stable; exact hfft
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
this : ∀ (b : Bool), f false b = b
⊢ (if true = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
this : ∀ (b : Bool), f false b = b
⊢ (if true = true then n else 0) % 2 = if f false (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
simp [this]
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
this : ∀ (b : Bool), f false b = b
⊢ n % 2 = if n % 2 = 1 then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
this : ∀ (b : Bool), f false b = b
⊢ n % 2 = if n % 2 = 1 then 1 else 0
Tactic:
apply (n.mod_two_eq_zero_or_one).elim <;> intro h <;> simp [h]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
b : Bool
⊢ f false b = b
Tactic:
cases b
State after:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ f false true = true

State before:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ f false true = true
Tactic:
exact f_stable
State after:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ f false true = true

State before:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
n : Nat
hfft : f false true = true
⊢ f false true = true
Tactic:
exact hfft
State after:
no goals

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

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 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
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0

case neg
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
h✝ : ¬n = 0
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
case pos hn =>
  cases hn; simp
  cases hftf : f true false
  case true =>
    have : ∀ b, f b false = b := λ b => by cases b; exact f_stable; exact hftf
    simp [this]
    apply m.mod_two_eq_zero_or_one.elim <;> intro h <;> simp [h]
  case false =>
    have : ∀ b, f b false = false := λ b => by cases b; exact f_stable; exact hftf
    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
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
case neg hn =>
  rw [if_neg hn]
  rfl
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
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
cases hn
State after:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ (if 0 = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (0 % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (0 % 2 = 1)) = true then 1 else 0

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

State before:
case refl
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
⊢ (if f true false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
Tactic:
cases hftf : f true false
State after:
case refl.false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ (if false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0

case refl.true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ (if true = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ (if true = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
Tactic:
case true =>
  have : ∀ b, f b false = b := λ b => by cases b; exact f_stable; exact hftf
  simp [this]
  apply m.mod_two_eq_zero_or_one.elim <;> intro h <;> simp [h]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ (if false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
Tactic:
case false =>
  have : ∀ b, f b false = false := λ b => by cases b; exact f_stable; exact hftf
  simp [this]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ (if true = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
Tactic:
have : ∀ b, f b false = b := λ b => by cases b; exact f_stable; exact hftf
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ (if true = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ (if true = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
Tactic:
simp [this]
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ m % 2 = if m % 2 = 1 then 1 else 0

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ m % 2 = if m % 2 = 1 then 1 else 0
Tactic:
apply m.mod_two_eq_zero_or_one.elim <;> intro h <;> simp [h]
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
b : Bool
⊢ f b false = b
Tactic:
cases b
State after:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f true false = true

State before:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f true false = true
Tactic:
exact f_stable
State after:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f true false = true

State before:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
⊢ f true false = true
Tactic:
exact hftf
State after:
no goals

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ (if false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0
Tactic:
have : ∀ b, f b false = false := λ b => by cases b; exact f_stable; exact hftf
State after:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
this : ∀ (b : Bool), f b false = false
⊢ (if false = true then m % 2 else 0) = if f (decide (m % 2 = 1)) false = true then 1 else 0

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

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
b : Bool
⊢ f b false = false
Tactic:
cases b
State after:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ f true false = false

State before:
case false
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ f false false = false

case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ f true false = false
Tactic:
exact f_stable
State after:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ f true false = false

State before:
case true
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = false
⊢ f true false = false
Tactic:
exact hftf
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
⊢ (if n = 0 then if f true false = true then m % 2 else 0
    else if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
rw [if_neg hn]
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 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 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 1 % 2 else 0) =
    if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
Tactic:
rfl
State after:
no goals