Zulip Chat Archive

Stream: new members

Topic: focusing goals


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?

Alastair Horn (Mar 27 2020 at 02:58):

You could use sorry to move to the next goal

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

Scott Morrison (Mar 27 2020 at 05:28):

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

Scott Morrison (Mar 27 2020 at 05:28):

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

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.

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:

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, { ... }

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.

Johan Commelin (Mar 27 2020 at 13:15):

Pretty prescient of its author (-;

Johan Commelin (Mar 27 2020 at 13:15):

That guy is a genius!


Last updated: Dec 20 2023 at 11:08 UTC