Contributing some string theorems

Stream: general

[LordRatte]

I recently wrote some theorems about strings to use in Advent of Code. I was wondering if there was a use-case for me to tidy them up and contribute them to the community somewhere.

It includes
theorem nat_string_append_toNat_isSome (a b : ℕ) : (toString a ++ toString b).toNat?.isSome = true
If you turn two numbers into strings and concatenate them, the result is still a number.
This is may-or-may not be too specific to be useful.

def toNumberString (n : ℕ) : {s : String // s.isNat}
A string that remembers it was a natural number. This is analogous to List.attach

I haven't contributed to the Lean community yet so I would appreciate some pointers.

[Eric Wieser]

I would guess that some of these are a good fit for the Batteries library

[Eric Wieser]

theorem Nat.toString_append_toString (a b : Nat) (ha : a ≠ 0) :
    toString a ++ toString b = toString (a * 10 ^ (log 10 b + 1) + b) := by

might be a slightly more useful theorem than (toString a ++ toString b).toNat?.isSome = true

[LordRatte]

theorem Nat.toString_append_toString (a b : Nat) (ha : a ≠ 0) :
    toString a ++ toString b = toString (a * 10 ^ (log 10 b + 1) + b)

I think I can pull that off. Is there a specific process I need to follow or do I jut open a PR and tag it with awaiting-review? I see that the core lean4 repo requires an issue to be raised first.

[Kevin Buzzard]

The suggestion was that you target https://github.com/leanprover-community/batteries