Proving properties of partial functions

Stream: lean4

[Jeremy Salwen]

In the lean4 documentation, it discusses how you cannot prove properties of partial functions, but then says

We are aware that proof assistants such as Isabelle provide a framework for defining partial functions that does not prevent users from proving properties about them. This kind of framework can be implemented in Lean 4. Actually, it can be implemented by users since Lean 4 is an extensible system. The developers current have no plans to implement this kind of support for Lean 4. However, we remark that users can implement it using a function that traverses the auxiliary unsafe definition generated by Lean, and produces a safe one using an approach similar to the one used in Isabelle.

I imagine I am not the first person interested in proving properties of partial functions in lean4. Has anyone attempted this approach in lean4? Is there a previous discussion of what would be involved?

[Jason Rute]

If this is related to https://proofassistants.stackexchange.com/questions/1883/simple-proof-about-string-split note I don’t think docs4#String.split is partial. It just uses the partial keyword (in its helper function) for expediency.

[Jeremy Salwen]

Yes, this is related, but i assume it is impossible to prove anything about String.split without proving something about it's auxiliary implementation function (which is a partial function)?

[Sebastian Ullrich]

The string functions in Lean 4 are optimized for programming, not proving, which is most apparent in the choice of UTF-8 encoding. Definitely not recommended for learning proving in Lean!

[Sebastian Ullrich]

If you do want to prove something about strings, I would suggest defining your own split based on the List Char representation (which is the "formal" definition of String, but not the one desired for programming)

[Henrik Böving]

I guess we could refactor the String stuff to use @implementedBy in the future maybe?

[Mario Carneiro]

yeah, I think I will eliminate the partial from those string functions at some point

[Mario Carneiro]

hopefully it should be possible to write it without partial and also without regressing the implementation, so that @[implemented_by] isn't needed

[Jeremy Salwen]

For some context, I was attempting to solve some Advent of Code problems in Lean, and then prove their correctness. But it seems like Lean is not designed for this type of verified programming? As in ~nobody is interested in proving properties of programs written in the typical style (using partial functions, etc)?

[Henrik Böving]

It is impossible to prove properties about programs written with partial functions right now as a simple matter of fact, this is not a question of interest. What people would have to be interested in is improving the heuristics for lean to automatically determine that programs terminate + refactoring where possible to non partial style programs. There are in principle a lot of people that care about proving things about Lean programs in Lean it's just that right now you have to put some effort in yourself to allow the system to do that.

[Mario Carneiro]

I (as Std maintainer) am interested in supporting that use case

[Mario Carneiro]

Lean 4 core repo basically doesn't care at all but tolerates patches to fix issues in Init

[Mario Carneiro]

Std is still under construction but I will say the same thing as I do to anyone trying out AOC: take notes about missing functionality and report them as issues

[Mario Carneiro]

For example: what string functions did you need? Were they missing, or opaque/partial? What properties did you need about them?

[Jeremy Salwen]

I am happy to help in any way possible. I certainly will report any missing functionality in Std. However, for opaque/partial functions, is it really helpful for me to report? You already know there are tons of partial functions in Std. Ideally you wouldn't have to rewrite every single one of those functions to be total, and instead have a generic mechanism for proving things about their behavior?

[Jason Rute]

@Jeremy Salwen I think you are conflating two things. The implementation of String.split uses partial when it doesn’t necessarily have to. The reason from this discussion is just that it was both written to be optimized and it wasn’t a priority at the time to prove stuff about it. (Also it maybe there is a third reason about needing it for bootstrapping.). I totally expect that such sting operations will be cleaned up to be able to prove things about them, especially if people like you find these cases and bring them to the attention of the Lean maintainers. Second, truly partial functions or functions one can’t prove are total present a special challenge. The reason Lean can prove things about recursive functions is that you prove they are total. This is foundational to Lean’s logic. Without this check on totality, you could loop forever and you have to prove you don’t. (Now, if you have a specific partial function you want to implement and prove something about, users here could give you advice on how to do it in the easiest way.)

[Mario Carneiro]

Jeremy Salwen said:

I am happy to help in any way possible. I certainly will report any missing functionality in Std. However, for opaque/partial functions, is it really helpful for me to report? You already know there are tons of partial functions in Std.

s/Std/core/. There are zero partial functions in Std outside of meta code, and if/when Std adopts the neglected string functions it will remove partial from them in the process

