## 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

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

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

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

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

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 :)

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)

#### Simon Hudon (Apr 16 2018 at 21:20):

I'll write both no worries. I was joking.

#### Kevin Buzzard (Apr 16 2018 at 21:22):

I'm not at a computer right now, but IIRC I think fin n already has an + but it is not very well behaved!

#### Simon Hudon (Apr 16 2018 at 21:23):

Actually, I think - is more problematic. And we don't have laws for them

#### Kevin Buzzard (Apr 16 2018 at 21:24):

My memory is that these structures on fin n are defined in core and didn't make it into a sensible mathematical object

#### Kevin Buzzard (Apr 16 2018 at 21:24):

I think 2+2 wasn't 2-2 in fin 4 for example

#### Kevin Buzzard (Apr 16 2018 at 21:25):

Docs -- yes I'd forgotten I'd left those in!

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

#reduce (2 : fin 4) - (2 : fin 4) -- ⟨0, _⟩

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

#reduce (2 : fin 4) + (2 : fin 4) -- ⟨0, _⟩

Try 1+2 and 1-2

#### Kevin Buzzard (Apr 16 2018 at 21:26):

Maybe that was it

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

1+2 is 3 and 1 - 2 is 0

#### Kevin Buzzard (Apr 16 2018 at 21:27):

2+2=0 so adding 2 and subtracting 2 should be the same

Thanks

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

hard to tell what is the rule here

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

it seems substration is truncated at zero

#### Kevin Buzzard (Apr 16 2018 at 21:27):

Subtracting is just subtraction on nat I think

Right

#### Kevin Buzzard (Apr 16 2018 at 21:28):

Does that make it a monoid?

:simple_smile:

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

I think I remember reading this discussion in the past

Right

#### Simon Hudon (Apr 16 2018 at 21:29):

What was the conclusion?

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

Current definitions are... odd

#### Kenny Lau (Apr 20 2018 at 05:29):

https://github.com/leanprover/mathlib/pull/109/commits

#### Kenny Lau (Apr 20 2018 at 05:29):

ext is in PR

Last updated: May 18 2021 at 17:44 UTC