Monday afternoon: metaprogramming session

Stream: Lean for the curious mathematician 2020

[Rob Lewis]

Hi everyone! The "intermediate track" for the afternoon is a tutorial about metaprogramming (i.e. writing your own tactics). We expect most people to follow the other track; this is aimed at people who have some familiarity with Lean already. If that sounds like you, and you're interested in metaprogramming, read on.

[Rob Lewis]

Under the assumption that many more people will watch these recorded than live, I pre-recorded the videos. They're all on YouTube for you to watch at your leisure. https://www.youtube.com/playlist?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2

[Rob Lewis]

I'll be around this afternoon if anyone has questions, comments, or wants to try something out.

[Carl Friedrich Bolz-Tereick]

Thanks a lot for doing the recording!

[Antoine Chambert-Loir]

When/where does this session take place?

[Johan Commelin]

@Rob Lewis

[Rob Lewis]

One sec! Zoom link is coming.

[Rob Lewis]

But the obvious place to start is the YouTube videos :)

[Rob Lewis]

There's like 90 minutes of stuff there.

[Rob Lewis]

https://vu-live.zoom.us/j/99368691219 (Password: 654479)

[Patrick Massot]

Rob, what we need to know is when people can do exercises.

[Rob Lewis]

Video 5 gets you to the point where you can tackle the first couple exercises I posted, as well as many from the Hitchhiker's Guide.

[Rob Lewis]

I'm happy to answer questions in the Zoom chat.

[Rob Lewis]

If people have watched the videos and want to work on exercises together, I can set that up too.

[Patrick Massot]

People who want the exercises can run leanproject get lftcm2020 then cp -r lftcm2020/src/exercises_sources/ lftcm2020/src/my_exercises before code lftcm2020 and see whatever sits in src/my_exercises/monday

[Amos Turchet]

is this "suggested" for those who already completed the NNG?

[Rob Lewis]

To clarify again for people joining this session: there's no "live presentation." I'll be hanging out in the Zoom room to answer questions. If you'd like to collaborate with people on the exercises, we can set that up too.

[Patrick Massot]

There is quite a gap from NNG to this session

[Scott Morrison]

@Amos Turchet, it might still be a jump.

[Rob Lewis]

But I have nothing to say if you don't have anything to ask :)

[Patrick Massot]

If you have done NNG but nothing else, then you should probably wait for tomorrow morning session.

[Johan Commelin]

@Amos Turchet There is also the "complex number game"

[Scott Morrison]

There are perhaps four levels of things to do:

1. the natural numbers game
2. leanproject get tutorial
3. leanproject get lftcm2020 and have a go at the exercises (really intended for later in the week)
4. Rob's meta-programming tutorials

[Johan Commelin]

And I think Kevin has some more games up his sleeve

[Scott Morrison]

And the natural numbers game also includes hanging out with Kevin and helping people who are working through the NNG.

[Amos Turchet]

yeah Kevin just gave stuff to do, I'll try that first and then follow the suggestions. Thanks!

[Scott Morrison]

Kevin is also saying right now that he has some extra levels/worlds available for people finished with the NNG but not ready to go on to more advanced things.

[Amos Turchet]

the "lost levels" are perfect to do after the NNG thanks!

[Rob Lewis]

I should add: even if you're not interested in writing metaprograms, the first two videos of the metaprogramming session should be reasonably accessible. They won't get you to the stage where you can do anything. But you could still learn something.

[Scott Morrison]

Seconding this --- the first two videos are useful as soon as you've done a few levels of the natural numbers game.

[Jeremy Avigad]

Can someone post the address for getting the local version of the natural numbers game?

[Jeremy Avigad]

(the lost levels)

[Amos Turchet]

you can see the link here

[Amos Turchet]

https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Mon.20afternoon.3A.20natural.20number.20game/near/203703423

[Vaibhav Karve]

@Rob Lewis Thank you for creating these videos. I have only watched #1 and #2 so far but they are so clearly explained. :clap: My plan is to get through all of your videos as my own pace spread out over this week.

[Rob Lewis]

