internlm/Lean-Github huggingface dataset:
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (i < k) && getBit (n / 2) i)
Tactic:
conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
Proof state after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n / 2 % 2 ^ k) i = (decide (i < k) && getBit (n / 2) i)
Theorem: Nat.getBit_mod_two_pow
Proof state before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n / 2 % 2 ^ k) i = (decide (i < k) && getBit (n / 2) i)
Tactic:
exact h_ind (n/2) k
Proof state after:
no goals
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
⊢ n = 0
Tactic:
cases n.eq_zero_or_pos
Proof state after:
case inl
n : Nat
h : ∀ (i : Nat), getBit n i = false
h✝ : n = 0
⊢ n = 0

case inr
n : Nat
h : ∀ (i : Nat), getBit n i = false
h✝ : n > 0
⊢ n = 0
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hzero : n = 0
⊢ n = 0
Tactic:
case inl hzero => exact hzero
Proof state after:
no goals
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
⊢ n = 0
Tactic:
case inr hpos =>
  have : n/2 < n := Nat.div_lt_self hpos (Nat.lt_succ_self 1)
  have : n/2 = 0 := eq_zero_of_getBit (n:=n/2) (λ i => h i.succ)
  have : n%2 = 0 := eq_mod2_of_decide (n:=0) (h 0)
  exact eq_of_div_mod_two_eq (n:=0) ‹n/2=0› ‹n%2=0›
Proof state after:
no goals
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hzero : n = 0
⊢ n = 0
Tactic:
exact hzero
Proof state after:
no goals
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
⊢ n = 0
Tactic:
have : n/2 < n := Nat.div_lt_self hpos (Nat.lt_succ_self 1)
Proof state after:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this : n / 2 < n
⊢ n = 0
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this : n / 2 < n
⊢ n = 0
Tactic:
have : n/2 = 0 := eq_zero_of_getBit (n:=n/2) (λ i => h i.succ)
Proof state after:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝ : n / 2 < n
this : n / 2 = 0
⊢ n = 0
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝ : n / 2 < n
this : n / 2 = 0
⊢ n = 0
Tactic:
have : n%2 = 0 := eq_mod2_of_decide (n:=0) (h 0)
Proof state after:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝¹ : n / 2 < n
this✝ : n / 2 = 0
this : n % 2 = 0
⊢ n = 0
Theorem: Nat.eq_zero_of_getBit
Proof state before:
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝¹ : n / 2 < n
this✝ : n / 2 = 0
this : n % 2 = 0
⊢ n = 0
Tactic:
exact eq_of_div_mod_two_eq (n:=0) ‹n/2=0› ‹n%2=0›
Proof state after:
no goals
Theorem: Nat.bitext
Proof state before:
m n : Nat
⊢ (∀ (i : Nat), getBit m i = getBit n i) → m = n
Tactic:
intro h
Proof state after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
⊢ m = n
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
⊢ m = n
Tactic:
have : m % 2 = n % 2 := eq_mod2_of_decide $ h 0
Proof state after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m = n
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m = n
Tactic:
have : m / 2 = n / 2 := by
  cases m.eq_zero_or_pos
  case inl hm => 
    cases hm; apply Eq.symm
    apply eq_zero_of_getBit
    exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
  case inr hm =>
    have : m/2 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
    exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
Proof state after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
this : m / 2 = n / 2
⊢ m = n
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
this : m / 2 = n / 2
⊢ m = n
Tactic:
exact eq_of_div_mod_two_eq ‹_› ‹_›
Proof state after:
no goals
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m / 2 = n / 2
Tactic:
cases m.eq_zero_or_pos
Proof state after:
case inl
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
h✝ : m = 0
⊢ m / 2 = n / 2

case inr
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
h✝ : m > 0
⊢ m / 2 = n / 2
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m = 0
⊢ m / 2 = n / 2
Tactic:
case inl hm => 
  cases hm; apply Eq.symm
  apply eq_zero_of_getBit
  exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
Proof state after:
no goals
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m > 0
⊢ m / 2 = n / 2
Tactic:
case inr hm =>
  have : m/2 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
  exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
Proof state after:
no goals
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m = 0
⊢ m / 2 = n / 2
Tactic:
cases hm
Proof state after:
case refl
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ 0 / 2 = n / 2
Theorem: Nat.bitext
Proof state before:
case refl
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ 0 / 2 = n / 2
Tactic:
apply Eq.symm
Proof state after:
case refl.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ n / 2 = 0 / 2
Theorem: Nat.bitext
Proof state before:
case refl.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ n / 2 = 0 / 2
Tactic:
apply eq_zero_of_getBit
Proof state after:
case refl.h.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ ∀ (i : Nat), getBit (n / 2) i = false
Theorem: Nat.bitext
Proof state before:
case refl.h.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ ∀ (i : Nat), getBit (n / 2) i = false
Tactic:
exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
Proof state after:
no goals
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m > 0
⊢ m / 2 = n / 2
Tactic:
have : m/2 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
Proof state after:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
hm : m > 0
this : m / 2 < m
⊢ m / 2 = n / 2
Theorem: Nat.bitext
Proof state before:
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
hm : m > 0
this : m / 2 < m
⊢ m / 2 = n / 2
Tactic:
exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
Proof state after:
no goals
Theorem: Nat.bitwise_div_two
Proof 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
Proof 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)
Theorem: Nat.bitwise_div_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_div_two
Proof 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
Proof state after:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise f 0 n / 2 = bitwise f (0 / 2) (n / 2)
Theorem: Nat.bitwise_div_two
Proof state before:
case refl
f : Bool → Bool → Bool
n : Nat
⊢ bitwise f 0 n / 2 = bitwise f (0 / 2) (n / 2)
Tactic:
unfold bitwise
Proof 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
Theorem: Nat.bitwise_div_two
Proof 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
Proof 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
Theorem: Nat.bitwise_div_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_div_two
Proof 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
Proof 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)
Theorem: Nat.bitwise_div_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_div_two
Proof 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
Proof state after:
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ bitwise f m 0 / 2 = bitwise f (m / 2) (0 / 2)
Theorem: Nat.bitwise_div_two
Proof 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
Proof 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
Theorem: Nat.bitwise_div_two
Proof 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
Proof 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
Theorem: Nat.bitwise_div_two
Proof 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]
Proof 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
Theorem: Nat.bitwise_div_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_div_two
Proof 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]
Proof 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)
Theorem: Nat.bitwise_div_two
Proof 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)]
Proof 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)
Theorem: Nat.bitwise_div_two
Proof 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
Proof 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)
Theorem: Nat.bitwise_div_two
Proof 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]
Proof 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)
Theorem: Nat.bitwise_div_two
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_div_two
Proof state before:
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ 1 / 2 = 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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
Theorem: Nat.bitwise_mod_two
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_mod_two
Proof 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
Proof 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