computable ZFSet.sInter

Stream: mathlib4

[RustyYato]

Currently ZFSet.sInter is noncomputable, would there be interest in making this function computable?
https://github.com/leanprover-community/mathlib4/blob/339689fb16756e4a0b52ddb36b83e0a81f327d0f/Mathlib/SetTheory/ZFC/Basic.lean#L864-L867

This can be done by doing (⋃₀ x).sep (fun y => ∀ z ∈ x, y ∈ z) since ZFSet.sUnion is computable.

This preserves the special case that ⋂₀∅=∅, since ⋃₀∅=∅, although not definitionally...

[Ruben Van de Velde]

Is there a specific problem this would solve?

[RustyYato]

No, I don't have one.
I am just learning lean and tried formalizing ZF on my own based off of Mathlib's implementation, and found this alternate way to define sInter to make it computable. So I thought it would be nice to have a computable version in Mathlib, since it seems like a minor change.

[Kyle Miller]

@Mario Carneiro might be interested. I see he has some TODO's in that file to make some things computable.

[Ruben Van de Velde]

As a general rule, mathlib doesn't make things computable just because it's possible, only when it's necessary

[Kevin Buzzard]

In fact making things computable can make it harder to prove theorems about them (this is why polynomials are noncomputable), and the main focus of mathlib is not computability but proving theorems.

[Yury G. Kudryashov]

I think that one of big issues with making things computable is that quite often they are computable but slow. E.g., for polynomials or matrices, one may want to have an optimized data representation for a task.

[Yury G. Kudryashov]

It would be nice to have some computable structures representing these objects and proofs of isomorphisms (e.g., for usage in tactics etc)

[Mario Carneiro]

@RustyYato From my end, I'm perfectly happy with a contribution which modifies the definition of sInter to that and reproving the characterizing lemmas.

[RustyYato]

Thanks for all the responses, I didn't realize that making things computable could slow it down! Although this does make sense in hindsight, since lean has more work to do to ensure the correctness of the proofs. I'll keep this in mind, and maybe I can learn how polynomials being noncomputable makes things faster. I didn't check that out yet so that looks like fun!

[RustyYato]

Thanks @Mario Carneiro, I'll put up a PR tomorrow.

[Mario Carneiro]

I don't think computability per se is important or relevant for the ZFC development in particular. The TODO in the code is actually about eliminating uses of lean's axiom of choice in the construction of a model of ZF - obviously you need choice to validate the choice axiom of ZFC, but it's not philosophically well motivated to also be using it to validate the axiom of replacement et al, but there are some technical issues to making it work out

[Eric Wieser]

Kevin Buzzard said:

can make it harder to prove theorems about them (this is why polynomials are noncomputable)

I think this is only half the picture; we decided in lean3 that the computability made things harder, and the cost of revisiting that decision (with Lean 4 and a better understanding of open scoped Classical) is very high, because so much of mathlib would have to change

[Mario Carneiro]

There were some people at the HIM semester who were pursuing sparse or dense computable polynomial representations; it may be a good idea to try upstreaming one of these to mathlib

[Eric Wieser]

I'll link https://github.com/leanprover-community/mathlib4/wiki/Computation-models-for-polynomials-and-finitely-supported-functions for some context for those who don't have it

[RustyYato]

while writing this, I noticed that there isn't a ZFSet.sep_empty theorem, so I'm adding that too since I need it to prove ZFSet.sInter_empty with the new formulation

[RustyYato]

Here's the PR, thanks everyone for your input, I learned a lot from this thread!
https://github.com/leanprover-community/mathlib4/pull/15624

[Yury G. Kudryashov]

RustyYato said:

I didn't realize that making things computable could slow it down!

If you're referring to my reply, then I didn't mean that computability will slow down the system. I meant that people may see that something is computable and try to actually use via #eval or native_decide, then find out that the definition is computable but very slow

[Eric Wieser]

Computable but (very) slow is still useful for quickly checking how a definition behaves on examples

[Dexin Zhang]

Mario Carneiro said:

obviously you need choice to validate the choice axiom of ZFC, but it's not philosophically well motivated to also be using it to validate the axiom of replacement et al, but there are some technical issues to making it work out

We can define computable axiom of replacement and ZFSet.range from computable lifts for functions of arbitrary arity. However it seems there are no such computable lifts in the current Lean4 -- I believe this is the biggest "technical issue" preventing us from a computable axiom of replacement :(

[Mario Carneiro]

Yes, we basically need a mechanism to lift arbitrary ZFC formulas to produce n-ary PSet functions. When I wrote that todo originally, I did enough investigation to determine that it is possible in general but needs some metaprogramming to be convenient

[Mario Carneiro]

There is some work in docs#PSet.Definable to do this, but docs#Classical.allDefinable is the cop-out solution because it seemed like too much trouble at the time

[Matthew Ballard]

Mario Carneiro said:

There were some people at the HIM semester who were pursuing sparse or dense computable polynomial representations; it may be a good idea to try upstreaming one of these to mathlib

Sounds like a killer app for Batteries.