Partial decidability

Stream: general

[Daniel Weber]

Consider the following example:

def funEq : Nat → (Nat → Nat) → (Nat → Nat) → Bool
  | 0, _, _ => true
  | n + 1, f, g => f n = g n && funEq n f g

theorem funEq.rfl {n : Nat} {f : Nat → Nat} : funEq n f f := by
  induction n <;> simp_all [funEq]

noncomputable instance : DecidableEq (Nat → Nat) := fun f g ↦
  if h : funEq 100 f g then Classical.propDecidable _ else .isFalse (fun nh ↦ (nh ▸ h) funEq.rfl)

example : (fun n ↦ 2 * n) ≠ (fun n ↦ 2 * n + (if 10 < n then 1 else 0)) := by
  decide

In this case, despite the Decidable instance being noncomputable, it can reduce some, before it gives up and uses Classical.propDecidable. This allows using decide, even on things which aren't decidable, but only have a certificate in some cases. Are there cases where this might be useful?

[Daniel Weber]

Why does this not work?

import Mathlib

set_option autoImplicit false

variable (p : Nat → Prop) [DecidablePred p]

noncomputable instance : Decidable (∃ a, p a) :=
  if h : ∃ a : Nat, a < 20 ∧ p a then .isTrue (h.rec fun w h ↦ ⟨w, h.2⟩) else Classical.propDecidable _

example : ∃ a : Nat, a < 20 ∧ a + 1 = 3 := by
  decide -- works

example : ∃ a : Nat, a + 1 = 3 := by
  decide -- works

example : ∃ a : Nat, ∃ b : Nat, b < 20 ∧ b < a := by
  decide -- works

example : ∃ a : Nat, a < 20 ∧ ∃ b : Nat, b < a := by
  decide -- fails

example : ∃ a : Nat, ∃ b : Nat, b < a := by
  decide -- fails

[Eric Wieser]

I would guess that src#Nat.decidableExistsLT is missing some short-circuiting

[Eric Wieser]

Oh, in the last case the problem is that the loop for the inner Exists runs before the outer one

[Daniel Weber]

Oh, it's because the loop for the outer Exists needs to be able to fully reduce the inner decidable instance?

[Daniel Weber]

May I ask how you debugged this? I had trouble doing that

[Daniel Weber]

Is there any way to make it attempt reducing everything at once?

[Eric Wieser]

Daniel Weber said:

May I ask how you debugged this? I had trouble doing that

I swapped the order of the binders and saw it worked

[Eric Wieser]

I think if you want to handle partial decidability properly, you need a PartiallyDecidable typeclsas

[Daniel Weber]

Yes, that's what I'm doing right now

[Eric Wieser]

class inductive PartiallyDecidable (P : Prop) (fuel : Nat) where
  | isTrue (h : P)
  | isFalse (h : ¬ P)
  | undecided

seems like a reasonable definition

[Daniel Weber]

What do you need fuel for?

[Daniel Weber]

I currently have

class inductive Semidecidable (p : Prop)
  | isFalse (h : ¬p) : Semidecidable p
  | isTrue (h : p) : Semidecidable p
  | give_up : Semidecidable p

[Eric Wieser]

So that you can pass your 20 around

[Eric Wieser]

Maybe I have it in the wrong place though

[Eric Wieser]

inductive PartiallyDecidable.Result (P : Prop) where
  | isTrue (h : P)
  | isFalse (h : ¬ P)
  | undecided

class PartiallyDecidable (P : Prop) where
  decide (fuel : ℕ) : PartiallyDecidable.Result P

instance Decidable.toPartiallyDecidable (P : Prop) [Decidable P] : PartiallyDecidable P where
  decide _ := match ‹Decidable P› with
    | .isTrue h => .isTrue h
    | .isFalse h => .isFalse h

seems a little better

[Eric Wieser]

Here's a working version:

import Mathlib

inductive PartiallyDecidable.Result (P : Prop) where
  | isTrue (h : P)
  | isFalse (h : ¬ P)
  | undecided

class PartiallyDecidable (P : Prop) where
  decide (fuel : ℕ) : PartiallyDecidable.Result P

instance Decidable.toPartiallyDecidable (P : Prop) [Decidable P] : PartiallyDecidable P where
  decide _ := match ‹Decidable P› with
    | .isTrue h => .isTrue h
    | .isFalse h => .isFalse h

instance PartiallyDecidable.not (P : Prop) [PartiallyDecidable P] : PartiallyDecidable ¬P where
  decide fuel := match ‹PartiallyDecidable P›.decide fuel with
    | .isTrue h => .isFalse (by simpa using h)
    | .isFalse h => .isTrue (by simpa using h)
    | .undecided => .undecided

instance partiallyDecidableExists (p : Nat → Prop) [h : ∀ i, PartiallyDecidable (p i)] : PartiallyDecidable (∃ m : Nat, p m) where
  decide fuel := go fuel fuel
