## Stream: maths

### Topic: new monoid struture on nat

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:06):

I am trying to use the (commutative) monoid structure on $\mathbb{N}$ given by  a + b = max a b, and I can easily prove that it is one by

instance : add_comm_monoid ℕ :=
zero := 0,


Yet I suspect this is the wrong way to do, as $\mathbb{N}$ already comes with a monoid structure and I can't end up with 3+5=5. I thought about introducing a new type, say $\mathbb{M}$, but then I can't use the already proven results which are true for $a, b : \mathbb{N}$. What is the right way to do this?

#### Johan Commelin (Feb 08 2021 at 08:14):

@Filippo A. E. Nuccio You can do

def new_thing := nat

def equiv_to_nat : new_thing \equiv nat := equiv.refl


and use the equiv to move back and forth. That's the most robust way.

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:15):

In the sense that I can apply, for instance, \equiv nat.zero_max?

#### Kevin Buzzard (Feb 08 2021 at 08:17):

I think it very much depends on what you want to do.

Here are some other ideas. If you want to use the + notation then you could make this instance of add_comm_monoid with a very high priority. If you don't want to use the monoid structure much and want to make new notation for it you could roll your own monoid structure. I think it all depends on what you want to use a lot and what you are prepared to do yourself.

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:19):

I certainly want to use the add_comm_monoid structure, with or without the + symbol. Since in the same file I would need to use both $\mathbb{N}$ (with the old good $3+5=8$) and the new $\mathbb{M}$ where $3+5=5$ (or whatever symbol I use), I am scared about changing the priority.

#### Kevin Buzzard (Feb 08 2021 at 08:20):

In particular I bet you can get 3+5=5 for nat by a high priority instance. But this might not be the best idea depending on what you want to do with this monoid structure. Johan's idea is the most principled idea but you will probably lose access to high-powered tactics like omega this way unless you manually keep pushing backwards and forwards

#### Kevin Buzzard (Feb 08 2021 at 08:20):

If you want to use the + symbol to mean two different things then Johan's approach is the best

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:20):

Oh, no, I won't need " high-powered" tactics for $\mathbb{N}$: only basic stuff, like max min and so on.

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:21):

Great! I'll go for Johan's approach. Is equiv "automatically" composing, so that I should write by equiv nat.zero_max, for instance?

#### Kevin Buzzard (Feb 08 2021 at 08:25):

Every definition comes with a cost, even new_thing. You will have to make all the structures on it that you want, and prove any theorems which aren't following from general monoid stuff. You can prove them by "abusing definitional equality" -- you have a goal with new_thing but you can change it to a nat goal using change and then prove it there. When you've finished abusing definitional equality and made your API you can mark your definition as irreducible and hopefully then you don't get any leaks. This way you should be able to use both +s with no trouble.

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:26):

Great, thanks! I'll try and keep my fingers crossed...

#### Kevin Buzzard (Feb 08 2021 at 08:26):

No, equiv isn't some magic thing, it's nothing more than the data of a bijection and its inverse, and a very big API

#### Kevin Buzzard (Feb 08 2021 at 08:27):

Post some code if you aren't sure how to use it

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:28):

For sure. I will first read data.equiv.basic to avoid useless questions, and then come back here for help! Thanks.

#### Mario Carneiro (Feb 08 2021 at 08:30):

When you've finished abusing definitional equality and made your API you can mark your definition as irreducible and hopefully then you don't get any leaks.

Actually, this is now considered bad practice, or more specifically it's a forward compatibility hazard for lean 4

#### Mario Carneiro (Feb 08 2021 at 08:30):

irreducible-after-the-fact is verboten

#### Mario Carneiro (Feb 08 2021 at 08:31):

Instead you should define a newtype structure that wraps the semireducible implementation definition

Oh, interesting

#### Mario Carneiro (Feb 08 2021 at 08:32):

i.e.

def real_impl := cauchy_seq
structure real := (out : real_impl)


#### Kevin Buzzard (Feb 08 2021 at 08:32):

This would be much harder work in practice

#### Kevin Buzzard (Feb 08 2021 at 08:33):

We want a copy of nat with a new +

#### Kevin Buzzard (Feb 08 2021 at 08:33):

But porting the gazillion theorems about nat will be harder work this way

#### Kevin Buzzard (Feb 08 2021 at 08:34):

Ie you can't just say "the new proof is just the old proof"

#### Mario Carneiro (Feb 08 2021 at 08:34):

I think it's still okay to have two defeq types with different instances...?

Oh sure

#### Mario Carneiro (Feb 08 2021 at 08:34):

but you have the usual unfolding hazard

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:35):

Having a new type seemed good for this, no?

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:56):

Well, I was able to advance using @Johan Commelin and @Kevin Buzzard 's advice: I now have

