internlm/Lean-Github huggingface dataset:
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
⊢ bitwise f m n < 2 ^ succ k
Tactic:
by_cases n = 0
Proof state after:
case pos
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
h✝ : n = 0
⊢ bitwise f m n < 2 ^ succ k

case neg
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
h✝ : ¬n = 0
⊢ bitwise f m n < 2 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : n = 0
⊢ bitwise f m n < 2 ^ succ k
Tactic:
case pos hn =>
  cases hn
  unfold bitwise; simp [hm]
  cases f true false <;> simp
  . exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
  . exact hmk
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
⊢ bitwise f m n < 2 ^ succ k
Tactic:
case neg hn =>
  unfold bitwise; simp [hm, hn]
  rw [←Nat.mul_two, Nat.pow_succ]
  have : m/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hmk
  have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hnk
  cases f (m%2=1) (n%2=1) <;> simp
  . apply Nat.mul_lt_mul_of_pos_right ?_ (Nat.zero_lt_succ 1)
    exact h_ind ‹_› ‹_›
  . calc
    bitwise f (m/2) (n/2) * 2 + 1 
      < bitwise f (m/2) (n/2) * 2 + 2 := Nat.lt_succ_self _
    _ = (bitwise f (m/2) (n/2)) * 2 + 1*2 := rfl
    _ = (bitwise f (m/2) (n/2) + 1) * 2 := (Nat.add_mul _ _ 2).symm
    _ ≤ 2^k * 2 := Nat.mul_le_mul_right 2 (h_ind ‹m/2 < 2^k› ‹n/2 < 2^k›)
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : n = 0
⊢ bitwise f m n < 2 ^ succ k
Tactic:
cases hn
Proof state after:
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ bitwise f m 0 < 2 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ bitwise f m 0 < 2 ^ succ k
Tactic:
unfold bitwise
Proof state after:
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ (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 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ (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 ^ succ k
Tactic:
simp [hm]
Proof state after:
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ (if f true false = true then m else 0) < 2 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ (if f true false = true then m else 0) < 2 ^ succ k
Tactic:
cases f true false <;> simp
Proof state after:
case refl.false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ 0 < 2 ^ succ k

case refl.true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ m < 2 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl.false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ 0 < 2 ^ succ k

case refl.true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ m < 2 ^ succ k
Tactic:
. exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
Proof state after:
case refl.true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ m < 2 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl.true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ m < 2 ^ succ k
Tactic:
. exact hmk
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl.false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ 0 < 2 ^ succ k
Tactic:
exact Nat.pos_pow_of_pos k.succ (Nat.zero_lt_succ 1)
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case refl.true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m : Nat
hmk : m < 2 ^ succ k
hm : ¬m = 0
hnk : 0 < 2 ^ succ k
⊢ m < 2 ^ succ k
Tactic:
exact hmk
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
⊢ bitwise f m n < 2 ^ succ k
Tactic:
unfold bitwise
Proof state after:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 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 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 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 ^ succ k
Tactic:
simp [hm, hn]
Proof state after:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
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 ^ succ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
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 ^ succ k
Tactic:
rw [←Nat.mul_two, Nat.pow_succ]
Proof state after:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
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
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
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
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2
Tactic:
have : m/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hmk
Proof state after:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this : m / 2 < 2 ^ k
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) * 2 + 1
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this : m / 2 < 2 ^ k
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) * 2 + 1
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2
Tactic:
have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hnk
Proof state after:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) * 2 + 1
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) * 2 + 1
    else bitwise f (m / 2) (n / 2) * 2) <
    2 ^ k * 2
Tactic:
cases f (m%2=1) (n%2=1) <;> simp
Proof state after:
case false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 < 2 ^ k * 2

case true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 + 1 < 2 ^ k * 2
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 < 2 ^ k * 2

case true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 + 1 < 2 ^ k * 2
Tactic:
. apply Nat.mul_lt_mul_of_pos_right ?_ (Nat.zero_lt_succ 1)
  exact h_ind ‹_› ‹_›
Proof state after:
case true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 + 1 < 2 ^ k * 2
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 + 1 < 2 ^ k * 2
Tactic:
. calc
  bitwise f (m/2) (n/2) * 2 + 1 
    < bitwise f (m/2) (n/2) * 2 + 2 := Nat.lt_succ_self _
  _ = (bitwise f (m/2) (n/2)) * 2 + 1*2 := rfl
  _ = (bitwise f (m/2) (n/2) + 1) * 2 := (Nat.add_mul _ _ 2).symm
  _ ≤ 2^k * 2 := Nat.mul_le_mul_right 2 (h_ind ‹m/2 < 2^k› ‹n/2 < 2^k›)
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case false
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 < 2 ^ k * 2
Tactic:
apply Nat.mul_lt_mul_of_pos_right ?_ (Nat.zero_lt_succ 1)
Proof state after:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) < 2 ^ k
Theorem: Nat.bitwise_lt_exp2
Proof state before:
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) < 2 ^ k
Tactic:
exact h_ind ‹_› ‹_›
Proof state after:
no goals
Theorem: Nat.bitwise_lt_exp2
Proof state before:
case true
f : Bool → Bool → Bool
k : Nat
h_ind : ∀ {m n : Nat}, m < 2 ^ k → n < 2 ^ k → bitwise f m n < 2 ^ k
m n : Nat
hmk : m < 2 ^ succ k
hnk : n < 2 ^ succ k
hm : ¬m = 0
hn : ¬n = 0
this✝ : m / 2 < 2 ^ k
this : n / 2 < 2 ^ k
⊢ bitwise f (m / 2) (n / 2) * 2 + 1 < 2 ^ k * 2
Tactic:
calc
bitwise f (m/2) (n/2) * 2 + 1 
  < bitwise f (m/2) (n/2) * 2 + 2 := Nat.lt_succ_self _
_ = (bitwise f (m/2) (n/2)) * 2 + 1*2 := rfl
_ = (bitwise f (m/2) (n/2) + 1) * 2 := (Nat.add_mul _ _ 2).symm
_ ≤ 2^k * 2 := Nat.mul_le_mul_right 2 (h_ind ‹m/2 < 2^k› ‹n/2 < 2^k›)
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
⊢ ∀ (i : Nat), getBit (bitwise f m n) i = f (getBit m i) (getBit n i)
Tactic:
intro i
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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✝))
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:
case succ i h_ind =>
  dsimp [getBit]; rw [bitwise_div_two, h_ind]
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
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
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
⊢ 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)
Theorem: Nat.bitwise_getBit
Proof 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]
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
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
Tactic:
cases hm
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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)
Theorem: Nat.bitwise_getBit
Proof 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]
Proof state after:
no goals
Theorem: Nat.bitwise_getBit
Proof 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
Proof 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
Theorem: Nat.bitwise_getBit
Proof 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
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
⊢ getBit (bitwise f m n) zero = f (getBit m zero) (getBit n zero)
Tactic:
unfold bitwise
Proof 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)