where
  go (fuel : Nat) : Nat → _
  | 0 => .undecided
  -- todo: could adjust how much fuel to give the sub-procedure
  | (n + 1) => match (h n).decide fuel with
    | .isTrue h => .isTrue ⟨n, h⟩
    | _ => go fuel n

#eval (inferInstance : PartiallyDecidable (∃ a : Nat, ∃ b : Nat, b < a)).decide 10
#eval (inferInstance : PartiallyDecidable (¬∃ a : Nat, ∃ b : Nat, b < a)).decide 10

[Mario Carneiro]

I've always wanted that type, although I have usually gone for the simpler

class inductive Semidecidable (p : Prop)
  | isTrue (h : p) : Semidecidable p
  | unknown : Semidecidable p

But people have pointed out (correctly) that this is a misuse of the term

[Mario Carneiro]

in particular, Semidecidable p in this style is the minimum you need to implement a decide-like tactic

[Eric Wieser]

Having isFalse is useful because then you can have a [Semidecidable P] : Semidecidable (¬P) instance

[Mario Carneiro]

The asymmetry is deliberate, I don't think that's a useful instance

[Mario Carneiro]

Instead there is [Decidable P] : Semidecidable P which would get used if you need to deal with negation

[Mario Carneiro]

or otherwise there is a direct instance

[Eric Wieser]

See my edit above, without it you can't decide ¬∃ a : Nat, ∃ b : Nat, b < a

[Eric Wieser]

At least, not without repeating every Semidecidable P instance for Semidecidable ¬P, which seems silly

[Mario Carneiro]

your instance is doing something different though with the fuel, that seems like a completely different typeclass

[Mario Carneiro]

the purpose of semidecidable instances is to construct proofs and never disproofs

[Eric Wieser]

I'm not sure how you implement partiallyDecidableExists without some notation of fuel

[Eric Wieser]

(other than hard-coding it in the instance itself)

[Mario Carneiro]

like I said, what you are doing with fuel looks like a completely different typeclass

[Mario Carneiro]

my notion of semidecidable doesn't do fuel based reasoning at all

[Mario Carneiro]

it just only proves positive results

[Eric Wieser]

Is Semidecidable (∃ a, p a) possible to provide an instance of for your version?

[Mario Carneiro]

possible yes, but there would not be such an instance

[Mario Carneiro]

it is always possible to write an instance for any proposition

[Eric Wieser]

Maybe I should have said "such that ∃ a : Nat, ∃ b : Nat, b < a can be decided with it"

[Mario Carneiro]

the purpose I would put it to is for deciding special purpose predicates where we are not really interested in negating it

[Eric Wieser]

I guess my PartiallyDecidable is starting to go into plausible territory

[Mario Carneiro]

exactly

[Joachim Breitner]

Mario Carneiro said:

I've always wanted that type, although I have usually gone for the simpler

class inductive Semidecidable (p : Prop)
  | isTrue (h : p) : Semidecidable p
  | unknown : Semidecidable p

But people have pointed out (correctly) that this is a misuse of the term

Here too! Is there a better term we would use?

[Jz Pan]

Eric Wieser said:

Here's a working version:

import Mathlib

inductive PartiallyDecidable.Result (P : Prop) where
  | isTrue (h : P)
  | isFalse (h : ¬ P)
  | undecided

class PartiallyDecidable (P : Prop) where
  decide (fuel : ℕ) : PartiallyDecidable.Result P

instance Decidable.toPartiallyDecidable (P : Prop) [Decidable P] : PartiallyDecidable P where
  decide _ := match ‹Decidable P› with
    | .isTrue h => .isTrue h
    | .isFalse h => .isFalse h

instance PartiallyDecidable.not (P : Prop) [PartiallyDecidable P] : PartiallyDecidable ¬P where
  decide fuel := match ‹PartiallyDecidable P›.decide fuel with
    | .isTrue h => .isFalse (by simpa using h)
    | .isFalse h => .isTrue (by simpa using h)
    | .undecided => .undecided

instance partiallyDecidableExists (p : Nat → Prop) [h : ∀ i, PartiallyDecidable (p i)] : PartiallyDecidable (∃ m : Nat, p m) where
  decide fuel := go fuel fuel
where
  go (fuel : Nat) : Nat → _
  | 0 => .undecided
  -- todo: could adjust how much fuel to give the sub-procedure
  | (n + 1) => match (h n).decide fuel with
    | .isTrue h => .isTrue ⟨n, h⟩
    | _ => go fuel n

#eval (inferInstance : PartiallyDecidable (∃ a : Nat, ∃ b : Nat, b < a)).decide 10
#eval (inferInstance : PartiallyDecidable (¬∃ a : Nat, ∃ b : Nat, b < a)).decide 10

Your definition has a problem that everything is PartiallyDecidable by just return undecided...

[Eric Wieser]

Yes, the fixed version of that problem already exists and is called Decidable :smile:

[Niels Voss]

What about something like

import Mathlib
set_option autoImplicit false
variable {α : Type*}

class inductive Semidecidable (p : Prop)
  | isTrue (h : p) : Semidecidable p
  | unknown : Semidecidable p

