rcases

Stream: mathlib4

[Jakob von Raumer]

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]

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]

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

[Jakob von Raumer]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

Yes, all the bulk work should be done in MetaM

[Mario Carneiro]

Or maybe TermElabM for some tactics

[Mario Carneiro]

TacticM is mostly only for interactive / frontend tactics

[Mario Carneiro]

rcases is done in mathlib4#182 :tada:

[Yury G. Kudryashov]

How do I call rcases from another tactic?

[Scott Morrison]

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

[Scott Morrison]

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

[Yury G. Kudryashov]

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]

So, probably I need the second option.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Henrik Böving]

Targets I would guess?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

(used Expr.toSyntax and Syntax.missing)

[Scott Morrison]

(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]

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]

This already is the case.

[Yaël Dillies]

Nevermind, I'm thinking of Lean 3

[Jakob von Raumer]

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

[Yaël Dillies]

Wait, does this syntax work in Lean 4?

[Yaël Dillies]

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]

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

[Kevin Buzzard]

brightred.png

[Yaël Dillies]

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

[Kevin Buzzard]

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]

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