You're welcome! I hope the clarity stays throughout the series, but no promises ;)

[Matt Earnshaw]

yes, thanks very much @Rob Lewis. I have watched 1-4 so far, just what I was looking for to break into lean metaprogramming properly

[Eric Wieser]

Regarding the add_nonneg_proof exercise - after I've done d ← get_decl n, how can I inspect the d object? Neithertrace d nor trace (expr.to_raw_fmt d) work, and that exhausts my list of inspection tools.

[Rob Lewis]

Ah, I didn't realize declaration doesn't have a formatting instance. trace d really should work. We can fix that. In the meantime, if you look around docs#declaration you'll see lots of functions operating on declarations. You can trace d.to_name, d.type, things like that.

[Damien Thomine]

Nice videos, and I can work on it at my own pace. There is one thing I don't quite understand, on the first exercise (write a tactic for finding contradictions), the following works :

do ctx ← local_context, exfalso, ctx.mfirst ( λ x, do apply x, ctx.mfirst ( λ y, exact y ) )

while this doesn't (nor does any variation I tried on this second version):

do ctx ← local_context, exfalso, ctx.mfirst ( λ x, do ctx.mfirst ( λ y, exact (x y) ) )

How come?

[Scott Morrison]

What error messages are you getting? Could you post a #mwe?

[Johan Commelin]

