Add some theorems for `String.substrEq` and `String.isPrefixOf`

[tjf801]

[tjf801]

awaiting-review

[kim-em]

Please merge main and resolve the conflict.

[tjf801]

awaiting-review

[tjf801]

awaiting-review

[chabulhwi]

@chabulhwi said:

By the way, I proved that List.IsPrefix is equivalent to List.isPrefixOf, and List.IsSuffix is equivalent to List.isSuffixOf. It'll be nice if Lean can automatically generate lemmas for isPrefixOf and isSuffixOf whenever I prove those for IsPrefix and IsSuffix. Do you think this is a good idea? If so, how do we do that?

@digama0 said:

the idea is to have all the lemmas about IsPrefix, and have a simp lemma saying isPrefixOf l1 l2 <-> IsPrefix l1 l2, and then you never have to worry about isPrefixOf again

@tjf801 I'm pretty sure String.IsPrefix and String.isPrefixOf are equivalent, as List.IsPrefix and List.isPrefixOf do. I suggest you replace your theorems about isPrefixOf with the IsPrefix counterparts.

[tjf801]

I'm pretty sure that String.IsPrefix is in Mathlib, so all of that would require upstreaming that definition from there. (On a related note, if String and List eventually both have IsPrefix in Batteries, would it be a good idea to turn the <+: operator, which currently is an alias for List.isPrefixOf into a typeclass? But that's a question for another time.)

However, in the time that this PR has been opened, I used these theorems to actually prove the equivalence between String.isPrefixOf and List.isPrefixOf, and at least the way I did it, it was non-trivial and uses most of these theorems about isPrefixOf specifically as dependencies. At this point in time, it's probably better to just close this PR and do a new one with all of these changes.

Also, I'm sorry! I didn't realize those two lines served a specific purpose. Won't make that mistake again 🫡