max_unsigned.lean

-- Return the maximum unsigned number of a given width.
def max_unsigned : ℕ → ℕ
| 0 := 0
| (nat.succ x) := 2 * max_unsigned x + 1

open tactic nat

/- Function for convertiong a nat into a Lean expression using nat.zero and nat.succ.
   Remark: the standard library already contains a tactic for converting nat into a binary encoding. -/
meta def nat.to_unary_expr : nat → tactic expr
| 0        := to_expr `(nat.zero)
| (succ n) := do n_expr ← nat.to_unary_expr n, to_expr `(nat.succ %%n_expr)

/- Tactic for constructing a proof that the binary encoding for n is equal to the unary encoding. -/
meta def mk_bin_eq_unary (n : nat) : tactic expr :=
do bin_expr   ← nat.to_expr n,
   unary_expr ← nat.to_unary_expr n,
   type       ← to_expr `(%%bin_expr = %%unary_expr),
   proof      ← to_expr `(eq.refl %%unary_expr),
   to_expr `(@id %%type %%proof)

section
/- Test mk_bin_eq_unary -/
set_option pp.numerals false
run_command mk_bin_eq_unary 10 >>= infer_type >>= trace
end

lemma max_unsigned_16 : max_unsigned 16 = 0xffff :=
by do
   /- Convert 16 from binary to unary -/
   h ← mk_bin_eq_unary 16,
   /- Use simp for replacing binary 16 with the unary 16 -/
   simp_using [h],
   /- Now we can unfold max_unsigned 16 times -/
   dunfold [`max_unsigned],
   /- (norm_num n) will evaluate an arithmetic expression n, and return a pair (new_n, pr) where
      pr is a proof for n = new_n.
      First, we extract the left-hand-side.
      In the future, simp will invoke norm_num.-/
   (lhs, rhs) ← target >>= match_eq,
   (new_lhs, pr) ← norm_num lhs,
   /- The right hand side is already in "normal form". So pr is a proof that the lhs is equal to the rhs,
      so, we can just use exact. -/
   exact pr