have rcases

Stream: general

[Patrick Massot]

For a very long time, I desired a tactic havec such that

havec ⟨...⟩ : ...,
{ ... }

(or havec ⟨...⟩ : ..., from ....) has the effect of

have : ...,
{ ... },
rcases this with ⟨...⟩

And I saw when translating the Hahn-Banach proof that SSReflect has it, and they use it all the time. I could try to hack something, but maybe @Mario Carneiro or @Simon Hudon could do that in two minutes. It would be nice to have it for the philosophy :boxing_glove: talk on Thursday.

[Mario Carneiro]

We usually call this let in term mode

[Patrick Massot]

I know it works in term mode, I used it during my jetlag insomnia last night. But I'd like to get it in tactic mode.

[Mario Carneiro]

I mean maybe havec isn't the most consistent choice of name

[Patrick Massot]

Oh I don't care at all about the name, I'd like to get the tactic!

[Patrick Massot]

But I guess we can't reuse the name let

[Sebastien Gouezel]

Johannes mentioned also once something we have in Isabelle:

have A (n:nat) : ...

which would be the same as

have A : \forall n, ...

without the need to assume n in the proof. Of course, if there is just one variable this is minor, but if there are several it is really handy.

[Patrick Massot]

Otherwise we could have rintros and rcases replacing their weaker analoues

[Patrick Massot]

I noticed SSReflect also has this, but it looks less crucial to me

[Patrick Massot]

(I know Mario seems to be in a good mood today, but let's not ask too much at the same time)

[Mario Carneiro]

These could replace have/let in principle

[Mario Carneiro]

have/let with args is also something that is available in term mode

[Patrick Massot]

These could replace have/let in principle

how?

[Mario Carneiro]

they extend the syntax

[Mario Carneiro]

so you can have have <foo> | <bar> := bla and have <foo> | <bar> : bla := bla as well

[Mario Carneiro]

although there is no real distinction with let when you are pattern matching

[Mario Carneiro]

if anything, let <foo> := bla in bla is misnamed

[Patrick Massot]

but I guess all this is defined in core, so why not doing a mathlib version that you would call as you wish?

[Mario Carneiro]

@Sebastian Ullrich How possible / efficient would it be to set up all the interactive core tactics as replacers? That is, they can be changed after the fact, mediated by an attribute or similar

[Sebastian Ullrich]

If by that you mean that they should do an indirection via an attribute when called, then that wouldn't help with changing their signature, which is encoded in the type, not the body, would it?

[Mario Carneiro]

That's true, but not entirely insurmountable in user code. You can have the tactic argument parser itself be a replacer

[Mario Carneiro]

Still, I'm thinking more along the lines of core lean support for a pattern like this

[Sebastian Ullrich]

Uhh... that doesn't sound like fun to implement

[Mario Carneiro]

I think you just have to tweak how reading cases in a tactic block translates to looking up the tactic tactic.interactive.cases

[Mario Carneiro]

if that lookup mechanism was configurable, we could change it to point at some other definition with a different signature

[Sebastian Ullrich]

Sure, that sounds much more reasonable than doing the replacement inside the core tactics. I had a PR once that implemented something like that, but it never landed for Lean 3.

[Mario Carneiro]

the replacer approach is only for today's lean which doesn't give us any other options