Zulip Chat Archive

Stream: new members

Topic: focusing goals


view this post on Zulip Jiekai (Mar 27 2020 at 02:56):

Just learned to use begin ... end { ... } to structure tactics. The first begin ... end block focuses on the first goal. Is it possible to work on the second goal first bypassing the the first goal?

view this post on Zulip Alastair Horn (Mar 27 2020 at 02:58):

You could use sorry to move to the next goal

view this post on Zulip Bryan Gin-ge Chen (Mar 27 2020 at 03:01):

You can also use show:

example :  × bool :=
begin
  split,
  show bool,
  { exact tt },
  exact 1
end

or if you are using mathlib, swap:

import tactic.basic

example :  × bool :=
begin
  split,
  swap,
  { exact tt },
  exact 1
end

view this post on Zulip Scott Morrison (Mar 27 2020 at 05:28):

There's also work_on_goal n { ... }.

view this post on Zulip Scott Morrison (Mar 27 2020 at 05:28):

(This requires that you finish the goal by the end of the { ... } block.)

view this post on Zulip Scott Morrison (Mar 27 2020 at 05:29):

As well as swap n which swaps the 1st and nth goals, there's rotate n which rotates (left) n times.

view this post on Zulip Johan Commelin (Mar 27 2020 at 05:55):

Scott Morrison said:

(This requires that you finish the goal by the end of the { ... } block.)

Oooh, I thought it didn't... :bulb:

view this post on Zulip Mario Carneiro (Mar 27 2020 at 06:08):

That actually sounds like a misfeature. If you are going to close the goal, you can just use swap n, { ... }

view this post on Zulip Scott Morrison (Mar 27 2020 at 13:14):

Sorry, my mistake, work_on_goal does what everyone thought: you're allowed to make partial progress.

view this post on Zulip Johan Commelin (Mar 27 2020 at 13:15):

Pretty prescient of its author (-;

view this post on Zulip Johan Commelin (Mar 27 2020 at 13:15):

That guy is a genius!


Last updated: May 14 2021 at 04:22 UTC