Zulip Chat Archive

Stream: general

Topic: goal selectors

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?

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

Johan Commelin (Mar 23 2020 at 12:11):

But it's still quite verbose

Johan Commelin (Mar 23 2020 at 12:11):

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

Mario Carneiro (Mar 23 2020 at 12:11):

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

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.

Mario Carneiro (Mar 23 2020 at 12:12):

numeric indexes are rarely the most maintainable

Johan Commelin (Mar 23 2020 at 12:13):

ok, fair enough

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.

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

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

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.

Simon Hudon (Mar 23 2020 at 17:17):

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

Last updated: Dec 20 2023 at 11:08 UTC