internlm/Lean-Github huggingface dataset:
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
apply Nat.succ_le_succ (zero_le _)
Proof state after:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
cases b <;> simp
Proof state after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: Nat.pred_size_eq_log
Proof state before:
n : ℕ
⊢ size n - 1 = log 2 n
Tactic:
refine binaryRec' (n := n) rfl ?hi
Proof state after:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n - 1 = log 2 n → size (bit b n) - 1 = log 2 (bit b n)
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n - 1 = log 2 n → size (bit b n) - 1 = log 2 (bit b n)
Tactic:
intro b n hb ih
Proof state after:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n - 1 = log 2 n
⊢ size (bit b n) - 1 = log 2 (bit b n)
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n - 1 = log 2 n
⊢ size (bit b n) - 1 = log 2 (bit b n)
Tactic:
cases n
Proof state after:
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero - 1 = log 2 zero
⊢ size (bit b zero) - 1 = log 2 (bit b zero)

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ size (bit b (succ n✝)) - 1 = log 2 (bit b (succ n✝))
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero - 1 = log 2 zero
⊢ size (bit b zero) - 1 = log 2 (bit b zero)

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ size (bit b (succ n✝)) - 1 = log 2 (bit b (succ n✝))
Tactic:
cases b <;> rfl
Proof state after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ size (bit b (succ n✝)) - 1 = log 2 (bit b (succ n✝))
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ size (bit b (succ n✝)) - 1 = log 2 (bit b (succ n✝))
Tactic:
rw [size_bit, bit_val, Nat.log_mul_add, Nat.succ_eq_add_one, Nat.add_sub_cancel, ← ih, Nat.sub_add_cancel]
Proof state after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ size (succ n✝)

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ size (succ n✝)

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
Proof state after:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
exact one_lt_two
Proof state after:
case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
exact Nat.succ_le_succ (Nat.zero_le _)
Proof state after:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
{ cases b <;> simp }
Proof state after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
{ simp }
Proof state after:
no goals
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: Nat.pred_size_eq_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.size_succ_eq_succ_log_succ
Proof state before:
n : ℕ
⊢ size (n + 1) = log 2 (n + 1) + 1
Tactic:
rw [← Nat.pred_size_eq_log, Nat.sub_add_cancel]
Proof state after:
n : ℕ
⊢ 1 ≤ size (n + 1)
Theorem: Nat.size_succ_eq_succ_log_succ
Proof state before:
n : ℕ
⊢ 1 ≤ size (n + 1)
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
Proof state after:
no goals
Theorem: Nat.mod2_succ_eq_one
Proof state before:
n : ℕ
⊢ (n + 1) % 2 = 1 ↔ n % 2 = 0
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ => cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.mod2_succ_eq_one
Proof state before:
case z

⊢ (0 + 1) % 2 = 1 ↔ 0 % 2 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.mod2_succ_eq_one
Proof state before:
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → ((bit b n✝ + 1) % 2 = 1 ↔ bit b n✝ % 2 = 0)
⊢ (bit b n✝ + 1) % 2 = 1 ↔ bit b n✝ % 2 = 0
Tactic:
cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.mod2_succ_eq_zero
Proof state before:
n : ℕ
⊢ (n + 1) % 2 = 0 ↔ n % 2 = 1
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ => cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.mod2_succ_eq_zero
Proof state before:
case z

⊢ (0 + 1) % 2 = 0 ↔ 0 % 2 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.mod2_succ_eq_zero
Proof state before:
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → ((bit b n✝ + 1) % 2 = 0 ↔ bit b n✝ % 2 = 1)
⊢ (bit b n✝ + 1) % 2 = 0 ↔ bit b n✝ % 2 = 1
Tactic:
cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.bnot_mod2_eq_zero
Proof state before:
n : ℕ
⊢ (!decide (n % 2 = 0)) = decide (n % 2 = 1)
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ => cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.bnot_mod2_eq_zero
Proof state before:
case z

