## Stream: metaprogramming / tactics

### Topic: access named arguments of declaration

#### Johan Commelin (Oct 29 2020 at 09:29):

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


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?

#### Mario Carneiro (Oct 29 2020 at 09:30):

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

#### 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  #### 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]  #### Johan Commelin (Oct 29 2020 at 09:37): But often they will be unique, right? #### Mario Carneiro (Oct 29 2020 at 09:38): They are whatever the user wrote #### 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. #### Mario Carneiro (Oct 29 2020 at 09:39): the autogenerated names are not disambiguated, so you will find a (or rather, ᾰ) a lot #### 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. #### 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]


#### Johan Commelin (Oct 29 2020 at 09:45):

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

#### Johan Commelin (Oct 29 2020 at 09:45):

Those will be unique 99.9% of the time.

#### Mario Carneiro (Oct 29 2020 at 09:46):

unless they are called this

#### Mario Carneiro (Oct 29 2020 at 09:46):

what do you want to do with this information?

#### Mario Carneiro (Oct 29 2020 at 09:46):

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

#### 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]


#### 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.

#### 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.

#### 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.

#### Johan Commelin (Oct 29 2020 at 09:51):

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

#### Johan Commelin (Oct 29 2020 at 09:51):

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

#### 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

#### Mario Carneiro (Oct 29 2020 at 09:54):

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

#### Johan Commelin (Oct 29 2020 at 09:54):

Hmm... that sounds a lot harder

#### 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

#### Johan Commelin (Oct 29 2020 at 09:54):

See the calc-step branch for what I currently have

#### 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

#### Johan Commelin (Oct 29 2020 at 09:55):

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

#### Mario Carneiro (Oct 29 2020 at 09:55):

well you have to classify the lemma anyway to use it

#### 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.

#### 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

#### Mario Carneiro (Oct 29 2020 at 09:57):

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

#### 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 ...


#### Johan Commelin (Oct 29 2020 at 09:58):

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

#### Johan Commelin (Oct 29 2020 at 09:58):

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

#### 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