## Stream: general

### Topic: ordered monoids

#### Johan Commelin (Jul 06 2019 at 14:57):

Is every canonically ordered monoid automatically cancellative?

#### Johan Commelin (Jul 06 2019 at 14:57):

Probably not, because it isn't in mathlib.

#### Chris Hughes (Jul 06 2019 at 15:02):

with_top nat is a counterexample

Aha, thanks

No it isn't

Why not?

#### Mario Carneiro (Jul 06 2019 at 15:05):

fin n with saturating addition is a counterexample

Sorry it is.

#### Mario Carneiro (Jul 06 2019 at 15:08):

There isn't really anything in the definition that looks like a cancellation law. Notice that lt_of_add_lt_add_left is just the contrapositive of add_le_add_left for total orders

Ok, thanks

#### Mario Carneiro (Jul 06 2019 at 15:10):

The comment for ordered_comm_monoid is a lie

#### Mario Carneiro (Jul 06 2019 at 15:11):

I think it is trying to describe ordered_cancel_comm_monoid

#### Johan Commelin (Jul 06 2019 at 15:46):

Right... I guess that might have added to the confusion for me.

#### Johan Commelin (Jul 06 2019 at 15:46):

Does it make sense to have a canonically_ordered_cancel_monoid?

#### Johan Commelin (Jul 06 2019 at 15:54):

I guess this is not provable:

instance [canonically_ordered_monoid α] [decidable_eq α] : ordered_comm_monoid (σ →₀ α) :=


#### Johan Commelin (Jul 06 2019 at 15:54):

You need the cancellative thing

#### Kevin Buzzard (Jul 06 2019 at 18:42):

Talking of canonically ordered monoids,

class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, lattice.order_bot α :=
(le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)


it occurred to me yesterday that this le_iff_exists_add axiom implies that that 0 ≤ b for all b, which makes it surprising that Lean asks for the lattice.order_botstructure; it could be generated automatically, because one can prove that bot must be 0 from the other stuff.

#### Kevin Buzzard (Jul 06 2019 at 18:44):

I guess that I'm saying that instead of canonically_ordered_monoid extending lattice.order_bot it should not mention it at all, and then there should just be an instance making a lattice.order_bot from a canonically ordered monoid.

#### Mario Carneiro (Jul 06 2019 at 18:45):

That's true, but you still want the structure to have both a bot and a zero. What if the structure already has a bot and a zero? Granted it's pretty unlikely that they are not defeq, but this definition permits it

#### Mario Carneiro (Jul 06 2019 at 18:47):

In any case I don't think that would be a very good instance - it is a kind of cross cutting thing, it will cause typeclass inference to get more complicated

#### Mario Carneiro (Jul 06 2019 at 18:47):

Then again, it's already an instance with this definition :thinking:

#### Kevin Buzzard (Jul 06 2019 at 18:49):

So it seems to me that it should be like the lt in a preorder: canonically_ordered_monoid should not extend lattice.order_bot but it should ask for three fields, le_iff_exists_add and then bot but with the := thing so that the user can define it if they want but if they don't it defaults to zero, and then a tactic can autogenerate bot_le if the user wants it to.

#### Mario Carneiro (Jul 06 2019 at 18:53):

it is already doing basically that

#### Mario Carneiro (Jul 06 2019 at 18:53):

You can stick (bot := 0) at the end and I think it will work

#### Kevin Buzzard (Jul 06 2019 at 18:57):

it is already doing basically that

It's not, at least in the sense that if I write this:

instance : canonically_ordered_comm_semiring mynat :=
zero := 0,
le := (≤),
le_refl := le_refl,
le_trans := le_trans,
le_antisymm := le_antisymm,
--  bot := ⊥,
--  bot_le := bot_le,
mul := (*),
mul_assoc := mul_assoc,
one := 1,
one_mul := one_mul,
mul_one := mul_one,
left_distrib := left_distrib,
right_distrib := right_distrib,
zero_mul := zero_mul,
mul_zero := mul_zero,
mul_comm := mul_comm,
zero_ne_one := zero_ne_one,
mul_eq_zero_iff := mul_eq_zero_iff }


then, unsurprisingly, it says

invalid structure value { ... }, field 'bot' was not provided
invalid structure value { ... }, field 'bot_le' was not provided


#### Kevin Buzzard (Jul 06 2019 at 18:58):

