Zulip Chat Archive

Stream: new members

Topic: expr: fields and @


view this post on Zulip Fabian Glöckle (Apr 17 2019 at 20:17):

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. (?)

view this post on Zulip Fabian Glöckle (Apr 17 2019 at 20:50):

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.

view this post on Zulip Fabian Glöckle (Apr 17 2019 at 22:08):

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

view this post on Zulip Simon Hudon (Apr 18 2019 at 00:13):

@ 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

view this post on Zulip Simon Hudon (Apr 18 2019 at 00:13):

It prints:

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

view this post on Zulip Simon Hudon (Apr 18 2019 at 00:14):

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

view this post on Zulip Keeley Hoek (Apr 18 2019 at 01:25):

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.

view this post on Zulip Fabian Glöckle (Apr 22 2019 at 21:31):

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

view this post on Zulip Fabian Glöckle (Apr 22 2019 at 21:33):

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.

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 15:03):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 15:28):

Hey! Sorry I forgot to answer

view this post on Zulip Simon Hudon (Apr 23 2019 at 15:30):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 15:31):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 15:34):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 15:37):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 15:38):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 18:16):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 18:18):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 18:19):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 18:27):

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.

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:04):

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?

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:05):

use mk_mapp instead of mk_app

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:08):

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)],

?

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:11):

Yes

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:11):

Instead of has_x_x_name you can use ``has_add.add

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:12):

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 α)

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:13):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:13):

try putting set_option pp.implicit true before your proof

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:15):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:15):

The error message should change

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:16):

still

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:16):

the number of the argument? #1 and #2

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:17):

Try replacing some i₁ with none

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:18):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:25):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:27):

we don't reach this point

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:28):

i.e. still the error

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:29):

How far does it get?

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:30):

till the mk_mapp I assume

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:30):

So if you put it before, it should print something

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:31):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:32):

Right, my bad

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:32):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:33):

I thought you had done that already

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:33):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:34):

yes

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:36):

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:36):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:41):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:41):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:42):

however, lean still reports

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

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:44):

The issue is with:

   has_x  mk_const has_x_name,
   has_x_x  mk_const has_x_x_name,

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:45):

Try putting this somewhere above your proof:

set_option pp.universes true
#check @has_add.add

view this post on Zulip Simon Hudon (Apr 23 2019 at 19:45):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:49):

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

view this post on Zulip Johan Commelin (Apr 23 2019 at 19:50):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:51):

:D :night_sky:

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 19:55):

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

view this post on Zulip Mario Carneiro (Apr 23 2019 at 19:59):

use unify to determine the universe variables

view this post on Zulip Mario Carneiro (Apr 23 2019 at 20:10):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:15):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:15):

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

view this post on Zulip Mario Carneiro (Apr 23 2019 at 20:16):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:20):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:22):

mk_meta_univ?

view this post on Zulip Simon Hudon (Apr 23 2019 at 20:23):

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

view this post on Zulip Patrick Massot (Apr 23 2019 at 20:25):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:26):

(α β : 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?

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:29):

like a normal function parameter?

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:31):

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

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:35):

ah, there is level.param

view this post on Zulip Fabian Glöckle (Apr 23 2019 at 20:54):

and the level list in declaration.defn

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 15:52):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 15:53):

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)

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:00):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:01):

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

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 16:02):

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

view this post on Zulip Simon Hudon (Apr 26 2019 at 16:05):

That's an error given by mk_app or mk_mapp

view this post on Zulip Simon Hudon (Apr 26 2019 at 16:07):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:14):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:14):

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

view this post on Zulip Simon Hudon (Apr 26 2019 at 16:18):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:19):

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

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 16:22):

I can solve that one

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 16:23):

Maybe I should apply for a job at MS

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:23):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:23):

Now we should have a minimal working example

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 16:24):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:25):

?

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 16:25):

You can't talk about terms in higher universes

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:27):

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

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 16:28):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:28):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:30):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:30):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:30):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:37):

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
}

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:38):

#check id_compatible works for me.

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:44):

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

view this post on Zulip Fabian Glöckle (Apr 26 2019 at 16:48):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:48):

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

view this post on Zulip Edward Ayers (Apr 26 2019 at 16:51):

Can anyone golf this down further?

view this post on Zulip Simon Hudon (Apr 26 2019 at 19:24):

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)

view this post on Zulip Mario Carneiro (Apr 26 2019 at 20:10):

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)

view this post on Zulip Johan Commelin (May 04 2019 at 08:56):

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

view this post on Zulip Mario Carneiro (May 04 2019 at 08:56):

yes, you can programmatically add docstrings to decls

view this post on Zulip Mario Carneiro (May 04 2019 at 08:56):

alias does this

view this post on Zulip Fabian Glöckle (May 06 2019 at 16:14):

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

view this post on Zulip Edward Ayers (May 06 2019 at 19:33):

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

view this post on Zulip Edward Ayers (May 06 2019 at 19:37):

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

view this post on Zulip Edward Ayers (May 06 2019 at 19:39):

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.

view this post on Zulip Edward Ayers (May 06 2019 at 19:57):

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.

view this post on Zulip Edward Ayers (May 06 2019 at 20:11):

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.

view this post on Zulip Edward Ayers (May 06 2019 at 20:51):

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?

view this post on Zulip Fabian Glöckle (May 28 2019 at 11:48):

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

view this post on Zulip Edward Ayers (May 28 2019 at 11:48):

No problem!


Last updated: May 08 2021 at 10:12 UTC