std4#160 case tactic, by type instead of by tag

Stream: std4

[Kyle Miller]

std4#160 is a tactic where case : t => tac means "focus on the goal that unifies with t" vs case t => tac for "focus on the goal with tag t." There are case-like variations, such as case : t1 | t2 => tac for (case : t1 => tac); (case : t2 => tac) or case : t with n₁ ... nₘ => tac for renaming inaccessible variables. The tactic is meant to be a replacement for the Lean 3 show tactic, but more amenable for structured proofs.

It's been in the PR queue for a couple months, so I figured I'd bring it up here for feedback/attention.

[Mario Carneiro]

Last time I looked at it I recall it had some syntax that was inconsistent with case and/or some more general extensions... case : t with n => tac should probably be case _ n : t => tac, and case : t1 | t2 => tac seems like it should be more like case : t1 | : t2 => tac if the body is supposed to be a matcher

[Mario Carneiro]

It's also a bit misleading/inconsistent to use | here when case : t | t => tac selects two goals but match x with | t | t => tac has an unreachable pattern

[James Gallicchio]

Perhaps it could select all goals that match t rather than a single goal that matches t?

[Kyle Miller]

@James Gallicchio I figured that if you want to run some tactic on all the matches, you could compose it with the repeat tactic, where if you wanted to go the other way and only select a single match there's not much you can do.

[Kyle Miller]

@Mario Carneiro I've pushed changes to std4#160 to make it be an extension to case syntax. It's now case _ : t => tac and case _ : t1 | _ : t2 => tac, where the _'s can be tag names like in case. Rather than with, now it's case _ n₁ ... nₘ : t => tac.

The | is coming from case itself, and it's operating in a similar way to that. I agree that it could be misleading that the way it allows case _ : t | _ : t => tac diverges from how match is processed, but I'm not really sure if there are any alternatives other than detecting it and disallowing it (I don't want to be so authoritarian here). On the other hand the type ascriptions are just a further refinement to tag-based matching, so maybe it's OK?

[Kyle Miller]

For simplicity (and to be sure the syntax isn't ambiguous between core case and this case), I made it so that if you're using |, then all cases need a type ascription.

[Kyle Miller]

Fun fact about case tag matching: case tag looks for a goal whose name is tag exactly, or otherwise if that fails a goal with tag as a suffix, or otherwise if that fails a goal with tag as a prefix.

[Mario Carneiro]

Kyle Miller said:

For simplicity (and to be sure the syntax isn't ambiguous between core case and this case), I made it so that if you're using |, then all cases need a type ascription.

You could avoid ambiguity by setting the priority of the syntax lower than the core case

[Mario Carneiro]

I think it also makes sense to have case' with the same syntax

[Mario Carneiro]

(which does the same thing as case but doesn't require that the goal is closed at the end)

[Kyle Miller]

Mario Carneiro said:

You could avoid ambiguity by setting the priority of the syntax lower than the core case

Ok, you got it. I pushed a version that allows optional type ascriptions.

[Kyle Miller]

Mario Carneiro said:

I think it also makes sense to have case' with the same syntax

Now this is in there too.

[Kyle Miller]

Is there anything else that's blocking std#160? Edit: it's been merged, thanks!