show with turnstile

Stream: Is there code for X?

[David A]

Is there any prior work on a show tactic with ⊢; i.e. one which could match (reordering goals) and unify hypotheses? This could make my proofs much more readable. Or is there another way to accomplish the same thing?

[Yaël Dillies]

What leads you to using show that much? Presentation style? because it's barely used in mathlib.

[David A]

The case I'm hitting now uses split_ifs over a fairly large if/else tree. I'd like to be able to annotate each proof branch with what hypotheses have been introduced, and potentially clean up those hypotheses. But I run into this in other cases too; I'd hardly call split_ifs common in my code.

[Eric Rodriguez]

I don't think it works for split_ifs, but the case tactic is nice for when these are generated from induction or such like

[Eric Rodriguez]

it's worth trying to see if it works but I doub tit

[David A]

Actually, a better reason is: after an rcases or rintro with multiple | to show which branch we're in. And usually what I'm doing is dispatching all but one of the cases with one-liners, but there's no reason the "interesting" case will be last. I need to reorder them but the only difference between the cases is what's been introduced.

[Yaël Dillies]

David A said:

there's no reason the "interesting" case will be last.

Surprisingly, there is. But it's quite an art to get your definitions to spit out the hardest case last.