Zulip Chat Archive

Stream: general

Topic: Tactic writing tutorial


view this post on Zulip Patrick Massot (Dec 03 2018 at 08:41):

More and more people are writing tactics, and providing bits of explanations here, but I never remember. So I decided to use my last hope option: I tried to teach it. The result is at https://github.com/leanprover-community/mathlib/blob/tactic_tutorial/docs/extras/tactic_writing.md Not only I hope this will help me remember this stuff, but also I hope it will allow experts to clear my misconceptions. And of course it would be a nice extra if it could teach someone something useful, so I'd be interested to know if any tactic writing newbie can read it (I know Johan already read it, because he carefully monitors our community repository).

view this post on Zulip Patrick Massot (Dec 03 2018 at 08:42):

Of course I also hope more stuff will be added here, by me or others. Don't hesitate to contribute, it's in the community repository.

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:02):

This is a really nice writeup. A comment: the "pseudo-python" syntax

t = infer_type(H)
return H if unify(e, t) else find_matching_type(e, HS)

was a bit confusing for me due to the infix conditional. Is this really how they do it in python? How about something a bit more C-like:

t = infer_type(H)
if unify(e, t):
  return H
else:
  find_matching_type(e, HS)

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:04):

although it occurs to me that what lean is doing with unify is more like a try catch than a conditional:

t = infer_type(H)
try:
  unify(e, t)
  return H
catch:
  find_matching_type(e, HS)

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:05):

What I wrote is indeed valid python

view this post on Zulip Johan Commelin (Dec 03 2018 at 09:05):

Yes, I thought so as well. So why did you call it pseudo-python?

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:05):

But I agree the try/except (not catch) version is closer to what is happening in Lean. But I didn't want to include too much python...

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:06):

You guys need to learn more python

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:06):

(NB: I don't know python, I'm inventing pythonic syntax on the fly. code highlighting says the word isn't catch)

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:06):

ah

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:06):

Maybe I should switch to a more generic imperative pseudo-code

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:06):

the funny thing is I've written several complete programs in python, but some of the syntax differences are meh

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:16):

@Jeremy Avigad you should take a look at this

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:18):

Parsing a token is introduced by lean.parser.tk followed by a string which must be taken from a predetermined list (the initial value of this list seems to be hardwired into Lean source code, in frontends/lean/token_table.cpp).

This list is added to when you use literals in notation, infix, or precedence.

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:20):

Importantly, marking something as a token causes it to no longer be a valid name, just like have

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:21):

which is why so many interactive tactics use the same few tokens : using generalizing with for separators

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:23):

Thanks Mario, this is one of the places where I hoped there would be clarifications

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:26):

Jeremy, I hope you don't mind I'm invading PIL's territory, but this tutorial is written from a different perspective, more hands-on and shallow. And of course you can contribute too!

view this post on Zulip Patrick Massot (Dec 03 2018 at 09:27):

Note to myself: I should replace paths to the core library or Lean source code with actual http links

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:40):

For the monad cheat sheet:

  • return: produce a value in the monad (type: A -> m A)
  • ma >>= f: get the value of type A from ma : m A and pass it to f : A -> m B. Alternate syntax: do a <- ma, f a
  • f <$> ma: apply the function f : A -> B to the value in ma : m A to get a m B. Same as do a <- ma, return (f a)
  • ma >> mb: same as do a <- ma, mb; here the return value of ma is ignored and then mb is called. Alternate syntax: do ma, mb
  • mf <*> ma: same as do f <- mf, f <$> ma, or do f <- mf, a <- ma, return (f a).
  • ma <* mb: same as do a <- ma, mb, return a
  • ma *> mb: same as do ma, mb, or ma >> mb. Why two notations for the same thing? Historical reasons
  • pure: same as return. Again, historical reasons

view this post on Zulip Mario Carneiro (Dec 03 2018 at 09:46):

  • failure: failed value (specific monads usually have a more useful form of this, like fail and failed for tactics)
  • ma <|> ma' recover from failure: runs ma and if it fails then runs ma'.
  • a $> mb: same as const a <$> mb or do mb, return a
  • ma <$ b: same as const b <$> ma or do ma, return b

