internlm/Lean-Github huggingface dataset:
Theorem: Nat.bitwise_getBit
Proof 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]
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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]
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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]
Proof 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))
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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]
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two_pow
Proof state before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ bitwise f m n % 2 ^ k = bitwise f (m % 2 ^ k) (n % 2 ^ k)
Tactic:
apply bitext
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n % 2 ^ k) i = getBit (bitwise f (m % 2 ^ k) (n % 2 ^ k)) i
Theorem: Nat.bitwise_mod_two_pow
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n % 2 ^ k) i = getBit (bitwise f (m % 2 ^ k) (n % 2 ^ k)) i
Tactic:
intro i
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n % 2 ^ k) i = getBit (bitwise f (m % 2 ^ k) (n % 2 ^ k)) i
Theorem: Nat.bitwise_mod_two_pow
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n % 2 ^ k) i = getBit (bitwise f (m % 2 ^ k) (n % 2 ^ k)) i
Tactic:
simp [getBit_mod_two_pow, bitwise_getBit f f_stable]
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i < k) && f (getBit m i) (getBit n i)) = f (decide (i < k) && getBit m i) (decide (i < k) && getBit n i)
Theorem: Nat.bitwise_mod_two_pow
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i < k) && f (getBit m i) (getBit n i)) = f (decide (i < k) && getBit m i) (decide (i < k) && getBit n i)
Tactic:
cases decide (i<k) <;> simp [f_stable]
Proof state after:
no goals
Theorem: Nat.bitwise_idempotent
Proof state before:
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n : Nat
⊢ bitwise f n n = n
Tactic:
apply Nat.bitext
Proof state after:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit n i
Theorem: Nat.bitwise_idempotent
Proof state before:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit n i
Tactic:
intro i
Proof state after:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n i : Nat
⊢ getBit (bitwise f n n) i = getBit n i
Theorem: Nat.bitwise_idempotent
Proof state before:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = b
n i : Nat
⊢ getBit (bitwise f n n) i = getBit n i
Tactic:
simp [Nat.bitwise_getBit f (h false), h]
Proof state after:
no goals
Theorem: Nat.bitwise_nilpotent
Proof state before:
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ bitwise f n n = 0
Tactic:
apply Nat.bitext
Proof state after:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit 0 i
Theorem: Nat.bitwise_nilpotent
Proof state before:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit 0 i
Tactic:
intro i
Proof state after:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n i : Nat
⊢ getBit (bitwise f n n) i = getBit 0 i
Theorem: Nat.bitwise_nilpotent
Proof state before:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n i : Nat
⊢ getBit (bitwise f n n) i = getBit 0 i
Tactic:
simp [Nat.bitwise_getBit f (h false), h]
Proof state after:
no goals
Theorem: Nat.bitwise_assoc
Proof state before:
f : Bool → Bool → Bool
f_stable : f false false = false
h : ∀ (a b c : Bool), f (f a b) c = f a (f b c)
l m n : Nat
⊢ bitwise f (bitwise f l m) n = bitwise f l (bitwise f m n)
Tactic:
apply Nat.bitext
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
h : ∀ (a b c : Bool), f (f a b) c = f a (f b c)
l m n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f (bitwise f l m) n) i = getBit (bitwise f l (bitwise f m n)) i
Theorem: Nat.bitwise_assoc
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
h : ∀ (a b c : Bool), f (f a b) c = f a (f b c)
l m n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f (bitwise f l m) n) i = getBit (bitwise f l (bitwise f m n)) i
Tactic:
intro i
Proof state after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
h : ∀ (a b c : Bool), f (f a b) c = f a (f b c)
l m n i : Nat
⊢ getBit (bitwise f (bitwise f l m) n) i = getBit (bitwise f l (bitwise f m n)) i
Theorem: Nat.bitwise_assoc
Proof state before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
h : ∀ (a b c : Bool), f (f a b) c = f a (f b c)
l m n i : Nat
⊢ getBit (bitwise f (bitwise f l m) n) i = getBit (bitwise f l (bitwise f m n)) i
Tactic:
simp [Nat.bitwise_getBit f f_stable, h]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
⊢ ∀ {m n : Nat}, bitwise (flip f) m n = bitwise f n m
Tactic:
intro m n
Proof state after:
f : Bool → Bool → Bool
m n : Nat
⊢ bitwise (flip f) m n = bitwise f n m
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
⊢ bitwise (flip f) m n = bitwise f n m
Tactic:
by_cases m = 0
Proof 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
Theorem: Nat.bitwise_flip
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : m = 0
⊢ bitwise (flip f) m n = bitwise f n m
Tactic:
cases hm
Proof state after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise (flip f) 0 n = bitwise f n 0
Theorem: Nat.bitwise_flip
Proof state before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise (flip f) 0 n = bitwise f n 0
Tactic:
unfold bitwise
Proof 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
Theorem: Nat.bitwise_flip
Proof 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]
Proof 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
Theorem: Nat.bitwise_flip
Proof 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
Proof 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
Theorem: Nat.bitwise_flip
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof 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
Proof 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
Theorem: Nat.bitwise_flip
Proof 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)]
Proof state after:
case refl
f : Bool → Bool → Bool
⊢ (if f true false = true then 0 else 0) = 0
Theorem: Nat.bitwise_flip
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_flip
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ bitwise (flip f) m n = bitwise f n m
Tactic:
unfold bitwise
Proof 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
Theorem: Nat.bitwise_flip
Proof 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]
Proof 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