Writing tactics: creating goals

Stream: general

[Alastair Horn]

Calling any lean programmers,

I am a maths undergraduate. After 'graduating' from the natural number game, I've investigated a little further and gone through most of Theorem Proving in Lean.
As I have some programming experience, I'd love to learn how to write tactics. I've been trying to teach myself how to do so but it has been difficult as my only real documentation of sorts has been https://leanprover-community.github.io/mathlib_docs/tactic_writing.html.

I've set myself a couple of mini goals: to recreate left specifically for or propositions, and split specifically for and propositions.
Here is my code:

open tactic
open tactic.interactive
open interactive (parse)
open lean.parser

-- This tactic is like `left`, but only works on ∨
meta def myorleft : tactic unit :=
do
  `(%%l ∨ %%r) ← target,
  -- Not a clue what I'm doing, want to create a goal of type l and use it
  (set_goals [l]) >>= tactic.exact

-- And similarly for ∧
meta def myandsplit : tactic unit :=
do
  `(%%l ∧ %%r) ← target,
  -- Just guessing, want to create two goals and then use them
  (and.intro) >>= tactic.exact,
  set_goals (l :: [r])

variables {p q : Prop}

theorem useorleft (h : p) : p ∨ q :=
begin
  myorleft,
  from h,
end

theorem useandsplit (h : q ∧ p): p ∧ q :=
begin
  myandsplit, {
    from h.right,
  }, {
    from h.left,
  },
end

How can I open goals for the user to prove, then form the correct type and close the main goal?

[Mario Carneiro]

An easy way to do this is to use tactic.applyc ``or.inl instead of (set_goals [l]) >>= tactic.exact

[Kevin Buzzard]

These are great mini goals. The only other reference I know of, other than the tutorial, is programming in Lean, which is incomplete and out of date but taught me a lot about monads (I had worked through a lot of learnyouahaskell by that point).

[Bryan Gin-ge Chen]

Time for me to point out again that the Logical Verification in Lean course notes also have a lot of great material on metaprogramming. :smiley:

[Mario Carneiro]

If you want to be a bit more controlled about it and do the unification yourself, you can create a goal of type l using g <- mk_mvar l, then create the desired proof term, which is `(or.inl %%l %%r %%g), then use it for the main goal using tactic.exact `(or.inl %%l %%r %%g), and finally give the newly created metavariable back to the user using gs <- get_goals, set_goals (g :: gs). This is what applyc is doing

[Alastair Horn]

Thank you so much everyone! I will check out learnyouahaskell, as I'm not experienced with functional programming. And those notes look handy. That's precisely what I've been looking for Mario :)

[Mario Carneiro]

meta def myorleft : tactic unit :=
do
  `(%%l ∨ %%r) ← target,
  g ← mk_meta_var l,
  exact `(@or.inl %%l %%r %%g),
  gs ← get_goals,
  set_goals (g :: gs)

variables {p q : Prop}

theorem useorleft (h : p) : p ∨ q :=
begin
  myorleft,
  from h,
end

[Mario Carneiro]

meta def myorleft : tactic unit :=
applyc ``or.inl

variables {p q : Prop}

theorem useorleft (h : p) : p ∨ q :=
begin
  myorleft,
  from h,
end

[Mario Carneiro]

Note that if you forget to give the metavariable back to the user, you will end up in a funny state where there are no goals but the proof term still has a metavariable in it. This happens every once in a while and indicates a bug in the tactic

meta def myorleft : tactic unit :=
do
  `(%%l ∨ %%r) ← target,
  g ← mk_meta_var l,
  exact `(@or.inl %%l %%r %%g)

theorem useorleft {p q : Prop} (h : p) : p ∨ q :=
begin
  myorleft,
  -- goals accomplished?
end -- tactic failed, result contains meta-variables

[Alastair Horn]

Wonderful! And I've managed to do the and one now too

[Kevin Buzzard]

Bryan Gin-ge Chen said:

Time for me to point out again that the Logical Verification in Lean course notes also have a lot of great material on metaprogramming. :smiley:

I'm reading through them now so I won't forget again :-)

[Patrick Massot]

@Alastair Horn I know the tactic writing doc misses a section on manipulating the goal, it's been on my TODO list forever. Feel free to transform the conversation you had with Mario into a new section and open a pull request (ask here or google github opening a pull request if needed).

[Patrick Massot]

@Rob Lewis Do you know why https://leanprover-community.github.io/mathlib_docs/tactic_writing.html has no code block syntax highlighting?

[Rob Lewis]

I think the docs don't do syntax highlighting at all right now. There was a reason for this at the beginning, I don't remember what.

[Rob Lewis]

I'll look into it when I have time.

[Bryan Gin-ge Chen]

The Lean 3 changes were merged into pygments master, so I was going to try and add syntax highlighting to doc-gen after their next release.

[Rob Lewis]

Oh, nice!

[Jasmin Blanchette]

@Bryan Gin-ge Chen : We just released a new edition of the book, at

https://lean-forward.github.io/logical-verification/2020/index.html#material

It's now 50 pages of so longer than before and has color. The material on metaprogramming has been greatly expanded. I'd be grateful for any feedback.

[Bryan Gin-ge Chen]

Great! I'll take a look when I have a chance.

[Patrick Massot]

I'm a bit confused by all those Dutch courses. How many Lean courses are there at VU? Is it like one by Rob and one by Jasmin?

[Jasmin Blanchette]

Yep.

[Jasmin Blanchette]

You can see the list at https://lean-forward.github.io then click "events".

[Jasmin Blanchette]

Rob's is BSc level and focused on introduction/elimination rules for connectives, using proof terms / structured proofs.

[Jasmin Blanchette]

Mine is an MSc-level course and it's mostly backward/tactical proofs, with the focus on practical applications (but a bit of logical mastur***n at the beginning of course to learn the syntax -- Chapters 2 and 3 of the book).

[Alastair Horn]

@Jasmin Blanchette it looks great! Thanks