Zulip Chat Archive

Stream: mathlib4

Topic: rcases


Jakob von Raumer (Dec 22 2021 at 08:38):

As I've kind of announced a while ago, I started trying to port @Mario Carneiro 's rcases tactic. This is what I have so far.

Jakob von Raumer (Dec 22 2021 at 08:40):

Am I right thinking that the whole thing with get_local_and_type isn't really needed as long as we carry along the FVarSubst to prevent losing track of variables?

Mario Carneiro (Dec 22 2021 at 08:44):

Yes. I haven't looked into the new APIs for this but it looks like that should work

Jakob von Raumer (Dec 22 2021 at 08:47):

There's substCore which just returns the updated FVarsSubst, and I think cases does the same

Mario Carneiro (Dec 22 2021 at 08:47):

Looking at the code for substCore though, it only ever seems to insert into the FVarsSubst, not read from it

Mario Carneiro (Dec 22 2021 at 08:48):

In the common case I guess there is a lot of overwriting in that map?

Mario Carneiro (Dec 22 2021 at 08:50):

well, try it and see I guess. I'm sure leo & co already put some thought into it, and rcases just delegates to those functions

Jakob von Raumer (Dec 22 2021 at 09:38):

Mario Carneiro said:

In the common case I guess there is a lot of overwriting in that map?

Yes, it's usually only read if we want to correlate an "old" fvarId to a "new" one after the substitution

Jakob von Raumer (Dec 22 2021 at 09:39):

Seems to me as if compared to Lean 3 it's now become easier to use all of these things in MetaM instead of TacticM, that's also quite a change

Mario Carneiro (Dec 22 2021 at 09:42):

Yes, all the bulk work should be done in MetaM

Mario Carneiro (Dec 22 2021 at 09:42):

Or maybe TermElabM for some tactics

Mario Carneiro (Dec 22 2021 at 09:43):

TacticM is mostly only for interactive / frontend tactics

Mario Carneiro (Feb 06 2022 at 10:46):

rcases is done in mathlib4#182 :tada:

Yury G. Kudryashov (Nov 26 2022 at 19:26):

How do I call rcases from another tactic?

Scott Morrison (Nov 26 2022 at 19:39):

Do you want to call the "frontend", by generating the syntax (in which case you might be looking for evalTactic)?

Scott Morrison (Nov 26 2022 at 19:40):

Otherwise Std.Tactic.RCases.rcases looks like a reasonable entrypoint.

Yury G. Kudryashov (Nov 26 2022 at 19:54):

The original line was

  rcases none (pexpr.of_expr temp_e) $ rcases_patt.tuple ([new_nm, eq_nm].map rcases_patt.one),

Yury G. Kudryashov (Nov 26 2022 at 19:54):

So, probably I need the second option.

Yury G. Kudryashov (Nov 26 2022 at 20:28):

What is the meaning of the arguments to Std.Tactic.RCases.rcases?

Yury G. Kudryashov (Nov 26 2022 at 20:29):

I can guess the meaning of pat (the rcases pattern) and g (main goal). What is tgts?

Henrik Böving (Nov 26 2022 at 20:32):

Targets I would guess?

Yury G. Kudryashov (Nov 26 2022 at 20:40):

I see that it expects Syntax here and there. How do I convert an Expr to a Syntax?

Yury G. Kudryashov (Nov 26 2022 at 20:40):

Do I need to add it as a local constant first?

Yury G. Kudryashov (Nov 26 2022 at 21:14):

(used Expr.toSyntax and Syntax.missing)

Scott Morrison (Nov 26 2022 at 22:05):

(Side comment: I find the frequent need to interface with functions that want Syntax astonishingly painful. Your simp question on the other thread is another typical example.)

Jakob von Raumer (Dec 22 2022 at 20:52):

Would people except me be interested in having an extension of the rcases syntax with a token to cause the obtained variable to be cleared immediately? I'm working with big structures of which I sometimes want to omit some variables but using _ still clutters my contexts.

Yaël Dillies (Dec 22 2022 at 20:53):

This already is the case.

Yaël Dillies (Dec 22 2022 at 20:54):

Nevermind, I'm thinking of Lean 3

Jakob von Raumer (Dec 22 2022 at 20:54):

Perfect :sweat_smile: Just completely skipped that line in the doc, couldn't remember the syntax

Yaël Dillies (Dec 22 2022 at 20:55):

Wait, does this syntax work in Lean 4?

Yaël Dillies (Dec 22 2022 at 20:56):

I really have to make #mathlib4 bright red or something on my side. I keep wanting to give Lean 3 answers to Lean 4 questions.

Jakob von Raumer (Dec 22 2022 at 21:00):

It's in the doc of Std.Tactic.RCases, so I guess it works :D

Kevin Buzzard (Dec 22 2022 at 21:06):

brightred.png

Yaël Dillies (Dec 22 2022 at 21:07):

I'm not sure I can make it blink, though!

Kevin Buzzard (Dec 22 2022 at 21:08):

In the app: cog in top right -> manage streams, click on stream and change colour. I was confused by this when I saw someone else using Zulip and all their colours were different. They might be assigned randomly for each user?

Yaël Dillies (Dec 22 2022 at 21:09):

Yeah, I know all that. I think they are random.


Last updated: Dec 20 2023 at 11:08 UTC