#eval equiv_to_nat.to_fun ((equiv_to_nat.inv_fun 8 ) + (equiv_to_nat.inv_fun 5)) ## 8
#eval equiv_to_nat.to_fun ((equiv_to_nat.inv_fun 3 ) + (equiv_to_nat.inv_fun 5)) ## 5


although I am not particularly proud of the name maxumal of my type (easy to improve) and the fact that I have no symbols neither for the type nor for the equivalence.

#### Filippo A. E. Nuccio (Feb 08 2021 at 08:58):

And I also have

#eval equiv_to_nat.to_fun ((equiv_to_nat.inv_fun 2) + (equiv_to_nat.inv_fun 0)) ##2
#eval equiv_to_nat.to_fun ((equiv_to_nat.inv_fun 5) + (equiv_to_nat.inv_fun 8)) ##8


showing that the monoid is commutative, it has a zero (and that I know other numbers other than 3,5,8). Still, I guess @Mario Carneiro is not happy with the solution, right?

#### Mario Carneiro (Feb 08 2021 at 09:11):

I don't see anything particularly wrong with that, although it looks pretty painful to use

#### Mario Carneiro (Feb 08 2021 at 09:12):

also I don't know what ## is

#### Filippo A. E. Nuccio (Feb 08 2021 at 09:14):

It is my way to try to render the result of the evaluation in Zulip... :sick: Hopefully improved a bit

#### Johan Commelin (Feb 08 2021 at 09:21):

@Filippo A. E. Nuccio Note that if e is an equive, then you can use e.symm to get the inverse equiv. The simp lemmas are written in terms of e.symm instead of e.inv_fun.

#### Filippo A. E. Nuccio (Feb 08 2021 at 09:22):

@Johan Commelin Thanks! This has already simplified a bit of things...

#### Kevin Buzzard (Feb 08 2021 at 09:35):

And an equiv has a coercion to function, so you don't need to_fun

#### Filippo A. E. Nuccio (Feb 08 2021 at 09:45):

I have also introduced a bit of notation, it now reads

#eval ℘ ((℘⁻¹ 8) + (℘⁻¹ 5)) -- 8


#### Kevin Buzzard (Feb 08 2021 at 10:09):

One disadvantage of calling this max operation + is that it stops you from using numerals on it. To get (37 : X) working, X needs to have 0, 1 and + (and then it uses binary, using n + n to double and then adding 1 as appropriate).

#### Kevin Buzzard (Feb 08 2021 at 10:15):

def N := ℕ

def zero : N := (37 : ℕ)
def one : N := (42 : ℕ)
def add (a b : N) : N := (3 * a + b - 2 : ℕ)

instance : has_zero N := ⟨zero⟩
instance : has_one N := ⟨one⟩

#check (37 : N) -- works


#### Filippo A. E. Nuccio (Feb 08 2021 at 10:16):

Yes, you are right. But since most of my things will be m and not 37, I can live with it,

#### Kevin Buzzard (Feb 08 2021 at 10:17):

#eval (37 : N) -- 382954


#### Filippo A. E. Nuccio (Feb 08 2021 at 11:19):

Kevin Buzzard said:

#eval (37 : N) -- 382954


Damn! You beated me:

def one : 𝕄 := (℘⁻¹ 42 : 𝕄)
instance : has_one 𝕄 := ⟨one⟩
instance: has_add 𝕄 := by apply_instance
#eval (37 : 𝕄) -- 42


:clap: :trophy:

#### Kevin Buzzard (Feb 08 2021 at 11:52):

I'm assuming that this is not your original application of this stuff? :-)

#### Filippo A. E. Nuccio (Feb 08 2021 at 13:03):

Not quite, indeed.. :wink:

#### Kevin Buzzard (Feb 08 2021 at 13:07):

There are some cool puzzles you can make here aren't there. You define your own 0,1,+ operations on some random type and then each numeral becomes a little program.

#### Kevin Buzzard (Feb 08 2021 at 13:08):

I guess more generally each num becomes a program

#### Kevin Buzzard (Feb 08 2021 at 13:09):

Wow it's almost as if maths has something to do with computer programming

#### Ryan Lahfa (Feb 08 2021 at 13:18):

Kevin Buzzard said:

Wow it's almost as if maths has something to do with computer programming

Curry-Howard intensifies

#### Kyle Miller (Feb 08 2021 at 18:56):

Kevin Buzzard said:

One disadvantage of calling this max operation + is that it stops you from using numerals on it. To get (37 : X) working, X needs to have 0, 1 and + (and then it uses binary, using n + n to double and then adding 1 as appropriate).

Something to look forward to in Lean 4 is the OfNat typeclass, which gives you direct access to the natural number, so you can avoid there needing to be a natural homomorphism from Nat in cases like this.

def TropicalNat := Nat

notation "Nat🌴" => TropicalNat