access named arguments of declaration

Stream: metaprogramming / tactics

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

But often they will be unique, right?

[Mario Carneiro]

They are whatever the user wrote

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

Those will be unique 99.9% of the time.

[Mario Carneiro]

unless they are called this

[Mario Carneiro]

what do you want to do with this information?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Hmm... that sounds a lot harder

[Mario Carneiro]

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

[Johan Commelin]

See the calc-step branch for what I currently have

[Johan Commelin]

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]

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

[Mario Carneiro]

well you have to classify the lemma anyway to use it

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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