goal selectors

Stream: general

[Johan Commelin]

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]

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]

But it's still quite verbose

[Johan Commelin]

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

[Mario Carneiro]

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

[Rob Lewis]

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]

numeric indexes are rarely the most maintainable

[Johan Commelin]

ok, fair enough

[Marc Huisinga]

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]

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

[Marc Huisinga]

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]

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

[Simon Hudon]

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