⊢ (!decide (0 % 2 = 0)) = decide (0 % 2 = 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.bnot_mod2_eq_zero
Proof state before:
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → (!decide (bit b n✝ % 2 = 0)) = decide (bit b n✝ % 2 = 1)
⊢ (!decide (bit b n✝ % 2 = 0)) = decide (bit b n✝ % 2 = 1)
Tactic:
cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.toNat_decide_mod2
Proof state before:
n : ℕ
⊢ Bool.toNat (decide (n % 2 = 0)) = (n + 1) % 2
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ => cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.toNat_decide_mod2
Proof state before:
case z

⊢ Bool.toNat (decide (0 % 2 = 0)) = (0 + 1) % 2
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.toNat_decide_mod2
Proof state before:
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.toNat (decide (bit b n✝ % 2 = 0)) = (bit b n✝ + 1) % 2
⊢ Bool.toNat (decide (bit b n✝ % 2 = 0)) = (bit b n✝ + 1) % 2
Tactic:
cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₀
Proof state before:
n m : ℕ
⊢ Bool.xor (decide (n % 2 = 0)) (decide (m % 2 = 0)) = decide ((n + m) % 2 = 1)
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ =>
  cases m using binaryRec with
  | z => cases b <;> simp [← Nat.two_mul]
  | f c _ _ =>
    cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₀
Proof state before:
case z
m : ℕ
⊢ Bool.xor (decide (0 % 2 = 0)) (decide (m % 2 = 0)) = decide ((0 + m) % 2 = 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₀
Proof state before:
case f
m : ℕ
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (bit b n✝ % 2 = 0)) (decide (m % 2 = 0)) = decide ((bit b n✝ + m) % 2 = 1)
⊢ Bool.xor (decide (bit b n✝ % 2 = 0)) (decide (m % 2 = 0)) = decide ((bit b n✝ + m) % 2 = 1)
Tactic:
cases m using binaryRec with
| z => cases b <;> simp [← Nat.two_mul]
| f c _ _ =>
  cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₀
Proof state before:
case f.z
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (bit b n✝ % 2 = 0)) (decide (0 % 2 = 0)) = decide ((bit b n✝ + 0) % 2 = 1)
⊢ Bool.xor (decide (bit b n✝ % 2 = 0)) (decide (0 % 2 = 0)) = decide ((bit b n✝ + 0) % 2 = 1)
Tactic:
cases b <;> simp [← Nat.two_mul]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₀
Proof state before:
case f.f
b : Bool
n✝¹ : ℕ
c : Bool
n✝ : ℕ
a✝¹ :
  bit b n✝¹ = n✝¹ →
    Bool.xor (decide (bit b n✝¹ % 2 = 0)) (decide (bit c n✝ % 2 = 0)) = decide ((bit b n✝¹ + bit c n✝) % 2 = 1)
a✝ :
  bit c n✝ = n✝ →
    Bool.xor (decide (bit b n✝¹ % 2 = 0)) (decide (bit c n✝ % 2 = 0)) = decide ((bit b n✝¹ + bit c n✝) % 2 = 1)
⊢ Bool.xor (decide (bit b n✝¹ % 2 = 0)) (decide (bit c n✝ % 2 = 0)) = decide ((bit b n✝¹ + bit c n✝) % 2 = 1)
Tactic:
cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₁
Proof state before:
n m : ℕ
⊢ Bool.xor (decide (n % 2 = 0)) (decide (m % 2 = 1)) = decide ((n + m) % 2 = 0)
Tactic:
cases m using binaryRec with
| z => simp
| f b _ _ =>
  cases n using binaryRec with
  | z => cases b <;> simp [← Nat.two_mul]
  | f c _ _ =>
    cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₁
