Zulip Chat Archive

Stream: general

Topic: decidable equality in ordered_semiring?


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

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

view this post on Zulip Kevin Buzzard (Mar 28 2021 at 08:30):

Didn't we once remove this assumption from field?

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

Actually I was looking at that just now

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

when did that happen?

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

I thought we added decidable_eq to field

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

(previously there were two classes, discrete_field and field)

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

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

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

view this post on Zulip Eric Wieser (Mar 28 2021 at 08:37):

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

view this post on Zulip Mario Carneiro (Mar 28 2021 at 08:37):

yes

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 28 2021 at 08:42):

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

view this post on Zulip Mario Carneiro (Mar 28 2021 at 08:42):

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

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

view this post on Zulip Eric Wieser (Mar 28 2021 at 08:49):

I'd lean towards just adding the missing field

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

view this post on Zulip Eric Wieser (Mar 28 2021 at 08:53):

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

view this post on Zulip Eric Wieser (Mar 28 2021 at 08:54):

But that looks plausible

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

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

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

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

view this post on Zulip Yury G. Kudryashov (Mar 28 2021 at 14:25):

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

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

view this post on Zulip Yury G. Kudryashov (Mar 28 2021 at 14:33):

I'm sorry if my golfing caused this regression.

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

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:27):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:27):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:28):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:29):

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

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

view this post on Zulip Yury G. Kudryashov (Apr 09 2021 at 09:32):

Could you please PR this attr?

view this post on Zulip Eric Wieser (Apr 09 2021 at 09:32):

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

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:35):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:36):

@[uses_axioms choice_free]?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:36):

where choice_free = [quot.sound, propext]

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

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

view this post on Zulip Johan Commelin (Apr 09 2021 at 09:37):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:38):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:38):

there is a theorem called axiom_of_choice but it is rarely used

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

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

view this post on Zulip Johan Commelin (Apr 09 2021 at 09:40):

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 09:44):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:49):

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

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

view this post on Zulip 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: May 11 2021 at 12:15 UTC