computable class

Stream: general

[Kyle Miller]

There had been some previous discussion about having a computable class that mirrors decidable, but for Type instead of Prop (two threads: 1 2). If it were possible, what this might let us do for mathlib is use mathematically convenient noncomputable definitions, then off to the side have decidable and computable instances for when we want to actually compute something. What I hope is (1) that this would free those who don't care about computability from having to think about adding the right decidability instances to their theorems (and even if you do care about computability, this is usually irrelevant information anyway), and (2) that this would alleviate diamond problems that come from including decidability instances in our class hierarchy.

The idea is to have a class

class computable {α : Type*} (x : α) :=
(compute : α)
(compute_eq : compute = x)

export computable(compute)

and then you would be able to write compute z when z is a noncomputable term that can be computed in some way.

When I've tried this in Lean 3, there's been a problem that computable instances need to be marked noncomputable, defeating the whole point of this class.

Lean 3 code

import logic.basic

class computable {α : Type*} (x : α) :=
(compute : α)
(compute_eq : compute = x)

open computable(compute)

structure erased (α : Type*) :=
(p : α → Prop)
(singleton : ∃ x, p x ∧ ∀ y, p y → y = x)

def erased.of {α : Type*} (x : α) : erased α :=
{ p := λ y, y = x,
  singleton := ⟨x, rfl, λ _, id⟩ }

noncomputable
def erased.out {α : Type*} (x : erased α) : α := x.singleton.some

noncomputable -- needs to be noncomputable??
instance {α : Type*} (x : α) : computable (erased.of x).out :=
{ compute := x,
  compute_eq := ((erased.of x).singleton.some_spec).1.symm }

noncomputable -- :-(
def foo {α : Type*} (x : α) : α := compute (erased.of x).out

Oddly, #eval is happy to compute with this noncomputable instance anyway:

#eval compute (erased.of 2).out
-- 2

I tried implementing Computable today in Lean 4, and in my small tests it is able to tell that these instances are computable.

class Computable {α : Type _} (x : α) where
  compute : α
  compute_eq : compute = x

export Computable(compute)

structure erased (α : Type _) where
  p : α → Prop
  singleton : ∃ x, p x ∧ ∀ y, p y → y = x

def erased.of (x : α) : erased α where
  p := λ y => y = x
  singleton := ⟨x, rfl, λ _ => id⟩

noncomputable
def erased.out (x : erased α) : α := Classical.choose x.singleton

instance (x : α) : Computable (erased.of x).out where
  compute := x
  compute_eq := (Classical.choose_spec (erased.of x).singleton).1.symm

def foo (x : α) : α := compute (erased.of x).out

section from_mathlib4

namespace WellFounded
variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}

unsafe def fix'.impl (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
  F x fun y _ => impl hwf F y

set_option codegen false in
@[implementedBy fix'.impl]
def fix' (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x := hwf.fix F x

end WellFounded

namespace Nat

variable (p : Nat → Prop)

private def lbp (m n : Nat) : Prop := m = n + 1 ∧ ∀ k, k ≤ n → ¬p k

variable [DecidablePred p] (H : ∃ n, p n)

private def wf_lbp : WellFounded (lbp p) := by
  refine ⟨let ⟨n, pn⟩ := H; ?_⟩
  suffices ∀ m k, n ≤ k + m → Acc (lbp p) k from fun a => this _ _ (Nat.le_add_left _ _)
  intro m
  induction m with refine fun k kn => ⟨_, fun | _, ⟨rfl, a⟩ => ?_⟩
  | zero => exact absurd pn (a _ kn)
  | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)

protected def find_x : {n // p n ∧ ∀ m, m < n → ¬p m} :=
(wf_lbp p H).fix' (C := fun k => (∀n, n < k → ¬p n) → {n // p n ∧ ∀ m, m < n → ¬p m})
  (fun m IH al => if pm : p m then ⟨m, pm, al⟩ else
      have this : ∀ n, n ≤ m → ¬p n := fun n h =>
        (Nat.eq_or_lt_of_le h).elim (fun e => by rw [e]; exact pm) (al n)
      IH _ ⟨rfl, this⟩ fun n h => this n $ Nat.le_of_succ_le_succ h)
  0 fun n h => absurd h (Nat.not_lt_zero _)

protected def find : Nat := (Nat.find_x p H).1

protected theorem find_spec : p (Nat.find p H) := (Nat.find_x p H).2.1

protected theorem find_min : ∀ {m : Nat}, m < Nat.find p H → ¬p m := @(Nat.find_x p H).2.2

protected theorem find_min' {m : Nat} (h : p m) : Nat.find p H ≤ m :=
Nat.ge_of_not_lt λ l => Nat.find_min p H l h

end Nat

end from_mathlib4

noncomputable
def inf (p : Nat → Prop) : Nat :=
let d := Classical.propDecidable
if h : ∃ n, p n then Nat.find _ h else 0

instance {p : Nat → Prop} [DecidablePred p] [Decidable (∃ n, p n)] : Computable (inf p) where
  compute := if h : ∃ n, p n then Nat.find p h else 0
  compute_eq := by
    split
    simp [inf, *]
    rename ∃ n, p n => h
    have : Eq.mpr_prop (eq_true h) True.intro = h := rfl
    rw [this]
    rename DecidablePred p => instp
    have : (λ a => Classical.propDecidable (p a)) = instp := by
      apply Subsingleton.elim
    rw [this]
    simp [inf, *]

instance (x : Nat) : Decidable (∃ n, n = x) := Decidable.isTrue ⟨x, rfl⟩

def bar (x : Nat) : Nat := compute (inf (λ n => n = x))

#eval compute (inf (λ n => n = 37))
-- 37

In this, there's the same erased example along with a noncomputable definition of inf for natural numbers that uses Nat.find to compute it.

This makes me wonder: is this a fundamental limitation of the noncomputability system in Lean 3, or is it a fixable bug?

[Eric Wieser]

I prototyped something like this a while ago, but with quite a different implementation

[Eric Wieser]

Although I guess actually that's not to similar to what you have, it just fits the same ambiguous "decidable but for Type" specification

[Kyle Miller]

If you think about decidable as being a term-level partial function to_bool : Prop -> bool that has the property that (to_bool p : Prop) = p, then it's clearer that this is what "decidable but for Type" sort of should be.

class decidable' (p : Prop) :=
(to_bool : bool)
(to_bool_eq : (to_bool : Prop) = p)

This does suggest that computable is too rigid in that it requires the computed value lie in the same type, so something like the following would be an alternative:

/-- Gives a type in which computations are more convenient.
Instances do not have to be computable. -/
class computable_type (α : Type*) (β : out_param $ Type*) :=
(cast : α ≃ β)

class computable {α : Type*} {β : out_param $ Type*} [computable_type α β] (x : α) :=
(compute : β)
(compute_eq : compute = computable_type.cast x)

However, I'm not sure this is necessary since you could always compute (to_foo x) for a relevant to_foo function.

[Kyle Miller]

It looks like with enough of what Mario calls "laundering" through docs#erased and of applying the inline attribute, it actually is possible to get this to work in Lean 3. When I'd tried using erased like this before, I couldn't get if to compute, but compute (if 0 < m then Inf {n | n < m} else 0) seems to work fine now that the instances are inline.

Lean 3 code

import data.set.basic
import order.order_iso_nat
import data.erased

class computable {α : Type*} (x : erased α) :=
(compute : α)
(compute_eq : compute = x.out)

abbreviation compute {α : Type*} (x : α) [computable (erased.mk x)] : α :=
computable.compute (erased.mk x)

lemma compute_eq {α : Type*} (x : α) [computable (erased.mk x)] : compute x = x :=
computable.compute_eq.trans (erased.out_mk _)

/-- This should only be used when `x` is not `noncomputable`.
It might not be necessary, since presumably you'd only `compute` noncomputable things,
but it's useful for the `if` test below. -/
@[priority 0, inline]
instance computable_default {α : Type*} (x : α) : computable (erased.mk x) :=
⟨x, (erased.out_mk _).symm⟩

@[inline]
instance computable.nat_Inf {p : ℕ → Prop} [decidable (∃ n, p n)] [decidable_pred p] :
  computable (erased.mk (Inf {n : ℕ | p n})) :=
if h : ∃ n, p n
then ⟨nat.find h, eq.trans (by convert (nat.Inf_def h).symm) (erased.out_mk _).symm⟩
else ⟨0, by { push_neg at h, simp [h], }⟩

instance (x : ℕ) : decidable (∃ n, n = x) := is_true ⟨x, rfl⟩

def foo (x : ℕ) : ℕ := compute (Inf {n | n = x})

@[inline]
instance computable.ite {p : Prop} [decidable p] {α : Type*} {x y : α}
  [computable (erased.mk x)] [computable (erased.mk y)] :
  computable (erased.mk (if p then x else y)) :=
if h : p then by rwa [if_pos h] else by rwa [if_neg h]

instance decidable.exists_nat_lt (m : ℕ) : decidable (∃ n, n < m) :=
if h : m = 0 then is_false (by simp [h])
else is_true begin
  cases m,
  exact (h rfl).elim,
  exact ⟨0, nat.succ_pos _⟩,
end

def baz (m : ℕ) : ℕ := compute (if 0 < m then Inf {n | n < m} else 0)

With Lean 4, you don't need this additional complexity, and

instance [Decidable p] (x y : α) [Computable x] [Computable y] : Computable (if p then x else y) :=
if h : p then (by simp [h]; assumption) else (by simp [h]; assumption)

works fine.

[Kyle Miller]

Here's another experiment along these lines. In the spoiler block there are computable instances for getting coefficients of simple polynomial expressions (addition, multiplication, constant powers), and this lets you evaluate, for instance,

#eval compute $ ((1 + polynomial.X : ℕ[X])^10).coeff 3
-- 120

The implementation I gave for pow is pretty bad (I think it's exponentially slow in the exponent), but in any case it can be evaluated faster by adding in a specialized instance that relies on the binomial theorem:

@[inline]
instance binomial_compute (n k : ℕ) :
  computable (erased.mk (((1 + polynomial.X) ^ n).coeff k : ℕ)) :=
⟨n.choose k, by simp [polynomial.coeff_one_add_X_pow]⟩

#eval compute $ ((1 + polynomial.X : ℕ[X])^10).coeff 3
-- 120

Lean 3 code

import data.set.basic
import order.order_iso_nat
import data.erased
import data.polynomial
import data.nat.choose

class computable {α : Type*} (x : erased α) :=
(compute : α)
(compute_eq : compute = x.out)

abbreviation compute {α : Type*} (x : α) [computable (erased.mk x)] : α :=
computable.compute (erased.mk x)

lemma compute_eq {α : Type*} (x : α) [computable (erased.mk x)] : compute x = x :=
computable.compute_eq.trans (erased.out_mk _)

/-- This should only be used when `x` is not `noncomputable`. -/
@[inline]
def computable_default {α : Type*} (x : α) : computable (erased.mk x) :=
⟨x, (erased.out_mk _).symm⟩

@[inline]
instance computable.nat_Inf {p : ℕ → Prop} [decidable (∃ n, p n)] [decidable_pred p] :
  computable (erased.mk (Inf {n : ℕ | p n})) :=
if h : ∃ n, p n
then ⟨nat.find h, eq.trans (by convert (nat.Inf_def h).symm) (erased.out_mk _).symm⟩
else ⟨0, by { push_neg at h, simp [h], }⟩

instance (x : ℕ) : decidable (∃ n, n = x) := is_true ⟨x, rfl⟩

def foo (x : ℕ) : ℕ := compute (Inf {n | n = x})

@[inline]
instance computable.ite {p : Prop} [decidable p] {α : Type*} {x y : α}
  [computable (erased.mk x)] [computable (erased.mk y)] :
  computable (erased.mk (if p then x else y)) :=
if h : p then by rwa [if_pos h] else by rwa [if_neg h]

instance decidable.exists_nat_lt (m : ℕ) : decidable (∃ n, n < m) :=
if h : m = 0 then is_false (by simp [h])
else is_true begin
  cases m,
  exact (h rfl).elim,
  exact ⟨0, nat.succ_pos _⟩,
end

instance decidable.exists_nat_lt' (m : ℕ) : decidable (∃ n, m < n) :=
is_true ⟨m + 1, lt_add_one m⟩

def baz (m : ℕ) : ℕ := compute (if 0 < m then Inf {n | n < m} else Inf {n | m < n})

section poly
open_locale big_operators polynomial

variables {R : Type*} [semiring R]

@[simp] lemma polynomial.C_coeff (r : R) (n : ℕ) : (polynomial.C r).coeff n = if n = 0 then r else 0 :=
begin
  convert_to (polynomial.C r * polynomial.X ^ 0).coeff n = _,
  simp,
  rw polynomial.coeff_C_mul_X_pow,
end

@[inline]
instance polynomial.C_coeff.compute (r : R) (n : ℕ) :
  computable (erased.mk $ (polynomial.C r).coeff n) :=
begin
  simp,
  apply computable_default,
end

@[inline]
instance polynomial.one_coeff.compute (n : ℕ) :
  computable (erased.mk $ (1 : R[X]).coeff n) :=
begin
  convert_to computable (erased.mk $ (polynomial.C (1 : R)).coeff n),
  apply polynomial.C_coeff.compute,
end

@[inline]
instance polynomial.X_coeff.compute (n : ℕ) :
  computable (erased.mk $ (polynomial.X : R[X]).coeff n) :=
begin
  use if (n = 1) then 1 else 0,
  simp,
  convert_to _ = ((polynomial.X : R[X]) ^ 1).coeff n,
  simp,
  rw [polynomial.coeff_X_pow],
end

@[inline]
instance polynomial.coeff_add.compute (p q : R[X]) (n : ℕ)
  [computable $ erased.mk $ p.coeff n] [computable $ erased.mk $ q.coeff n] :
  computable (erased.mk $ (p + q).coeff n) :=
begin
  use compute (p.coeff n) + compute (q.coeff n),
  simp [compute_eq],
end

@[inline]
instance polynomial.coeff_mul.compute (p q : R[X]) (n : ℕ)
  [∀ k, computable $ erased.mk $ p.coeff k] [∀ k, computable $ erased.mk $ q.coeff k] :
  computable (erased.mk $ (p * q).coeff n) :=
begin
  rw polynomial.coeff_mul,
  simp_rw [← (λ y, compute_eq (p.coeff y)), ← (λ y, compute_eq (q.coeff y))],
  apply computable_default,
end

@[inline]
instance polynomial.coeff_pow.compute (p : R[X])
  [∀ k, computable $ erased.mk $ p.coeff k] : Π (k n : ℕ),
  computable (erased.mk $ (p ^ k).coeff n) :=
begin
  intro k,
  induction k,
  intro n, simp, apply_instance,
  intro n,
  rw [pow_succ], resetI, apply_instance,
end

#eval compute (((1 + polynomial.X : ℕ[X])).coeff 3 : ℕ)
-- 0
#eval compute (((1 + polynomial.X : ℕ[X])^10).coeff 3 : ℕ)
-- 120

@[inline]
instance binomial_compute (n k : ℕ) :
  computable (erased.mk (((1 + polynomial.X) ^ n).coeff k : ℕ)) :=
⟨n.choose k, by simp [polynomial.coeff_one_add_X_pow]⟩

#eval compute (((1 + polynomial.X : ℕ[X])^10).coeff 3 : ℕ)
-- 120

end poly

[Kyle Miller]

Kyle Miller said:

This makes me wonder: is this a fundamental limitation of the noncomputability system in Lean 3, or is it a fixable bug?

If I've understood it correctly, this is fixable in Lean 3. The noncomputability checker wasn't skipping inductive type parameters in constructors (which I'm under the impression have no computational relevance), and if we make it skip those, the computable class would work just about the same between Lean 3 and Lean 4.

Would this break anything in theory?

Here's a PR: lean#693 (it passes all the tests on my machine, so it doesn't appear to have broken anything in that respect)

[Kyle Miller]

After the noncomputability checker, the compiler seems to do something similar and skip parameters and also additional computationally irrelevant arguments (these are handled by a separate mechanism in the noncomputability checker).

[Kyle Miller]

Another question: what's the actual role of noncomputable? If the noncomputability checker fails to say something is noncomputable, is the only effect that the code generator will eventually raise an error?

[Johan Commelin]

Kyle Miller said:

Here's another experiment along these lines. In the spoiler block there are computable instances for getting coefficients of simple polynomial expressions (addition, multiplication, constant powers), and this lets you evaluate, for instance,

#eval compute $ ((1 + polynomial.X : ℕ[X])^10).coeff 3
-- 120

That looks nice! I really like this. Of course something similar could be accomplished with norm_num. However, what I really like is the promise that this will get rid of all sorts of computability issues in definitions. We should be able to work with

class fintype (X : Type*) : Prop :=
cardinal.mk X < \omega

and just have some version of compute that takes care of computations in zmod 8 when needed.

[Johan Commelin]

Just to make sure, will

example : compute (((1 + polynomial.X : ℕ[X])^10).coeff 3) = 120 := rfl

also work?

[Kyle Miller]

That last one seems like the purview of norm_num, but there's nothing but the usual things stopping a rfl proof like that. That one's too big for my implementation, but something smaller is fine when it's using the binomial theorem instance:

example : compute (((1 + polynomial.X : ℕ[X])^3).coeff 2) = 3 := rfl

[Kyle Miller]

Johan Commelin said:

and just have some version of compute that takes care of computations in zmod 8 when needed.

I imagine finset could stay as-is, just with noncomputable operations in the API that become computable when you compute with the right decidability instances. Then, if we had your proposed fintype class, fintype.univ could noncomputably give a finset that becomes computable when computed. (I think that's behind fin_cases, which I think you're referring to with zmod 8.)

[Gabriel Ebner]

This is an interesting solution to the computing with polynomials issue.

[Gabriel Ebner]

I know you're keen on getting rid of the laundering, but the class Computable (x : Erased α) where compute : α ... variant has one big advantage, namely that you can write the blanket instance instance [Computable (erase a)] where compute := a ....

[Gabriel Ebner]

Without this blanket instance, I imagine it will be awkward to compute open terms like this:

def foo (n : ℕ) := compute $ ((1 + polynomial.X : ℕ[X])^(2*n)).coeff n

[Gabriel Ebner]

On second thought, I'm not sure the blanket instance helps at all.

[Gabriel Ebner]

BTW, you probably want to generalize your ite-compute instance so that it gets rid of classical.prop_decidable:

instance [Decidable p] {inst : Decidable p} (x y : α) [Computable x] [Computable y] :
    Computable (@ite _ p inst x y)

[Kyle Miller]

Gabriel Ebner said:

Without this blanket instance, I imagine it will be awkward to compute open terms like this:

def foo (n : ℕ) := compute $ ((1 + polynomial.X : ℕ[X])^(2*n)).coeff n

At least with how it's set up, this one is fine since the exponent is presumed to be computable, and it's up to the caller of foo to compute the natural number if necessary.

#eval foo 10
-- 184756