@Damien Thomine My guess (but I'm at about the same level as you) is that you can't simply write (x y), and you need something like mk_app x [y].

[Johan Commelin]

Of maybe exact ``(x y) will work?

[Scott Morrison]

maybe with some antiquotations?

[Johan Commelin]

Aah, probably... like I said: I'm very much a beginner myself. So you mean exact ``(%%x %%y) ?

[Scott Morrison]

Yes, but perhaps you need to elaborate it first, with to_expr ``(%%x %%y) >>= exact? I'd have to actually run the code to know.

[Billy Price]

Just practicing metaprogramming and I have an issue. As a warmup to what I actually want to do, I'd like to find and print everything in the context that look like this WF Γ A a. It looks like my "is_WF" function is wrong, since the filtered list is always empty. Is it because WF Γ A a actually has the structure ((WF Γ) A) a?

meta def is_WF : expr → bool
| `(TT.WF %% _) := tt
| _ := ff

meta def tactic.interactive.print_WFs : tactic unit :=
do
  x ← local_context >>= list.mfilter (λ h, do H ← infer_type h, return (is_WF H)),
  trace x,
  skip

[Rob Lewis]

@Damien Thomine You've actually stumbled onto something pretty subtle here.

Your second version should be fine, in principle. x y is equivalent to expr.app x y. Most of the time in your tactic, this is a badly formed expression -- it's something like a proof of B applied to a proof of A, which is type incorrect. Using expr.app doesn't give you any checks on whether your expressions are type correct. But this should be alright, because exact should realize the expression is badly formed and fail.

However, exact takes some shortcuts for efficiency reasons. The vast majority of expressions it gets are well typed. So it doesn't do a full check for correctness. It will notice that the proof of B applied to the proof of A is bad. But if you give it a proof of ¬B applied to a proof of A, I think, it will recognize that you have a function (B → false) applied to an argument and assume the result is of type false, without checking the argument.

So your tactic is actually succeeding. It's closing the goal with a badly formed proof. Of course this isn't valid. When the tactic is done running, the kernel gets its result, and needs to check that it's a term with the type you claim. But it isn't, so the kernel fails. Notice how in your failing example, the error is reported at the word example instead of at the tactic call by contr. Normally, if your tactic was bad, it would report the error at the tactic call.

meta def contr : tactic unit :=
do ctx ← local_context, exfalso, ctx.mfirst ( λ x, do ctx.mfirst ( λ y, exact (x y) ) )

example (A B C : Prop) (ha : A) (hb : B) (hna : ¬ A) : false :=
by contr

One workaround to this: you can ask the tactic to fully type check the term before feeding it into exact.

meta def contr : tactic unit :=
do ctx ← local_context, exfalso, ctx.mfirst ( λ x, do ctx.mfirst ( λ y, do type_check (x y), exact (x y) ) )

example (A B C : Prop) (ha : A) (hb : B) (hna : ¬ A) : false :=
by contr

[Rob Lewis]

This is a very slick solution to the exercise, by the way!

[Rob Lewis]

@Billy Price TT.WF takes three arguments? You probably want your match to be `(TT.WF _ _ _) .

[Rob Lewis]

The double %% in that position is used for binding a variable.

[Rob Lewis]

i.e. ``(TT.WF %%a %%b _) would let you use a and b on the right hand side.

[Billy Price]

Got it

[Billy Price]

thanks

[Billy Price]

Wow I made something that works, it finds any proofs of well-formedness of complex terms in the context, and uses cases to break it down and bring the simpler well-formedness proofs into the context, which will be caught by my WF_prover tactic.

meta def is_complex_WF : expr → bool
| `(TT.WF _ _ TT.term.star) := ff
| `(TT.WF _ _ TT.term.top) := ff
| `(TT.WF _ _ TT.term.bot) := ff
| `(TT.WF _ _ _) := tt
| _ := ff

meta def tactic.interactive.reduce_WFs : tactic unit :=
do
  local_context >>= list.mmap' (λ h, do H ← infer_type h, if (is_complex_WF H) then (do cases h, skip) else skip)

Here's a very simple use case,

example {Γ p q} : WF Γ Ω (p ⋀ q) → WF Γ Ω (p ⋁ q) :=
begin
  intro wfpq,
  reduce_WFs,
  WF_prover,
end

edit: forgot my WF_prover in the example proofs, which will essentially just apply WF.or and then grab the two well-formedness proofs we just extracted

[Billy Price]

My ambition is to have this work recursively and only pull out the WF proofs which are on variables, like getting just WF Γ Ω p and WF Γ Ω q from WF Γ Ω (⊤ ⋁ p ⋁ q). Does this already exist as a tactic?

[Rob Lewis]

There are a few ways you could do that. One way: your tactic could fail if it doesn't destruct anything. Then you can call repeat {reduce_WFs}, which will keep looking for things to destruct until nothing is left. A more efficient way: the cases tactic returns a list of the things it creates. So reduce_WFs could collect all of the new hypotheses that it creates using cases, and recurse on these. You'll want something with list.mfoldl instead of mmap'.

[Billy Price]

Can I prevent the cases tactic from adding the results to the context? And can I make it so that apply_rules WF_rules has access to the local context and also that list of well-formedness things I extracted?

[Rob Lewis]

I may be missing some context here... But no, I don't think you can stop cases from adding things to the context. Maybe you could clear things you don't want after. I'm not sure where apply_rule first into the picture.

[Damien Thomine]

Thank you very much for the explanation!

[Billy Price]

WF_rules contains things like WF.or {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q), so apply_rules WF_rules keeps hitting the target and resulting targets with appropriate rules (or assumption) until it can't make any more progress. In
the process of explaining that - I've found what apply_rules is under the hood, and I think I can pick this apart to do what I want. Thanks for introducing me to metaprogramming! I can read this stuff now.

[Billy Price]

Does meta constant mean it was implemented in C++?

meta constant cases_core (h : expr) (ns : list name := []) (md := semireducible) : tactic (list (name × list expr × list (name × expr)))

[Mario Carneiro]

yes

[Mario Carneiro]

well, it's not a necessity but a pretty strong correlation. Pretty much all meta constants in lean core have built in implementations in C++

[Mario Carneiro]

https://github.com/leanprover-community/lean/blob/master/src/library/tactic/cases_tactic.cpp#L648-L678

[Billy Price]

Is is possible to do what cases does without spilling the results into the local context? Just collect them into a list?

[Mario Carneiro]

collect what?

[Mario Carneiro]

the metavariables that cases produces exist in an extended context

[Billy Price]

In my mind, if I have h : WF Γ Ω (p ⋁ q), cases is a magic machine that gives me h_1 : WF Γ Ω q and h_2 : WF Γ Ω p. That's all I want out of it.

[Mario Carneiro]

What do you get instead?

[Billy Price]

I want the machine to deliver that as a list expr (I think) in my meta code so that I can feed it to meta def apply_rules (hs : list pexpr) (n : nat) : tactic unit (the one in tactic.core), and not dump all the results into the interactive context.

[Billy Price]

To directly answer your question it does work as I described - I just want it to not put the results into the context, just use them to prove stuff and then throw them away.

[Mario Carneiro]

perhaps you should prove theorems like WF Γ Ω (p ⋁ q) -> WF Γ Ω p and use them as necessary

[Billy Price]

Oh of course! Thanks :)