Proof state before:
case z
n : ℕ
⊢ Bool.xor (decide (n % 2 = 0)) (decide (0 % 2 = 1)) = decide ((n + 0) % 2 = 0)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₁
Proof state before:
case f
n : ℕ
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (n % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((n + bit b n✝) % 2 = 0)
⊢ Bool.xor (decide (n % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((n + bit b n✝) % 2 = 0)
Tactic:
cases n using binaryRec with
| z => cases b <;> simp [← Nat.two_mul]
| f c _ _ =>
  cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₁
Proof state before:
case f.z
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (0 % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((0 + bit b n✝) % 2 = 0)
⊢ Bool.xor (decide (0 % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((0 + bit b n✝) % 2 = 0)
Tactic:
cases b <;> simp [← Nat.two_mul]
Proof state after:
no goals
Theorem: Nat.xor_mod2₀₁
Proof state before:
case f.f
b : Bool
n✝¹ : ℕ
c : Bool
n✝ : ℕ
a✝¹ :
  bit b n✝¹ = n✝¹ →
    Bool.xor (decide (bit c n✝ % 2 = 0)) (decide (bit b n✝¹ % 2 = 1)) = decide ((bit c n✝ + bit b n✝¹) % 2 = 0)
a✝ :
  bit c n✝ = n✝ →
    Bool.xor (decide (bit c n✝ % 2 = 0)) (decide (bit b n✝¹ % 2 = 1)) = decide ((bit c n✝ + bit b n✝¹) % 2 = 0)
⊢ Bool.xor (decide (bit c n✝ % 2 = 0)) (decide (bit b n✝¹ % 2 = 1)) = decide ((bit c n✝ + bit b n✝¹) % 2 = 0)
Tactic:
cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
Proof state after:
no goals
Theorem: Nat.div_mod2
Proof state before:
n : ℕ
⊢ n / 2 + n % 2 = (n + 1) / 2
Tactic:
induction n using Nat.binaryRec' with
| z => rfl
| f b _ _ _ => cases b <;> simp [bit_val, mul_add_div, mul_add_mod]
Proof state after:
no goals
Theorem: Nat.div_mod2
Proof state before:
case z

⊢ 0 / 2 + 0 % 2 = (0 + 1) / 2
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.div_mod2
Proof state before:
case f
b : Bool
n✝ : ℕ
a✝¹ : n✝ = 0 → b = true
a✝ : n✝ / 2 + n✝ % 2 = (n✝ + 1) / 2
⊢ bit b n✝ / 2 + bit b n✝ % 2 = (bit b n✝ + 1) / 2
Tactic:
cases b <;> simp [bit_val, mul_add_div, mul_add_mod]
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
⊢ (n : ℕ) → C n
Tactic:
intro n
Proof state after:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
⊢ C n
Theorem: Nat.parityZeroCases
Proof state before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
⊢ C n
Tactic:
cases n using Nat.binaryRec' with
| z => exact z
| f b n hb =>
  cases b with
  | true => simpa [← Nat.two_mul] using o _
  | false =>
    match n with
    | 0 => exact absurd (hb rfl) Bool.noConfusion
    | n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
case z
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
⊢ C 0
Tactic:
exact z
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
case f
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
b : Bool
n : ℕ
hb : n = 0 → b = true
a✝ : bit b n = n → C (bit b n)
⊢ C (bit b n)
Tactic:
cases b with
| true => simpa [← Nat.two_mul] using o _
| false =>
  match n with
  | 0 => exact absurd (hb rfl) Bool.noConfusion
  | n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
case f.true
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : n = 0 → true = true
a✝ : bit true n = n → C (bit true n)
⊢ C (bit true n)
Tactic:
simpa [← Nat.two_mul] using o _
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
case f.false
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : n = 0 → false = true
a✝ : bit false n = n → C (bit false n)
⊢ C (bit false n)
Tactic:
match n with
| 0 => exact absurd (hb rfl) Bool.noConfusion
| n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : 0 = 0 → false = true
a✝ : bit false 0 = 0 → C (bit false 0)
⊢ C (bit false 0)
Tactic:
exact absurd (hb rfl) Bool.noConfusion
Proof state after:
no goals
Theorem: Nat.parityZeroCases
Proof state before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n✝ n : ℕ
hb : n + 1 = 0 → false = true
a✝ : bit false (n + 1) = n + 1 → C (bit false (n + 1))
⊢ C (bit false (n + 1))
Tactic:
simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
Proof state after:
no goals
Theorem: Nat.size_le_self
Proof state before:
n : ℕ
⊢ size n ≤ n
Tactic:
induction n using Nat.binaryRec' with
| z => exact le_refl _
| f b n hb ih =>
  rw [size_bit]
  cases b
  simp
  apply Nat.add_le_add (c := 1) ih
  { cases n
    exact absurd (hb rfl) Bool.noConfusion
    exact Nat.succ_le_succ (Nat.zero_le _) }
  simp
  apply Nat.succ_le_succ
  apply le_trans
  apply ih
  apply le_add_left
  cases b
  simpa using λ h ↦ absurd (hb h) Bool.noConfusion
  simp
Proof state after:
no goals
Theorem: Nat.size_le_self
Proof state before:
case z

⊢ size 0 ≤ 0
Tactic:
exact le_refl _
Proof state after:
no goals
Theorem: Nat.size_le_self
Proof state before:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ size (bit b n) ≤ bit b n
Tactic:
rw [size_bit]
Proof state after:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ succ (size n) ≤ bit b n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ succ (size n) ≤ bit b n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
cases b
Proof state after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ bit false n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ bit false n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
simp
Proof state after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ n + n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ succ (size n) ≤ n + n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply Nat.add_le_add (c := 1) ih
Proof state after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ 1 ≤ n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ 1 ≤ n

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
{ cases n
  exact absurd (hb rfl) Bool.noConfusion
  exact Nat.succ_le_succ (Nat.zero_le _) }
Proof state after:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ bit true n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
simp
Proof state after:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ n + n + 1

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ succ (size n) ≤ n + n + 1

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply Nat.succ_le_succ
Proof state after:
case f.true.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.true.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply le_trans
Proof state after:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ ?f.true.a.b

case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ?f.true.a.b ≤ n + n

case f.true.a.b
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ℕ

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ size n ≤ ?f.true.a.b

case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ?f.true.a.b ≤ n + n

case f.true.a.b
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ ℕ

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply ih
Proof state after:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.true.a.a
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ n ≤ n + n

case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
apply le_add_left
Proof state after:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ n
⊢ bit b n ≠ 0
Tactic:
cases b
Proof state after:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ bit false n ≠ 0

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0