named subgoals with `obtain`

Stream: mathlib4

[Jireh Loreaux]

@Mario Carneiro Is there any way to get named subgoals from obtain or rcases? I assume not because I can't see any place this would be supported in the rcases pattern syntax.

[Mario Carneiro]

no

[Mario Carneiro]

the subgoals are named using the constructors

[Mario Carneiro]

it would be nice to filter out the single constructor case though so that you don't get those inl.intro.intro.intro.intro.intro.inr goal names

[Mario Carneiro]

I'm not sure there is a sensible way to put goal names in the syntax, you can get exponentially more subgoals than you have pattern syntax

[Jireh Loreaux]

In fact, I wanted it for the case where there is more than one constructor. Right now, we can only use · to focus the resulting subgoals (or use the ugly auto-generated names).

[Mario Carneiro]

I'm not sure how you would do better than the auto-generated names though

[Mario Carneiro]

none of the other cases tactics allow you to name the subgoals either

[Mario Carneiro]

they let you refer to a subgoal by the name that has been decided for it

[Mario Carneiro]

but you can do that just as well using case after rcases

[Jireh Loreaux]

Fair enough.

[Mario Carneiro]

why are the auto-generated names ugly in your case?

[Jireh Loreaux]

Just because of the nesting.

[Mario Carneiro]

but I mean isn't that exactly what you want here?

[Mario Carneiro]

maybe you should show more of your actual example

[Jireh Loreaux]

This is artificial, as I don't have an actual example at hand (this occurred to me weeks ago).

import Lean

example (p q r s : Prop) (h : p ∨ q ∨ r ∨ s) : True := by
  obtain (hp | hq | hr | hs) := h
  case inl => trivial -- hp
  case inr => trivial -- hs
  case inr.inl => trivial -- hq
  case inr.inr => trivial -- hr

I certainly didn't correctly predict which case corresponded to which hypothesis.

[Jireh Loreaux]

My idea for a syntax would be something like:

import Lean

example (p q r s : Prop) (h : p ∨ q ∨ r ∨ s) : True := by
  obtain (@?p(hp) | @?q(hq) | @?r(hr) | @?s(hs)) := h
  case p => trivial -- hp
  case q => trivial -- hq
  case r => trivial -- hr
  case s => trivial -- hs

[Aaron Liu]

Jireh Loreaux said:

import Lean

example (p q r s : Prop) (h : p ∨ q ∨ r ∨ s) : True := by
  obtain (hp | hq | hr | hs) := h
  case inl => trivial -- hp
  case inr => trivial -- hs
  case inr.inl => trivial -- hq
  case inr.inr => trivial -- hr

I certainly didn't correctly predict which case corresponded to which hypothesis.

You can make it work

example (p q r s : Prop) (h : p ∨ q ∨ r ∨ s) : True := by
  obtain hp | hq | hr | hs := h
  case inl => trivial -- hp
  case inr.inl => trivial -- hq
  case inr.inr.inl => trivial -- hr
  case inr.inr.inr => trivial -- hs

[Mario Carneiro]

the correct case naming for the first example is

example (p q r s : Prop) (h : p ∨ q ∨ r ∨ s) : True := by
  obtain (hp | hq | hr | hs) := h
  case inl => trivial -- hp
  case inr.inl => trivial -- hq
  case inr.inr.inl => trivial -- hr
  case inr.inr.inr => trivial -- hs

this is confounded by the fact that case lets you refer to a substring (postfix?) of the case instead of writing the whole thing

[Jireh Loreaux]

sure, good point, I didn't pick the case names correctly. Doing that makes more sense, but it still gives ugly names

[Jireh Loreaux]

nevertheless, it would be nice to be able to give these names.

[Mario Carneiro]

these are the same names you would get if you used match to pattern match it

[Jireh Loreaux]

I understand. It makes sense, I'm just wishing for more freedom.

[Jireh Loreaux]

Mario Carneiro said:

this is confounded by the fact that case lets you refer to a substring (postfix?) of the case instead of writing the whole thing

This is very weird. Certainly I wouldn't have confused myself above if this had just failed when I typed case inr =>

[Mario Carneiro]

it is very helpful when you have a bunch of random stuff at the beginning of the case name from the current goal prior to the case split

[Jireh Loreaux]

