rcases names

Stream: general

[Patrick Massot]

I guess rcases doesn't (recursively) invent names because using autogenerated names is evil. But could we get a tactic which uses trace to indicate what is the structure of angle brackets that would need to be used, possibly with suggested names? Sometimes I spend quite a long time to figure out what to put after rcases ... with

[Simon Hudon]

Let's say you have h : a ∧ (b ∨ c), what would you like rcases h with to print?

[Patrick Massot]

I didn't think about disjunctions. I'm always using rcases with exists and conjunctions.

[Simon Hudon]

Can you show me an example where you'd like rcases to give you more information?

[Mario Carneiro]

In that case it would probably print rcases h with ⟨h_1, h_2 | h_2⟩

[Simon Hudon]

It would be cool if that kind of information could be fed to the IDE to generate snippets, now that I think of it. Maybe that can be done

[Mario Carneiro]

this certainly seems doable. I don't think it will be smart enough to not name variables that are eliminated after the match (i.e. h : ∃ a b, a = b should become ⟨a, _, rfl⟩ rather than ⟨a, b, rfl⟩) but otherwise it should be possible. It may do weird things with dependent functions, like this:

def f : ℕ ⊕ ℕ → Prop
| (sum.inl a) := 0 < a ∧ a < 1
| (sum.inr a) := ∃ b, a < b ∧ b < a

example (h : ∃ n, f n) : false :=
by rcases h with ⟨a|a, _, _, _⟩

[Reid Barton]

In the same spirit, how about filling in a _ whose type is a structure with a { ... } snippet with field names already entered

[Mario Carneiro]

There is one example of "hints" being used in mathlib thus far, and I just use the error message in that case

example : ∃ n, 1 = n :=
by simpa using ⟨1, rfl⟩

-- simpa failed, 'using' expression type not directly inferrable. Try:
--
-- simpa ... using
-- show Exists
--   (eq 1),
-- from Exists.intro 1 rfl
-- state:
-- ⊢ Exists (eq 1)

[Mario Carneiro]

all support for editor interaction was focused on the "holes" API, and that seems to have died. We probably won't see anything new here until lean 4

[Simon Hudon]

I had to stare at it for a while. It can be pretty aggressive indeed. I wonder if we could direct the IDE to do increasingly deep matching.

[Reid Barton]

I guess you could write a tactic which uses trace to produce some output which the user is supposed to copy and paste in, yeah. Kind of clunky but better than nothing

[Simon Hudon]

For now, we can already start supporting snippet: clauses in error messages. I have some ideas how to pick up on them in emacs at least.

[Simon Hudon]

@Reid Barton I agree. And then progressively, you can automate that "copy and paste"

[Mario Carneiro]

Interesting idea. Whatever API you have has to be compatible with core lean error messages though

[Simon Hudon]

I agree. The best would be to choose a keyword (e.g. snippet) that we know isn't used in core lean. That way, in the worse case, the plugin does nothing

[Mario Carneiro]

I started trying to implement this, but there is a problem with recursive definitions:

example (n : nat) : true :=
by rcases n with _|⟨_|⟨_|⟨_|⟨_|⟨_|_⟩⟩⟩⟩⟩; trivial

[Simon Hudon]

I did not see that coming. How about we use a default depth, maybe 3? Or just don't follow recursive references

[Mario Carneiro]

would the depth be cumulative over all splits or just for the one recursive? i.e. if there are two nats

[Simon Hudon]

I would make that depth the maximum distance between any one case split and the root of the type term. E.g. in ℕ × (ℕ ⊕ ℕ) match on the root product (1) then twice on the nat on the left, then match on the sum on the right (2), and then once on each nat.

[Simon Hudon]

It might get ugly fast though if you have structures with 10 fields include each other.

[Mario Carneiro]

what do you mean include each other?

[Simon Hudon]

like:

structure big_struct1 := -- ten fields

structure big_struct2 := -- ten fields of type `big_struct1`

structure big_struct3 := -- ten fields of type `big_struct2`

[Mario Carneiro]

meh, it's still finite. Users will have to use discretion

[Mario Carneiro]

or adjust the depth

[Mario Carneiro]

rcases_hint and rintro_hint are now in mathlib! It was a bit more complicated than I originally thought, since you have to do basically the same thing as rcases except backwards so there is lots of similar but different code from rcases.

[Patrick Massot]

did you push that?

[Simon Hudon]

Awesome! You really don't waste a minute, do you?

[Patrick Massot]

Simon, beware that recent discussion about that happened in the add_comm_group tactic thread (my bad)

[Simon Hudon]

That's where you guys are hiding!