# Zulip Chat Archive

## Stream: general

### Topic: How to prove decidability?

#### Li Yao'an (Dec 23 2019 at 07:03):

I was reproving things about the natural numbers, when I thought it would be good to show that le (<=) is decidable.

decidable is an inductive class constructed either by p or (not p), so supposing I construct a function f taking in two natural numbers a and b, and gives a proof of either `a <= b`

or `\not(a <= b)`

, and additionally showed that f was decidable, then I could possibly show that <= was decidable with some ite statement over another function g that tells us which statement we are trying to prove. But firstly, we would have to show g was decidable, and I can't seem to show that.

How should I proceed to show the decidability of (a class of) statements?

Edit: Now that I think of it, I'm not sure what the syntax of the statement I'm trying to prove is.

#### Mario Carneiro (Dec 23 2019 at 07:50):

Certainly you can't prove decidability by case analysis. This is essentially assuming what you want to prove

#### Mario Carneiro (Dec 23 2019 at 07:50):

The actual statement you want to prove is:

instance decidable_le : decidable_rel ((<=) : nat -> nat -> Prop) := sorry

#### Mario Carneiro (Dec 23 2019 at 07:51):

In the case of le on natural numbers, the proof goes by induction on one argument and cases on the other

#### Mario Carneiro (Dec 23 2019 at 07:52):

You have to show that `0 <= b`

is true, `succ a <= 0`

is false, and `succ a <= succ b`

iff `a <= b`

#### Li Yao'an (Dec 23 2019 at 08:39):

Thanks for the reply; I am now less confused.

On a theoretical note, suppose I had written the function f (inductively). Additionally, I prove that f either outputs a proof of ` a <= b `

or `\not a <= b`

. Is there any way to formalize the line of reasoning "f is computable and hence proves that ` a <= b `

is decidable?

On a more practical note, I tried to fill in the sorry for the statement you gave (I sorried out the details):

instance decidable_le : decidable_rel ((≤) : nat -> nat -> Prop) |0 b := sorry |(succ a) 0 := sorry |(succ a) (succ b) := begin specialize decidable_le a b, cases decidable_le with h h, admit, admit end

but I'm getting "rec_fn_macro only allowed in meta definitions". What is this error?

#### Mario Carneiro (Dec 23 2019 at 11:15):

Are you sure? The following gives me no errors:

open nat instance decidable_le : decidable_rel ((≤) : nat -> nat -> Prop) |0 b := sorry |(succ a) 0 := sorry |(succ a) (succ b) := begin specialize decidable_le a b, cases decidable_le with h h, admit, admit end

#### Li Yao'an (Dec 24 2019 at 01:55):

My bad, the error only seems to appear once I fill in the admits. Give me some time to generate a somewhat MWE. (I used lots of lemmas.)

#### Li Yao'an (Dec 24 2019 at 02:10):

Here's a code:

namespace hidden inductive nat : Type |zero : nat |succ : nat → nat namespace nat constant le : nat → nat → Prop infix ` ≤ ` := le axiom p1 : ∀ b : nat, zero ≤ b axiom p2 : ∀ a : nat, ¬succ a ≤ zero axiom p3 : ∀ a b : nat, succ a ≤ succ b ↔ a ≤ b instance decidable_le : decidable_rel ((≤) : nat -> nat -> Prop) -- rec_fn_macro only allowed in meta definitions |zero b := begin apply is_true, exact p1 b end |(succ a) zero := begin apply is_false, exact p2 a end |(succ a) (succ b) := begin specialize decidable_le a b, cases decidable_le with h h, apply is_false, rwa p3, apply is_true, rwa p3 end end nat end hidden

#### Kevin Buzzard (Dec 24 2019 at 10:26):

(deleted)

#### Kevin Buzzard (Dec 24 2019 at 10:42):

Interesting! Changing `instance`

to `theorem`

(which is not what you want) makes the error go away.

#### Kevin Buzzard (Dec 24 2019 at 10:45):

It might be something to do with the fact that you're using constants. They get very little love here, nobody ever uses them (perhaps for reasons like this?)

#### Mario Carneiro (Dec 24 2019 at 13:08):

It has to do with the `noncomputable`

markings associated with use of constants and axioms

#### Mario Carneiro (Dec 24 2019 at 13:08):

compare:

namespace hidden inductive nat : Type |zero : nat |succ : nat → nat namespace nat def le : nat → nat → Prop := sorry infix ` ≤ ` := le theorem p1 : ∀ b : nat, zero ≤ b := sorry theorem p2 : ∀ a : nat, ¬succ a ≤ zero := sorry theorem p3 : ∀ a b : nat, succ a ≤ succ b ↔ a ≤ b := sorry instance decidable_le : decidable_rel ((≤) : nat -> nat -> Prop) |zero b := begin apply is_true, exact p1 b end |(succ a) zero := begin apply is_false, exact p2 a end |(succ a) (succ b) := begin specialize decidable_le a b, cases decidable_le with h h, apply is_false, rwa p3, apply is_true, rwa p3 end end nat end hidden

#### Li Yao'an (Dec 26 2019 at 01:50):

Thanks. It seems fixed now.

Previously, in my second case, I proved p2 directly: since le a b was defined as ` \exists x, a + x = b `

, I used choice to pick an x and prove false. Changing this to cases resolves the computability issue and removes the error.

Last updated: May 11 2021 at 00:31 UTC