tactic look around

Stream: general

[Patrick Massot]

Assume I write

class foo :=
(bar : nat)

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

[Patrick Massot]

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]

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]

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]

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]

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]

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

[Simon Hudon]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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.