How to prove theorem about hashes/string/metaprogramming?

Stream: lean4

[Kitsune Kiriha]

As the title indicates.
For example:

theorem t1 : mixHash 0 0 = 3866779316627607737 := by
  sorry

theorem t2 : "123".isNat := by
  sorry

Simple tactics does not work.

Are there some tactic that dedicates to these theorem?

[Henrik Böving]

mixHash is an opaque extern function, you cannot prove anything about it with normal tactics. The only thing you could possibly do would be to run native_decide.

[Henrik Böving]

Though I fear this is a bit of an #xy problem, proving things about mixHash should usually never be necessary.

[Kitsune Kiriha]

Thanks! native_decide is just what I want to seek.

[Kitsune Kiriha]

Another things is that I found https://localhost/mathlib4_docs/Batteries/Data/String/Lemmas.html#String.foldl_eq contains some lemma (e.g., String.foldl_eq) about strings. But the new API (String slice API) has no theorem about it.

So this make theorems like "123".isNat and further "123".toNat? = some 123, etc. very complicated to prove with normal ways.

[Henrik Böving]

Theorems for the new String API are on the list of our standard library team now that the API has finally settled though I can't make any concrete promises for a timeline at the moment.