# Zulip Chat Archive

## Stream: general

### Topic: decidable equality in ordered_semiring?

#### Mario Carneiro (Mar 28 2021 at 06:51):

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 (Mar 28 2021 at 06:53):

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 (Mar 28 2021 at 08:30):

Didn't we once remove this assumption from `field`

?

#### Mario Carneiro (Mar 28 2021 at 08:31):

Actually I was looking at that just now

#### Mario Carneiro (Mar 28 2021 at 08:31):

when did that happen?

#### Mario Carneiro (Mar 28 2021 at 08:31):

I thought we added `decidable_eq`

to `field`

#### Mario Carneiro (Mar 28 2021 at 08:31):

(previously there were two classes, `discrete_field`

and `field`

)

#### Kevin Buzzard (Mar 28 2021 at 08:32):

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 (Mar 28 2021 at 08:33):

right, which seems to suggest that it is better to have `decidable_eq`

in all the basic classes rather than not

#### Mario Carneiro (Mar 28 2021 at 08:35):

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 (Mar 28 2021 at 08:37):

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

#### Mario Carneiro (Mar 28 2021 at 08:37):

yes

#### Mario Carneiro (Mar 28 2021 at 08:38):

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 (Mar 28 2021 at 08:39):

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 (Mar 28 2021 at 08:40):

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

#### Mario Carneiro (Mar 28 2021 at 08:41):

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 (Mar 28 2021 at 08:42):

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

#### Mario Carneiro (Mar 28 2021 at 08:42):

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

#### Mario Carneiro (Mar 28 2021 at 08:47):

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 (Mar 28 2021 at 08:49):

I'd lean towards just adding the missing field

#### Mario Carneiro (Mar 28 2021 at 08:50):

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 (Mar 28 2021 at 08:53):

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

#### Eric Wieser (Mar 28 2021 at 08:54):

But that looks plausible

#### Mario Carneiro (Mar 28 2021 at 08:55):

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 (Mar 28 2021 at 12:05):

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 (Mar 28 2021 at 14:24):

@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 (Mar 28 2021 at 14:25):

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

#### Yury G. Kudryashov (Mar 28 2021 at 14:25):

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

#### Mario Carneiro (Mar 28 2021 at 14:26):

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 (Mar 28 2021 at 14:33):

I'm sorry if my golfing caused this regression.

#### Alistair Tucker (Apr 09 2021 at 09:11):

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 (Apr 09 2021 at 09:26):

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 (Apr 09 2021 at 09:27):

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

#### Mario Carneiro (Apr 09 2021 at 09:27):

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

#### Mario Carneiro (Apr 09 2021 at 09:28):

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

#### Mario Carneiro (Apr 09 2021 at 09:29):

#### Mario Carneiro (Apr 09 2021 at 09:30):

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 (Apr 09 2021 at 09:32):

Could you please PR this attr?

#### Eric Wieser (Apr 09 2021 at 09:32):

Would `@[avoids_axiom classical.choice]`

be a better spelling that `@[intuit]`

?

#### Mario Carneiro (Apr 09 2021 at 09:34):

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 (Apr 09 2021 at 09:35):

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

#### Mario Carneiro (Apr 09 2021 at 09:36):

`@[uses_axioms choice_free]`

?

#### Mario Carneiro (Apr 09 2021 at 09:36):

where `choice_free = [quot.sound, propext]`

#### Damiano Testa (Apr 09 2021 at 09:37):

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 (Apr 09 2021 at 09:37):

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

#### Johan Commelin (Apr 09 2021 at 09:37):

For non-mathlib projects, it might be nice to have `sorry_free`

as well.

#### Mario Carneiro (Apr 09 2021 at 09:38):

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

#### Mario Carneiro (Apr 09 2021 at 09:38):

there is a theorem called `axiom_of_choice`

but it is rarely used

#### Mario Carneiro (Apr 09 2021 at 09:39):

plus, in lean avoiding `choice`

is a lot more about LEM than it is about AC as set theorists know it

#### Johan Commelin (Apr 09 2021 at 09:40):

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 (Apr 09 2021 at 09:40):

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

.

#### Eric Wieser (Apr 09 2021 at 09:44):

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

#### Mario Carneiro (Apr 09 2021 at 09:49):

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

#### Mario Carneiro (Apr 09 2021 at 09:49):

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

#### Mario Carneiro (Apr 09 2021 at 09:51):

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

Last updated: Dec 20 2023 at 11:08 UTC