[Mario Carneiro]

you can also scope subproofs so that the cases is only used to prove an intermediate statement

[Mario Carneiro]

i.e. have : WF Γ Ω p, { cases h, assumption }

[Billy Price]

I can't do this because h is an expr, what am I supposed to do? I ambivalent to the use of cases, can I just retrieve the result of applying this function?

lemma WF.and_elim  : WF Γ Ω' (p ⋀ q) → WF Γ Ω' p ∧ WF Γ Ω' q := by {intro h, cases h, tidy}

meta def decompose_WF : expr → expr → list expr
| _ `(TT.WF _ _ TT.term.star) := []
| _ `(TT.WF _ _ TT.term.top) := []
| _ `(TT.WF _ _ TT.term.bot) := []
| h `(TT.WF _ _ (TT.term.and _ _)) := cases (TT.WF.and_elim h)
-- other cases omitted

[Billy Price]

Here's an improved version, thought now I get errors (pasted below) why can't it figure out those implicit arguments?

meta def decompose_WF : expr → expr → tactic (list (name × list expr))
| _ `(TT.WF _ _ TT.term.star) := return []
| _ `(TT.WF _ _ TT.term.top) := return []
| _ `(TT.WF _ _ TT.term.bot) := return []
| h `(TT.WF _ _ (TT.term.and _ _)) := cases (expr.app `(TT.WF.and_elim) h)
| h `(TT.WF _ _ (TT.term.or _ _)) := cases (expr.app `(TT.WF.or_elim) h)
| h `(TT.WF _ _ (TT.term.imp _ _)) := cases (expr.app `(TT.WF.imp_elim) h)
| h `(TT.WF _ _ (TT.term.pair _ _)) := cases (expr.app `(TT.WF.pair_elim) h)
| h `(TT.WF _ _ (TT.term.comp _ _)) := cases (expr.app `(TT.WF.comp_elim) h)
| h `(TT.WF _ _ (TT.term.all _ _)) := cases (expr.app `(TT.WF.all_elim) h)
| h `(TT.WF _ _ (TT.term.ex _ _)) := cases (expr.app `(TT.WF.ex_elim) h)
| _ _ := return []

TT.WF.and_elim : ∀ {Γ : list TT.type} {p q : TT.term} {Ω' : TT.type}, TT.WF Γ Ω' (p ⋀ q) → TT.WF Γ Ω' p ∧ TT.WF Γ Ω' q
don't know how to synthesize placeholder
context:
decompose_WF : expr → expr → tactic (list (name × list expr)),
h : expr,
_x : list level,
_x _x : expr,
_x : list level,
_x _x : expr
⊢ list TT.typeLean

don't know how to synthesize placeholder
context:
decompose_WF : expr → expr → tactic (list (name × list expr)),
h : expr,
_x : list level,
_x _x : expr,
_x : list level,
_x _x : expr
⊢ TT.typeLean

don't know how to synthesize placeholder
context:
decompose_WF : expr → expr → tactic (list (name × list expr)),
h : expr,
_x : list level,
_x _x : expr,
_x : list level,
_x _x : expr
⊢ TT.termLean

don't know how to synthesize placeholder
context:
decompose_WF : expr → expr → tactic (list (name × list expr)),
h : expr,
_x : list level,
_x _x : expr,
_x : list level,
_x _x : expr
⊢ TT.termLean

[Rob Lewis]

Remember that using expr.app directly doesn't do any kind of unification or type inference at all. When you write `(TT.WF.and_elim) Lean has no idea what the implicit arguments should be, and using expr.app to apply it to h won't help.

[Rob Lewis]

You probably want something like e ← mk_app `TT.WF.and_elim [h], cases e

[Rob Lewis]

For anyone who followed my metaprogramming tutorial and is looking for more practice: I posted a topic in the metaprogramming stream here with a proposal that came up yesterday. With what you learned from the videos and a bit of ingenuity, this project is totally in scope.

[Billy Price]

Cool thanks :). While debugging, I noticed my tactic wouldn't update its behaviour in other files that import it, after I make a change. Once I restart the lean server, it updates. Is this expected behaviour, something wrong with my setup or a bug in Lean?

[Rob Lewis]

This isn't expected and I haven't seen it before. Are you using any custom flags for the Lean process?

[Billy Price]

I don't know what that is

[Rob Lewis]

Then probably not.

[Rob Lewis]

What if you change the type of a declaration that's used in an imported file, does it notice that?

[Billy Price]

It doesn't notice that, in fact it doesn't even recognise anything newly declared in the imported file until I restart the lean server

[Rob Lewis]

Is this in VSCode?

[Billy Price]

yes

[Billy Price]

I tried to recreate the error with two fresh files, and the error doesn't occur.

[Billy Price]

Is it because I use sorry in some places in the file?

[Rob Lewis]

I don't think so. I don't remember seeing this behavior before.

[Rob Lewis]

I need to go in a second. Maybe if you post a #mwe someone can try to reproduce.

[Billy Price]

I've figured out the issue, part of it is a vs-code bug, but it could possibly be fixed on the lean side?

Steps to reproduce

1. leanproject new bugtest
2. create src/file1.Lean and src/file2.lean within vs code (pay attention to capitalisation)
3. in file2.lean put import file1
4. Rename file1.Lean to file1.lean (remove the capitalisation), either in vs-code's browser or elsewhere
5. Observe vs-code does not detect this change in the opened tab-name (this can be fixed by reopening the tab, but regardless the following issues still occur)
6. Put def foo : ℕ := 3 in file1.lean in vs-code
7. do #check foo in file2.lean and observe it doesn't recognise it.
8. Restart the lean server and observe it now recognises it
9. Make any change to file1.lean (like change the type of foo or just delete foo) and observe it doesn't update in file2.lean until the lean server or vs code is restarted (after which the problem still persists).

There seems to be nothing you can do to fix this broken import relationship. I got it working again by changing the file name of file1.lean beyond capitalisation, say to file0.lean, in my normal non-vs-code file browser, after which vs-code recognises file1.lean has been deleted from the disk, and then the import relationship is fixed again, once the import is changed to import file0

This issue also occurs when capitalising or uncapitalising other parts of the filename, say File1.lean vs file1.lean, which is arguably more likely to occur.

Can anyone else reproduce this, and is this something I should register as an issue on the vscode github or the vscode-lean
github?

[Billy Price]

I think this might be the lean extension, since I've just noticed at the top of the Lean Infoview, it never updates the filename from file1.Lean, even after restarting the lean server and restarting vs-code. Once the file name is changed beyond just uncapitalisation, it recognises the change and fixes the link.

[Patrick Massot]

The VSCode Lean extension has changed a lot in the last few weeks (with great results!), so having a new bug in this area is rather plausible.

[Billy Price]

Is the lean extension responsible for the lean server? Because it's not just the info-view that fails to update the import.

[Patrick Massot]

No, the Lean extension is not responsible for the Lean server. However there were also changes on the Lean side to accommodate the new fancy widgets.

[Billy Price]

Where should I submit this as an issue? It’s not clear to me where the source of the problem is

[Patrick Massot]

If you can't reproduce the issue without VSCode I would put it in the vscode-lean repo. In any case you expect Gabriel to handle it, and he is currently unavailable.

[Patrick Massot]

I also think this conversation has drifted and should not be in that stream. @Mario Carneiro could you move this to the general stream (since the first message of Billy mentioning this bug)?

[Notification Bot]

This topic was moved by Scott Morrison to #general > VS code updating bug?