focusing goals

Stream: new members

[Jiekai]

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?

[Alastair Horn]

You could use sorry to move to the next goal

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

Scott Morrison said:

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

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Johan Commelin]

Pretty prescient of its author (-;

[Johan Commelin]

That guy is a genius!