decidable equality in ordered_semiring?

Stream: general

[Mario Carneiro]

Would anyone object to adding the assumption of decidable le/lt/eq in ordered_semiring? I think we've talked about this class and its strange counterexamples before, so perhaps it needs a more throrough refactoring than this, but the fact that it doesn't have a ≤ b → 0 ≤ c → c * a ≤ c * b as an axiom and instead derives this using asymmetry is frustrating my attempts to reduce AC in certain foundational areas (like nat.semiring).

[Mario Carneiro]

The earlier discussion on the pathologies of ordered_semiring is here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology/near/225129909

[Kevin Buzzard]

Didn't we once remove this assumption from field?

[Mario Carneiro]

Actually I was looking at that just now

[Mario Carneiro]

when did that happen?

[Mario Carneiro]

I thought we added decidable_eq to field

[Mario Carneiro]

(previously there were two classes, discrete_field and field)

[Kevin Buzzard]

Right, and everyone used to say to the mathematicians ", if you want a field, use discrete_field and don't ask any questions"

[Mario Carneiro]

right, which seems to suggest that it is better to have decidable_eq in all the basic classes rather than not

[Mario Carneiro]

it also occurs to me that we can use an auto_param to supply the classical proof by default, so that most structure instances won't even need to change

[Eric Wieser]

Does a classical proof in a decidable class field make the entire structure uncomputable though?

[Mario Carneiro]

yes

[Mario Carneiro]

For fields I think that's fine because you will almost certainly have an if x = 0 in the definition of inv anyway

[Mario Carneiro]

Really, I'm not sure there is much of a downside to making even really basic classes like group require decidability. If you are a programmer then probably everything in sight has decidable eq, and if you are a mathematician then it doesn't matter

[Kevin Buzzard]

If you're a mathematician then don't you just get completely confused by any mention of decidable?

[Mario Carneiro]

You shouldn't generally see it at all unless you are looking at the definition of the structure or are adding it as a field in the structure instance (and the latter can be solved by an auto param as mentioned)

[Mario Carneiro]

for the former issue, there isn't much we can do besides documentation and library notes

[Mario Carneiro]

it certainly wouldn't be the first time something is stated slightly oddly to support formalization

[Mario Carneiro]

An alternative proposal specific to ordered_semiring is to add a ≤ b → 0 ≤ c → c * a ≤ c * b and the commuted version as fields, with an autoparam to provide a proof from the lt theorem. I think it would be better in this case to just delete the lt theorem though, wikipedia doesn't think it should be an axiom of ordered rings

[Eric Wieser]

I'd lean towards just adding the missing field

[Mario Carneiro]

like this?

/-- An `ordered_semiring α` is a semiring `α` with a partial order such that
multiplication with a positive number and addition are monotone. -/
@[protect_proj]
class ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_comm_monoid α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_lt_mul_of_pos_left :  ∀ a b c : α, a < b → 0 < c → c * a < c * b)
(mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
(mul_le_mul_of_nonneg_left :  ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b . prove_mul_le_mul_of_nonneg_left)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c . prove_mul_le_mul_of_nonneg_right)

[Eric Wieser]

I'm not remotely qualified to comment on what the correct axioms are

[Eric Wieser]

But that looks plausible

[Mario Carneiro]

I think, to avoid the pathologies, we should remove the "cancellation" from this definition, as in

/-- An ordered additive commutative monoid
is an additive commutative monoid with a partial order,
in which addition is monotone. -/
@[protect_proj, ancestor add_comm_monoid partial_order]
class ordered_add_comm_monoid (α : Type u)
      extends add_comm_monoid α, partial_order α :=
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)

/-- An `ordered_semiring α` is a semiring `α` with a partial order such that
multiplication with a positive number and addition are monotone. -/
@[protect_proj]
class ordered_semiring (α : Type u) extends semiring α, ordered_add_comm_monoid α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_le_mul_of_nonneg_left :  ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c)

But this is really a different definition, so the refactoring would be bigger

[Jannis Limperg]

Mario Carneiro said:

Really, I'm not sure there is much of a downside to making even really basic classes like group require decidability. If you are a programmer then probably everything in sight has decidable eq, and if you are a mathematician then it doesn't matter

The one programming counterexample I can think of is function spaces, which people coming from Haskell would expect to be monoids.

[Yury G. Kudryashov]

@Mario Carneiro Whatever you decide to do, could you please add a comment saying something like "these extra fields are here to make some proofs about nat independent of the axiom of choice"?

[Yury G. Kudryashov]

And I think that we should have an attribute + linter for definitions/lemmas that must not depend on AC.

[Yury G. Kudryashov]

Otherwise people like me can accidentally golf the proof and make them classical.

[Mario Carneiro]

Yeah, that makes sense. In fact I'm pretty sure there was a regression at one point wrt AC free proofs in core

[Yury G. Kudryashov]

I'm sorry if my golfing caused this regression.

[Alistair Tucker]

Did anything happen about this? i.e. is there an attribute you can put on a lemma to indicate its proof independent of AC so that's not golfed away?

[Eric Wieser]

I don't think it was in this thread, but I think @Mario Carneiro wrote such an attribute, and I think it would be reasonable to have in mathlib

[Mario Carneiro]

I didn't implement this attribute, although I still think it is a good idea

[Mario Carneiro]

right now the nearest equivalent is the decidable namespace and associated linter

[Mario Carneiro]

Oh wait, actually I did write an attribute for this once

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/intuitionistic.20logic/near/224372999

[Mario Carneiro]

I used a variation on this code to double check that I didn't miss anything in the last round of AC cleanup in core

[Yury G. Kudryashov]

Could you please PR this attr?

[Eric Wieser]

Would @[avoids_axiom classical.choice] be a better spelling that @[intuit]?

[Mario Carneiro]

I think it would be better to have a positive statement, "this theorem depends only on these axioms", since otherwise something silly like sorry could sneak in

[Mario Carneiro]

but also there should be "presets" for commonly used axiom sets

[Mario Carneiro]

@[uses_axioms choice_free]?

[Mario Carneiro]

where choice_free = [quot.sound, propext]

[Damiano Testa]

I would also prefer a positive assertion, but, if an exception is made, no_AC is a common abbreviation that I have seen.

[Mario Carneiro]

I thought about using AC in the name but I don't think we use that abbreviation anywhere in mathlib

[Johan Commelin]

For non-mathlib projects, it might be nice to have sorry_free as well.

[Mario Carneiro]

it's usually called "classical" and/or "choice"

[Mario Carneiro]

there is a theorem called axiom_of_choice but it is rarely used

[Mario Carneiro]

plus, in lean avoiding choice is a lot more about LEM than it is about AC as set theorists know it

[Johan Commelin]

I wouldn't mind tagging several of the larger lemmas in lean-liquid with sorry_free to make sure they stay that way during the frequent refactors of the project.

[Johan Commelin]

They are usually in files that import other files that still contain sorry.

[Eric Wieser]

Does anyone ever care about avoiding quot.sound and propext?

[Mario Carneiro]

No axioms lean is interesting because you can compute with those proofs

[Mario Carneiro]

this might come up if you want to execute a function defined by well founded recursion using rfl

[Mario Carneiro]

Also if you are doing proof translation to coq or something you might want to avoid quot.sound