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


(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: Aug 03 2023 at 10:10 UTC