Feature Request: Partial Decision Algorithm

[kckennylau]

Zulip discussions:

• #Is there code for X? > Partial decision
• #general > Partial decidability

This is a feature request to build something like Decidable but which is allowed to not return a definite result for all inputs.

Testcase (working code):

import Mathlib

inductive PartialDecide (α : Prop) : Type
  | decided (prf : α) : PartialDecide α
  | undecided : PartialDecide α

def PartialDecide.result {α : Prop} : PartialDecide α → Prop
  | decided _ => α
  | undecided => True

theorem PartialDecide.prf {α : Prop} : (h : PartialDecide α) → h.result
  | decided prf => prf
  | undecided => trivial

def sumOfKPrimes (k n : ℕ) := ∃ primes : List ℕ, primes.all Nat.Prime ∧ primes.length = k ∧ primes.sum = n

def foo (f : List ℕ) :=
  match f with
  | List.nil => True
  | List.cons s f' => sumOfKPrimes 2 s ∧ (foo f')

def foo_of : (target : List ℕ) → (evidence : List (ℕ × ℕ)) → PartialDecide (foo target)
  | [], [] => .decided trivial
  | [], (e :: et) => .undecided
  | (t :: tt), [] => .undecided
  | (t :: tt), (e :: et) => match foo_of tt et with
      | .decided ih => if h : e.1 + e.2 = t ∧ e.1.Prime ∧ e.2.Prime then
          .decided ⟨⟨[e.1, e.2], by simp [h]⟩, ih⟩ else .undecided
      | .undecided => .undecided

example : foo [13, 18, 20] :=
  (foo_of [13, 18, 20] [(2,11), (5,13), (3,17)]).prf

example : let tg := [13, 18, 20]; foo tg := by
  intro tg
  exact (foo_of tg [(2,11), (5,13), (3,17)]).prf

Note that the above example only has decided which returns the proof, and undecided which returns nothing, but it has also been remarked that it should have three potential outputs: that is, it should also return a proof of the negation.