Zulip Chat Archive

Stream: general

Topic: Writing tactics: creating goals


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alastair Horn (Mar 29 2020 at 01:23):

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

view this post on Zulip 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 :-)

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Mar 29 2020 at 11:57):

I'll look into it when I have time.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Mar 29 2020 at 14:42):

Oh, nice!

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Apr 03 2020 at 12:42):

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

view this post on Zulip 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?

view this post on Zulip Jasmin Blanchette (Apr 03 2020 at 13:40):

Yep.

view this post on Zulip Jasmin Blanchette (Apr 03 2020 at 13:40):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Alastair Horn (Apr 12 2020 at 12:29):

@Jasmin Blanchette it looks great! Thanks


Last updated: May 16 2021 at 22:14 UTC