ordered monoids

Stream: general

[Johan Commelin]

Is every canonically ordered monoid automatically cancellative?

[Johan Commelin]

Probably not, because it isn't in mathlib.

[Chris Hughes]

with_top nat is a counterexample

[Johan Commelin]

Aha, thanks

[Chris Hughes]

No it isn't

[Johan Commelin]

Why not?

[Mario Carneiro]

fin n with saturating addition is a counterexample

[Chris Hughes]

Sorry it is.

[Mario Carneiro]

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

[Johan Commelin]

Ok, thanks

[Mario Carneiro]

The comment for ordered_comm_monoid is a lie

[Mario Carneiro]

I think it is trying to describe ordered_cancel_comm_monoid

[Johan Commelin]

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

[Johan Commelin]

Does it make sense to have a canonically_ordered_cancel_monoid?

[Johan Commelin]

I guess this is not provable:

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

[Johan Commelin]

You need the cancellative thing

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

it is already doing basically that

[Mario Carneiro]

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

[Kevin Buzzard]

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 :=
{ add := (+),
  add_assoc := add_assoc,
  zero := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  add_comm := add_comm,
  le := (≤),
  le_refl := le_refl,
  le_trans := le_trans,
  le_antisymm := le_antisymm,
  add_le_add_left := add_le_add_left,
  lt_of_add_lt_add_left := lt_of_add_lt_add_left,
--  bot := ⊥,
--  bot_le := bot_le,
  le_iff_exists_add := le_iff_exists_add,
  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]

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

[Mario Carneiro]

I mean stick (bot := 0) in canonically_ordered_monoid

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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]

it's basically exact rfl

[Johan Commelin]

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)
      extends add_comm_monoid α, add_left_cancel_semigroup α,
              add_right_cancel_semigroup α, partial_order α :=
(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. -/
class ordered_add_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
(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. -/
@[to_additive ordered_add_comm_monoid]
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]

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]

It actually was in core once

[Johan Commelin]

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

[Johan Commelin]

Mario Carneiro said:

It actually was in core once

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

it has special VM support

[Johan Commelin]

I see.

[Johan Commelin]

And why does it need lemmas about nat and int?

[Johan Commelin]

Or would it be enough if it knew has_add nat?

[Johan Commelin]

etc..

[Mario Carneiro]

It doesn't, I think

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

Or does norm_num need them?

[Mario Carneiro]

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

[Johan Commelin]

Why ring?

[Mario Carneiro]

because it is used by norm_num lemmas

[Johan Commelin]

How many lemmas does norm_num need?

[Mario Carneiro]

several, but they are all quite basic

[Mario Carneiro]

and purpose built

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

It will be pretty efficient even in lean

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

How much work do you estimate this to be?

[Mario Carneiro]

maybe 1/3 of mathlib's norm_num

[Mario Carneiro]

it's pretty straightforward what needs to be done

[Johan Commelin]

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

[Mario Carneiro]

1 day? If I actually do it on that day

[Johan Commelin]

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

[Reid Barton]

I think maybe waiting a week or so would help

[Johan Commelin]

Because of your current refactor? Or what?

[Johan Commelin]

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

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

[Mario Carneiro]

I believe so

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Oooh cool! That will be helpful!

[Johan Commelin]

Is it transitively closed?

[Mario Carneiro]

I don't think so

[Mario Carneiro]

It shouldn't be

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Let me see if I can adapt that code.

[Gabriel Ebner]

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]

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

[Gabriel Ebner]

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]

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]

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]

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]

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]

(the answer to the second question is no)

[Mario Carneiro]

maybe @[extern_cpp] is a better name

[Jannis Limperg]

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]

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

[Gabriel Ebner]

Lean 4 uses @[extern]:

/- Nat basic instances -/
@[extern "lean_nat_add"]
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]

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

[Mario Carneiro]

perhaps that should be a separate attribute

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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.