expr: fields and @

Stream: new members

[Fabian Glöckle]

Hello everyone, in meta I am trying to build an expr for @has_add.add _ _ _ _. How are class/structure fields and the @-notation implemented? When I ask expr.app_fn about to_expr ``(@has_add.add), I get has_add.add. (?)

[Fabian Glöckle]

To be more precise, I want the has_add.add part to be dynamic (generated from a string to also support has_mul.mul etc.); the @is always needed.

[Fabian Glöckle]

Is the @ an annotation? My tests indicate no...

meta def diagnose : tactic (option (name × expr)) :=
do exp ← to_expr ``(@has_add.add),
   res ← pure $ expr.is_annotation exp,
   type ← infer_type exp,
   trace type,
   trace res,
   return res

--> trace output:

Π {α : Type ?} [c : has_add α], α → α → α
none

without the @:

?m_1 → ?m_1 → ?m_1
none

[Simon Hudon]

@ is used by the elaborator. It is only present pre-terms (i.e. pexpr). Consider:

meta def foo : tactic unit :=
do let e := ``(@has_add.add ),
   tactic.trace e.to_raw_fmt,
   tactic.trace e.is_annotation,
   let e := ``(has_add.add ),
   tactic.trace e.to_raw_fmt,
   tactic.trace e.is_annotation

run_cmd foo

[Simon Hudon]

It prints:

[macro annotation (const has_add.add [])]
(some (@, has_add.add))
(const has_add.add [])
none

[Simon Hudon]

``(@has_add.add) is a pre-term but to_expr makes it into a term

[Keeley Hoek]

I'm not sure what you want it to "behave like @ for", but be aware of tactic.mk_mapp which lets you provided all of the (even implicit) arguments implicitly or explicitly.

[Fabian Glöckle]

