Zulip Chat Archive

Stream: general

Topic: tactic look around


view this post on Zulip Patrick Massot (Mar 06 2018 at 10:23):

Assume I write

class foo :=
(bar : nat)

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Simon Hudon (Mar 07 2018 at 01:22):

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

view this post on Zulip 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