class SemidecidablePred (p : α → Prop) where
  decide (a : α) (n : ℕ) : Semidecidable (p a)
  isFalse (a : α) (h : ∀ n : ℕ, decide a n = .unknown) : ¬p a

instance (p : α → Prop) [DecidablePred p] : SemidecidablePred p where
  decide a _ := if h : p a then .isTrue h else .unknown
  isFalse a h := by aesop

instance : SemidecidablePred (fun (f, g) => (f : ℕ → ℕ) ≠ g) where
  decide p n := if h : p.1 n = p.2 n then .unknown else .isTrue (by aesop)
  isFalse p h := by
    simp at h
    change ∀ n, ¬¬(p.1 n = p.2 n) at h
    aesop

[Niels Voss]

I don't think it generally makes sense to talk about an individual proposition as Semidecidable Nevermind, I think you can

[Jz Pan]

I think your Semidecidable is in here https://en.wikipedia.org/wiki/Computably_enumerable_set

[Niels Voss]

Yes, is this not the most common definition of semidecidability? Maybe we could have partial decidability as a "best-effort" decision procedure and semidecidability as the more formal definition

[Matt Diamond]

Is there a relation between SemidecidablePred and docs#RePred ? I suppose it's analogous to docs#DecidablePred and docs#ComputablePred

[Niels Voss]

I'm hoping that's the case

[Niels Voss]

Here's a slight generalization of my past code:

import Mathlib
set_option autoImplicit false
variable {α : Type*}

class inductive PossiblyDecidable (p : Prop)
  | isTrue (h : p) : PossiblyDecidable p
  | unknown : PossiblyDecidable p
deriving Repr, DecidableEq

private def decideRec (p : Prop) (decide : ℕ → PossiblyDecidable p) : ℕ → PossiblyDecidable p
| 0 => PossiblyDecidable.unknown
| n+1 => match decideRec p decide n with
  | .isTrue h => .isTrue h
  | .unknown => decide n

class Semidecidable (p : Prop) where
  decide (n : ℕ) : PossiblyDecidable p
  decideLe (n m : ℕ) (h₁ : n ≤ m) (h₂ : decide m = .unknown) : decide n = .unknown
  isFalse (h : ∀ n : ℕ, decide n = .unknown) : ¬p

def Semidecidable.strongMk {p : Prop} (decide : ℕ → PossiblyDecidable p)
  (isFalse : (∀ n : ℕ, decide n = .unknown) → ¬p) : Semidecidable p where
  decide := decideRec p decide
  decideLe n m h₁ h₂ := by
    induction h₁ using Nat.leRec with
    | refl => exact h₂
    | @le_succ_of_le k h₂ ih =>
      unfold decideRec at h₂
      aesop
  isFalse h := by
    apply isFalse
    intro n
    specialize h (n + 1)
    unfold decideRec at h
    aesop

instance (p : Prop) [Decidable p] : Semidecidable p where
  decide _ := if h : p then .isTrue h else .unknown
  decideLe := by aesop
  isFalse := by aesop

instance (f : ℕ → ℕ) (g : ℕ → ℕ) : Semidecidable (f ≠ g) := Semidecidable.strongMk
  (fun n => if h : f n = g n then .unknown else .isTrue (by change f ≠ g; aesop))
  (fun h => by aesop)

At first, the extra condition in Semidecidable might appear to be more restrictive, but I think it can speed up computation when using Semidecidable

[Niels Voss]

Actually, I'm not sure which formulation is better for performance

[Niels Voss]

There's also

instance (p : Prop) [Semidecidable p] [Semidecidable ¬p] : Decidable p :=
  let m (n : ℕ) : Option (Decidable p) := match Semidecidable.decide n, Semidecidable.decide n with
  | .isTrue (h₁ : p), .isTrue (h₂ : ¬p) => absurd h₁ h₂
  | .isTrue (h₁ : p), .unknown => some (Decidable.isTrue h₁)
  | .unknown, .isTrue (h₂ : ¬p) => some (Decidable.isFalse h₂)
  | .unknown, .unknown => none
  have h : ∃ n : ℕ, (m n).isSome := by
    by_contra! hc
    have : ¬p := Semidecidable.isFalse (by intro n; specialize hc n; aesop)
    have : ¬¬p := Semidecidable.isFalse (by intro n; specialize hc n; unfold m at hc; split at hc <;> aesop)
    contradiction
  (m (Nat.find h)).get (Nat.find_spec h)

although this has the potential to cause diamonds

[Jz Pan]

Matt Diamond said:

Is there a relation between SemidecidablePred and docs#RePred ? I suppose it's analogous to docs#DecidablePred and docs#ComputablePred

According to Wikipedia, Semidecidable is also called recursively enumerable which is RePred. To me, the differences between RePred and ComputablePred vs DecidablePred is that the former use formalized computability concept, while DecidablePred uses meta computability concept, i.e. if you use Classical then everything becomes DecidablePred, while it's false for RePred and ComputablePred.