request for lemmas about Array and List .isPrefixOf

Stream: general

[Frederick Pu]

I think the following characterizing lemmas of isPrefixOf are very useful when trying to prove stuff about programs that use the function

theorem Array.isPrefixOf_toList_isPrefixOf {α} [BEq α] (x y : Array α) : x.isPrefixOf y → x.toList.isPrefixOf y.toList := sorry

theorem List.subset_of_isPrefixOf {α} [BEq α] (x y : List α) : x.isPrefixOf y → x ⊆ y := sorry

[Frederick Pu]

would it be possible to get a PR for proving these?

[Frederick Pu]

also should this go into batteries or mathlib

[Ruben Van de Velde]

Are you asking someone else to prove these lemmas for you, or are you saying that you proved them?

[Frederick Pu]

i haven't proved them yet

[Frederick Pu]

and i cant find them in mathlib anywhere

[Frederick Pu]

i think i should be able to prove both myself since it's just induction

[Ruben Van de Velde]

That's probably a good place to start, then

[Ruben Van de Velde]

Though loogle found docs#Array.isPrefixOf_toList

[Frederick Pu]

any luck on the sublist?

[Ruben Van de Velde]

Assuming LawfulBEq, you get docs#List.isPrefixOf_iff_prefix and docs#List.IsPrefix.subset

[Frederick Pu]

it's weird that grind doesn't always use this lemma tho:
docs#Array.isPrefixOf_toList

[Frederick Pu]

nvm i accidently expanded Array.isPrefixOf before using the grind