# Zulip Chat Archive

## 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