## Stream: general

### Topic: tactic look around

#### Patrick Massot (Mar 06 2018 at 10:23):

Assume I write

class foo :=
(bar : nat)

instance : foo :=
{ bar := by magic }


#### Patrick Massot (Mar 06 2018 at 10:24):

Can I write a tactic magic which knows that the instance I'm trying to create has type foo and the current field I'm working on is called bar?

#### Patrick Massot (Mar 06 2018 at 10:33):

The motivation for this question is https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/indexed_product.lean (look at all lines containing funext)

#### Scott Morrison (Mar 06 2018 at 13:45):

I'm also interested in this question! As far as I understand, this isn't possible, but it seems quite desirable for tactics to be able to know the "reason" they have been invoked.

#### Simon Hudon (Mar 06 2018 at 19:04):

The closest I can find is decl_name which tells you the name of the declaration being elaborated. I haven't tried but I'm not sure resolve_name would work on it to then get the type

#### Simon Hudon (Mar 06 2018 at 19:09):

What you could try is

instance : foo :=
begin magic ... end


Where magic acts a bit like refine and use structure_fields to apply funext ; ... for every fields for which it works and leaves the other ones untouched.

#### Scott Morrison (Mar 07 2018 at 00:40):

@Simon Hudon, decl_name works fine, but feeding that into resolve_name just gets an error message identifier not found. Oh well!

#### Simon Hudon (Mar 07 2018 at 00:41):

I'm not too surprised. I'm looking at that file right now and I think target is more promising.

#### Simon Hudon (Mar 07 2018 at 00:41):

I think the tactic will look like:

instance monoid [∀ i, monoid \$ f i] : monoid (Π i : I, f i) :=
by lifted_instance [indexed_product.has_one,indexed_product.semigroup]


#### Simon Hudon (Mar 07 2018 at 01:22):

Here's what I ended up with: https://github.com/PatrickMassot/lean-differential-topology/pull/1

#### Simon Hudon (Mar 07 2018 at 01:23):

The Lean developers added pexpr.mk_structure_instance after I complained about it but I never got around to using it. I think it's a very nice feature.

Last updated: May 16 2021 at 05:21 UTC