Zulip Chat Archive

Stream: new members

Topic: tactics to simplify this?


view this post on Zulip Chris M (Jul 05 2020 at 05:36):

Are there good tactics to simplify this? in particular, the three line proof of the two cases is literally the same. Can I somehow just say "do this twice"? Also, can I combine the three apply into one command?

import order.lattice
import tactic

variables {α : Type*} [lattice α]
variables x y z : α
-- BEGIN
example : x  y = y  x :=
begin
    apply le_antisymm,
    {
        apply le_inf,
        apply inf_le_right,
        apply inf_le_left,
    },
    {
        apply le_inf,
        apply inf_le_right,
        apply inf_le_left,
    }
end

view this post on Zulip Alex J. Best (Jul 05 2020 at 05:37):

There are a few, you can do all_goals { blah } to run the tactic blah on all goals, or use a semicolon instead of a comma after one tactic to run the subsequent tactic on all goals produced by the first.

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 05:39):

There's also tactic#repeat for your first question. For your second, you can combine the apply like this: apply le_inf inf_le_right inf_le_left, but at that point you may as well just write exact le_inf inf_le_right inf_le_left.

view this post on Zulip Alex J. Best (Jul 05 2020 at 05:39):

And apply is applying functions / implications backwards from the goal, so you can chain them like so

example : x  y = y  x :=
begin
    apply le_antisymm;
    { apply le_inf inf_le_right inf_le_left, },
end

view this post on Zulip Yury G. Kudryashov (Jul 05 2020 at 05:59):

Or just := le_antisymm (le_inf inf_le_right inf_le_left) (le_inf inf_le_right inf_le_left) without begin ... end

view this post on Zulip Yury G. Kudryashov (Jul 05 2020 at 06:00):

If you use lemma instead of example, then you'll be able to #print this lemma and see the actual expression generated by tactics.

view this post on Zulip Kevin Buzzard (Jul 05 2020 at 08:07):

There might also be a WLOG trick?


Last updated: May 06 2021 at 23:11 UTC