new monoid struture on nat

Stream: maths

[Filippo A. E. Nuccio]

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]

@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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Filippo A. E. Nuccio]

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]

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]

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]

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

[Kevin Buzzard]

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]

data.equiv.basic is a good read

[Kevin Buzzard]

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

[Filippo A. E. Nuccio]

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

[Mario Carneiro]

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]

irreducible-after-the-fact is verboten

[Mario Carneiro]

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

[Kevin Buzzard]

Oh, interesting

[Mario Carneiro]

i.e.

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

[Kevin Buzzard]

This would be much harder work in practice

[Kevin Buzzard]

We want a copy of nat with a new +

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Filippo A. E. Nuccio]

Oh sure

[Mario Carneiro]

but you have the usual unfolding hazard

[Filippo A. E. Nuccio]

Having a new type seemed good for this, no?

[Filippo A. E. Nuccio]

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]

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]

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

[Mario Carneiro]

also I don't know what ## is

[Filippo A. E. Nuccio]

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

[Johan Commelin]

@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]

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

[Kevin Buzzard]

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

[Filippo A. E. Nuccio]

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

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

#eval (37 : N) -- 382954

[Filippo A. E. Nuccio]

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]

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

[Filippo A. E. Nuccio]

Not quite, indeed.. :wink:

[Kevin Buzzard]

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]

I guess more generally each num becomes a program

[Kevin Buzzard]

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

[Ryan Lahfa]

Kevin Buzzard said:

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

Curry-Howard intensifies

[Kyle Miller]

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