feat: add List.commonPrefix and its lemmas

[chabulhwi]

The function List.commonPrefix returns the longest common prefix of
two lists.

Co-authored-by: Kyle Miller [email protected]

---

The changes in this pull request were initially included in #987.

[eric-wieser]

Can you add commonPrefix_cons_cons as a lemma too?

[chabulhwi]

I'll do it after I have dinner!

[chabulhwi]

I'll do it after I have dinner!

Since I'm going to redefine commonPrefix, I'll do it after I get more rest.

[eric-wieser]

Does it makes sense to define this instead as

Suggested change

	/-- Returns the longest common prefix of two lists. -/
	def commonPrefix [DecidableEq α] : (l₁ l₂ : List α) → List α
	| [], _ => []
	| _, [] => []
	| a₁::l₁, a₂::l₂ =>
	if a₁ = a₂ then
	a₁ :: (commonPrefix l₁ l₂)
	else
	[]
	/-- Extract the longest common prefix of two lists, and the remainder of each list. -/
	def extractCommonPrefix [DecidableEq α] : (l₁ l₂ : List α) → List α × List α × List α
	| [], l₂ => ([], [], l₂)
	| l₁, [] => ([], l₁, [])
	| a₁ :: l₁, a₂ :: l₂ =>
	if a₁ = a₂ then
	let (common, l₁, l₂) := extractCommonPrefix l₁ l₂
	(a₁ :: common, l₁, l₂)
	else
	([], a₁ :: l₁, a₂ :: l₂)

which gives you the extra data you want at the same time.

[chabulhwi]

Yesterday, I found Substring.commonPrefix and decided to create a List version of it. Perhaps I should've followed @fgdorais's suggestion more strictly. I'll modify my code after I get some rest.

[fgdorais]

You can then add commonPrefix as an abbrev to grab just the first component.

[fgdorais]

For your convenience, here is the tail recursive version of Eric's extractCommonPrefix.

def extractCommonPrefixTR [DecidableEq α] (l₁ l₂ : List α) : List α
  loop [] l₁ l₂
where
  loop (acc : List) : (l₁ l₂ : List α) → List α
  | [], l₂ => (acc.reverse, [], l₂)
  | l₁, [] => (acc.reverse, l₁, [])
  | a₁::l₁, a₂::l₂ =>
    if a₁ = a₂ then
      loop (a₁ :: acc) l₁ l₂
    else
      (acc.reverse, l₁, l₂)

@[csimp] theorem extractCommonPrefix_eq_extractCommonPrefixTR :
    @extractCommonPrefix = @extractCommonPrefixTR := sorry

Let me know if you run into issues proving the csimp theorem.

[chabulhwi]

You can then add commonPrefix as an abbrev to grab just the first component.

How about having both of these definitions without making commonPrefix an abbrev? That'd make it easier to add new lemmas about commonPrefix.

[fgdorais]

Try the abbrev first. In principle, the abbrev should cut down on the number of necessary lemmas. Let's see how it works out in practice. Take your time and ping me here or on Zulip if you run into issues.