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


(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