Partial decision

Stream: Is there code for X?

[Kenny Lau]

In another thread (#new members > Force evaluation of List.tail ) I wrote the following code (on top of @Kevin Cheung 's predicate):

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

[Kenny Lau]

In particular, I made a typeclass for partial decision algorithms. Basically, you can now write an algorithm to either produce a proof of some proposition h, or alternatively does nothing.

[Kenny Lau]

Has this been done before?

[Kenny Lau]

it's basically Decidable but with an extra option that it doesn't have to decide

[Kenny Lau]

For a simple example (basically the same example, but I can explain this in text), consider the predicate "n is the sum of two primes". It is obviously decidable, but the naive decision algorithm has complexity O(n log n), and it would be way more efficient if I could tell Lean which two primes to use. Of course, there's no guarantee that I would really produce two correct primes, so the function would also need to know what to do if my witnesses are incorrect.

So, with PartialDecide, if the witnesses are correct, then the function would produce a proof; and otherwise, it doesn't mean the proposition in question is wrong, but simply that the witnesses are incorrect, so the function does not give any useful result.

[Eric Wieser]

I think I have a post about this somewhere, possibly two

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Partial.20decidability/near/483540450

[Eric Wieser]

I'd argue that it's useful to have "true, false, or undecided", not just "true or undecided"

[Kenny Lau]

@Eric Wieser so why wasn't it implemented?

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/issues/26046