(also solved if you can name your own cases :wink:, but I understand this is simply not supported anywhere, so it's a nontrivial request.)

[Jireh Loreaux]

You can justifiably ignore me now.

[Mario Carneiro]

There isn't really precedent for what the syntax could be, but for a bikeshed example let's say that pat @ ?hcan be used as an rcases pattern, and the semantics are that it will replace the case name for that pattern unless you use it again in a nested pattern or do additional pattern matching after it (inside pat or in dependent patterns that come later)

[Mario Carneiro]

then you would be able to do

  obtain (hp @ ?hp | hq @ ?hq | hr @ ?hr | hs @ ?hs) := h
  case hp => trivial -- hp
  case hq => trivial -- hq
  case hr => trivial -- hr
  case hs => trivial -- hs

[Jireh Loreaux]

That would be nice.

[Jireh Loreaux]

Perhaps a more relevant example is something like this:

import Mathlib.Logic.IsEmpty

example {X : Sort*} : True := by
  obtain (h | h) := isEmpty_or_nonempty X
  case inl => trivial
  -- proceed with the rest of the proof without a focused goal
  -- maybe this part is long
  trivial

It would be much nicer if the case were named isEmpty instead of inl.

[Jireh Loreaux]

I'm sure that something like this is what made me want this feature in the first place.

[Jireh Loreaux]

Another good example would be when using docs#ENNReal.trichotomy

[Johan Commelin]

In things like match branches, you name the hypotheses when you select the branch. So, I'm thinking something like

  rcases h using (?p | ?q | ?r | ?s) with
  | p hp => trivial
  | q hq => trivial
  | r hr => trivial
  | s hs => trivial

But:

1. The current syntax is rcases h with pat instead of using pat with
2. I'm not sure how this would fit into obtain...

[Johan Commelin]

3. I'm not sure how to make this recursive.

[Mario Carneiro]

rcases and obtain are almost exactly the same, the argument order is just the other way around

[Mario Carneiro]

I don't think this makes a whole lot of sense, the ?p things are patterns here, they name values not goals

[Mario Carneiro]

what does rcases e with <?p, ?q> mean?

[Mario Carneiro]

I was thinking you could have ?h as a shorthand for h @ ?h but it would be both a variable name and a goal name in that case

[Johan Commelin]

I'm aware that my proposed syntax deviates from the established one. It's also not fleshed out at all.
I mostly wanted to see if we could somehow reuse something from match branches. Probably not

[Jireh Loreaux]

I think the var_name @ ?goal_name syntax makes sense, because then you are re-naming the constructor. You could even apply it only on certain constructors, as is:

obtain h @ ?isEmpty | h := isEmpty_or_nonempty X

[Jireh Loreaux]

I don't think the syntactic sugar ?h for h @ ?h is necessary, and I think it could lead some users to create weird variable / goal names. But :shrug:

[Jireh Loreaux]

Johan Commelin said:

I mostly wanted to see if we could somehow reuse something from match branches.

to be honest, I think we should intentionally keep the syntax separate since matching and rcases patterns just work differently. If we start merging the syntax, I think it's likely to lead to confusion.

[Eric Wieser]

Mario Carneiro said:

it is very helpful when you have a bunch of random stuff at the beginning of the case name from the current goal prior to the case split

Could we have case *.inl for this instead?

[Kyle Miller]

The full tag matching procedure I've found to be surprising:

• It looks for the first goal with an exact match.
• If that fails, it looks for the first goal with a matching suffix.
• If that fails, it looks for the first goal with a matching prefix.

It hasn't been clear to me if people use the last one.

[Bhavik Mehta]

Mario Carneiro said:

it would be nice to filter out the single constructor case though so that you don't get those inl.intro.intro.intro.intro.intro.inr goal names

Apologies for necroposting, just wanted to mention lean4#6550 for this exact thing

[Kyle Miller]

An idle thought I had about the display of case names: I wonder if it would be reasonable to show just the end of a case name if that's unique, and have a hover or other UI affordance to show the whole thing? At least in your example, doing case inl => ... works because of the way cases look for a matching suffix.

(This is independent of having obtain create shorter case names.)

[Kyle Miller]

There are a few motivations for this thought:

• #general > lean4.infoview.showGoalNames is false in the web editor @ 💬 is about how case names are disabled in https://live.lean-lang.org/, but they're necessary information if you're wanting to use case with a case name. Abbreviated case names might be a good compromise, and one we might want as the default everywhere.
• #lean4 > user-facing metavariable names shared between goals @ 💬 is about how metavariable user names aren't really namespaced. I think we should have some kind of namespacing system that prevents metavariables from accidentally being used across proof branches. That would go toward making case names longer though, opposite of the direction of lean4#6550.
• #lean4 > ?n metavariable unexpectedly filled @ 💬 is related to the previous point. The application elaborator uses the names of the arguments of the function being elaborated to create new metavariables(!). I don't think these names should be user-accessible, or at least they should be deeper in some hierarchy of namespaces so that you can't access them unless you really mean to.

[Bhavik Mehta]

On your point 2, it could make case names longer, but I don't think that's in opposition to my issue. Specifically, if there is a branch in the proof, then there are genuinely two cases, and so the longer case name would be reasonable. My issue is specifically about inserting bits in the case name when there's no new branch made!

[Kyle Miller]

The reason I'm saying that 2 is in opposition is that a natural solution is to extend the prefix whenever there is any sort of tactic scope being entered whatsoever, even when there isn't more than one branch.

Imagine if even refine created a fresh metavariable naming scope

[Bhavik Mehta]

Ah, I was imagining only extending the prefix if there is a branch...

[Kyle Miller]

The thought here is that the common case for refine is that you want fresh metavariables, so a way it could work is that it enters a new naming scope, and when ?a elaborates it gets this scope as a prefix. This could solve the accidental reuse problem that has shown up in convert_to and congrm as well.

This doesn't solve the problem where it's not possible to distinguish between wanting to reference a preexisting metavariable and creating a new one though. You possibly might want to refer to such a metavariable in a refine.