Zulip Chat Archive

Stream: maths

Topic: new monoid struture on nat


view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 08:06):

I am trying to use the (commutative) monoid structure on N\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 N\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 M\mathbb{M}, but then I can't use the already proven results which are true for a,b:Na, b : \mathbb{N}. What is the right way to do this?

view this post on Zulip 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.

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 08:15):

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

view this post on Zulip 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.

view this post on Zulip 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 N\mathbb{N} (with the old good 3+5=83+5=8) and the new M\mathbb{M} where 3+5=53+5=5 (or whatever symbol I use), I am scared about changing the priority.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 08:20):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 08:26):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:26):

data.equiv.basic is a good read

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:27):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 08:30):

irreducible-after-the-fact is verboten

view this post on Zulip Mario Carneiro (Feb 08 2021 at 08:31):

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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:32):

Oh, interesting

view this post on Zulip Mario Carneiro (Feb 08 2021 at 08:32):

i.e.

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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:32):

This would be much harder work in practice

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:33):

We want a copy of nat with a new +

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:33):

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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 08:34):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 08:34):

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

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 08:34):

Oh sure

view this post on Zulip Mario Carneiro (Feb 08 2021 at 08:34):

but you have the usual unfolding hazard

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 08:35):

Having a new type seemed good for this, no?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 08 2021 at 09:11):

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

view this post on Zulip Mario Carneiro (Feb 08 2021 at 09:12):

also I don't know what ## is

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 09:22):

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

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 09:35):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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,

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:17):

#eval (37 : N) -- 382954

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 11:52):

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

view this post on Zulip Filippo A. E. Nuccio (Feb 08 2021 at 13:03):

Not quite, indeed.. :wink:

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 13:08):

I guess more generally each num becomes a program

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 13:09):

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

view this post on Zulip 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

view this post on Zulip 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