decidable_rel in total_order

Stream: new members

[Jiang Jiedong]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Eric Wieser]

src#localization.decidable_le might be a good example

[Mauricio Collares]

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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Jiang Jiedong]

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]

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!