Thanks!
@Simon Hudon Can I add this annotation to an arbitrary application pexpr? (No, because meta constant macro_def : Type belongs to the kernel?!)
@Keeley Hoek Can I build such an app which involves terms of the form var <n> I which I can bind later on? (I got failed to infer type, unexpected bound variable occurrence when using var`terms which are not (yet) bound.)

[Fabian Glöckle]

My goal is to add a declaration like

def has_add_compatible :=
λ (α : Type u) (β : Type v) [i₁ : has_add α] [i₂ : has_add β] (f : α → β),
  ∀ {x y}, f (@has_add.add α i₁ x y) = @has_add.add β i₂ (f x) (f y)

to the environment with has_add.addbeing a template parameter which could also be set to has_mul.mul.

[Fabian Glöckle]

Do my questions make sense? Can I further elaborate on anything? Any help is appreciated :slight_smile:

[Simon Hudon]

Hey! Sorry I forgot to answer

[Simon Hudon]

You don't need to generate @ to create that definition. The following has the same effect:

do add <- mk_const has_add.add,
   return $ add α i₁ x y

[Simon Hudon]

or more simply: mk_mapp `has_add.add [α,i₁,x,y]

[Simon Hudon]

While in writing an expression like @has_add.add α i₁ x y you need the added tool of @ to specify implicit arguments, in building expr trees, you have to work harder if you want to omit an implicit argument. That's because app f x means the same whether the type of the expression f is Π x : t, t' or Π {x : t}, t'.

[Simon Hudon]

If you want to omit the first implicit argument, you have to first discover that it is indeed an implicit argument, then, you have to create a meta variable v of the right type and feed it to f: app f v. Then you have "omitted" the first arguments: you're relying on unification to figure out what it is

[Simon Hudon]

You can also use tactic.mk_app which behaves very similarly to what I described

[Fabian Glöckle]

Great, thanks, that clears up my questions about how app works for exprand pexpr!

[Fabian Glöckle]

I was trying to mix this with reflected code like in the following, is that possible?

meta def add_compatible_def (x : string) : command :=
do let has_x_name := name.mk_string (string.append "has_" x) name.anonymous,
   let has_x_x_name := name.mk_string x has_x_name,
   has_x ← mk_const has_x_name,
   has_x_x ← mk_const has_x_x_name,
   decl_type ← to_expr ``(Π (α : Type) (β : Type) [%%has_x α] [%%has_x β], (α → β) → Prop),
   decl_body ← to_expr ``(λ (α : Type) (β : Type) [i₁ : %%has_x α] [i₂ : %%has_x β] (f : α → β),
                          ∀ {x y : α}, f (%%has_x_x α i₁ x y) = %%has_x_x β i₂ (f x) (f y)),
   decl ← pure $ mk_definition `compatible [`u, `v] decl_type decl_body,
   add_decl decl

[Fabian Glöckle]

Currently the reflected code does not accept the arguments this way:

failed to synthesize type class instance for
α β : Type,
i₁ : has_add α,
i₂ : has_add β,
f : α → β,
x y : α
⊢ has_add Type
Additional information:
context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

[Simon Hudon]

Instead of using Π and λ in your quasiquotes, use mk_local' to create variables like α and β and the instances, then you use to_expr and quasiquotes to create ``((%%α → %%β) → Prop)and you use pis to create the pis and similarly with lambdas to create the lambdas.

[Fabian Glöckle]

very convenient :)
I tried:

meta def add_compatible_def (x : string) : command :=
do let has_x_name := name.mk_string (string.append "has_" x) name.anonymous,
   let has_x_x_name := name.mk_string x has_x_name,
   has_x ← mk_const has_x_name,
   has_x_x ← mk_const has_x_x_name,
   α ← mk_local' `α binder_info.default (sort (level.succ level.zero)),
   β ← mk_local' `β binder_info.default (sort (level.succ level.zero)),
   i₁ ← mk_local' `i₁ binder_info.inst_implicit (has_x α),
   i₂ ← mk_local' `i₂ binder_info.inst_implicit (has_x β),
   type_main ← to_expr ``((%%α → %%β) → Prop),
   let decl_type := expr.pis [α, β, i₁, i₂] type_main,
   f ← mk_local' `f binder_info.default (pi `a binder_info.default α β),
   x ← mk_local' `x binder_info.implicit α,
   y ← mk_local' `y binder_info.implicit α,
   app₁ ← mk_app has_x_x_name [α, i₁, x, y],
   app₂ ← mk_app has_x_x_name [β, i₂, (f x), (f y)],
   body_main ← to_expr ``(%%f (%%app₁) = %%app₂),
   let decl_body := expr.lambdas [α, β, i₁, i₂, f] (expr.pis [x, y] body_main),
  --  decl_body ← to_expr ``(λ (α : Type) (β : Type) [i₁ : %%has_x α] [i₂ : %%has_x β] (f : α → β),
  --                         ∀ {x y : α}, f (%%has_x_x α i₁ x y) = %%has_x_x β i₂ (f x) (f y)),
   trace decl_type,
   trace decl_body,
   decl ← pure $ mk_definition `compatible [`u, `v] decl_type decl_body,
   add_decl decl

It throws

[app_builder] failed to create an 'has_add.add'-application, failed to solve unification constraint for #2 argument (has_add α =?= has_add α)

What is the mistake?

[Simon Hudon]

use mk_mapp instead of mk_app

[Fabian Glöckle]

replacing with

   app₁ ← mk_mapp has_x_x_name [some α, some i₁, some x, some y],
   app₂ ← mk_mapp has_x_x_name [some β, some i₂, some (f x), some (f y)],

?

[Simon Hudon]

Yes

[Simon Hudon]

Instead of has_x_x_name you can use ``has_add.add

[Fabian Glöckle]

Replacing these lines I still get the same error

[app_builder] failed to create an 'has_add.add'-application, failed to solve unification constraint for #1 argument (has_add α =?= has_add α)

[Fabian Glöckle]

Instead of has_x_x_name you can use ``has_add.add

Yes, in the end I wanted to be able to write add_compatible_def "mul" or similar

[Simon Hudon]

try putting set_option pp.implicit true before your proof

[Fabian Glöckle]

I put it above the definition, but to no effect..

[Simon Hudon]

The error message should change

[Fabian Glöckle]

still

[app_builder] failed to create an 'has_add.add'-application, failed to solve unification constraint for #2 argument (has_add α =?= has_add α)

[Fabian Glöckle]

the number of the argument? #1 and #2

[Simon Hudon]

Try replacing some i₁ with none

[Fabian Glöckle]

[app_builder] failed to create an 'has_add.add'-application, there are missing implicit arguments

[Simon Hudon]

If you add infer_type app₁ >>= trace before mk_mapp, what does it print?

[Fabian Glöckle]

we don't reach this point

[Fabian Glöckle]

i.e. still the error

[Simon Hudon]

How far does it get?

[Fabian Glöckle]

till the mk_mapp I assume

[Simon Hudon]

So if you put it before, it should print something

[Fabian Glöckle]

but you want trace information on app1?
then I can't put it above its definition

[Simon Hudon]

Right, my bad

[Fabian Glöckle]

till the mk_mapp I assume

the error is app_builder_exception, more information can be obtained using command set_option trace.app_builder true

[Simon Hudon]

I thought you had done that already

[Fabian Glöckle]

(which I already used when I pasted the error messages above)

[Fabian Glöckle]

yes

[Fabian Glöckle]

infer_type i₁ >>= trace btw gives has_add α as expected

[Simon Hudon]

Then try replacing app₁ ← mk_app has_x_x_name [α, i₁, x, y] with app₁ ← to_expr ``(@has_add.add %%α %%i₁ %%x %%y), to see what kind of error we can get

[Fabian Glöckle]

strangely, it worked to replace only app1in this way, leaving app2 as is

[Fabian Glöckle]

the trace of decl_bodyis λ (α β : Type) [i₁ : has_add α] [i₂ : has_add β] (f : α → β), ∀ {x y : α}, f (x + y) = f x + f y

[Fabian Glöckle]

however, lean still reports

failed to add declaration 'compatible' to environment, type has metavariables
  Π (α β : Type) [i₁ : has_add α] [i₂ : has_add β], (α → β) → Prop

[Simon Hudon]

The issue is with:

   has_x ← mk_const has_x_name,
   has_x_x ← mk_const has_x_x_name,

[Simon Hudon]

Try putting this somewhere above your proof:

set_option pp.universes true
#check @has_add.add

[Simon Hudon]

It will show you that has_add.add has one universe parameter u_1. Do you see that?

[Fabian Glöckle]

genius! here we go (has_add.{0} α =?= has_add.{?l_1} α) is the error from before I didn't understand

[Johan Commelin]

Too bad there isn't a universe-emoji...

[Fabian Glöckle]

:D :night_sky:

[Fabian Glöckle]

now the question is how to (dynamically) construct the has_addconstant with the right universe?

[Mario Carneiro]

use unify to determine the universe variables

[Mario Carneiro]

In this case, it seems like you are assuming that has_x already exists and has type has_[x] : Type u -> Type u. In that case, you can replace the mk_const invocations, which create a universe metavariable, with an explicit expr.const with universe u = 0 (replace the has_x and has_x_x lines with these):

   let has_x : expr := expr.const has_x_name [level.zero],
   let has_x_x : expr := expr.const has_x_x_name [level.zero],

[Fabian Glöckle]

Yes that is what I assume, and it works this way!

[Fabian Glöckle]

And all predefined has_... live in universe zero?

[Mario Carneiro]

no, they have type Type u -> Type u, so if you want alpha to have Type 0 then you have to set u = 0

[Fabian Glöckle]

how would I achieve the effect of α β : Type*?

[Fabian Glöckle]

mk_meta_univ?

[Simon Hudon]

(α β : Type*) is short for (α : Type u) (β : Type v) where u and v are not meta universes but universe parameters

[Patrick Massot]

Be careful that last message is unfortunately inaccurate, this is a well known bug

[Fabian Glöckle]

(α β : Type*) is short for (α : Type u) (β : Type v) where u and v are not meta universes but universe parameters

how can I declare universe parameters for my declaration?

[Fabian Glöckle]

like a normal function parameter?

[Fabian Glöckle]

meta def add_compatible_def (x : string) (u v : level): command ?

[Fabian Glöckle]

ah, there is level.param

[Fabian Glöckle]

and the level list in declaration.defn

[Fabian Glöckle]

Next questions :)
What does [app_builder] failed to create an 'mul_compatible'-application, failed to retrieve declarationmean?

[Fabian Glöckle]

My code:

def mul_compatible' {α β : Type} [has_mul α] [has_mul β] (f : α → β) : Prop :=
∀ {x0 x1 : α}, f (x0 * x1) = f x0 * f x1

lemma mul_compatible_id' {α : Type} [has_mul α]: mul_compatible' (id : α → α) := λ x y, rfl

meta def add_compatible_id_lemma : command :=
do has_mul ← mk_const `has_mul,
   α ← mk_local' `α binder_info.implicit (sort (level.succ level.zero)),
   i ← mk_local' `i binder_info.inst_implicit (has_mul α),
   let ida : expr := const `id [level.succ level.zero],
   stmt ← mk_app `mul_compatible' [α, α, i, i, ida α],  -- <-- error here
   let decl_type := expr.pis [α, i] stmt,
   x ← mk_local' `x binder_info.default α,
   y ← mk_local' `y binder_info.default α,
   let rf : expr := const `rfl [level.succ level.zero],
   mcapp ← mk_app `mul_compatible' [α, α, i, i, ida α, x, y],
   let decl_body := expr.lambdas [α, i, x, y] (rf mcapp),
   add_decl $ declaration.thm `id_compatible [] decl_type (task.pure decl_body)

[Fabian Glöckle]

I'd like to generate the lemma mul_compatible_id'by code in a way such that I can later adapt it to other has_xsituations (hence no quasiquotations).

[Fabian Glöckle]

@Simon Hudon Do you have an idea what I did wrong?

[Kevin Buzzard]

@Fabian Glöckle do you have any comments on the univalence thread going on in the main chat?

[Simon Hudon]

That's an error given by mk_app or mk_mapp

[Simon Hudon]

There's an option that you can set to give more details about the application you're trying to build. The error message should mention which one

[Fabian Glöckle]

The error message is

app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`

what I posted is already message from activating trace.app_builder

[Edward Ayers]

I got [app_builder] failed to create an 'mul_compatible''-application, failed to solve unification constraint for #4 argument (has_mul α =?= has_mul α)

[Simon Hudon]

try set_option pp.implicit true and set_option pp.universes true

[Edward Ayers]

[app_builder] failed to create an 'mul_compatible''-application, failed to solve unification constraint for #4 argument (has_mul.{0} α =?= has_mul.{?l_1} α)

[Kevin Buzzard]

I can solve that one

[Kevin Buzzard]

Maybe I should apply for a job at MS

[Fabian Glöckle]

I got [app_builder] failed to create an 'mul_compatible''-application, failed to solve unification constraint for #4 argument (has_mul α =?= has_mul α)

Sorry, you are right. Replacing the first line of the metacommand with

let has_mul : expr := const `has_mul [level.zero],

gives my error

[Fabian Glöckle]

Now we should have a minimal working example

[Kevin Buzzard]

Fabian, remember also to build a proper ZFC version of your tactic, which only allows Type and Prop for most basic definitions

[Fabian Glöckle]

?

[Kevin Buzzard]

You can't talk about terms in higher universes

[Fabian Glöckle]

:D no that was not the problem (though I still do not understand how to use universe parameters when building code)

[Kevin Buzzard]

Most mathematicians don't need those higher universes, so write a version that only works for things in Type and my mathematician's wager is that this never bothers us at all. I'm not really suggesting you do it, it's just that I am getting more and more weirded out by all this insistence on polymorphism when all it has done for me as a mathematician was cause me problems

[Edward Ayers]

Ah, the problem is that mk_app `mul_compatible' [α, α, i, i, ida α, x, y] is not allowed because mul_compatible' only accepts 5 arguments.

[Edward Ayers]

It's a shame Lean couldn't do that unification problem.

[Fabian Glöckle]

Oh right; i had thought it appeared in the first one :o

[Fabian Glöckle]

what would i do to specify the right type for the rfl (and do I need to?)

[Edward Ayers]

open tactic expr

def mul_compatible' {α β : Type} [has_mul α] [has_mul β] (f : α → β)  : Prop :=
∀ {x0 x1 : α}, f (x0 * x1) = f x0 * f x1

lemma mul_compatible_id' {α : Type} [has_mul α]: mul_compatible' (id : α → α) := λ x y, rfl

meta def add_compatible_id_lemma : command :=
do has_mul : expr ← pure $ const `has_mul [level.zero],
   α ← mk_local' `α binder_info.implicit (sort (level.succ level.zero)),
   i ← mk_local' `i binder_info.inst_implicit (has_mul α),
   ida : expr ← pure $ const `id [level.succ level.zero],
   stmt ← mk_app `mul_compatible' [α, α, i, i, ida α],  -- <-- error here
  let decl_type := expr.pis [α, i] stmt,

   x ← mk_local' `x binder_info.default α,
   y ← mk_local' `y binder_info.default α,
   xy ← mk_app `has_mul.mul [i, x, y],
   rf ← mk_app `rfl [xy],
   let decl_body := expr.lambdas [α, i, x, y] (rf),
   add_decl $ declaration.thm `id_compatible [] decl_type (task.pure decl_body)

-- set_option trace.app_builder true
-- set_option pp.all true
-- set_option formatter.hide_full_terms false
run_cmd do {
  add_compatible_id_lemma
}

[Edward Ayers]

#check id_compatible works for me.

[Fabian Glöckle]

Oh great, thanks
It turns out these weren't issues with metaprogramming but with understanding the rflproof :D

[Fabian Glöckle]

I really appreciate the helpful atmosphere here, thanks again!!

[Edward Ayers]

You can get Lean to do most of the work:

open tactic expr

def mul_compatible' {α β : Type} [has_mul α] [has_mul β] (f : α → β)  : Prop :=
∀ {x0 x1 : α}, f (x0 * x1) = f x0 * f x1

lemma mul_compatible_id' {α : Type} [has_mul α]: mul_compatible' (id : α → α) := λ x y, rfl

meta def add_compatible_id_lemma : command :=
do
   target ← to_expr ```(Π {α : Type} [has_mul α], mul_compatible' (id : α → α)),
   g ← mk_mvar,
   gs ← get_goals,
   set_goals [g],
   change target,
   intro_lst [`α, `i, `x,`y], -- or just `intron 4`
   reflexivity,
   set_goals gs,
   g ← instantiate_mvars g,
   add_decl $ declaration.thm `id_compatible [] target (task.pure g)


run_cmd do {
  add_compatible_id_lemma
}

#check id_compatible

[Edward Ayers]

Can anyone golf this down further?

[Simon Hudon]

Try:

meta def add_compatible_id_lemma : command :=
do target ← to_expr ```(Π {α : Type} [has_mul α], mul_compatible' (id : α → α)),
   (_,g) ← solve_aux target $ do
   { intro_lst [`α, `i, `x,`y], -- or just `intron 4`
     reflexivity },
   g ← instantiate_mvars g,
   add_decl $ declaration.thm `id_compatible [] target (task.pure g)

[Mario Carneiro]

meta def add_compatible_id_lemma : command :=
do
   target ← to_expr ```(Π {α : Type} [has_mul α], mul_compatible' (id : α → α)),
   g ← to_expr ```(λ α i x y, rfl : %%target),
   add_decl $ declaration.thm `id_compatible [] target (task.pure g)

[Johan Commelin]

Can your tactics also add docstrings to the new declarations? @Mario Carneiro Is such a thing possible?

[Mario Carneiro]

yes, you can programmatically add docstrings to decls

[Mario Carneiro]

alias does this

[Fabian Glöckle]

thank you three for the immediate golfing instinct by the way
my real code is for generic has_xyz though where i couldn't use quotations so easily
any ideas on how to improve this? https://github.com/faabian/mathlib/blob/meta/meta.lean

[Edward Ayers]

Maybe something like this. It's not much shorter but you don't have to worry about universes anywhere.

meta def add_compatible_def (x : string): command :=
do let T : expr := expr.sort $ level.succ $ level.param `v,
   let has_x_name := mk_simple_name ("has_" ++ x),
   let has_x_x_name := has_x_name <.> x,
   has_x ← mk_const has_x_name,
   t ← mk_const has_x_x_name >>= infer_type,
   ((ty :: cl :: domain), codomain) ← mk_local_pis t,
   let arity := domain.length,
   let target_self := codomain =  ty,
   target_prop ← is_prop codomain,
   decl_type ← to_expr ```(Π {α β :%%T} [%%has_x α] [%%has_x β] (f : α → β), Prop),
   (_,decl_body) ← solve_aux decl_type (do
     [α,β,i₁,i₂,f] ← intros,
     vars ← list.mmap (λ n, do
        refine_forall (mk_simple_name ("x" ++ to_string n)) α
     ) $ list.range arity,
     app₁ ← mk_app has_x_x_name $ vars,
     app₂ ← mk_app has_x_x_name $ list.map (expr.app f) vars,
     body_main ← if target_self then to_expr ``(%%f (%%app₁) = %%app₂)
                  else (if target_prop then to_expr ``(%%app₁ ↔ %%app₂)
                        else to_expr ``(%%app₁ = %%app₂)),
     exact body_main
   ),
   decl_body ← instantiate_mvars decl_body,
   let decl_name := mk_simple_name (x ++ "_compatible"),
   add_decl $ mk_definition decl_name (collect_univ_params decl_type) decl_type decl_body  -- universes here
   -- todo: allow both → and ↔ for Prop-valued?

run_cmd add_compatible_def "mul"
run_cmd add_compatible_def "ternary"
run_cmd add_compatible_def "lt"
run_cmd add_compatible_def "to_string"
#print mul_compatible
#print ternary_compatible
#print lt_compatible
#print to_string_compatible

[Edward Ayers]

I defined refine_forall as:

/-- Take a goal `⊢ Prop` and fill with a `pi` to get a new goal `n : type ⊢ Prop` -/
meta def refine_forall (n : name) (type : expr) : tactic expr := do
    f_type ← to_expr ```(%%type → Prop),
    f ← mk_meta_var f_type,
    tactic.exact (expr.pi n binder_info.default type (expr.app f (expr.var 0))),
    set_goals [f],
    intro n

[Edward Ayers]

Your code looks fine. If you are having to explicitly write out universe terms then Lean probably provides a tactic that means you don't have to.

[Edward Ayers]

I prefer always having local variables held in the tactic_state's context rather than using mk_local and friends. This is because you don't have to worry about pretty names and unique names etc. But there is nothing wrong with the mk_local way.

[Edward Ayers]

There should be a way to replace count_vars, arrow_list, with tactic.mk_local_pis, tactic.get_pi_arity and so on. They are in /library/init/meta/tactic.lean and expr.lean.

[Edward Ayers]

This has been a good exercise for me. Here are some problems that I had:
- If I write to_expr ```(Π {α β}, ... it makes a new universe metavariable. Then I get told off for trying to make a decl with a metavariable in it. I couldn't find a nice way of telling the tactic_state to turn all remaining universe metas in to universe parameters instead. Am I not seeing the tactic?
- refine_forall (and refine_pi) is a utility function that I use a lot and find really useful. Is there a version of this in mathlib or core?
- Is it better to use mk_local_pis and expr.pis or to wrap things in tactics?

[Fabian Glöckle]

Thanks @Edward Ayers for your tricks, that solved my universe issues!

[Edward Ayers]

No problem!