the way String.extract handles invalid byte positions

Stream: lean4

[Bulhwi Cha]

Consider the following evaluations:

#eval "ㄱㄴㄷ".extract ⟨0⟩ ⟨1⟩ -- output: "ㄱㄴㄷ"
#eval "ㄱㄴㄷ".extract ⟨0⟩ ⟨2⟩ -- "ㄱㄴㄷ"
#eval "ㄱㄴㄷ".extract ⟨0⟩ ⟨3⟩ -- "ㄱ"

I think it'd be better if the first two outputs were "ㄱ" instead of "ㄱㄴㄷ". But I'm not sure it's necessary. What do you think?

[Damiano Testa]

This seems similar to my troubles in this thread.

[Sebastian Ullrich]

Absent further motivation, the rule is garbage in, garbage out

[Eric Wieser]

Where the garbage here is using ⟨i⟩ to construct invalid string positions

[Bulhwi Cha]

Mario Carneiro said:

The difficult part about string manipulation is that everything uses the Pos type, which is not necessarily a valid UTF8 char boundary in the string, and the string functions have a variety of (mostly garbage and not at all consistent) ways to handle these invalid locations. We could painstakingly prove how each of them handles this case, but it is basically a misuse of the library so I think it is safe to just restrict to the case where the position is valid for the string.

To that end, we introduce the Pos.Valid type, which asserts that the position is the UTF8 length of some initial substring. We can prove some strong theorems about the behavior of all the main functions, but with awkward input values. The ValidFor type makes this a bit easier; it works especially well for the String.Iterator type but we also have a version for Substring.

[Bulhwi Cha]

Thanks to @Mario Carneiro, we already have some tools in Batteries that make it less painful to prove theorems about string manipulations.

[Bulhwi Cha]

Still, some theorems I'm trying to prove can't use Pos.Valid or ValidFor. I think a few string functions are currently defined in a way that it's hard to prove theorems about them. But I'm not asking for refactoring. I just wanted to talk about this matter.

[Bulhwi Cha]

Bulhwi Cha said:

Still, some theorems I'm trying to prove can't use Pos.Valid or ValidFor. I think a few string functions are currently defined in a way that it's hard to prove theorems about them.

Consider the following theorem:

theorem extract_eq_extract_append_extract (s : String) (i j k : Pos) (hle₁ : i ≤ j) (hle₂ : j ≤ k) :
    s.extract i k = s.extract i j ++ s.extract j k := by
  sorry

#eval "ㄱㄴㄷ".extract ⟨3⟩ ⟨6⟩ -- output: "ㄴ"
#eval "ㄱㄴㄷ".extract ⟨3⟩ ⟨4⟩ -- "ㄴㄷ"
#eval "ㄱㄴㄷ".extract ⟨4⟩ ⟨6⟩ -- ""

A mistake I made in the statement (fixed)

-    s.extract i j = s.extract i j ++ s.extract j k := by
+    s.extract i k = s.extract i j ++ s.extract j k := by

What hypotheses do I need to add to this theorem?

[Bulhwi Cha]

Sebastian Ullrich said:

the rule is garbage in, garbage out

Why do we let garbage in?

[Mario Carneiro]

because it's easier not to have additional hypotheses on the inputs for practical reasons

[Mario Carneiro]

but these functions should be treated as not having useful values when the inputs are not valid

[Mario Carneiro]

The theorem extract_eq_extract_append_extract you wrote above should hold if i,j,k are all Pos.Valid (if you fix the statement to use s.extract i k on the left)

[Mario Carneiro]

It is also possible to characterize what extract does in general, it basically sanitizes both positions by setting them to String.endPos if not valid

[Mario Carneiro]

and you could take advantage of this observation to prove that extract_eq_extract_append_extract still holds if k is not valid, although it's not really necessary

[Bulhwi Cha]

Bulhwi Cha said:

Still, some theorems I'm trying to prove can't use Pos.Valid or ValidFor.

I was mistaken about Pos.Valid. I can use it for the theorems I'm trying to prove.

[Bulhwi Cha]

Mario Carneiro said:

The theorem extract_eq_extract_append_extract you wrote above should hold if i,j,k are all Pos.Valid (if you fix the statement to use s.extract i k on the left)

Oh, I haven't noticed. I fixed it.

[Bulhwi Cha]

theorem extract_eq_extract_append_extract (s : String) (i j k : Pos)
    (hval₁ : i.Valid s) (hval₂ : j.Valid s) (hval₃ : k.Valid s) (hle₁ : i ≤ j) (hle₂ : j ≤ k) :
    s.extract i k = s.extract i j ++ s.extract j k := by
  sorry

Thank you very much for your explanation, Mario. You're amazing.