[Mario Carneiro]

And yes, it is helpful to report. There are plenty of partial functions in lean core but a grep doesn't tell me which ones have actually come up in the course of verification activity and which are implementation details that are only ever used for "regular" programming

[Mario Carneiro]

Also, the terminology is inherited from PL theory but partial really isn't the best word for these functions. It is meant here in the sense of a function that does not necessarily terminate, but it is somewhat at odds with the mathematical notion of a partial function meaning a function which is not defined on its whole domain. There are lots of ways to represent mathematical partial functions in lean and none of them use the partial keyword.

[Mario Carneiro]

For example, you can have a function which has a precondition as a hypothesis:

def Array.get' (a : Array α) (i : Nat) (h : i < a.size) : α := a.get ⟨i, h⟩

or you can have a function which returns an option type so that it can tell you whether it was defined or not at that point:

def Array.get?' (a : Array α) (i : Nat) : Option α := a[i]?

There is even a more complicated variant on the option type which can be used to handle the case where it is not decidable whether the function was in fact defined or not (this is the part α type from mathlib3 but it hasn't been ported yet), and this can be used to represent nonterminating functions as mathematical partial functions (this is how the theory of Turing machines is set up).

The quote from Leo at the top of the thread is an acknowledgement that the reduction of arbitrary nonterminating computations to mathematical functions is both possible and done in practice in the Isabelle theorem prover, and the partial keyword is an MVP version of that concept which doesn't do all of that but still allows for general recursion without breaking the logic, which is what the devs needed to implement practical programs in lean 4.

[Jeremy Salwen]

which ones have actually come up in the course of verification activity and which are implementation details that are only ever used for "regular" programming

I think the reason I was confused is because my approach was:

1. Write a bunch of programs in lean the "regular" way.
2. Go back and prove some facts about their behavior.

For what I've gathered, it seems like the response is "nobody does that in Lean". That there are basically two use cases: The people who are proving things about programs, who are careful to avoid partial functions, and only call functions whose transitive dependencies avoid partial, and the people who are writing practical programs just to do something, who are happy to use partial for simplicity or speed.

[Jason Rute]

I think for a lot of use cases it is easy to avoid partial, but there are certainly times I have found it the easiest thing to do. I would add a third category of people:

• People who start by writing code that works and later go back through proving stuff about it, cleaning up the code as they do, replacing any partial or unsafe or tricky monadic code with code which is easier to prove stuff about.

[Jeremy Salwen]

But it seems like nobody is actively working on improving this workflow of proving things about practical Lean programs? The focus is mostly on reducing the amount of partial or unsafe functions in libraries so it takes less effort to port to a "provable" form?

[Mario Carneiro]

You keep saying that nobody is working on this or that and this is false

[Mario Carneiro]

I'm trying to tell you that we do want to support this use case but there isn't a whole lot of manpower around and our priorities are very divided

[Mario Carneiro]

But one of the biggest motivators to get things done is having someone who is actually using the stuff and reporting issues as they run into problems using it

[Mario Carneiro]

Just to be clear re: partial: this is an incomplete feature. It is good enough to write programs but not good enough for verification. We know this, and would like to do it better, but there are a bunch of other things that have to get done first, some of which are dependencies and some of which are higher priority

[Mario Carneiro]

In an ideal world, you would be able to use partial and get a definition which can be proved correct after the fact (on the inputs for which the definition terminates)

[Mario Carneiro]

the mechanism for doing this is known, it's just a lot of work

[Jeremy Salwen]

Sorry, I don't mean to imply some sort of criticism, I am only trying to understand the current status. If there is WIP branch for proving with partial functions, or a hacky workaround that is used by other users then I would want to know about it.

I meant my comment in a specific sense "nobody is actively working on improving this workflow". By this workflow I was referring to the process of rewritingpartial and unsafe functions to a form amenable to proving.

I am happy to report all the issues I encounter with verifying practical AdventOfCode solutions, should I post them as Github issues?

[Mario Carneiro]

Do you have a specific issue you are trying to solve? The discussion has been about generalities so for so there isn't much to point at

[Mario Carneiro]

There is WIP work for proving various things in Std, some of which is in open PRs and some of which is on master, but it's not clear to me if that's what you are looking for

[Mario Carneiro]

If you provide a #mwe I'm sure we can work out how you would rewrite it to make it amenable to proving