# Zulip Chat Archive

## 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 ℕ :=
{ add := max,
add_assoc := max_assoc,
zero := 0,
zero_add := λ _, nat.zero_max,
add_zero := λ _, nat.max_zero,
add_comm := max_comm, }
```

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

data.equiv.basic is a good read

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

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

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...?

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

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⟩
instance : has_add N := ⟨add⟩
#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
instance : Add Nat🌴 where
add := Nat.max
instance : OfNat Nat🌴 n where
ofNat := (OfNat.ofNat n : Nat)
example (m : Nat🌴) : m + 37 = 37 + m :=
sorry
```

Last updated: May 18 2021 at 07:19 UTC