view this post on Zulip Scott Morrison (Dec 03 2018 at 10:00):

oof <* and <$ are so confusing... "return the value on the ???"

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:29):

Does anyone know how to print the list of currently registered tokens?

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:30):

#print notation

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:31):

hm, generalizing isn't on that list

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:32):

with and using are not there either

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:41):

Reading the code, I don't see any other way of listing all tokens, although you can test if a name is a token easily enough

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:41):

i.e. #print wit and #print with give different errors

view this post on Zulip Kenny Lau (Dec 03 2018 at 20:41):

so... it is a Δ1 set

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:53):

  • a $> mb: same as const a <$> mb or do mb, return a
  • ma <$ b: same as const b <$> ma or do ma, return b

Are these const descriptions really correct? It looks like const is missing its type argument

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:55):

it's implicit

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:55):

const a := λ_, a

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:56):

Actually most of these are actually defined using const, many more than I used, but it's not a very transparent way to write it

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:57):

map_const α β := map ∘ const β

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:57):

crystal clear

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:58):

map_const is <$ btw

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:59):

oops, it's not implicit

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:59):

Here I see function.const : Π {α : Sort u_1} (β : Sort u_2), α → β → α

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:59):

And I don't see how it would make sense to have it implicit

view this post on Zulip Patrick Massot (Dec 03 2018 at 20:59):

how would you infer it?

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:59):

you would normally write that with B implicit

view this post on Zulip Mario Carneiro (Dec 03 2018 at 20:59):

because it's inferrable from the last argument

view this post on Zulip Patrick Massot (Dec 03 2018 at 21:00):

when you apply the constant function yes, but not when talking about the function

view this post on Zulip Mario Carneiro (Dec 03 2018 at 21:00):

but const is often used partially applied, and in that case having it implicit can be problematic

view this post on Zulip Patrick Massot (Dec 03 2018 at 21:00):

we're almost synchronous

view this post on Zulip Patrick Massot (Dec 03 2018 at 22:16):

So, should I open a PR, or are there more suggestions, contributions, or questions?

view this post on Zulip Rob Lewis (Dec 03 2018 at 22:38):

This looks really nice, Patrick, thanks! I see a few small mistakes/typos. I can make adjustments myself or comment on a PR, either way is no problem. But it's bedtime now, so tomorrow.

view this post on Zulip Jeremy Avigad (Dec 04 2018 at 00:53):

@Patrick Massot Indeed, this is very nice. Do you want to consider becoming one of the authors of Programming in Lean? For personal reasons, I'd like to maintain tight control over TPiL (because it has been a labor of love for a number of years), but we never got very far with PiL, and I'd be happy to have collaborators for that. (We added Jared Roesch to the list of authors early on, because he intended to work on it, but in the end he never did, so his name should be removed.) In Amsterdam, I can show you how to set up and maintain the Sphinx repository (but maybe you are already comfortable doing that). A caveat: the repository is set up for a Linux installation of Sphinx, and I don't know if it is possible to get it running on Windows. (I know that Rob Lewis has had trouble getting our Logic and Proof running on Windows.)

view this post on Zulip Patrick Massot (Dec 04 2018 at 09:17):

@Jeremy Avigad Thanks for the kind words and your trust. I think there is room for both an informal tutorial and PIL. But I'd love to help with any documentation project. I've already compiled TPIL, so I guess I could handle compiling PIL as well. I'm tempted to write we can discuss all this in Amsterdam, but unfortunately I'll be extremely busy after the Amsterdam workshop, so maybe we should start now, especially if you have something specific in mind (not that I really have time, but it will be much worse after Christmas).

view this post on Zulip Patrick Massot (Dec 04 2018 at 09:18):

@Rob Lewis please feel free to correct typos and mistakes directly. The community repository is dedicated to that. I think you can even do the correction from github, without pulling the branch. And pulling the branch won't be a problem either, there is nothing to compile, it's all markdown.

view this post on Zulip Patrick Massot (Dec 04 2018 at 09:19):

Actually maybe we should consider including a Lean file gathering all examples from the tutorial. I have it on my computer of course, but I wouldn't know where to put it in the repository


Last updated: May 09 2021 at 20:11 UTC