Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add List.commonPrefix and its lemmas #994

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: add List.commonPrefix and its lemmas #994

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions Batteries/Data/List/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,16 @@ namespace List

/-! ## New definitions -/

/-- 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
[]

Comment on lines +13 to +22
Copy link
Member

@eric-wieser eric-wieser Oct 16, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@chabulhwi chabulhwi Oct 16, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@chabulhwi chabulhwi Oct 16, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

/--
Computes the "bag intersection" of `l₁` and `l₂`, that is,
the collection of elements of `l₁` which are also in `l₂`. As each element
Expand Down
50 changes: 50 additions & 0 deletions Batteries/Data/List/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -482,6 +482,56 @@ theorem Sublist.erase_diff_erase_sublist {a : α} :

end Diff

/-! ### prefix, suffix, infix -/

section

variable [DecidableEq α]

theorem commonPrefix_comm (l₁ l₂ : List α) : commonPrefix l₁ l₂ = commonPrefix l₂ l₁ := by
cases l₁ <;> cases l₂ <;> simp only [commonPrefix]
next a₁ l₁ a₂ l₂ =>
split
· subst a₁
simp only [↓reduceIte, cons.injEq, true_and]
apply commonPrefix_comm
· next h =>
simp [Ne.symm h]

theorem commonPrefix_prefix_left (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₁ := by
match l₁, l₂ with
| [], _ => simp [commonPrefix]
| _::_, [] => simp [commonPrefix]
| a₁::l₁, a₂::l₂ =>
simp only [commonPrefix]
split
· next h =>
simp only [h, ↓reduceIte, cons_prefix_cons, true_and]
apply commonPrefix_prefix_left
· next h =>
simp [h]

theorem commonPrefix_prefix_right (l₁ l₂ : List α) : commonPrefix l₁ l₂ <+: l₂ := by
rw [commonPrefix_comm]
apply commonPrefix_prefix_left

theorem commonPrefix_append_append (p l₁ l₂ : List α) :
commonPrefix (p ++ l₁) (p ++ l₂) = p ++ commonPrefix l₁ l₂ := by
Comment on lines +518 to +519
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add commonPrefix_cons_cons as a lemma too?

Copy link
Contributor Author

@chabulhwi chabulhwi Oct 16, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll do it after I have dinner!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll do it after I have dinner!

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

match p with
| [] => rfl
| a::p => simpa [commonPrefix] using commonPrefix_append_append p l₁ l₂

theorem not_prefix_and_not_prefix_symm_iff {l₁ l₂ : List α} (hp : commonPrefix l₁ l₂ = []) :
¬l₁ <+: l₂ ∧ ¬l₂ <+: l₁ ↔ l₁ ≠ [] ∧ l₂ ≠ [] ∧ l₁.head? ≠ l₂.head? := by
match l₁, l₂ with
| [], _ => simp
| _, [] => simp
| a₁::l₁, a₂::l₂ =>
simp only [commonPrefix, ite_eq_right_iff, reduceCtorEq, imp_false] at hp
simp [hp, Ne.symm hp]

end

/-! ### drop -/

theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)
Expand Down