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
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
dsimp, but none of them would touch
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?