Zulip Chat Archive

Stream: general

Topic: goal selectors


view this post on Zulip Johan Commelin (Mar 23 2020 at 12:02):

In Coq they have really nice goal selectors. You can write things like

    2,5,8: cbn; by rewrite right_identity.
    3,4: symmetry; apply left_identity.

in your proof scripts. How hard would it be to get that for Lean tactic proofs?

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:11):

I remember @Scott Morrison had a work_on_goal 1 { tac } tactic that is used by tidy scripts; that could be adapted to select multiple goals

view this post on Zulip Johan Commelin (Mar 23 2020 at 12:11):

But it's still quite verbose

view this post on Zulip Johan Commelin (Mar 23 2020 at 12:11):

It would be nice if we could now hack Lean to support really short goal selectors

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:11):

I'm not sure I want to encourage this kind of proof style though

view this post on Zulip Rob Lewis (Mar 23 2020 at 12:12):

No, I think the cost of hacking Lean to support this is way higher than the value of the slightly shorter proofs it would allow.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:12):

numeric indexes are rarely the most maintainable

view this post on Zulip Johan Commelin (Mar 23 2020 at 12:13):

ok, fair enough

view this post on Zulip Marc Huisinga (Mar 23 2020 at 12:16):

what's the recommended way to deal with proofs with lots of cases where there's perhaps lots of duplication at the start of some cases, somewhere in the middle of some cases and at the end of some cases?
assume that lemmas might not make sense because due to their specialized nature they will only be used in this one proof, and that we can't change the predicates that we work on to cause less duplication.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:17):

I will often use ; try { tac } if tac works on say 4 of the 16 goals I just got

view this post on Zulip Marc Huisinga (Mar 23 2020 at 12:18):

in the past i've used multiple any_goalscommands to deal with this, but it's terrible for maintainability because it makes the proofs very difficult to follow

view this post on Zulip Sebastian Ullrich (Mar 23 2020 at 12:47):

case already accepts multiple goal tag names. Unfortunately goal tags aren't used widely in Lean 3.

view this post on Zulip Simon Hudon (Mar 23 2020 at 17:17):

@Sebastian Ullrich nice! I didn't even know that.


Last updated: May 11 2021 at 14:11 UTC