I don't want my player to have to worry about bot. I might just make another constructor.

#### Mario Carneiro (Jul 06 2019 at 18:59):

I mean stick (bot := 0) in canonically_ordered_monoid

#### Mario Carneiro (Jul 06 2019 at 19:01):

I think having a custom constructor would solve a lot of problems, but lean magic only works on the builtin constructor which makes this unattractive

#### Kevin Buzzard (Jul 06 2019 at 19:02):

lean magic includes i_just_proved_all_teh_theorems or whatever it's called now (structure_helper I think)

#### Mario Carneiro (Jul 06 2019 at 19:03):

One way to recover the structure notation is to have an auxiliary class with the arguments. nonneg_comm_group was my attempt at this, but I think in practice it ends up just being one more class in the hierarchy

#### Kevin Buzzard (Jul 06 2019 at 19:11):

I mean stick (bot := 0) in canonically_ordered_monoid

In preorder we see

(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)


So the question is how to prove bot_le; I can't even right click on order_laws_tac to see what it's doing.

#### Mario Carneiro (Jul 06 2019 at 19:35):

If clicking doesn't work you can always put it somewhere else, i.e. #print order_laws_tac and then click on it there

#### Mario Carneiro (Jul 06 2019 at 19:35):

it's basically exact rfl

#### Johan Commelin (May 01 2020 at 09:29):

Ordered monoids are a big mess, I think. They are partly "locked" into core. Lots of lemmas are duplicated. In core we don't have the to_additive machinery. Sometimes assumptions are unnecessary. Etc...

It would be a big relief if this could be moved out of core and into mathlib. Is this at all an option? core probably needs that nat is an example of an ordered additive commutative monoid. But does that mean we need the general class in core?

-- in core
class ordered_cancel_add_comm_monoid (α : Type u)
(add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c)

-- #####################

-- in mathlib (on a local branch)
/-- An ordered (additive) commutative monoid is a commutative monoid
with a partial order such that addition is an order embedding, i.e.
a + b ≤ a + c ↔ b ≤ c. These monoids are automatically cancellative. -/
(add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)

/-- An ordered commutative monoid is a commutative monoid
with a partial order such that addition is an order embedding, i.e.
a * b ≤ a * c ↔ b ≤ c. These monoids are automatically cancellative. -/
class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
(mul_le_mul_left       : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c)


#### Johan Commelin (May 01 2020 at 13:13):

Without to_additive I fear that the multiplicative and additive versions will diverge, which doesn't seem like a good idea.
Moving to_additive into core would be one option. But I don't really like that idea, because it will become harder to change it...

#### Mario Carneiro (May 01 2020 at 13:14):

It actually was in core once

#### Johan Commelin (May 01 2020 at 13:14):

Therefore I would very much prefer moving these classes out of core and into mathlib...

#### Johan Commelin (May 01 2020 at 13:14):

Mario Carneiro said:

It actually was in core once

