## Stream: new members

### Topic: decidable_rel in total_order

#### Jiang Jiedong (Jun 03 2023 at 10:45):

Hi everyone!
I was trying to prove some ≤ relation on some quotient type is a total order. I find that I need to fill a term: decidable_le : decidable_rel (≤). So what does this decidable property really means? And how should I provide a proof for it? I tried to read the definition of decidable_rel in init.core but got totally lost on how to prove something is decidable by myself :broken_heart: Thanks for any help!

#### Jiang Jiedong (Jun 03 2023 at 10:52):

By the way, what does it mean when some relation is undecidable? Is there any example?

#### Mario Carneiro (Jun 03 2023 at 11:02):

a relation that is not decidable is one where there is no algorithm that can give a Bool result and is always equivalent to the proposition

#### Mario Carneiro (Jun 03 2023 at 11:03):

Classically, there always exists such an algorithm, since one of return true or return false will work, but we often care specifically about ways to prove decidable results that are not noncomputable so that lean can actually eval the result

#### Eric Wieser (Jun 03 2023 at 11:05):

Usually the approach to proved decidability is to say "this expression is equivalent to some simpler expression, and we already know how to decide that one"

#### Eric Wieser (Jun 03 2023 at 11:05):

For quotient types, you would usually start with quotient.rec_on_subsingleton₂

#### Eric Wieser (Jun 03 2023 at 11:15):

src#localization.decidable_le might be a good example

#### Mauricio Collares (Jun 03 2023 at 11:25):

Less precisely, think of the total order on the set {True, False} in which True comes before False if and only if the Riemann hypothesis is true. This is a perfectly valid total order, but it is pretty hard to write a decidable instance (that is, a provably-correct algorithm which terminates and returns whether a < b for a, b elements of the set {True, False}) for this total order. Note that this does not mean that this is undecidable, though, just that no one currently knows how to write a decision procedure for it.

#### Jiang Jiedong (Jun 03 2023 at 19:53):

Thanks! Now I has moved out from quotient types, but still stuck at this point:
Let  Γ₀ be a linear_ordered_comm_monoid, I am trying to define a relation r.le on Γ₀ × ℕ+. (Think elements x = (x.fst, x.snd) : Γ₀ × ℕ+as a representation of x.fst^(1/x.snd).) So I define

 def r.le [linear_ordered_comm_monoid Γ₀]: (Γ₀ × ℕ+) → (Γ₀ × ℕ+) → Prop := λ x, λ y, ∃ (n : ℕ+), x.fst^(n * y.snd : ℕ) ≤ y.fst^(n * x.snd : ℕ)


How to show such a relation is decidable? I cannot find the correct theorem in mathlib tells me how decidable property interact with existence.

#### Jiang Jiedong (Jun 03 2023 at 19:57):

Maybe more importantly, is it decidable or not? If not, can I avoid this decidable problem? I wonder why a linear_order is required to be decidable in the first place? :upside_down:

#### Jiang Jiedong (Jun 03 2023 at 20:03):

Or could I impose some mild condition on Γ₀ to make this relation decidable?

#### Eric Wieser (Jun 03 2023 at 20:59):

Note you always have the option of cheating and writing classical.dec_rel _ -- TODO: is this decidable?

#### Eric Wieser (Jun 03 2023 at 21:00):

This is what we do with equality on the real numbers, which we know is not decidable

#### Eric Wieser (Jun 03 2023 at 21:12):

Isn't

∃ (n : ℕ+), x.fst^(n * y.snd : ℕ) ≤ y.fst^(n * x.snd : ℕ)


the same as

∃ (n : ℕ+), x.fst^(y.snd : ℕ)^(n : ℕ) ≤ y.fst^(x.snd : ℕ)^(n : ℕ)


which is the same as the following?

x.fst^(y.snd : ℕ) ≤ y.fst^(x.snd : ℕ)


#### Eric Wieser (Jun 03 2023 at 21:12):

If so then you're done because that inequality is already decidable thanks to linear_ordered_comm_monoid!

#### Jiang Jiedong (Jun 04 2023 at 03:55):

Eric Wieser said:

Isn't

∃ (n : ℕ+), x.fst^(n * y.snd : ℕ) ≤ y.fst^(n * x.snd : ℕ)


the same as

∃ (n : ℕ+), x.fst^(y.snd : ℕ)^(n : ℕ) ≤ y.fst^(x.snd : ℕ)^(n : ℕ)


which is the same as the following?

x.fst^(y.snd : ℕ) ≤ y.fst^(x.snd : ℕ)


For linear ordered group, this is true, however for linear ordered monoid this fails. Here is an additive example. Consider the following set Γ₀ = {1,2,...,n-1,+∞} equipped with the obvious total order, and set all additive equations with results greater the n to +∞. Then for any x y : Γ₀ × ℕ+, we have r.le x y since we can always find n such that(n * y.snd) ⬝ x.fst = (n * x.snd) ⬝ y.fst = +∞, but (y.snd : ℕ) ⬝ x.fst ≤ (x.snd : ℕ) ⬝ y.fst may not hold.

#### Jiang Jiedong (Jun 04 2023 at 03:58):

Eric Wieser said:

Note you always have the option of cheating and writing classical.dec_rel _ -- TODO: is this decidable?

Thank you very much! This classical.dec_rel _ -- TODO: is this decidable? is exactly what I want!

Last updated: Dec 20 2023 at 11:08 UTC