Just some copy and paste

tactic2.lean

/-
constant eq_test {sz:size}: sbitvec sz → bitvector sz → Prop
  

axiom eq_const (sz:size): ∀ (z:ℤ),
    eq_test (sbitvec.of_int sz z) (bitvector.of_int sz z)

meta instance eq_const_decidable (sz:size): decidable (∀ (z:ℤ),
    eq_test (sbitvec.of_int sz z) (bitvector.of_int sz z)) :=
-- Run z3 here. (this works only if instance supports meta tag.)
sorry

axiom eq_add (sz:size): ∀ (z:ℤ) (s1 s2:sbitvec sz) (b1 b2:bitvector sz),
    eq_test s1 b1 → eq_test s2 b2 →
    eq_test (s1.add s2) (b1.add b2)
-- and..

meta instance eq_add_decidable (sz:size): decidable (∀ 
    (z:ℤ) (s1 s2:sbitvec sz) (b1 b2:bitvector sz),
    eq_test s1 b1 → eq_test s2 b2 →
    eq_test (s1.add s2) (b1.add b2)) :=
-- Run z3 here. (this works only if instance supports meta tag.)
sorry

axiom eq_udiv (sz:size): ∀ (z:ℤ) (s1 s2:sbitvec sz) (b1 b2:bitvector sz),
    eq_test s1 b1 → eq_test s2 b2 → b2 ≠ bitvector.zero sz →
    eq_test (s1.add s2) (b1.add b2)

meta def fff (x:name) : tactic unit :=



def TT (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))

def prove (ax:size → Prop):io bool :=
-/

/-
sz_expr ← to_expr ```(sz),
the_sz ← eval_expr size sz_expr,

a1_res ← eval_expr (sbitvec the_sz) a1,

simp_lemmas ← simp_lemmas.mk_default,
simp_target simp_lemmas,
e ← target,
trace e,


  trace "----",
  e ← delta [`bitvector.add , `sbitvec.add, `sbitvec.of_bv, `bitvector.of_int,
             `has_coe] e,
  trace e,
  trace "----",
  simp_lemmas ← simp_lemmas.mk_default,
  simp_target simp_lemmas,
  e ← target,
  trace e,

a1_res ← eval_expr (sbitvec the_sz) a1
-/


/-

  -- Let's make `x = 0x....`
  --xeq ← to_expr ```(%%x = (bitvector.of_int sz 123)),
  xeq ← to_expr ```(mk_eq sz %%x (bitvector.of_int sz 123)),
  -- Let's make `y = 0x....`
  --yeq ← to_expr ```(%%y = (bitvector.of_int sz 456)),
  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)))
  (e, _, _) ← rewrite xeq e,
  (e, _, _) ← rewrite yeq e,
  sz_expr ← to_expr ```(sz),
  trace e,
  -/