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?