letI/exactI within do notation

Stream: metaprogramming / tactics

[Eric Wieser]

Is there any way to make letI or exactI work within do notation? I can't work out how to nest a tactic application appropriatel. The failing example where I don't try anything is:

import tactic.core

meta def expr.has_add (t : tactic.instance_cache) :
  tactic (tactic.instance_cache × has_add expr) :=
do
  (t, add) ← t.mk_app `has_add.add [],
  pure (t, { add := λ a b, add a b })

run_cmd show tactic unit, from do
  c ← tactic.mk_instance_cache `(ℕ),
  (_, inst) ← expr.has_add c,
  let e := `(1 : ℕ).to_expr + `(2 : ℕ),
  -- failed to synthesize type class instance for
  -- inst : has_add expr
  -- ⊢ has_add expr
  tactic.trace e

[Alex J. Best]

Can you just give up on having nice notation for what you want?

import tactic.core

meta def expr.has_add (t : tactic.instance_cache) :
  tactic (tactic.instance_cache × has_add expr) :=
do
  (t, add) ← t.mk_app `has_add.add [],
  pure (t, { add := λ a b, add a b })

run_cmd show tactic unit, from do
  c ← tactic.mk_instance_cache `(ℕ),
  (_, inst) ← expr.has_add c,
  let e := @has_add.add _ inst `(1 : ℕ).to_expr `(2 : ℕ),
  -- failed to synthesize type class instance for
  -- inst : has_add expr
  -- ⊢ has_add expr
  tactic.trace e

[Eric Wieser]

Yeah, I guess that's not too bad

[Eric Wieser]

A related but subtly different question: how can I inject local exprs into the tactic cache?

/-- Produce the term `λ {a : α} [add_comm_monoid α], (by apply_instance : has_add α)` -/
meta def get_has_add_from_add_comm_monoid : tactic (expr) :=
do
  u ← tactic.mk_meta_univ,
  α ← tactic.mk_local' `α binder_info.implicit (expr.sort u.succ),
  add_comm_monoid_α ← tactic.mk_app `add_comm_monoid [α] >>= tactic.mk_local' `_inst_2 binder_info.inst_implicit,
  -- this line fails, it doesn't know to use the local`add_comm_monoid_α `
  ret ← tactic.mk_app `has_add [α] >>= tactic.mk_instance,
  tactic.lambdas [α, add_comm_monoid_α] ret

run_cmd get_has_add_from_add_comm_monoid
-- tactic.mk_instance failed to generate instance for
--   has_add α