[GOAL]
m k : ℕ
⊢ shiftl m (k + 1) = m * 2 ^ (k + 1)
[PROOFSTEP]
show bit0 (shiftl m k) = m * (2 ^ k * 2)
[GOAL]
m k : ℕ
⊢ bit0 (shiftl m k) = m * (2 ^ k * 2)
[PROOFSTEP]
rw [bit0_val, shiftl_eq_mul_pow m k, mul_comm 2, mul_assoc]
[GOAL]
m : ℕ
⊢ shiftl' true m 0 + 1 = (m + 1) * 2 ^ 0
[PROOFSTEP]
simp [shiftl, shiftl', pow_zero, Nat.one_mul]
[GOAL]
m k : ℕ
⊢ shiftl' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)
[PROOFSTEP]
change bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
[GOAL]
m k : ℕ
⊢ bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
[PROOFSTEP]
rw [bit1_val]
[GOAL]
m k : ℕ
⊢ 2 * shiftl' true m k + 1 + 1 = (m + 1) * (2 ^ k * 2)
[PROOFSTEP]
change 2 * (shiftl' true m k + 1) = _
[GOAL]
m k : ℕ
⊢ 2 * (shiftl' true m k + 1) = (m + 1) * (2 ^ k * 2)
[PROOFSTEP]
rw [shiftl'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2]
[GOAL]
m k : ℕ
⊢ div2 (m / 2 ^ k) = m / 2 ^ (k + 1)
[PROOFSTEP]
rw [div2_val, Nat.div_div_eq_div_mul, Nat.pow_succ]
[GOAL]
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
⊢ shiftl' b m n ≠ 0
[PROOFSTEP]
induction n
[GOAL]
case zero
b : Bool
m : ℕ
h : m ≠ 0
⊢ shiftl' b m zero ≠ 0
[PROOFSTEP]
simp [bit_ne_zero, shiftl', *]
[GOAL]
case succ
b : Bool
m : ℕ
h : m ≠ 0
n✝ : ℕ
n_ih✝ : shiftl' b m n✝ ≠ 0
⊢ shiftl' b m (succ n✝) ≠ 0
[PROOFSTEP]
simp [bit_ne_zero, shiftl', *]
[GOAL]
⊢ size 0 = 0
[PROOFSTEP]
simp [size]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ size (bit b n) = succ (size n)
[PROOFSTEP]
rw [size]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
conv =>
  lhs
  rw [binaryRec]
  simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
  lhs
  rw [binaryRec]
  simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
  lhs
  rw [binaryRec]
  simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
lhs
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n)
[PROOFSTEP]
rw [binaryRec]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| if n0 : bit b n = 0 then Eq.mpr (_ : ℕ = ℕ) 0
  else
    let n' := div2 (bit b n);
    let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
    Eq.mpr (_ : ℕ = ℕ) (succ (binaryRec 0 (fun x x => succ) n'))
[PROOFSTEP]
simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ succ (binaryRec 0 (fun x x => succ) (div2 (bit b n))) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
rw [div2_bit]
[GOAL]
⊢ size (bit1 0) = 1
[PROOFSTEP]
rw [size_bit1, size_zero]
[GOAL]
b : Bool
m n : ℕ
h : shiftl' b m n ≠ 0
⊢ size (shiftl' b m n) = size m + n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
b : Bool
m n : ℕ
h✝ : shiftl' b m n ≠ 0
h : shiftl' b m zero ≠ 0
⊢ size (shiftl' b m zero) = size m + zero
[PROOFSTEP]
simp [shiftl'] at h ⊢
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : shiftl' b m (succ n) ≠ 0
⊢ size (shiftl' b m (succ n)) = size m + succ n
[PROOFSTEP]
simp [shiftl'] at h ⊢
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ size (bit b (shiftl' b m n)) = size m + succ n
[PROOFSTEP]
rw [size_bit h, Nat.add_succ]
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
by_cases s0 : shiftl' b m n = 0 <;> [skip; rw [IH s0]]
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
by_cases s0 : shiftl' b m n = 0
[GOAL]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
skip
[GOAL]
case neg
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : ¬shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
rw [IH s0]
[GOAL]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
rw [s0] at h ⊢
[GOAL]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b 0 = 0
s0 : shiftl' b m n = 0
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
cases b
[GOAL]
case pos.false
m n✝ n : ℕ
h✝ : shiftl' false m n✝ ≠ 0
IH : shiftl' false m n ≠ 0 → size (shiftl' false m n) = size m + n
h : ¬bit false 0 = 0
s0 : shiftl' false m n = 0
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
exact absurd rfl h
[GOAL]
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
have : shiftl' true m n + 1 = 1 := congr_arg (· + 1) s0
[GOAL]
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : shiftl' true m n + 1 = 1
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
rw [shiftl'_tt_eq_mul_pow] at this 
[GOAL]
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
[GOAL]
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
[PROOFSTEP]
simp only [zero_add, one_mul] at this 
[GOAL]
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
[PROOFSTEP]
obtain rfl : n = 0 :=
  Nat.eq_zero_of_le_zero (le_of_not_gt fun hn => ne_of_gt (pow_lt_pow_of_lt_right (by decide) hn) this)
[GOAL]
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
hn : n > 0
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
case pos.true
n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n ≠ 0
IH : shiftl' true 0 0 ≠ 0 → size (shiftl' true 0 0) = size 0 + 0
s0 : shiftl' true 0 0 = 0
this : 2 ^ 0 = 1
⊢ succ (size 0) = succ (size 0 + 0)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ n < 2 ^ size n
[PROOFSTEP]
rw [← one_shiftl]
[GOAL]
n : ℕ
⊢ n < shiftl 1 (size n)
[PROOFSTEP]
have : ∀ {n}, n = 0 → n < shiftl 1 (size n) := by simp
[GOAL]
n : ℕ
⊢ ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ n < shiftl 1 (size n)
[PROOFSTEP]
apply binaryRec _ _ n
[GOAL]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ 0 < shiftl 1 (size 0)
[PROOFSTEP]
apply this rfl
[GOAL]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ ∀ (b : Bool) (n : ℕ), n < shiftl 1 (size n) → bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
intro b n IH
[GOAL]
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
⊢ bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
by_cases h : bit b n = 0
[GOAL]
case pos
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
apply this h
[GOAL]
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
rw [size_bit h, shiftl_succ]
[GOAL]
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < bit0 (shiftl 1 (size n))
[PROOFSTEP]
exact bit_lt_bit0 _ IH
[GOAL]
m n : ℕ
h : size m ≤ n
⊢ 2 > 0
[PROOFSTEP]
decide
[GOAL]
m n : ℕ
⊢ m < 2 ^ n → size m ≤ n
[PROOFSTEP]
rw [← one_shiftl]
[GOAL]
m n : ℕ
⊢ m < shiftl 1 n → size m ≤ n
[PROOFSTEP]
revert n
[GOAL]
m : ℕ
⊢ ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
[PROOFSTEP]
apply binaryRec _ _ m
[GOAL]
m : ℕ
⊢ ∀ {n : ℕ}, 0 < shiftl 1 n → size 0 ≤ n
[PROOFSTEP]
intro n
[GOAL]
m n : ℕ
⊢ 0 < shiftl 1 n → size 0 ≤ n
[PROOFSTEP]
simp
[GOAL]
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (∀ {n_1 : ℕ}, n < shiftl 1 n_1 → size n ≤ n_1) → ∀ {n_1 : ℕ}, bit b n < shiftl 1 n_1 → size (bit b n) ≤ n_1
[PROOFSTEP]
intro b m IH n h
[GOAL]
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
⊢ size (bit b m) ≤ n
[PROOFSTEP]
by_cases e : bit b m = 0
[GOAL]
case pos
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
e : bit b m = 0
⊢ size (bit b m) ≤ n
[PROOFSTEP]
simp [e]
[GOAL]
case neg
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
e : ¬bit b m = 0
⊢ size (bit b m) ≤ n
[PROOFSTEP]
rw [size_bit e]
[GOAL]
case neg
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
e : ¬bit b m = 0
⊢ succ (size m) ≤ n
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.zero
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
e : ¬bit b m = 0
h : bit b m < shiftl 1 zero
⊢ succ (size m) ≤ zero
[PROOFSTEP]
exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
[GOAL]
case neg.succ
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < shiftl 1 (succ n)
⊢ succ (size m) ≤ succ n
[PROOFSTEP]
apply succ_le_succ (IH _)
[GOAL]
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < shiftl 1 (succ n)
⊢ m < shiftl 1 n
[PROOFSTEP]
apply lt_imp_lt_of_le_imp_le (fun h' => bit0_le_bit _ h') h
[GOAL]
m n : ℕ
⊢ m < size n ↔ 2 ^ m ≤ n
[PROOFSTEP]
rw [← not_lt, Decidable.iff_not_comm, not_lt, size_le]
[GOAL]
n : ℕ
⊢ 0 < size n ↔ 0 < n
[PROOFSTEP]
rw [lt_size]
[GOAL]
n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ size n = 0 ↔ n = 0
[PROOFSTEP]
have := @size_pos n
[GOAL]
n : ℕ
this : 0 < size n ↔ 0 < n
⊢ size n = 0 ↔ n = 0
[PROOFSTEP]
simp [pos_iff_ne_zero] at this 
[GOAL]
n : ℕ
this : ¬size n = 0 ↔ ¬n = 0
⊢ size n = 0 ↔ n = 0
[PROOFSTEP]
exact Decidable.not_iff_not.1 this
[GOAL]
n : ℕ
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ List.length (bits n) = size n
[PROOFSTEP]
induction' n using Nat.binaryRec' with b n h ih
[GOAL]
case z
⊢ List.length (bits 0) = size 0
[PROOFSTEP]
simp
[GOAL]
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (bits (bit b n)) = size (bit b n)
[PROOFSTEP]
rw [size_bit, bits_append_bit _ _ h]
[GOAL]
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (b :: bits n) = succ (size n)
[PROOFSTEP]
simp [ih]
[GOAL]
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ bit b n ≠ 0
[PROOFSTEP]
simpa [bit_eq_zero_iff]
