Creating random test from proposition using tactic library

tactic.lean

open tactic

private constant mk_eq (sz:size) (x y:bitvector sz): x = y
constant smt_eq {sz:size}: sbitvec sz → sbitvec sz → Prop

theorem eq_add2 (sz:size): ∀ (x y: bitvector sz),
    smt_eq (sbitvec.add (sbitvec.of_bv x) (sbitvec.of_bv y))
           (sbitvec.of_bv (bitvector.add x y)) :=
by do
  x ← intro `x,
  y ← intro `y,
  e ← target,
  sz_expr ← to_expr ```(sz),
  sz_val ← eval_expr size sz_expr,
  match e with
  | (expr.app (expr.app (expr.app its_smt_eq _) lhs) rhs) := do
          --(expr.app (expr.app (expr.const s_op _) s1) s2))
          --(expr.app _ (expr.app (expr.app (expr.const b_op _) b1) b2))) := do
    -- Let's make `x = 0x....`
    xeq ← to_expr ```(mk_eq sz %%x (bitvector.of_int sz 123)),
    -- Let's make `y = 0x....`
    yeq ← to_expr ```(mk_eq sz %%y (bitvector.of_int sz 456)),
    e ← target, -- goal: expr (smt_eq (add (of_bv x) (of_bv y)) (of_bv (bitvector.add x y)))
    (lhs, _, _) ← rewrite xeq lhs,
    (lhs, _, _) ← rewrite yeq lhs,
    trace lhs,
    (rhs, _, _) ← rewrite xeq rhs,
    (rhs, _, _) ← rewrite yeq rhs,
    trace rhs,
    -- Failed to synthesize [reflected (sbitvec sz_val)]
    lhs_val ← eval_expr (sbitvec sz_val) lhs,
    rhs_val ← eval_expr (sbitvec sz_val) rhs,
    unsafe_run_io (run_smt_test lhs_val rhs_val) -- Run z3!
  | _ := target >>= trace
  end