Zulip Chat Archive

Stream: general

Topic: rcases names


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 06 2018 at 20:34):

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

view this post on Zulip Simon Hudon (Aug 06 2018 at 20:38):

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 21:19):

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

view this post on Zulip 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

view this post on Zulip 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, _, _, _⟩

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Aug 06 2018 at 21:32):

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 21:33):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Aug 06 2018 at 23:14):

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 23:18):

what do you mean include each other?

view this post on Zulip 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`

view this post on Zulip Mario Carneiro (Aug 06 2018 at 23:21):

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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 23:21):

or adjust the depth

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 08 2018 at 11:02):

did you push that?

view this post on Zulip Simon Hudon (Aug 08 2018 at 21:07):

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

view this post on Zulip Patrick Massot (Aug 08 2018 at 21:10):

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

view this post on Zulip Simon Hudon (Aug 08 2018 at 21:37):

That's where you guys are hiding!


Last updated: May 14 2021 at 04:22 UTC