Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC