Way to recover computability?

Stream: general

[Andreas Poulsen]

I find it odd, that the following doesn't work:

import data.finsupp
open finsupp
#eval (single (1:ℕ) (1:ℕ))

It fails with the message code generation failed, VM does not have code for 'classical.choice', presumably because data.finsupp is a noncomputable theory. However, if I copy the definition of single, adding that the parameters must have decidable equality, it works fine:

variables {M : Type} [has_zero M] [decidable_eq M] {α : Type} [decidable_eq α]

def my_single (a : α) (b : M) : α →₀ M :=
⟨if b = 0 then ∅ else {a}, pi.single a b, λ a', begin
  obtain rfl | hb := eq_or_ne b 0,
  { simp },
  rw [if_neg hb, finset.mem_singleton],
  obtain rfl | ha := eq_or_ne a' a,
  { simp [hb] },
  simp [pi.single_eq_of_ne', ha],
end⟩

#eval (my_single (1:ℕ) (1:ℕ))

which seems to indicate that decidable_eq was actually the missing non-computable component, not choice. Which in turn means, that if I copy the entire data/finsupp/defs.lean file into my own project and add decidability assumptions on everything, I should be able to #eval my functions then.

My question is, if there is a way to propagate decidability information in Lean (maybe Lean4?) so that I don't have to that, and can just rely on the mathlib as-is?

(Note, that what I actually want to use is data.mv_polynomials, which depend on finsupp and add_monoid_algebra, so duplicating everything and updating it to use my version will require some work.)

Thank you advance for any hints you can give me :)

[Eric Wieser]

If you use docs#dfinsupp instead then everything already has these assumptions

[Kyle Miller]

If you don't mind a little #xy, what's your personal motivation for computability? Are you wanting to write a program to compute something (and prove the program is correct)? Are you wanting to #eval a couple values to test things out? Are you wanting it to be computable out of principle?

[Eric Wieser]

In lean4 you can use a @[csimp] attribute to replace single with my_single in the VM

[Kyle Miller]

@Eric Wieser I thought you couldn't -- my_single has a different type, but last I checked csimp needs a definition with the same type.

[Andreas Poulsen]

Of course, it's part of an experiment at school to see how much of Gröbner bases and Buchbergers algorithm we can formalize. But, not being able to run the resulting algorithm seems silly :)

[Kyle Miller]

finsupp isn't a great data structure for actually computing with polynomials, which you might want to consider if you haven't already

[Kyle Miller]

There are a lot of performance issues (the sets only use decidable equality, so there are quadratic operations all over the place) and places where you can have accidental memory leaks (due to the coefficients being stored as functions; you'd need to periodically memoize them yourself).

[Andreas Poulsen]

That's true, but being able to just use mv_polynomials or add_monoid_algebra was tempting, since we're not going for speed.
Otherwise we have to spend a bunch of time proving basic ring axioms before we can get started

[Kyle Miller]

Maybe consider defining a polynomial typeclass and writing your algorithms to work with that, rather than specifically working with mv_polynomials

[Kyle Miller]

and create an instance for mv_polynomials with the appropriate additional decidability assumptions to make things computable

[Andreas Poulsen]

Interesting idea. It'd be a hecking huge typeclass, but it could work.

[Kyle Miller]

That way (1) things are computable, as you want, and (2) one could swap in an efficient polynomial implementation at some point

[Eric Wieser]

Kyle Miller said:

and create an instance for mv_polynomials with the appropriate additional decidability assumptions to make things computable

I don't really see how that would work

[Andreas Poulsen]

Your second point there is a very good point. Sometimes making things more abstract is actually a good way to make it more tractable

[Andreas Poulsen]

@Eric Wieser I guess something like

instance [decidable_eq A] [decidable_eq B] : polynomial_like (mv_polynomial A B) := ...

but we might into the same issue with having to propagate the decidable_eq's.

[Eric Wieser]

I don't see how that's going to help, because if you have x : mv_polynomial A B then that x is almost certainly noncomputable

[Eric Wieser]

So any function converting it into your computable representation is too late

[Kyle Miller]

I think the trick is that you're only ever going to be able to evaluate the Groebner basis algorithms on polynomials that Lean knows are computable, so you can assume such an x is computable

[Kyle Miller]

and inside the Groebner basis algorithms it's going to use the ring structure from the polynomial_like class, which you define in a computable way in that instance. (So I guess this doesn't save you from having to prove ring axioms...)

[Andreas Poulsen]

But, I think @Eric Wieser has a point: right now I can't evaluate a mv_polynomial, even though every part of it is computable. So sticking it behind a computable typeclass would just move the problem somewhere else, I'd have the issue when I try implementing the type class

[Andreas Poulsen]

But maybe we'll start there. At least it'll get us started, then we can worry about implementing computable polynomials later on :)

[Mario Carneiro]

You should not need to prove any ring axioms here. Just make a type of polynomial representations, and a function from that to mv_polynomial and prove that repr (a + b) = repr a + repr b etc

[Mario Carneiro]

docs#onote is a good example of that pattern. It does ordinal arithmetic computably and then has a repr function to relate everything to arithmetic on "real" ordinals (which are noncomputable). You can infer all the axioms by lifting them across that function

[Andreas Poulsen]

@Mario Carneiro thank you for the reference, that seems like a good pattern to know about. Thank you all so much for your inputs, it's greatly appreciated :)