Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: letI/exactI within do notation


Eric Wieser (Jul 28 2022 at 13:17):

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 (Jul 28 2022 at 13:21):

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 (Jul 28 2022 at 13:42):

Yeah, I guess that's not too bad

Eric Wieser (Jul 28 2022 at 13:47):

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 α

Last updated: Dec 20 2023 at 11:08 UTC