Zulip Chat Archive

Stream: general

Topic: setext

Patrick Massot (Apr 16 2018 at 16:14):

Core lib has a funext tactic which allows to replace apply funext, intro x by funext x. Would it be a good idea to copy the definition of this tactic to get a setext tactic?

Kenny Lau (Apr 16 2018 at 16:14):

the funext tactic is really repeat {apply funext, intro x} though

Kenny Lau (Apr 16 2018 at 16:15):

but right, set.ext can only be used once

Kenny Lau (Apr 16 2018 at 16:15):

well you can just set setext to be apply set.ext; intro x

Patrick Massot (Apr 16 2018 at 16:16):

I want x to be an argument of the tactic

Kenny Lau (Apr 16 2018 at 16:16):

sure

Patrick Massot (Apr 16 2018 at 16:16):

It's mostly a cosmetic question, but also about consistency

Patrick Massot (Apr 16 2018 at 16:17):

Because I keep trying setext x before remembering it doesn't work yet

Mario Carneiro (Apr 16 2018 at 17:35):

@Simon Hudon I recall discussing a generic ext tactic as a complement to the monotonicity tactic, perhaps it would help here

Simon Hudon (Apr 16 2018 at 17:38):

Yes, I have it in lean-lib. I can create a pull request. I have a extensionality attribute that I used to tag extentionality on sets, stream and maybe other things too

Patrick Massot (Apr 16 2018 at 20:02):

nice

Simon Hudon (Apr 16 2018 at 20:53):

I just submitted a pull request: https://github.com/leanprover/mathlib/pull/104

Simon Hudon (Apr 16 2018 at 20:54):

In tests/examples.lean you should see a bunch of situations where ext is useful.

Simon Hudon (Apr 16 2018 at 20:54):

Let me know if you think there should be more extensionality lemmas

Patrick Massot (Apr 16 2018 at 20:55):

Thanks!

Patrick Massot (Apr 16 2018 at 20:55):

Can you give it names like with funext?

Patrick Massot (Apr 16 2018 at 20:56):

Oh, you put sorries in tests again :disappointed:

Simon Hudon (Apr 16 2018 at 20:57):

Yes. ext will apply all extensionality lemmas that make sense while ext a b c will only apply three (not necessarily the same) and name the introduced locals a,b, c,

Patrick Massot (Apr 16 2018 at 20:57):

What is this ext1 I see in tests? Apply it only once?

Patrick Massot (Apr 16 2018 at 20:57):

like congr_n 1?

Simon Hudon (Apr 16 2018 at 20:57):

It shouldn't affect the built because the final proof is just trivial

Patrick Massot (Apr 16 2018 at 20:57):

Ahah

Simon Hudon (Apr 16 2018 at 20:58):

I don't know of congr_n 1 but it sounds like you got the right idea

Simon Hudon (Apr 16 2018 at 20:59):

(I'm so glad congr_n exists! I'll be able to use that now!)

Patrick Massot (Apr 16 2018 at 21:00):

I was looking to my mathlib tactics docs to point to and, shame on me, I didn't include congr_n! :disappointed:

Simon Hudon (Apr 16 2018 at 21:00):

shake head in disapproval

Simon Hudon (Apr 16 2018 at 21:03):

Would it be useful to have a monoid and add_monoid instance for fin n in mathlib?

Patrick Massot (Apr 16 2018 at 21:06):

What would be the law? Again some truncation thing?

Simon Hudon (Apr 16 2018 at 21:07):

Yes. It would be modulo arithmetic with the modulo baked into the type

Patrick Massot (Apr 16 2018 at 21:08):

Oh, modulo

Patrick Massot (Apr 16 2018 at 21:08):

That's a bit sneaky

Patrick Massot (Apr 16 2018 at 21:08):

https://github.com/leanprover/mathlib/pull/105

Simon Hudon (Apr 16 2018 at 21:09):

What kind of sneaky? Evil-sneaky or just effective-sneaky?

Patrick Massot (Apr 16 2018 at 21:10):

I don't know. People could be taken off guard. But who would want to add elements of fin n anyway?

Simon Hudon (Apr 16 2018 at 21:10):

After a quick survey, there's me

Simon Hudon (Apr 16 2018 at 21:13):

The other alternative I see is the p ≡ q [MOD k] notation but that looks more restricted. fin n is usable in other contexts that congruences or equalities.

Patrick Massot (Apr 16 2018 at 21:14):

I notice your ext PR doesn't include documentation :unamused:

Simon Hudon (Apr 16 2018 at 21:15):

What's this documentation thing?

Simon Hudon (Apr 16 2018 at 21:15):

Alright, I'll add a comment :)

Simon Hudon (Apr 16 2018 at 21:15):

Is that better?

Patrick Massot (Apr 16 2018 at 21:16):

By the way, you told me we found a bug in wlog when I asked questions about it. Did you manage to fix it?

Simon Hudon (Apr 16 2018 at 21:17):

That's true! I forgot about it. It was pretty tricky. I'll get back to it.

Simon Hudon (Apr 16 2018 at 21:17):

Sorry for the delay

Patrick Massot (Apr 16 2018 at 21:17):

Adding a docstring to tactic/interactive.lean would be good enough. Then I can copy it to tactic.md

Patrick Massot (Apr 16 2018 at 21:17):

But in this case I could also write the docstring I guess

Patrick Massot (Apr 16 2018 at 21:18):

The problem is I could write nonsense

Patrick Massot (Apr 16 2018 at 21:19):

There is no delay problem with wlog, I was only asking so you don't forget

Simon Hudon (Apr 16 2018 at 21:19):

Thanks for reminding me

Patrick Massot (Apr 16 2018 at 21:20):

Speaking of documentation, I wonder if @Sebastian Ullrich of @Gabriel Ebner could answer Kevin's questions in https://github.com/leanprover/mathlib/blob/master/docs/extras/calc.md (you only need to search for "Kevin" in this file)