## Stream: general

### Topic: rcases names

#### Patrick Massot (Aug 06 2018 at 11:08):

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 (Aug 06 2018 at 17:54):

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

#### Patrick Massot (Aug 06 2018 at 20:34):

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

#### Simon Hudon (Aug 06 2018 at 20:38):

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

#### Mario Carneiro (Aug 06 2018 at 21:19):

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

#### Simon Hudon (Aug 06 2018 at 21:23):

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 (Aug 06 2018 at 21:26):

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 (Aug 06 2018 at 21:29):

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

#### Mario Carneiro (Aug 06 2018 at 21:29):

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 (Aug 06 2018 at 21:31):

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 (Aug 06 2018 at 21:31):

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 (Aug 06 2018 at 21:31):

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 (Aug 06 2018 at 21:32):

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 (Aug 06 2018 at 21:32):

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

#### Mario Carneiro (Aug 06 2018 at 21:33):

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

#### Simon Hudon (Aug 06 2018 at 21:35):

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 (Aug 06 2018 at 23:06):

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 (Aug 06 2018 at 23:09):

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

#### Mario Carneiro (Aug 06 2018 at 23:10):

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

#### Simon Hudon (Aug 06 2018 at 23:14):

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 (Aug 06 2018 at 23:14):

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

#### Mario Carneiro (Aug 06 2018 at 23:18):

what do you mean include each other?

#### Simon Hudon (Aug 06 2018 at 23:20):

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 (Aug 06 2018 at 23:21):

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

#### Mario Carneiro (Aug 08 2018 at 11:00):

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 (Aug 08 2018 at 11:02):

did you push that?

#### Simon Hudon (Aug 08 2018 at 21:07):

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