I guess it was moved out of it for a reason (-;

#### Mario Carneiro (May 01 2020 at 13:15):

at least, a kind of crappy version of it was, and I wrote the current version and PR'd it, and Leo said no, so there is now a massive workaround in algebra.group to fix all the attributes that should be in core

#### Johan Commelin (May 01 2020 at 13:16):

Why does core need int again? Shouldn't nat be enough?

#### Mario Carneiro (May 01 2020 at 13:16):

it has special VM support

I see.

#### Johan Commelin (May 01 2020 at 13:16):

And why does it need lemmas about nat and int?

#### Johan Commelin (May 01 2020 at 13:17):

Or would it be enough if it knew has_add nat?

etc..

#### Mario Carneiro (May 01 2020 at 13:17):

It doesn't, I think

#### Mario Carneiro (May 01 2020 at 13:17):

At least, I can't think of a reason off hand

#### Johan Commelin (May 01 2020 at 13:17):

So... could we move almost all of the algebraic hierarchy out of core?

#### Johan Commelin (May 01 2020 at 13:18):

Or does norm_num need them?

#### Mario Carneiro (May 01 2020 at 13:18):

we don't need ring int in core, but we do need ring and int in core

#### Johan Commelin (May 01 2020 at 13:18):

Why ring?

#### Mario Carneiro (May 01 2020 at 13:18):

because it is used by norm_num lemmas

#### Johan Commelin (May 01 2020 at 13:18):

How many lemmas does norm_num need?

#### Mario Carneiro (May 01 2020 at 13:19):

several, but they are all quite basic

#### Mario Carneiro (May 01 2020 at 13:19):

and purpose built

#### Mario Carneiro (May 01 2020 at 13:20):

https://github.com/leanprover-community/lean/blob/master/library/init/algebra/norm_num.lean

#### Johan Commelin (May 01 2020 at 13:22):

Hmm... so it wants to know about ordered_rings... that doesn't sound good.

#### Mario Carneiro (May 01 2020 at 13:22):

it wants to know an unbounded number of things about number theoretic functions, which is why norm_num in mathlib is so large

#### Mario Carneiro (May 01 2020 at 13:23):

it's easy to scale back and move things around there

#### Mario Carneiro (May 01 2020 at 13:23):

there is an open issue in my head to rewrite tactic.norm_num in lean

#### Johan Commelin (May 01 2020 at 13:23):

So... are there parts that could move to mathlib... or is norm_num locking it all up?

#### Mario Carneiro (May 01 2020 at 13:24):

there isn't really any reason to have it in C++ except possibly efficiency

#### Mario Carneiro (May 01 2020 at 13:25):

as far as I know that's about it for algebra in the C++, except for the mysterious @[algebra] attribute

#### Mario Carneiro (May 01 2020 at 13:25):

https://github.com/leanprover-community/lean/blob/master/library/init/algebra/classes.lean

#### Johan Commelin (May 01 2020 at 13:25):

Hmm... but we want norm_num to be efficient, right?

#### Mario Carneiro (May 01 2020 at 13:26):

It will be pretty efficient even in lean

#### Mario Carneiro (May 01 2020 at 13:26):

this is not the kind of program that benefits greatly from native implementation

#### Mario Carneiro (May 01 2020 at 13:27):

but we will have to do performance tests to see what the damage is

#### Johan Commelin (May 01 2020 at 13:27):

How much work do you estimate this to be?

#### Mario Carneiro (May 01 2020 at 13:28):

maybe 1/3 of mathlib's norm_num

#### Mario Carneiro (May 01 2020 at 13:29):

it's pretty straightforward what needs to be done

#### Johan Commelin (May 01 2020 at 13:29):

I meant: is this 1 day, 1 week, 1 month?

#### Mario Carneiro (May 01 2020 at 13:29):

1 day? If I actually do it on that day

#### Johan Commelin (May 01 2020 at 13:30):

What do we need to do to make this issue in your head bubble to the top of your priority queue?

#### Reid Barton (May 01 2020 at 13:31):

I think maybe waiting a week or so would help

#### Johan Commelin (May 01 2020 at 13:32):

Because of your current refactor? Or what?

#### Johan Commelin (May 01 2020 at 13:57):

@Mario Carneiro So... if I leave the definition of ordered_add_comm_monoid in core, do you think I can move almost all lemmas about it to mathlib?

#### Johan Commelin (May 01 2020 at 13:57):

The lemmas that norm_num needs are all in that file you linked to?

I believe so

#### Johan Commelin (May 01 2020 at 13:59):

Ok, maybe that is the easiest way forward. Then I don't have to pester you about norm_num :stuck_out_tongue_wink:

#### Mario Carneiro (May 01 2020 at 13:59):

there is an official list of definitions used by the C++

#### Mario Carneiro (May 01 2020 at 14:03):

https://github.com/leanprover-community/lean/blob/master/src/library/constants.txt

#### Johan Commelin (May 01 2020 at 14:05):

Oooh cool! That will be helpful!

#### Johan Commelin (May 01 2020 at 14:05):

Is it transitively closed?

I don't think so

It shouldn't be

#### Mario Carneiro (May 01 2020 at 14:07):

these are constants that are directly referenced somewhere in C++

#### Johan Commelin (May 01 2020 at 14:08):

Ok, would you mind writing 20 lines of lean code that will print the transitive closure?

#### Johan Commelin (May 01 2020 at 14:08):

It's probably almost the same as printing all the places a name is used... but not exactly

#### Johan Commelin (May 01 2020 at 14:10):

In the other thread you wrote

import all

open tactic
run_cmd do
env ← get_env,
let l := env.fold mk_name_set \$ λ d t,
d.value.fold t (λ e _ t, match e with
| expr.const n [] :=
if n = with_zero.ordered_add_comm_monoid then
name_set.insert t d.to_name
else t
| _ := t
end),
tactic.trace l


#### Johan Commelin (May 01 2020 at 14:10):

Let me see if I can adapt that code.

#### Gabriel Ebner (May 01 2020 at 14:22):

Mario Carneiro said:

there is an official list of definitions used by the C++

Note that this list is far from exhaustive. For example, most definitions that are overridden in the VM don't appear there. Or the definitions necessary for tactics.

#### Johan Commelin (May 01 2020 at 14:25):

So... is there an automated way to figure out which lemmas can be moved to mathlib?

#### Gabriel Ebner (May 01 2020 at 14:52):

I think the list in constants.txt is pretty accurate when it comes to lemmas. It's just very incomplete for definitions. However, first we need to excise norm_num.

#### Mario Carneiro (May 04 2020 at 07:34):

What do you think about adding a @[magic] attribute (naming TBD) that is required on all definitions or lemmas referenced in C++? It should be possible to check this from the C++ file that constants.txt generates, as well as in DECLARE_VM_BUILTIN and other macros that construct bindings

#### Gabriel Ebner (May 04 2020 at 07:45):

I'm not enthusiastic. This sounds like a lot of work. If it's just about moving stuff to mathlib, the easiest approach is delete-test-move-back. Tactics written in Lean also reference definitions and lemmas, should these be tagged with magic as well?

#### Mario Carneiro (May 04 2020 at 07:47):

no, this is just so that the lean code has a visible marker that its behavior is affected in some way by C++

#### Mario Carneiro (May 04 2020 at 07:48):

I really don't like that there is no evidence in the file that nat.add does something different than its definition and mynat.add is mysteriously much worse

#### Mario Carneiro (May 04 2020 at 07:51):

(the answer to the second question is no)

#### Mario Carneiro (May 04 2020 at 07:51):

maybe @[extern_cpp] is a better name

#### Jannis Limperg (May 04 2020 at 07:53):

Agda has something like that; they use the syntax {-# BUILTIN #-}. This allows the standard library to be a separate project from Agda itself (though with Lean's current release cadence, there'd be little benefit to that).

#### Mario Carneiro (May 04 2020 at 07:53):

I don't know of any language that doesn't have some sigil on builtins except lean

#### Gabriel Ebner (May 04 2020 at 07:53):

Lean 4 uses @[extern]:

/- Nat basic instances -/
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
| a, Nat.zero   => a
| a, Nat.succ b => Nat.succ (Nat.add a b)


I'd be oke with moving closer to Lean 4.

#### Mario Carneiro (May 04 2020 at 07:54):

although I am also interested in extending this beyond just VM builtins to things like lemmas with external linkage to C++

#### Mario Carneiro (May 04 2020 at 07:55):

perhaps that should be a separate attribute

#### Mario Carneiro (May 04 2020 at 07:56):

I don't know whether it is necessary or useful to put the C++ name of the extern function in the attribute. Unlike lean 4, you can't really use those names to call the function in lean 3

#### Mario Carneiro (May 04 2020 at 07:56):

so you would still need the DECLARE_VM_BUILTIN macro, and the best you could do is double check that the names declared in both places match

#### Gabriel Ebner (May 04 2020 at 07:57):

I think @[extern] without c++ function name would be fine.

#### Mario Carneiro (May 04 2020 at 08:01):

Jannis Limperg said:

Agda has something like that; they use the syntax {-# BUILTIN #-}`. This allows the standard library to be a separate project from Agda itself (though with Lean's current release cadence, there'd be little benefit to that).

Well, there seems to be good reason to move core theorems and definitions to mathlib. I think the main blocker to moving builtins out of core is that it would break the tests. How does Agda do tests?

#### Jannis Limperg (May 04 2020 at 08:31):

I don't know the codebase too well, but from what I recall, the Agda setup is this: Agda ships with a super minimal 'builtin library' containing only the builtins. The tests import these and define a few other things in a 'test standard library'. The real standard library that users work with also imports the builtins and builds on them. One could probably also ignore the builtin library completely, instead binding the builtins manually, but I don't know why one would.

With that said, Agda has way less builtins than Lean, so the ergonomics are probably different.

Last updated: May 08 2021 at 10:12 UTC