SizedStr

Stream: general

[Asei Inoue]

I'm surprised that I cannot show this by try?

def SizedStr (n : Nat) := { s : String // s.length ≤ n }

def String.takeSized (s : String) (n : Nat) : SizedStr n :=
  let str := (s.take n).copy
  have : str.length ≤ n := by
    fail_if_success try?
    sorry
  ⟨str, this⟩

[Asei Inoue]

How can I show this?

[Jakub Nowak]

@loogle String.take

[Jakub Nowak]

@loogle String.take

[loogle]

:search: String.take

[Jakub Nowak]

There aren't any lemmas about String.take.

[Jakub Nowak]

There isn't much verification API around string at all it seems. You would have to create it. Or you could try using List Char or Array Char instead of String.

[cmlsharp]

Ah that’s a real shame. I suppose the difficulty is UTF-8?

[Henrik Böving]

These lemmas are on the list of the stdlib team and will come. We recently finished the refactoring to the new string API and the next evolutionary step for strings is to provide external proofs for the new API