5
$\begingroup$

I am new to lean, working on proving a simple lemma in lean4.

lemma String.split_empty (c): String.split "" c = [""]

I tried looking for existing theorems in mathlib4, but it seems like there are no existing theorems about String.split? In any case, I thought it should be easy to prove myself.

My first thought was to just expand definitions and it will probably become trivial. I was able to rewrite String.split with rw [String.split] But this reveals a helper function String.splitAux that will not be rewritten by rw [String.splitAux]. I tried a few other tactics like unfold, simp, and dsimp, but none of them would touch splitAux.

I did notice that String.splitAux is a "partial def" unlike String.split docs so perhaps that is why it is not playing nice with theorem proving?

Any advice on what tactics I should use here? Are there tactics that will just compute the answer directly here?

$\endgroup$
4
  • $\begingroup$ Maybe you wanna try desctructing c? $\endgroup$
    – ice1000
    Commented Dec 9, 2022 at 6:09
  • $\begingroup$ I believe c is irrelevant to the proof. It is just tells us what characters to split on, but the string is empty, so c will never be called. $\endgroup$ Commented Dec 9, 2022 at 6:30
  • $\begingroup$ You're right! I wrote an answer @JeremySalwen $\endgroup$
    – ice1000
    Commented Dec 9, 2022 at 7:52
  • $\begingroup$ Your best bet would be to either implement your own version of split which doesn’t use partial or raise it as an issue in the Lean Zulip or even as a GitHub issue. $\endgroup$
    – Jason Rute
    Commented Dec 9, 2022 at 14:10

1 Answer 1

4
$\begingroup$

I personally believe that this is impossible. Note that the signature of splitAux is:

@[specialize] partial def splitAux
   (s : String) (p : Char → Bool)
   (b : Pos) (i : Pos) (r : List String) : List String

According to a description of partial on: https://leanprover.github.io/lean4/doc/lean3changes.html

It says:

Finally, since we "seal" the auxiliary definition using an opaque constant, we cannot reason about partial definitions.

So, you probably cannot prove anything about it. I found it in the following paragraph:

General recursion is very useful in practice, and it would be impossible to implement Lean 4 without it. The keyword partial implements a very simple and efficient approach for supporting general recursion. Simplicity was key here because of the bootstrapping problem. That is, we had to implement Lean in Lean before many of its features were implemented (e.g., the tactic framework or support for wellfounded recursion). Another requirement for us was performance. Functions tagged with partial should be as efficient as the ones implemented in mainstream functional programming languages such as OCaml. When the partial keyword is used, Lean generates an auxiliary unsafe definition that uses general recursion, and then defines an opaque constant that is implemented by this auxiliary definition. This is very simple, efficient, and is sufficient for users that want to use Lean as a regular programming language. A partial definition cannot use unsafe features such as unsafeCast and ptrAddrUnsafe, and it can only be used to implement types we already known to be inhabited. Finally, since we "seal" the auxiliary definition using an opaque constant, we cannot reason about partial definitions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.