Zulip Chat Archive

Stream: general

Topic: have rcases


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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:27):

We usually call this let in term mode

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:29):

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

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

view this post on Zulip Patrick Massot (Jun 18 2019 at 20:36):

But I guess we can't reuse the name let

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

view this post on Zulip Patrick Massot (Jun 18 2019 at 20:37):

Otherwise we could have rintros and rcases replacing their weaker analoues

view this post on Zulip Patrick Massot (Jun 18 2019 at 20:37):

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

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:43):

These could replace have/let in principle

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:44):

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

view this post on Zulip Patrick Massot (Jun 18 2019 at 20:45):

These could replace have/let in principle

how?

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:46):

they extend the syntax

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:46):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:47):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 20:48):

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

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

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

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

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

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

view this post on Zulip Sebastian Ullrich (Jun 18 2019 at 21:01):

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

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

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

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

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