Powers of two by doubling

Doubling a counter once per element of a list multiplies it by 2 ^ length (List.foldl_add_self_eq_mul_two_pow), and the least power of two above n, 2 ^ Nat.size n, is at most 2 * n + 1 (Nat.two_pow_size_le). Together they bound unary counters built by doubling once per binary digit.

Main results

• List.foldl_add_self_eq_mul_two_pow: l.foldl (fun m _ => m + m) m = m * 2 ^ l.length.
• Nat.two_pow_size_le: 2 ^ Nat.size n ≤ 2 * n + 1.

theorem List.foldl_add_self_eq_mul_two_pow {α : Type u_1} (l : List α) (m : ℕ) : foldl (fun (m : ℕ) (x : α) => m + m) m l = m * 2 ^ l.length

Doubling a counter once per element of a list multiplies it by 2 ^ length.

theorem Nat.two_pow_size_le (n : ℕ) : 2 ^ n.size ≤ 2 * n + 1

2 ^ Nat.size n is the least power of two above n, so it is at most 2 * n + 1.