How to prove decidability?

Stream: general

[Li Yao'an]

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]

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

[Mario Carneiro]

The actual statement you want to prove is:

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

(deleted)

[Kevin Buzzard]

Interesting! Changing instance to theorem (which is not what you want) makes the error go away.

[Kevin Buzzard]

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]

It has to do with the noncomputable markings associated with use of constants and axioms

[Mario Carneiro]

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]

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.