Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: access named arguments of declaration


view this post on Zulip Johan Commelin (Oct 29 2020 at 09:29):

#print has_add.add
-- def has_add.add : Π {α : Type u} [c : has_add α], α → α → α :=
-- λ (α : Type u) [c : has_add α], [has_add.add c]

Suppose I have e <- resolve_name `has_add.add. How do I ask lean what the names are of its arguments?
Or rather, suppose I know that it has an argument called c. How do I ask lean at which position this argument is?

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:30):

I guess you could get the type and look for binders with that name

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:34):

open tactic
meta def find_named_arg (n : name) : expr  option 
| (expr.pi a _ _ e) := if n = a then some 0 else nat.succ <$> find_named_arg e
| _ := none

run_cmd do
  d  get_decl ``has_add.add,
  n  find_named_arg `c d.type,
  trace n -- 1

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:36):

Note however that the names are not unique:

open tactic
meta def find_named_arg (n : name) : expr  list 
| (expr.pi a _ _ e) := (if n = a then [0] else []) ++ nat.succ <$> find_named_arg e
| _ := []

run_cmd do
  d  get_decl ``has_add.add,
  trace $ find_named_arg `a d.type -- [2, 3]

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:37):

But often they will be unique, right?

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:38):

They are whatever the user wrote

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:38):

Your first version of find_named_arg will just return the first occurence, right? I guess that's good enough for me.

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:39):

the autogenerated names are not disambiguated, so you will find a (or rather, ) a lot

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:39):

Mario Carneiro said:

They are whatever the user wrote

Right, which means that if it's not an auto-generated name, then it's very likely to be unique.

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:42):

instances however are disambiguated:

open tactic
meta def arg_names : expr  list name
| (expr.pi a _ _ e) := a :: arg_names e
| _ := []

def foo [has_lt ] [has_le ] :      := λ x y, x

run_cmd do
  d  get_decl ``foo,
  trace $ arg_names d.type -- [_inst_1, _inst_2, a, a]

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:45):

Right, but for my application I care about things like hc : 0 < c.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:45):

Those will be unique 99.9% of the time.

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:46):

unless they are called this

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:46):

what do you want to do with this information?

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:46):

We haven't really been cultivating an environment of "binder names matter"

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:48):

Also explicit _ arguments:

def foo [has_lt ] [has_le ] :  (_ : ) (_ : ),  := by intros; assumption

run_cmd do
  d  get_decl ``foo,
  trace $ arg_names d.type -- [_inst_1, _inst_2, _x, _x]

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:49):

I'm trying to build a tactic that will help beginners. Many beginners don't understand the naming convention. If they are doing a simple calculations and the want to change the goal from x < y to 2 * x < 2 * y, which lemma do they need? I've collected a list of lemmas, and its currently ~70 lines long. I already know it is not complete, and should probably be twice as long.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:50):

So I want to build a calc_step tactic, that will be help the user "say what they want". And calc_step? should tell them the lemma they are looking for.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:51):

At the moment you can write calc_step 2 mul L, and it will change x < y into 2 * x < 2 * y, and discharge the side goal 0 < 2 by norm_num.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:51):

But the way it works is that it uses a custom database of 70 curated lemmas.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:51):

Now I would like to make it extensible using an attribute.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:53):

So I need to know which place to plug in the value c for lemmas like 0 < c -> c * a < c * b -> a < b

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:54):

you should analyze the type of the theorem for that rather than relying on names

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:54):

Hmm... that sounds a lot harder

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:54):

in this case, c is the only non-propositional argument that doesn't appear in the goal

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:54):

See the calc-step branch for what I currently have

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:55):

Mario Carneiro said:

in this case, c is the only non-propositional argument that doesn't appear in the goal

Unless the goal was stated as an iff

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:55):

In which case you need to look at both sides of the goal

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:55):

well you have to classify the lemma anyway to use it

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:56):

Ok, this analyzing of the type sounds like a good idea. But I guess I'll need a ton of help to pull it off. Good thing that we have this stream.

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:56):

if you go to theorems about nat for instance the forms are exactly the same but the variables are called k,m,n instead

view this post on Zulip Mario Carneiro (Oct 29 2020 at 09:57):

and we can't decide whether n names the first or second variable ;)

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:57):

No sure. I was thinking that the attribute would look like

@[calc_step (`c, [`hc])]
lemma foo_bar ...

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:58):

So the names would be tailored to the lemma that is being tagged.

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:58):

But if we can change it to @[calc_step] lemma foobar that would be even nicer.

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 10:00):

If you have h and want to change it to h', can you do have h' : ..., by library_search?


Last updated: May 09 2021 at 21:10 UTC