## Stream: general

### Topic: Writing tactics: creating goals

#### Alastair Horn (Mar 29 2020 at 01:05):

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 (Mar 29 2020 at 01:12):

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

#### Kevin Buzzard (Mar 29 2020 at 01:13):

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 (Mar 29 2020 at 01:14):

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 (Mar 29 2020 at 01:16):

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 (Mar 29 2020 at 01:19):

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 (Mar 29 2020 at 01:19):

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 (Mar 29 2020 at 01:20):

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 (Mar 29 2020 at 01:23):

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 (Mar 29 2020 at 01:23):

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

#### Kevin Buzzard (Mar 29 2020 at 01:46):

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 (Mar 29 2020 at 11:05):

@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 (Mar 29 2020 at 11:06):

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

#### Rob Lewis (Mar 29 2020 at 11:57):

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 (Mar 29 2020 at 11:57):

I'll look into it when I have time.

#### Bryan Gin-ge Chen (Mar 29 2020 at 13:59):

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.

Oh, nice!

#### Jasmin Blanchette (Apr 03 2020 at 12:40):

@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 (Apr 03 2020 at 12:42):

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

#### Patrick Massot (Apr 03 2020 at 13:40):

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?

Yep.

#### Jasmin Blanchette (Apr 03 2020 at 13:40):

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

#### Jasmin Blanchette (Apr 03 2020 at 13:41):

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

#### Jasmin Blanchette (Apr 03 2020 at 13:43):

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 (Apr 12 2020 at 12:29):

@Jasmin Blanchette it looks great! Thanks

Last updated: May 16 2021 at 22:14 UTC