Stream: general

Topic: have rcases

Patrick Massot (Jun 18 2019 at 20:20):

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 (Jun 18 2019 at 20:27):

We usually call this let in term mode

Patrick Massot (Jun 18 2019 at 20:28):

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 (Jun 18 2019 at 20:29):

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

Patrick Massot (Jun 18 2019 at 20:35):

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

Patrick Massot (Jun 18 2019 at 20:36):

But I guess we can't reuse the name let

Sebastien Gouezel (Jun 18 2019 at 20:37):

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 (Jun 18 2019 at 20:37):

Otherwise we could have rintros and rcases replacing their weaker analoues

Patrick Massot (Jun 18 2019 at 20:37):

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

Patrick Massot (Jun 18 2019 at 20:39):

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

Mario Carneiro (Jun 18 2019 at 20:43):

These could replace have/let in principle

Mario Carneiro (Jun 18 2019 at 20:44):

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

Patrick Massot (Jun 18 2019 at 20:45):

These could replace have/let in principle

how?

Mario Carneiro (Jun 18 2019 at 20:46):

they extend the syntax

Mario Carneiro (Jun 18 2019 at 20:46):

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

Mario Carneiro (Jun 18 2019 at 20:47):

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

Mario Carneiro (Jun 18 2019 at 20:48):

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

Patrick Massot (Jun 18 2019 at 20:48):

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 (Jun 18 2019 at 20:54):

@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 (Jun 18 2019 at 20:59):

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 (Jun 18 2019 at 21:00):

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

Mario Carneiro (Jun 18 2019 at 21:01):

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

Sebastian Ullrich (Jun 18 2019 at 21:01):

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

Mario Carneiro (Jun 18 2019 at 21:02):

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 (Jun 18 2019 at 21:03):

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

Sebastian Ullrich (Jun 18 2019 at 21:05):

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 (Jun 18 2019 at 21:06):

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

Last updated: May 13 2021 at 21:12 UTC